theorem
proved
deltaStructural_D3
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation on GitHub at line 130.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
127/-! ## Key Theorem: The Two Formulas Agree at D = 3 -/
128
129/-- The structural formula equals 3/2 at D = 3. -/
130theorem deltaStructural_D3 : deltaStructural 3 = 3 / 2 := by
131 unfold deltaStructural faceCount faceVertexCount
132 norm_num
133
134/-- The axis-additive formula equals 3/2 at D = 3. -/
135theorem deltaAxisAdditive_D3 : deltaAxisAdditive 3 = 3 / 2 := by
136 unfold deltaAxisAdditive
137 norm_num
138
139/-- **MAIN THEOREM**: At the physical dimension D = 3, the structural
140 derivation and the axis-additive formula give the same result.
141
142 This means Δ(3) = 3/2 is derived from cube geometry, not calibrated. -/
143theorem delta_D3_derived :
144 deltaStructural 3 = deltaAxisAdditive 3 := by
145 rw [deltaStructural_D3, deltaAxisAdditive_D3]
146
147/-! ## Why D/2 is the Correct Generalization
148
149Although `deltaStructural` and `deltaAxisAdditive` differ for D ≠ 3,
150only D = 3 is physical. The axis-additive formula D/2 is the
151correct effective formula because:
152
1531. It matches the structural value at D = 3.
1542. It has the required axis-additive structure (f(a+b) = f(a) + f(b)).
1553. It is the unique such formula (proved in TauStepExclusivity). -/
156
157/-- The structural formula can be rewritten as D / 2^{D-2} for D ≥ 2.
158 We verify this directly at D = 3. -/
159theorem deltaStructural_alt_D3 :
160 deltaStructural 3 = (3 : ℝ) / (2 ^ (3 - 2) : ℕ) := by