ComponentPair
plain-language theorem explainer
A component pair is the product of one oriented polygon-gluing component with one standard closed orientable surface (classified by genus). Cosmology certificates that match corrected boundary pieces to target surfaces cite this type. It is a one-line type abbreviation, not a proved statement.
Claim. A component pair is an ordered pair $(C,S)$ where $C$ is an oriented polygon-gluing component (Phase-38 face-orientation data on a Phase-36 polygon cell) and $S$ is a standard closed orientable surface classified by its genus $g\in\mathbb{Z}$.
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ to the genus of the boundary of a regular neighborhood of the positive excursion set. The target identity is that the total desingularized boundary genus equals $b_1$, with boundary component count $b_0+b_2$ and boundary Euler characteristic $2(b_0-b_1+b_2)$.
An oriented polygon-gluing component packages a Phase-36 polygon cell (edge gluing and vertex-link audits) together with a face-orientation assignment and a count of orientation contradictions. A standard surface type is simply a closed orientable surface labeled by its genus $g$, with Euler characteristic $2-2g$.
The pairing type records the abstract match used by finite combinatorial certificates before any embedded geometric map is supplied. Downstream validity asks that the polygon orientation certificate succeed and that the polygon Euler characteristic equal the standard-surface Euler characteristic.
proof idea
Definitional abbreviation only: the type is the Cartesian product of OrientedPolygonGluingComponent with StandardSurfaceType. No proof obligations, tactics, or lemmas.
why it matters
Phase 35–39 of the regular-neighborhood boundary genus bridge assemble corrected edge-paired face components and oriented polygon gluings into a finite certificate that total genus equals $b_1$. This pair type is the atomic unit of that assembly: lists of pairs feed total genus and total Euler sums, the local validity predicate, and the forgetful map from later embedded-map obligations back to abstract pairs.
The module status remains partial through Phase 44 and conditional at Phase 47: arithmetic and numeric certificates are closed, but the embedded digital-cubical collapse and the homeomorphism of corrected component cellulations to actual regular-neighborhood boundary components stay open. The doc-comment on the ordered pairing states that a later geometric theorem must replace this abstract pairing with an embedded map. Within Recognition cosmology this is bookkeeping for the desingularized foam interface, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.