deltaAxisAdditive

formal source

 122  (faceCount D : ℝ) / (faceVertexCount D : ℝ)
 123
 124/-- The axis-additive formula (from exclusivity proof). -/
 125noncomputable def deltaAxisAdditive (D : ℕ) : ℝ := (D : ℝ) / 2
 126
 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). -/