phiInvSq_eq_two_minus_phi

formal source

  57  linarith [hkey]
  58
  59/-- 1/φ² = 2 - φ. Proof: φ²·(2-φ) = 2φ² - φ³ = 2(φ+1) - (2φ+1) = 1. -/
  60theorem phiInvSq_eq_two_minus_phi : 1 / phi^2 = 2 - phi := by
  61  have hpos : phi^2 ≠ 0 := ne_of_gt (pow_pos phi_pos 2)
  62  have h2 : phi^2 = phi + 1 := phi_sq_eq
  63  have h3 : phi^3 = 2 * phi + 1 := phi_cubed_eq
  64  have hkey : phi^2 * (2 - phi) = 1 := by nlinarith [h2, h3]
  65  rw [eq_comm, eq_div_iff hpos]
  66  linarith [hkey]
  67
  68/-- 1/φ³ = 2φ - 3 (= the Cabibbo-angle factor). -/
  69theorem phiInvCubed_eq_two_phi_minus_three : 1 / phi^3 = 2 * phi - 3 := by
  70  have hpos : phi^3 ≠ 0 := ne_of_gt (pow_pos phi_pos 3)
  71  have hsq : phi^2 = phi + 1 := phi_sq_eq
  72  have h3 : phi^3 = 2 * phi + 1 := phi_cubed_eq
  73  have hkey : phi^3 * (2 * phi - 3) = 1 := by nlinarith [hsq, h3]
  74  rw [eq_comm, eq_div_iff hpos]
  75  linarith [hkey]
  76
  77/-! ## Domain instances. -/
  78
  79/-- Senolytic target ratio. -/
  80noncomputable def senolyticTargetRatio : ℝ := phiInv
  81
  82/-- Gini ceiling (RS prediction). -/
  83noncomputable def giniCeiling : ℝ := phiInv
  84
  85/-- Counter-cyclical policy balance. -/
  86noncomputable def policyBalance : ℝ := phiInv
  87
  88/-- Stem-cell reserve decay per phi-rung. -/
  89noncomputable def stemCellDecay : ℝ := phiInv
  90