faceVertexCount
plain-language theorem explainer
The definition supplies the vertex count on each (D-1)-face of a D-cube as the power 2^{D-1}. Researchers deriving the uncallibrated lepton mass correction Δ(D) = D/2 cite it to replace the continuous solid angle 4π with its discrete counterpart. The formula is a direct combinatorial encoding with no auxiliary lemmas or reductions.
Claim. The number of vertices on each (D-1)-dimensional face of a D-dimensional hypercube equals $2^{D-1}$.
background
The module derives the dimension correction Δ(D) = D/2 from cube geometry without calibration to observed masses. It contrasts the e→μ step (active edges over continuous solid angle 4π) with the μ→τ step (face count over discrete vertex measure). The vertex count therefore functions as the discrete analog of solid angle. Upstream results establish that the underlying simplicial ledger counts remain collision-free and that the combinatorial extension adds no new RS content.
proof idea
One-line definition that directly encodes the binary coordinate structure of a hypercube: each of the D-1 face directions admits two choices, yielding the power 2^{D-1}. No lemmas are invoked; the body is the closed-form expression itself.
why it matters
The definition supplies the discrete measure V(D) required by deltaStructural, which in turn feeds delta_derived_not_calibrated and the discrete_continuous_duality theorem. It realizes the framework landmark that the μ→τ correction equals F/V with V = 2^{D-1}, confirming Δ(3) = 3/2 is forced by geometry rather than fitted. The result closes the combinatorial gap between hypercube faces and the eight-tick octave without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.