cube_faces_exact
plain-language theorem explainer
The lemma establishes that the number of faces on a three-dimensional cube equals exactly six when expressed in the reals. Researchers deriving the forced muon and tau mass steps from T9 in the Recognition Science lepton ladder would cite this to fix the geometric coefficient in the step function. The proof is a one-line wrapper that unfolds the definition of cube_faces and normalizes the arithmetic.
Claim. The number of faces of the three-dimensional cube is exactly six: $F_3 = 6$, where $F_D = 2D$ denotes the face count of the $D$-cube.
background
In the T10 module the lepton ladder is constructed from the electron mass (T9), the golden ratio, and three geometric constants extracted from the 3-cube: passive edges E_p = 11, faces F = 6, and wallpaper groups W = 17. The upstream definition cube_faces (D : ℕ) : ℕ := 2 * D supplies the general formula; the present lemma simply specializes it to D = 3 and casts the result to ℝ so that it can be subtracted from or added to real-valued expressions involving α and π. The module doc states that these cube-derived numbers replace the two axioms previously present in LeptonGenerations.lean.
proof idea
The proof is a one-line wrapper. It applies simp only [cube_faces] to replace the identifier with the body 2 * 3, then invokes norm_num to evaluate the resulting integer expression to 6.
why it matters
This exact value is substituted directly into the main theorem lepton_ladder_forced_from_T9, which asserts that the muon-tau step equals 6 - (2*17+3)/2 * α and thereby forces the observed masses from T9 and the eight-tick structure. It also appears in the supporting lemma step_mu_tau_bounds that supplies the numerical interval (5.86, 5.87). The declaration therefore closes the geometric part of the T10 necessity argument that D = 3 and the cube face count are forced by the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.