geometric_seed_factor_eq_11
plain-language theorem explainer
Recognition Science counts passive field edges on the cubic lattice Q₃ to obtain the integer factor in the fine-structure seed. The geometric seed factor is defined as the number of non-transition edges per atomic tick at D=3, and this theorem confirms the count equals 11. Gauge-coupling derivations cite the result when factorizing α as 4π times the passive-channel multiplicity. The proof is a one-line native decision that evaluates the edge-count definition directly.
Claim. The number of passive field edges on the three-dimensional cube equals 11: $N_ {passive} = 12 - 1 = 11$.
background
The module derives α⁻¹ from the geometry of the cubic ledger Q₃ forced by the Meta-Principle on Z³. Cube geometry at D=3 gives 8 vertices, 12 edges and 6 faces; one edge is traversed per recognition event (active), leaving 11 passive field edges that dress the vacuum coupling. The sibling definition geometric_seed_factor : ℕ := passive_field_edges D therefore evaluates to this passive count. Upstream structures such as SpectralEmergence.of record that the same Q₃ geometry simultaneously forces the gauge content SU(3)×SU(2)×U(1) and three generations, while PhiForcingDerived.of supplies the J-cost background for the underlying ledger factorization.
proof idea
The proof is a term-mode one-liner that applies native_decide to the definition of passive_field_edges at D=3 and confirms the numerical result 11.
why it matters
The equality supplies the integer 11 that appears in the geometric seed 4π·11 used for the fine-structure constant. It is invoked by geometric_seed_eq to assemble the full seed and by coupling_formulas_distinct and coupling_geometric_factors to separate the geometric constants for α (11 passive edges), α_s (17 wallpaper groups) and sin²θ_w ((3-φ)/6). In the framework it closes the passive-channel count inside the eight-tick octave on the D=3 lattice, consistent with T8 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.