cube_faces_exact
plain-language theorem explainer
The lemma establishes that the face count of the three-dimensional cube equals exactly six. Researchers deriving forced muon-tau mass steps from geometric constants in the lepton ladder would cite this when substituting into step functions. The proof is a direct simplification of the cube_faces definition followed by numeric normalization.
Claim. The number of faces of the three-dimensional cube is exactly six: $F_3 = 6$, where $F_D$ denotes the face count of the $D$-dimensional cube given by $F_D = 2D$ (or the matching case for $D=3$).
background
In the T10 necessity module the lepton ladder is forced from the T9 electron mass together with geometric constants that include the cube face count $F=6$. The cube_faces function appears in multiple upstream modules as the face count of the $D$-cube; AlphaDerivation and PlanckScaleMatching define it by $F_D = 2D$, while PMNSCorrections supplies the explicit match yielding 6 for $D=3$. These definitions sit inside the Recognition framework's derivation of spatial dimension $D=3$ from the eight-tick octave.
proof idea
The proof is a one-line wrapper that applies simp to unfold the cube_faces definition and then uses norm_num to reduce the resulting arithmetic expression to the equality 6 = 6.
why it matters
This exact value is invoked inside lepton_ladder_forced_from_T9 (the main T10 theorem) and inside step_mu_tau_bounds to substitute the face count into the expression for the muon-tau step. It supplies one of the geometric inputs (alongside passive edges $E_p=11$ and wallpaper groups $W=17$) required to close the forcing chain from T9 through cube geometry and the fine-structure constant, directly supporting the claim that the lepton generations are determined by the Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.