eleven_is_forced
plain-language theorem explainer
The passive edge count of the three-cube equals eleven. Researchers deriving the fine-structure constant from cubic ledger geometry cite this identity to fix the normalization factor in the curvature term. The proof evaluates the hypercube edge formula at dimension three and subtracts the single active edge.
Claim. $11 = 3 · 2^{2} - 1$, where the right-hand side counts the passive edges of the three-dimensional cube.
background
Cube edges are defined by the formula D · 2^(D-1). In the cubic ledger for D=3 this yields twelve total edges. One edge is active during a recognition event; the remaining eleven are passive field edges. The module derives α^{-1} from the geometry of this cubic ledger, with the geometric seed given by total curvature 4π multiplied by the passive edge count eleven.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the arithmetic identity.
why it matters
This identity pins the factor eleven in the geometric seed Ω(∂Q₃) = 4π × 11 used for the curvature term in the alpha derivation. It rests on the forced D=3 from the eight-tick octave and supplies the passive-edge count required by the module's main results on 4π from Gauss-Bonnet and the 103/102π^5 seam term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.