deltaAxisAdditive_D3

formal source

 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
 161  unfold deltaStructural faceCount faceVertexCount
 162  norm_num
 163
 164/-- In D = 3 specifically, 2^{D-2} = 2^1 = 2, so we get D/2. -/
 165theorem deltaStructural_eq_half_D3 : deltaStructural 3 = (3 : ℝ) / 2 := deltaStructural_D3