total_fermions_eq_cube_edges
plain-language theorem explainer
Equality between the total fermion count and the unit cube edge count is asserted by direct numerical evaluation. Particle physicists working in Recognition Science cite this to confirm that three generations of four fermions each yield the same count as the twelve cube edges. The proof applies the decide tactic to reduce both sides to the numeral twelve and verify identity.
Claim. The total number of fermions, given by the product of the number of generations and fermions per generation, equals the number of edges of the unit cube: $3$ generations times $4$ fermions per generation yields $12$, matching the unit cube edge count.
background
In the module on three generations of fermions from Recognition Science, the Standard Model fermion content is tied to spatial dimension D via cube geometry. Upstream definitions fix cubeEdges as the constant 12 in FreudenthalTriangulationCert, RSBridge, and the local module. totalFermions is the product of generationCount and fermionsPerGeneration. The module setting states that three generations equal D, each generation contains four fermions, and the resulting twelve Weyl fermions match the cube edges.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic evaluates the constant definitions on each side of the equality and confirms they are identical.
why it matters
This theorem supplies the cube_edge_match field inside the GenerationCert record, which certifies the numerical link between fermion counts and cube geometry. It supports the framework identification of three generations with D = 3 from the forcing chain and closes a consistency check in the particle-physics derivation. The result feeds directly into the GenerationCert construction that assembles the full set of generation properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.