OrientedPolygonComponentOk
plain-language theorem explainer
Predicate recording that a Phase-38 oriented polygon-gluing component has a successful face-orientation solve: every face receives a sign and the contradiction count is zero. Cosmology certificates cite it as the orientability gate inside closed-surface and component-pair audits. The body is a two-literal conjunction on the component fields, not a derived theorem.
Claim. An oriented polygon-gluing component $C$ passes the orientation audit when the number of faces assigned equals the face count of its underlying polygon component and the number of orientation sign contradictions is zero: $\mathrm{facesAssigned}(C)=\mathrm{faces}(C)$ and $\mathrm{orientationContradictions}(C)=0$.
background
This module builds the algebraic bridge from a compact cubical 3-region with 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, boundary components equal $b_0+b_2$, boundary Euler equals $2(b_0-b_1+b_2)$, and total genus collapses to $b_1$. Phases 35–37 reduce that claim to finite polygon-gluing certificates (binary edge pairing, cyclic quotient-vertex links, corrected Euler data).
Phase 38 packages one such component with an orientation solve. The structure carries a Phase-36 polygon-gluing component plus two audit fields: how many faces received a sign assignment, and how many sign contradictions the solver found. Phase 39 treats full assignment with zero contradictions as the orientability gate before inheriting the Phase-37 genus theorem.
The predicate here is exactly that gate on a single component. It does not assert homeomorphism to a smooth regular-neighborhood boundary; it only records the decidable orientation success condition used by later combinatorial surface witnesses.
proof idea
Definitional abbreviation, not a proof. The proposition is the conjunction of two field equalities on an oriented polygon-gluing component: faces assigned equals the underlying polygon face count, and orientation contradictions equal zero. Downstream proofs typically unfold this name and discharge the literals by native_decide on concrete numeric certificates.
why it matters
Phase 39 of the regular-neighborhood boundary bridge: the orientability gate that lets an oriented certificate inherit the Phase-37 polygon-gluing genus theorem without claiming the missing homeomorphism. Module status remains partial through Phase 44 and conditional at Phase 47; this definition only records the orientation half of the combinatorial surface package.
It is required by CombinatorialClosedOrientableSurface (Euler ok, cyclic links, orientation ok, closed quadrangulation), by paired-component validity against a target standard-surface Euler characteristic, and by the concrete Phase-44 embedded-map obligation builder. Dyadic numeric theorems (genus-125 component, large/medium/small spheres, sponge R20 gluing) unfold it and decide the literals on fixed witnesses. In the broader RS cosmology readout it is bookkeeping for desingularized foam-interface genus, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.