faceCount_D3
plain-language theorem explainer
The theorem asserts that the face count in three dimensions equals six. Researchers deriving the structural correction for the tau lepton mass step would cite this value to obtain the facet-mediated term without empirical fitting. The proof is a direct computational evaluation of the faceCount definition at D=3.
Claim. The number of faces on the three-dimensional cube satisfies $F(3)=6$.
background
The module derives the dimension correction Δ(D)=D/2 from cube geometry without calibration to observed masses. Face count F(D) supplies the numerator in Δ(D)=F(D)/V(D) where V(D)=2^{D-1} is the vertex count per face, acting as the discrete analog of solid angle for the μ→τ transition. This mirrors the e→μ step in which the continuous solid angle 4π supplies the differential contribution 1/(4π).
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the definition of faceCount at dimension 3.
why it matters
This supplies the concrete input F(3)=6 required to compute Δ(3)=3/2 in the facet-mediated lepton step. It supports the claim that the correction is forced by the framework, linking to the T8 step that fixes D=3 and to the Recognition Composition Law. No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.