fermions_eq_half_aut
plain-language theorem explainer
The equality asserts that twice the chiral fermion flavor count equals the order of the automorphism group of the three-cube. Researchers deriving Standard Model particle counts from discrete geometry on the hypercube would cite this identity. The proof is a one-line native decision procedure that evaluates the explicit numerical definitions of both sides.
Claim. $2f = a(3)$, where $f$ is the total number of chiral fermion flavors obtained by summing color-sector and hypercharge-sector contributions each scaled by three generations and two chiralities, and $a(D)$ is the order of the hyperoctahedral group $B_D$ given by $2^D D!$.
background
The module derives Standard Model structure from the forced datum D=3, yielding the binary cube Q3 with eight vertices. The definition aut_order(D) computes the order of the hyperoctahedral group B_D as signed permutations of D coordinate axes, giving |B_D| = 2^D * D!. The definition fermion_flavors sums quarks (color dimension times three face pairs times two chiralities) and leptons (hypercharge dimension times three face pairs times two chiralities) to obtain 24 chiral states. The module states that |Aut(Q3)| = 48 equals the number of chiral fermionic states in the Standard Model.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the equality directly from the closed-form expressions for fermion_flavors and aut_order at D=3.
why it matters
This identity supplies the numerical link between the forced dimension D=3 and the observed 48 chiral fermionic states, completing the self-consistency loop in the module that runs from T8 through Q3 to the gauge content and three generations. It supports the claim that the cube symmetry group accounts for the full fermion state space without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.