C_kernel_pos

formal source

 112  exact inv_eq_of_mul_eq_one_right key
 113
 114/-- `C` is positive. -/
 115theorem C_kernel_pos : 0 < C_kernel := by
 116  rw [C_kernel_eq_two_minus_phi]
 117  have h := phi_lt_two
 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