C_kernel_lt_half

formal source

 118  linarith
 119
 120/-- `C < 1/2` (strictly less than the half-rung budget). -/
 121theorem C_kernel_lt_half : C_kernel < 1 / 2 := by
 122  rw [C_kernel_eq_two_minus_phi]
 123  have h := phi_gt_onePointFive
 124  linarith
 125
 126/-! ## §3. Numerical band -/
 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