`muTauContribution`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
domain: Physics
line: 222 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation on GitHub at line 222.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 219
 220/-- The μ→τ normalized contribution: F / (discrete measure).
 221    Each face contributes, normalized by its vertex anchoring points. -/
 222noncomputable def muTauContribution : ℝ :=
 223  (faceCount 3 : ℝ) / (discreteMeasure2DFace : ℝ)
 224
 225/-- The μ→τ contribution equals 3/2. -/
 226theorem muTauContribution_eq : muTauContribution = 3 / 2 := by
 227  unfold muTauContribution discreteMeasure2DFace faceCount faceVertexCount
 228  norm_num
 229
 230/-- **The Duality Theorem**: Both steps follow the same pattern.
 231
 232    e→μ: contribution = (active edges) / (continuous measure) = 1/(4π)
 233    μ→τ: contribution = (face count) / (discrete measure) = F/V = 3/2
 234
 235    The vertex count V is the "discrete solid angle" for faces. -/
 236theorem discrete_continuous_duality :
 237    -- e→μ uses 1/(continuous measure)
 238    eMuContribution = 1 / (4 * Real.pi) ∧
 239    -- μ→τ uses F/(discrete measure)
 240    muTauContribution = (6 : ℝ) / 4 ∧
 241    -- The discrete measure is the vertex count
 242    discreteMeasure2DFace = 4 := by
 243  constructor
 244  · rfl
 245  constructor
 246  · unfold muTauContribution discreteMeasure2DFace faceCount faceVertexCount
 247    norm_num
 248  · rfl
 249
 250/-! ## Why Vertices Specifically?
 251
 252The vertex count is forced as the normalization factor because:

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.