C_kernel_band

formal source

 127
 128/-- **THEOREM.** Numerical band: `0.380 < C < 0.390` from
 129    `1.61 < φ < 1.62` via the `2 - φ` closed form. -/
 130theorem C_kernel_band :
 131    (0.380 : ℝ) < C_kernel ∧ C_kernel < (0.390 : ℝ) := by
 132  rw [C_kernel_eq_two_minus_phi]
 133  have h_lo : 1.61 < phi := phi_gt_onePointSixOne
 134  have h_hi : phi < 1.62 := phi_lt_onePointSixTwo
 135  refine ⟨?_, ?_⟩ <;> linarith
 136
 137/-! ## §4. The half-rung budget identity
 138
 139The crown identity: `J(φ) + C = 1/2`. The penalty for one rung crossing
 140plus the kernel-amplitude saving fills exactly the half-rung budget.
 141-/
 142
 143/-- The first-rung J-cost penalty has closed form `φ - 3/2`. -/
 144theorem Jphi_penalty_eq_phi_minus_three_halves :
 145    Jphi_penalty = phi - 3 / 2 := rfl
 146
 147/-- The first-rung J-cost penalty equals the J-cost evaluated at φ. -/
 148theorem Jphi_penalty_eq_Jcost_phi :
 149    Jphi_penalty = Cost.Jcost phi := by
 150  unfold Jphi_penalty Cost.Jcost
 151  have h_phi_ne : phi ≠ 0 := ne_of_gt phi_pos
 152  have h_sq := phi_sq_eq
 153  field_simp
 154  nlinarith [sq_pos_of_pos phi_pos, h_sq]
 155
 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]