Balanced transitions on actual face-paired edge stars
Abstract
Each actual occurrence contributes one transition; path ends are signature changes.
RawFacePairing on an arbitrary finite type T retains every actual face slot, the involutive face pairing and its inverse slot maps. GlobalEdge is the equivalence class generated by paired slots. A Boolean color is shared on that class. ValidColoring requires every local face to have one or two low edges. No manifold or geometric realization is a hypothesis of these combinatorial statements. Prefix notation denotes the named definitions; snd is the second projection of an occurrence.
Theorem 1.1 (Path ends and successor signature).
Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/EdgeStarTransitions.path_end_signature_and_next (✓ std3). ∎
Source. Repository-derived.
Commentary.
An occurrence is a path end exactly when its incoming and successor signatures differ. Face-slot transport identifies the successor signature with the outgoing face low-count-two indicator. The local six-bit incidence classification relates these signatures to the color counts on the adjacent faces.
Theorem 1.2 (Rise equals fall and path-end count is even).
Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/EdgeStarTransitions.global_edge_balance (✓ std3). ∎
Source. Repository-derived.
Commentary.
Paired flags admit a reversed orientation because partner flags cannot lie in one successor cycle. The resulting successor preserves the global edge. Reindexing the finite fiber balances false-to-true and true-to-false transitions; each path end is one of these two transitions.
For the original CFMP §27.1 source correspondence, let the input be the actual fixed-point-free face involution and its actual four-vertex permutations, taking the omitted vertex to the target omitted vertex and composing to the identity across paired faces. Restrict each permutation to the three vertices of that same face, using finSuccAboveEquiv and Equiv.subtypeEquiv. This gives the sigma field of the existing ActualCornerTransport.Pairing; the opposite-corner slot carries exactly the two endpoints of the corresponding source edge. Retain one shared quotient coloring for which every local face has one or two low edges. No three-edge transport is chosen independently of the original vertex map.
ActualCornerTransport numbers a face slot by its opposite corner, whereas EdgeStarTransitions lists its three edges by increasing local edge index. The fixed slot coordinate change rho is the identity for face 0 and swaps slots 0 and 2 for faces 1, 2 and 3. The derived faceMap is rho_target composed with sigma_source composed with rho_source. Under this coordinate correspondence, each one-step paired-edge identification is the same on T×Fin6. Equality of the generated relations induces an equivalence F of their global-edge quotients with F(P(i))=edgeLabel(i), where P is ActualCornerTransport’s source projection. The occurrence-fiber equivalence keeps i itself, and the color is transported through F inverse. Thus repeated local occurrences and a single shared color are preserved.
For this source data and valid coloring, apply global_edge_balance to the derived RawFacePairing at F(e). False and true code adjacent face low counts one and two, so N12 is rise and N21 is fall. The theorem gives N12=N21 and even own-color path-end multiplicity. path_end_signature_and_next identifies every own-color P4 path end, including the complementary high-color path, with a signature change. M has only face count one and C only face count two; the P4 low and high middle edges have signatures (2,2) and (1,1), respectively, and contribute no change.
This source-interface application does not supply a generic Lean carrier relating the original ideal triangulation to the same manifold N, nor identify the constructed successor with N’s actual normal-circle traversal. For an external projection P to a separately chosen edge type, surjectivity and P(i)=P(j) if and only if the source generated edge relation holds are still required; compatibility with paired slots alone is insufficient. Actual analytic angle bounds and common geometric realization remain separate obligations.