discreteMeasure_eq_4
plain-language theorem explainer
The theorem states that the discrete measure on each 2D face equals 4, the vertex count of a square. Researchers deriving the facet-mediated muon-to-tau correction in the Recognition Science lepton ladder cite this step when assembling Δ = F/V. The proof is a direct one-line application of the face-vertex-count result specialized to dimension 3.
Claim. Let $V$ be the discrete measure on a 2D face. Then $V = 4$.
background
The TauStepDeltaDerivation module derives Δ(D) = D/2 from cube geometry without mass calibration. The μ→τ step is facet-mediated: the leading term is the facet count F = 2D and the correction is Δ = F/V where V is the discrete measure per facet. The module identifies V with the vertex count of the face, treating it as the discrete analog of the solid angle 4π that appears in the e→μ edge-mediated step.
proof idea
The proof is a one-line wrapper that applies the faceVertexCount_D3 lemma.
why it matters
This equality supplies the concrete value V = 4 required for the Δ(3) = 3/2 term in the lepton-generation chain. It mirrors the 1/(4π) fractional contribution derived earlier for the e→μ step and anchors the discrete side of the Recognition Science forcing chain (T5–T8). The result feeds sibling derivations such as delta_D3_derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.