C_kernel_eq_two_minus_phi

formal source

  95
  96/-- **THEOREM.** `C = φ⁻² = 2 - φ`. Proof: `φ⁻² = 1/φ² = 1/(φ+1)`, and
  97    `(φ+1)(2-φ) = 2φ+2-φ²-φ = φ+2-(φ+1) = 1`, so `(φ+1)⁻¹ = 2-φ`. -/
  98theorem C_kernel_eq_two_minus_phi : C_kernel = 2 - phi := by
  99  unfold C_kernel
 100  have h_phi_pos := phi_pos
 101  have h_sq : phi ^ 2 = phi + 1 := phi_sq_eq
 102  have h_phi_p1_pos : 0 < phi + 1 := by linarith
 103  -- Step 1: phi^(-2 : ℝ) = (phi^2)⁻¹ via rpow_neg and rpow_natCast
 104  have hpow : phi ^ (-(2 : ℝ)) = (phi ^ (2 : ℕ))⁻¹ := by
 105    rw [Real.rpow_neg h_phi_pos.le]
 106    congr 1
 107    rw [show ((2 : ℝ)) = ((2 : ℕ) : ℝ) from by norm_num, Real.rpow_natCast]
 108  -- Step 2: (phi^2)⁻¹ = (phi+1)⁻¹ via phi^2 = phi + 1
 109  rw [hpow, h_sq]
 110  -- Step 3: (phi+1)⁻¹ = 2 - phi via the product identity (phi+1)(2-phi) = 1
 111  have key : (phi + 1) * (2 - phi) = 1 := by nlinarith [h_sq]
 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