alpha_kernel

formal source

  85def C_kernel : ℝ := phi ^ (-(2 : ℝ))
  86
  87/-- The kernel exponent (for cross-reference; same as `alphaLock`). -/
  88def alpha_kernel : ℝ := (1 - 1 / phi) / 2
  89
  90/-- The first-rung J-cost penalty (recurs across direct detection,
  91    BIT cosmic-aging, biofilm quorum, etc.). -/
  92def Jphi_penalty : ℝ := phi - 3 / 2
  93
  94/-! ## §2. The closed-form identity `C = 2 - φ` -/
  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