Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Noncommutative edge return orbits

Abstract

For the original paired-edge relation, the six edge slots split into two families and every actual edge chain is exactly an orbit of the corresponding return word.

Definition 1.1 (Original edge equivalence closure).

Lean statement: D5/S3/Geometry/Hyperideal/ReturnCycleWords.edgeClass

Formalization. D5/S3/Geometry/Hyperideal/ReturnCycleWords.edgeClass (✓ std3).

Source. Repository-derived.

Commentary.

edgeClass is the equivalence closure of the original edgeRel(pairing u v); all later orbit statements refer to this unchanged relation.

Definition 1.2 (Edge family).

Lean statement: D5/S3/Geometry/Hyperideal/ReturnCycleWords.family

Formalization. D5/S3/Geometry/Hyperideal/ReturnCycleWords.family (✓ std3).

Source. Repository-derived.

Commentary.

family is false on slots 0, 3 and 5 and true on slots 1, 2 and 4. It records the low/high edge family without identifying the two families.

Definition 1.3 (Representative edge slot).

Lean statement: D5/S3/Geometry/Hyperideal/ReturnCycleWords.baseEdge

Formalization. D5/S3/Geometry/Hyperideal/ReturnCycleWords.baseEdge (✓ std3).

Source. Repository-derived.

Commentary.

The low family uses representative slot 0 and the high family representative slot 1.

Definition 1.4 (Normalized edge coordinate).

Lean statement: D5/S3/Geometry/Hyperideal/ReturnCycleWords.normalizeEdge

Formalization. D5/S3/Geometry/Hyperideal/ReturnCycleWords.normalizeEdge (✓ std3).

Source. Repository-derived.

Commentary.

The six slot multipliers are [1, 1, v*u, u squared, u, u], in slot order 0 through 5. The normalized coordinate is in representative slot 0 for the low family and slot 1 for the high family.

Definition 1.5 (Edge return word).

Lean statement: D5/S3/Geometry/Hyperideal/ReturnCycleWords.returnWord

Formalization. D5/S3/Geometry/Hyperideal/ReturnCycleWords.returnWord (✓ std3).

Source. Repository-derived.

Commentary.

The low return word is v inverse times u squared and the high return word is v squared times u.

Definition 1.6 (Return subgroup).

Lean statement: D5/S3/Geometry/Hyperideal/ReturnCycleWords.returnGroup

Formalization. D5/S3/Geometry/Hyperideal/ReturnCycleWords.returnGroup (✓ std3).

Source. Repository-derived.

Commentary.

returnGroup is the subgroup closure of the selected return word, so inverse and product powers remain inside the same actual family.

For the low return word ell = v inverse times u squared, centrality has a concrete consequence when u and v generate the entire group. Assume the subgroup closure of {u,v} equals the whole group and ell belongs to its center. Centrality gives Commute(u,ell), while the group identity v = u squared times ell inverse expresses v in terms of u and a central element.

The existing inverse, power and product rules for Commute therefore give Commute(u,v). Every pair in {u,v} commutes; Mathlib’s Subgroup.isMulCommutative_closure then proves that their generated subgroup is commutative. The generation assumption identifies this subgroup with the whole group. Thus a group generated by these two elements is commutative whenever its low return word is central.

Consequently, in a noncommutative group generated by the marked pair u,v, the low return word cannot be central. The generation hypothesis concerns the same marked pair used in the edge relation. A concrete matrix group still requires identification of the marked matrices, proof of their generation, and the actual return orders before this application supplies information about its edge degrees.

Assume now that Omega is finite, with the same opposite-group action and marked elements u,v. For a sheet x and either edge family, let n be the minimal period of x under its return word. This period is positive. The existing actual-edge orbit characterization identifies the full fiber of the original quotient map P over the representative occurrence with three copies of the return orbit, so the fiber contains exactly three times n actual occurrences.

The bijection retains the actual local slot: low slots are 0, 3 and 5, and high slots are 1, 2 and 4. Each of these three slot fibers has exactly n elements. The middle slot is 5 in the low family and 2 in the high family; its fiber therefore has n elements, while the two other slots together have twice n elements. These are occurrence counts in the unchanged paired-edge quotient, with no identification of repeated local incidences.

Concretely, a period index selects an iterate of the normalized sheet coordinate, and the chosen slot uses the inverse of its original normalization multiplier to recover the actual sheet. Normalization and uniqueness below the minimal period make this assignment a bijection. Finiteness of Omega suffices; the action need not be free, faithful or transitive. Applying these counts to a concrete geometric model still requires identifying its marked action and return periods; the occurrence calculation alone does not establish endpoint orientation or link topology.

Theorem 1.7 (Actual edge equivalence is exactly a return orbit).

Lean statement: D5/S3/Geometry/Hyperideal/ReturnCycleWords.actual_edge_orbit_iff

Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/ReturnCycleWords.actual_edge_orbit_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every group G, every type Omega with the opposite-group action, all u,v in G and occurrences a,b in Omega times Fin(6), the equivalence closure of the original edgeRel(pairing u v) relates a and b exactly when they have the same low/high family and some element of the corresponding returnGroup sends the normalized coordinate of a to that of b. The forward proof checks every actual face-slot generator and propagates the invariant through reflexive, symmetric and transitive chains. The reverse proof expands a subgroup word into actual three-step cycles and connects every occurrence to its normalized representative. No finiteness, faithfulness, transitivity or freeness assumption is used. This characterizes the edge relation only; it does not assert endpoint orientation, link topology, metric geometry, Euler characteristic or a polygon-manifold realization.

References