fermions_eq_D_times_V
plain-language theorem explainer
The theorem establishes that the chiral fermion flavor count equals three times the vertex count of the three-dimensional binary cube. Researchers assembling the Standard Model spectrum from the forced dimension D=3 would cite this identity when verifying the 24-state count. The proof is a direct computational verification that native_decide resolves on the explicit definitions of the flavor count and vertex function.
Claim. The chiral fermion flavor count equals three times the vertex count of the three-dimensional binary cube, or equivalently $3 times 2^3$.
background
In the Spectral Emergence module the binary cube Q_3 arises once D=3 is fixed by the upstream forcing chain. The sibling definition V(D) returns the vertex count 2^D of the D-dimensional hypercube. The fermion_flavors definition assembles quarks and leptons from sector dimensions, face-pair count, and two chiralities per sector, producing the integer 24. The local setting is the self-consistency loop that maps T8 (D=3) through the eight-tick octave and phi-ladder to the observed gauge content and particle spectrum.
proof idea
The proof is a one-line term wrapper that applies native_decide to evaluate both sides of the equality on the concrete natural numbers supplied by the definitions of fermion_flavors and V.
why it matters
This identity populates the spectral_emergence master theorem by supplying the concrete count 24 = D times 2^D that matches the chiral fermion states of the Standard Model. It realizes the D times 2^D prediction that follows from the automorphism group order of Q_3 once T8 forces three spatial dimensions. The result closes the numerical step between the cube combinatorics and the 48 total fermionic degrees of freedom (including antiparticles) with zero free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.