componentPairingGenusTotal_eq_surfaceTypeGenusTotal
plain-language theorem explainer
Equal-length lists of oriented polygon-gluing components and standard surface types have matching total genus after ordered pairing: the pairing's summed target genus equals the surface list's summed genus. Phase-43 cosmology certificates that close component pairings against surface-type classifications cite this identity. Proof is list induction on the source, discharging empty cases by length and reducing each cons step via successor injectivity.
Claim. Let $C_s$ be a finite list of oriented polygon-gluing components and $S_s$ a finite list of standard closed orientable surfaces (each classified by an integer genus). If $|C_s|=|S_s|$, then the total target genus of the ordered pairing $C_s\mathbin{\mathrm{zip}}S_s$ equals $\sum_i g(S_i)$, the total genus of $S_s$.
background
This module builds the algebraic bridge for the desingularized regular-neighborhood boundary of a compact cubical positive region in the cosmogenesis pipeline. After raw cubical boundaries expose nonmanifold edges, the readout switches to the boundary of a regular neighborhood; the target identity is that total desingularized boundary genus equals the region's first Betti number $b_1$.
An oriented polygon-gluing component packages a Phase-36 polygon cell/link audit with a face-orientation solve (assigned faces and contradiction count). A standard surface type is a closed orientable surface classified solely by its integer genus $g$, with Euler characteristic $2-2g$. The ordered component pairing is the zip of a component list with a surface-type list; its genus total sums the target genus of each pair, while the surface-type genus total sums $g$ over the surface list alone.
The equality is the pure length-matched bookkeeping step between those two totals. It does not yet encode validity of pairs (orientation success or Euler match); those gates live in neighboring predicates used by the Phase-43 closing theorem.
proof idea
Term-mode proof by induction on the component list $C_s$, generalizing the surface list $S_s$.
Nil case: case-split on $S_s$. Both empty gives rfl (both totals are $0$). Nonempty $S_s$ contradicts the length hypothesis by simp.
Cons case: case-split on $S_s$. Empty target again contradicts length. On cons S Ss, successor injectivity of Nat yields equal tail lengths. Unfolding both totals produces the additive goal $g(S)+\mathrm{pairing\text{-}total}(\mathrm{zip,tails})=g(S)+\mathrm{surface\text{-}total}(\mathrm{tail})$; rewrite by the inductive hypothesis on the tails.
No external lemmas beyond list induction, Nat.succ.inj, and the definitions of zip-pairing and the two genus sums.
why it matters
Feeds the sole downstream consumer componentPairingCloses_of_surfaceTypeClassificationCloses, the Phase-43 pairing bridge: a closed standard-surface classification yields a closed finite component pairing. That theorem's first step extracts equal list lengths and needs this identity so pairing genus totals inherit the classified surface genus totals.
In the module arc (Phases 27–47), this is pure arithmetic scaffolding inside the polygon-gluing and orientability certificate stack. Earlier phases already force boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and genus $b_1$ under corrected component counts; Phase 37–39 wrap polygon gluing and orientation into the same genus algebra. The equality keeps the paired readout aligned with the surface-type side without re-deriving sums.
It does not close the still-open embedded digital-cubical collapse or the regular-neighborhood homeomorphism; the module status remains partial through Phase 44 and conditional at Phase 47 on those geometric gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.