faceCount
plain-language theorem explainer
The definition states that the number of faces of a D-dimensional hypercube equals 2D. Researchers deriving the muon-to-tau mass correction in Recognition Science cite this when assembling the structural formula for the dimension-dependent shift without empirical fitting. It is supplied as a direct algebraic expression that requires no lemmas or reductions.
Claim. The face count $F(D)$ of a $D$-dimensional hypercube satisfies $F(D) = 2D$.
background
The module derives the dimension correction for the muon-to-tau lepton step from hypercube geometry. It contrasts the electron-to-muon step, which uses the continuous solid angle $4π$, with the muon-to-tau step, which normalizes face count by the discrete vertex count of each face. The vertex count thereby acts as the discrete analog of solid angle, yielding the correction term $Δ(D) = F(D)/V(D)$ where $V(D)$ is the vertex count per face.
proof idea
This is a one-line definition that directly encodes the combinatorial count of faces in a D-hypercube. No lemmas from upstream results on spectral emergence or J-cost minimization are applied; the factor of 2 per dimension follows at once from the geometry of opposing faces.
why it matters
The definition supplies the numerator for the structural expression $Δ(D) = faceCount(D) / faceVertexCount(D)$ used in downstream results such as deltaStructural_D3 and delta_derived_not_calibrated. Those theorems confirm that the geometric formula equals 3/2 at D=3 and agrees with the axis-additive form, closing the calibration-free step in the forcing chain that produces D=3 spatial dimensions. It touches the question whether all lepton mass corrections can be obtained from hypercube combinatorics alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.