lambda_rec_is_root

formal source

  92noncomputable def K (lambda : ℝ) : ℝ :=
  93  lambda ^ 2 / lambda_rec ^ 2 - 1
  94
  95theorem lambda_rec_is_root : K lambda_rec = 0 := by
  96  unfold K lambda_rec ell0
  97  simp only [one_pow, div_one]
  98  ring
  99
 100theorem lambda_rec_unique_root (lambda : ℝ) (hlambda : lambda > 0) :
 101    K lambda = 0 ↔ lambda = lambda_rec := by
 102  unfold K lambda_rec ell0
 103  simp only [one_pow, div_one]
 104  constructor
 105  · intro h
 106    have hsq : lambda ^ 2 = 1 := by linarith
 107    have : (lambda - 1) * (lambda + 1) = 0 := by nlinarith
 108    rcases mul_eq_zero.mp this with h1 | h1
 109    · linarith
 110    · linarith
 111  · intro h
 112    rw [h]; ring
 113
 114theorem lambda_rec_is_forced :
 115    ∃! lambda : ℝ, lambda > 0 ∧ K lambda = 0 := by
 116  use lambda_rec
 117  constructor
 118  · exact ⟨lambda_rec_pos, lambda_rec_is_root⟩
 119  · intro y ⟨hy_pos, hy_root⟩
 120    exact (lambda_rec_unique_root y hy_pos).mp hy_root
 121
 122/-! ## The Complete G Derivation Chain (Q1 Answer)
 123
 124This section closes the full chain from Q3 cube geometry to κ = 8φ⁵:
 125