half_rung_budget

formal source

 156/-- **THE HALF-RUNG BUDGET IDENTITY.** `J(φ) + C = 1/2`, the structural
 157    forcing of `C = φ⁻²` as the unique spatial-kernel amplitude
 158    consistent with the first-rung cost penalty. -/
 159theorem half_rung_budget : Jphi_penalty + C_kernel = 1 / 2 := by
 160  rw [Jphi_penalty_eq_phi_minus_three_halves, C_kernel_eq_two_minus_phi]
 161  ring
 162
 163/-- Equivalent form: `2 J(φ) + 2 C = 1`. -/
 164theorem half_rung_budget_doubled :
 165    2 * Jphi_penalty + 2 * C_kernel = 1 := by
 166  have h := half_rung_budget
 167  linarith
 168
 169/-- `C` is the complement of `J(φ)` within the half-rung budget. -/
 170theorem C_is_complement_of_Jphi :
 171    C_kernel = 1 / 2 - Jphi_penalty := by
 172  have h := half_rung_budget
 173  linarith
 174
 175/-- Numerical: `J(φ) + C ≈ 1/2`, with both individually positive. -/
 176theorem half_rung_components_band :
 177    (0.110 : ℝ) < Jphi_penalty ∧ Jphi_penalty < (0.120 : ℝ) ∧
 178    (0.380 : ℝ) < C_kernel ∧ C_kernel < (0.390 : ℝ) := by
 179  refine ⟨?_, ?_, C_kernel_band.1, C_kernel_band.2⟩
 180  · unfold Jphi_penalty
 181    have h := phi_gt_onePointSixOne
 182    linarith
 183  · unfold Jphi_penalty
 184    have h := phi_lt_onePointSixTwo
 185    linarith
 186
 187/-! ## §5. Discrimination from the competing hypothesis `C = φ⁻³ᐟ²`
 188
 189The competing value `C' = φ⁻³ᐟ² ≈ 0.486` from