OrientedPolygonGluingComponent
plain-language theorem explainer
An oriented polygon-gluing component packages one Phase-36 polygon cellulation together with Phase-38 face-orientation solve data: how many faces received a sign and how many sign contradictions remain. Cosmology bridge proofs cite it as the carrier type for closed orientable surface certificates and component pairings. It is a pure data structure, so there is no proof body.
Claim. An oriented polygon-gluing component is a record $(P, f_{\mathrm{asg}}, n_{\mathrm{ctr}})$ where $P$ is a polygon-glued surface component (quotient vertices, split edges, faces, Euler characteristic, and vertex-link audit), $f_{\mathrm{asg}} \in \mathbb{Z}$ is the number of faces that received an orientation assignment, and $n_{\mathrm{ctr}} \in \mathbb{N}$ counts orientation sign contradictions found by the solver.
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. After desingularization and edge-pairing, Phase 36 supplies finite polygon-gluing components; Phase 38 adds a face-sign constraint solve on each component.
A plain polygon-gluing component records quotient vertex count, split-edge count, face count, Euler characteristic, and a local vertex-link audit (how many links, how many are single cycles). The oriented variant wraps that record with two solver outputs: faces assigned and orientation contradictions. The orientation solver is said to succeed when every face is assigned and the contradiction count is zero.
The surrounding development stays combinatorial: cell counts and decidable audits stand in for geometric realization. Homeomorphism of these cellulations to actual regular-neighborhood boundary components remains open.
proof idea
No proof: this is a structure definition with three fields and automatic Repr / DecidableEq instances. The mathematical content is the field layout itself, extending the Phase-36 polygon component by the two Phase-38 orientation-solve counters.
why it matters
Phase 39's orientability gate is stated on this type: if every polygon component has a full face-orientation assignment with zero contradictions, the oriented certificate inherits the Phase-37 polygon-gluing genus theorem. Downstream, CombinatorialClosedOrientableSurface packages Euler-ok, cyclic links, orientation-ok, and closed quadrangulation on one such component. ClosedSurfaceClassification is a named hypothesis relating these components to standard surface types when Euler characteristics match. Component pairings (ComponentPair, componentPairing, ComponentPairingCloses) zip lists of oriented components against standard surfaces and check that inventory (count, Euler, genus) matches the regular-boundary readout forced by the Betti triple, including total genus $b_1$. The type therefore sits on the path from finite certificates to the conditional closed-surface classification, without closing the missing embedded homeomorphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.