Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Noncommutative Holonomy in Finite-Group Skew Products

Abstract

Ordered noncommutative holonomy controls periods and orbit families of a finite-group skew product.

Let f be a self-map of X, let c assign a group element to each base state, and update the fibre by right multiplication. The ordered product of charges along the actual base orbit is the holonomy; its order matters when the fibre group is noncommutative.

A returning base cycle therefore acts on the fibre by one right translation. For a finite fibre group, the lifted period is the base period times the order of that translation. Two lifts lie on the same periodic orbit exactly when their displacement belongs to the subgroup generated by holonomy, and the resulting orbit-family cardinality is the corresponding subgroup index.

Definition 1.1 (Ordered holonomy).

Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupHolonomy

Formalization. D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupHolonomy (✓ std3).

Source. Repository-derived.

Commentary.

The recursive ordered product of fibre charges along a base orbit.

Theorem 1.2 (Empty holonomy).

Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupHolonomy_zero

Proof. Machine-checked in Lean as D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupHolonomy_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The length-zero holonomy is the group identity.

Theorem 1.3 (Concatenation of holonomy).

Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupHolonomy_add

Proof. Machine-checked in Lean as D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupHolonomy_add (✓ std3). ∎

Source. Repository-derived.

Commentary.

Holonomy over a concatenated time interval factors into the first ordered product followed by the product along the shifted orbit.

Definition 1.4 (Right skew step).

Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkewStepRight

Formalization. D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkewStepRight (✓ std3).

Source. Repository-derived.

Commentary.

The base advances by f and the fibre is multiplied on the right by the current charge.

Theorem 1.5 (Iterated skew transport).

Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkew_iterate

Proof. Machine-checked in Lean as D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkew_iterate (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every natural iterate is the base iterate paired with right multiplication by the ordered holonomy.

Theorem 1.6 (Repeated returning blocks).

Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkew_iterate_block

Proof. Machine-checked in Lean as D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkew_iterate_block (✓ std3). ∎

Source. Repository-derived.

Commentary.

When the base returns after p steps, k repeated blocks multiply the fibre by the kth power of the p-step holonomy.

Theorem 1.7 (Exact lifted return criterion).

Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkew_return_iff

Proof. Machine-checked in Lean as D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkew_return_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

A lifted state returns at time n exactly when the base minimal period times the order of its holonomy divides n.

Theorem 1.8 (Lifted minimal period).

Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkew_minimalPeriod

Proof. Machine-checked in Lean as D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkew_minimalPeriod (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite fibre group, the lifted minimal period is the base minimal period multiplied by the holonomy order.

Theorem 1.9 (Equality of lifted periodic orbits).

Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkew_periodicOrbit_eq_iff

Proof. Machine-checked in Lean as D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkew_periodicOrbit_eq_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

Two lifts over one periodic base point have the same periodic orbit exactly when the fibre displacement lies in the subgroup of holonomy powers.

Definition 1.10 (Orbit family over a base point).

Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkewOrbitFamily

Formalization. D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkewOrbitFamily (✓ std3).

Source. Repository-derived.

Commentary.

The family collects the periodic orbits obtained by varying the initial fibre coordinate.

Definition 1.11 (Coset quotient parametrization).

Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkewOrbitQuotientEquivFamily

Formalization. D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkewOrbitQuotientEquivFamily (✓ std3).

Source. Repository-derived.

Commentary.

The left-coset quotient by the holonomy subgroup is equivalent to the lifted orbit family over a periodic base point.

Theorem 1.12 (Orbit-family cardinality).

Lean statement: D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkewOrbitFamily_card

Proof. Machine-checked in Lean as D5/S1/Dynamics/PeriodicOrbits/SkewGroupHolonomy.groupSkewOrbitFamily_card (✓ std3). ∎

Source. Repository-derived.

Commentary.

The number of lifted orbit classes is the index of the subgroup generated by the ordered holonomy.

References