one_oh_two_is_forced
plain-language theorem explainer
102 equals 2 times 3 times 17 as the base normalization constant forced by D=3 cube geometry, specifically 6 faces times 17 wallpaper groups. Researchers deriving the fine-structure constant from the cubic ledger cite this to fix the seam-count denominator. The proof is a single native_decide call that evaluates the arithmetic identity directly.
Claim. The normalization base satisfies $102 = 2 times 3 times 17$, equivalently $6 times 17$ where 6 is the face count of the unit cube $Q_3$ and 17 is the number of wallpaper groups.
background
The module derives alpha inverse from the discrete cubic ledger in three dimensions. The unit cell $Q_3$ has 8 vertices, 12 edges and 6 faces; one edge is active per atomic tick, leaving 11 passive field edges. The base normalization is defined as 6 faces times 17 wallpaper groups, producing the integer 102 that appears in the curvature term 103/102 pi^5. Upstream, the PrimitiveDistinction.from theorem reduces seven independent axioms to four structural conditions plus three definitional facts, supplying the axiomatic setting for the ledger construction.
proof idea
The proof is a one-line term-mode wrapper that invokes the native_decide tactic to confirm the numerical equality on natural numbers.
why it matters
This theorem supplies the explicit normalization step inside the alpha derivation, where 102 = 6 times 17 anchors the seam-count denominator before the Gauss-Bonnet curvature 4 pi times 11 is assembled. It directly implements the D=3 and eight-tick octave landmarks of the forcing chain and feeds the main constructive derivation of alpha inverse from voxel seam topology. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.