lambda_rec_unique_root

formal source

  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
 1261. The Q₃ cube has 8 vertices, 12 edges, 6 faces (from DimensionForcing)
 1272. Curvature quanta |κ| = 4 are distributed over 8 faces of S² bounding
 128   each vertex of Q₃, with Gauss-Bonnet normalization χ(S²) = 2
 1293. Balance condition: J_bit = J_curv forces λ_rec = 1/√2 (lambda_0)
 1304. In RS-native units where ℓ₀ = 1, λ_rec = ℓ₀ = 1 (the discrete