euler_closure
plain-language theorem explainer
euler_closure supplies the integer 1 that closes the seam count for cubic 3-manifolds in the alpha derivation. Workers assembling the curvature term 103/102π^5 cite this constant when adding the Euler contribution to the 102 base from faces and wallpaper groups. The definition is a direct constant assignment encoding the topological closure constraint.
Claim. The Euler characteristic contribution for manifold closure on a closed orientable 3-manifold assembled from cubes equals 1.
background
The module derives α^{-1} from the geometry of the cubic ledger on Z^3. One atomic tick traverses a single active edge while the remaining 11 passive edges couple to vacuum geometry. Cube counts are fixed by D=3: 8 vertices, 12 edges, 6 faces. The base normalization uses 6 faces times 17 wallpaper groups to reach 102; the Euler term supplies the final increment to 103.
proof idea
Direct definition that assigns the constant 1. No lemmas or tactics are invoked; the value stands for the Euler characteristic constraint on closed orientable 3-manifolds patched from cubes.
why it matters
This supplies the +1 that produces seam_numerator 103, which enters the curvature term inside alpha_ingredients_from_D3_cube. The parent theorem alpha_ingredients_from_D3_cube records the full provenance: geometric_seed_factor from cube edges minus active edges, seam_numerator from faces times wallpaper groups plus this closure, and seam_denominator from the same base. It completes the D=3 cube contribution to the 103/102π^5 term in the alpha derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.