discreteMeasure2DFace
plain-language theorem explainer
The declaration defines the discrete measure on a 2D face of the 3-cube as the vertex count of its square boundary. Researchers deriving the μ to τ lepton generation step would cite this to anchor the discrete contribution in the mass correction formula. The definition is a direct specialization of the general face vertex count to three dimensions.
Claim. Let $V$ be the discrete measure on a 2D face of the 3-cube. Then $V := 2^{3-1} = 4$.
background
This module derives the dimension-dependent correction Δ(D) = D/2 from cube geometry without calibration to observed masses. The goal is to show that Δ(3) = 3/2 is forced by the framework. The vertex count of a (D-1)-hypercube face is given by faceVertexCount D := 2^(D-1). For D=3, each face is a square with four vertices, serving as the discrete anchoring points. This builds on structures from SpectralEmergence, which forces exactly three particle generations from face-pair count, and PhiForcingDerived for J-cost minimization. The module compares the e→μ step (using continuous solid angle 4π) with the μ→τ step (using discrete vertex count as the analog of solid angle).
proof idea
This is a one-line definition that applies the faceVertexCount function to dimension 3.
why it matters
It supplies the discrete measure used in the μ→τ contribution calculation, which equals 3/2. This feeds the duality theorem showing that both e→μ and μ→τ steps follow the pattern of active elements divided by their respective measures (continuous 4π versus discrete vertex count). It realizes the key insight that vertex count is the discrete analog of the solid angle in the lepton generation steps. This closes part of the first-principles derivation of Δ(D) = D/2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.