dyadicSpongeR20_correctedComponentGenus
plain-language theorem explainer
For the Phase-34 dyadic-sponge corrected boundary (one high-genus piece plus 52 spheres), the half-Euler readout with value −72 yields total genus 125. Cosmology and foam-interface workers cite this as the numeric genus certificate for the R20 sponge. The proof is a pure native_decide arithmetic check on the explicit component list.
Claim. Let $C$ be the Phase-34 corrected boundary-component list for the dyadic sponge (one genus-$125$ component together with $52$ spheres). With half-Euler input $-72$, the corrected total genus $C_{\mathrm{count}} - (-72)$ equals $125$.
background
This module builds the algebraic bridge between a compact 3D cubical region’s Betti triple $(b_0,b_1,b_2)$ and the topology of the boundary of a regular neighborhood of the exact positive region. After Phase 25 found nonmanifold edges on the raw cubical boundary, Phase 26 switched to that desingularized readout. The bridge asserts boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total desingularized genus exactly $b_1$.
Genus is read by correctedComponentGenusFromHalfEuler: component count minus an explicitly supplied half-Euler integer, so the doubled-boundary identity is never hidden behind integer division. The input list dyadicSpongeR20CorrectedComponents is the Phase-34 assembly for the dyadic sponge: one genus-125 component plus fifty-two sphere components. Half-Euler $-72$ is the numeric certificate paired with that list.
proof idea
One-line computational certificate. Unfold the genus definition (count minus half-Euler) on the concrete list of fifty-three corrected components with half-Euler $-72$, then discharge the integer equality $53-(-72)=125$ by native_decide. No geometric lemmas are invoked; the term is pure finite arithmetic on the recorded component data.
why it matters
Closes the Phase-34/35 numeric genus gate for the dyadic sponge R20 inside the regular-neighborhood boundary program (Phases 27–47). Module status is partial theorem through Phase 44 and conditional at Phase 47, with zero sorry and no new axioms; this declaration is one of the horizon/dyadic numeric certificates the file actually proves.
It feeds the algebraic half of the component-assembly story: once corrected edge-paired face components have the canonical count and Euler half-sum, total genus is forced to $b_1$. Downstream polygon-gluing (Phase 36/37) and orientability (Phase 39) wrappers reduce to the same assembly data. It does not discharge the still-open embedded digital-cubical collapse or the homeomorphism of corrected cellulations to true regular-neighborhood boundary components. In the broader Recognition chain it is a cosmology-side arithmetic witness, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.