muTauContribution
plain-language theorem explainer
muTauContribution defines the normalized μ→τ contribution in the lepton generation sequence as the ratio of the face count in three dimensions to the discrete vertex measure on each face. Researchers deriving particle mass ladders from geometric principles in Recognition Science would reference this when establishing the facet-mediated correction term. The definition is a direct one-line ratio using the face count and discrete measure functions from the same module.
Claim. The normalized μ→τ contribution is defined by $F / V$ where $F = 2D$ is the face count of the D-hypercube and $V$ is the vertex count of a 2-dimensional face, evaluated at $D=3$ to yield $3/2$.
background
This definition appears in the module deriving the dimension-dependent correction Δ(D) = D/2 from cube geometry without reference to observed masses. The face count is given by faceCount(D) := 2 * D, representing the number of (D-1)-dimensional faces of a D-hypercube. The discrete measure on a 2D face is discreteMeasure2DFace := faceVertexCount(3), which equals 4, the number of vertices anchoring each square face. The module contrasts the e→μ step, which uses a continuous solid angle measure 4π, with the μ→τ step, which uses this discrete vertex count as the analog of a solid angle for facets. This sets up the duality between continuous and discrete contributions in the lepton generation ladder.
proof idea
This is a one-line definition that computes the ratio of faceCount applied to 3 and discreteMeasure2DFace, casting both to real numbers.
why it matters
This definition supplies the explicit value for the μ→τ contribution in the duality theorem discrete_continuous_duality, which states that both lepton steps follow the same normalized pattern: e→μ uses 1 over continuous measure while μ→τ uses face count over discrete measure. It advances the first-principles derivation of Δ(3) = 3/2, consistent with the Recognition Science framework's forcing of D = 3 spatial dimensions. The result supports the mass formula on the phi-ladder by providing the geometric correction without empirical fitting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.