eleven_is_passive_edges
plain-language theorem explainer
Eleven equals the total edges of the three-dimensional hypercube minus the single active edge per recognition tick. Derivations of the fine-structure constant cite this count to normalize the isotropic geometric seed 4π·11. The proof reduces to direct numerical evaluation of the closed-form hypercube edge expression.
Claim. In three spatial dimensions the passive edge count is eleven, where the hypercube edge total equals twelve and exactly one edge is active per recognition tick.
background
The module proves that the geometric seed factor 4π in the fine-structure constant derivation is fixed by isotropic coupling in three dimensions. The hypercube edge count in dimension d is d times two to the power of d minus one. The active edges per tick equals one by the single-transition rule per atomic tick. This local setting assumes the dimension equals three, as required by the linking condition in the dimension-forcing chain. Upstream results supply the active-edges definition as one and the hypercube-edge formula.
proof idea
The proof is a term-mode application of native_decide that evaluates the arithmetic equality from the hypercube edge definition and the active-edge count.
why it matters
This result supplies the factor eleven in the geometric seed 4π·11 that appears in the alpha derivation formula. It closes the edge-counting step in the solid-angle exclusivity argument that forces the unique isotropic measure 4π in three dimensions. The placement aligns with the dimension-forcing chain that yields D equals three and the isotropy requirement for recognition events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.