lepton_span_eq_N0
plain-language theorem explainer
lepton_span_eq_N0 establishes that the sum of the two lepton generation steps equals N0 evaluated at dimension 3, confirming the total lepton span matches W. Mass modelers working on fermion sectors in Recognition Science cite it to anchor the derived lepton torsion geometry. The proof is a direct numerical check via native_decide on the constant integer definitions.
Claim. The sum of the passive-field edges and cube faces at dimension 3 equals $N_0(3)$.
background
In the Sector-Dependent Generation Torsion module, N0(d) is defined as 2 S0(d) + cube_body, where S0(d) counts the vertices of the d-dimensional cube. The lepton steps are given by passive_field_edges(3) for the first generation and cube_faces'(3) for the second. The module verifies algebraic constraints on the cell counts {13, 11, 6, 8} for Q3, with lepton torsion fully derived from cube geometry while quark assignments remain data-supported hypotheses.
proof idea
The proof is a one-line wrapper that invokes native_decide to verify the numerical equality between the precomputed lepton steps and N0(3).
why it matters
This theorem confirms the lepton total span equals N0, which is the D=3 coincidence W = 2V + 1 = N0 derived without data in the module. It supplies a dimension-forcing condition that aligns with the unified forcing chain landmarks T7 (eight-tick octave) and T8 (D = 3). The result closes the lepton-sector verification step in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.