muTauContribution
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the face count or vertex count from more primitive axioms.
- Does not extend the ratio to dimensions other than D=3.
- Does not incorporate continuous measures such as solid angles.
- Does not connect the value to experimental lepton masses or calibration.
formal statement (Lean)
222noncomputable def muTauContribution : ℝ :=
proof body
Definition body.
223 (faceCount 3 : ℝ) / (discreteMeasure2DFace : ℝ)
224
225/-- The μ→τ contribution equals 3/2. -/