muTauContribution_eq
plain-language theorem explainer
The declaration proves the muon-to-tau contribution equals exactly 3/2 in the lepton generation sequence. A physicist computing structural corrections to particle masses from cube geometry would cite this equality when fixing the tau rung. The proof reduces the claim to an arithmetic identity by unfolding the contribution, face-count, and vertex-count definitions then normalizing the result.
Claim. In the Recognition Science derivation, the facet-mediated correction for the muon-to-tau generation step satisfies $contribution = 3/2$, where the correction is the ratio of facet count $F=2D$ to the discrete per-facet vertex measure $V=2^{D-1}$ evaluated at $D=3$.
background
The module derives the dimension-dependent correction term Δ(D)=D/2 directly from the geometry of the D-dimensional cube, without any calibration to observed masses. The local setting contrasts the e→μ edge-mediated step, whose differential contribution is 1/(4π) from the continuous solid-angle measure, with the μ→τ facet-mediated step, whose differential contribution per facet is 1/V from the discrete vertex count. Upstream results supply the vertex count definition V(D)=2^D from SpectralEmergence and the J-cost potential used in related cosmological constructions.
proof idea
The term proof unfolds the definitions of muTauContribution, discreteMeasure2DFace, faceCount, and faceVertexCount, then applies norm_num to evaluate the resulting rational expression directly to 3/2.
why it matters
The equality supplies the explicit value Δ(3)=3/2 required by the first-principles lepton generation chain, confirming the duality between edge and facet contributions stated in the module. It anchors the structural input to the mass formula without empirical fitting and aligns with the framework's forcing chain that selects D=3 spatial dimensions. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.