cubeEdges
plain-language theorem explainer
Cube edge count is fixed at the integer 12. Physicists tracing fermion generations in Recognition Science cite it to equate the 12 Weyl fermions (three generations of four fermions each) with cube geometry. The definition is a direct constant assignment that re-exports the same value from the Freudenthal triangulation certificate.
Claim. Let $E$ be the number of edges of the unit cube. Then $E = 12$.
background
In the module on three generations of fermions from RS, the Standard Model spectrum is tied to spatial dimension D = 3, identified with cube face-pair count. Each generation holds four fermions, so the total of 12 Weyl fermions is set equal to the cube edge count. The module states: 'Lean: 3 generations, 4 × 3 = 12 = cube edges.'
proof idea
The definition is a direct constant assignment of 12. It imports and re-exports the identical definition from FreudenthalTriangulationCert.cubeEdges.
why it matters
The constant supplies the right-hand side of the equality totalFermions = cubeEdges inside the GenerationCert structure. It realizes the link from forcing-chain step T8 (D = 3) to the observed three generations. Downstream results include total_fermions_eq_cube_edges and the FreudenthalCert structure that records cubeEdges = 12 as part of its cube data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.