Jphi_penalty_eq_phi_minus_three_halves

formal source

 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]
 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