phi_forcing_complete

formal source

 211This is DERIVED, not assumed. The constraint r² = r + 1 emerges
 212from the closure axiom, which itself is motivated by the additive
 213structure of J-cost. -/
 214theorem phi_forcing_complete :
 215    ∀ r : ℝ, r > 0 → r ≠ 1 →
 216      (1 + r = r^2) →  -- Closure condition
 217      r = phi := by
 218  intro r hr _hne h_closure
 219  -- h_closure is exactly r² = r + 1
 220  have h_eq : r^2 = r + 1 := by linarith
 221  have h_phi_eq : phi ^ 2 = phi + 1 := phi_sq_eq
 222  -- The difference (r - φ) satisfies: (r-φ)(r+φ-1) = 0
 223  have h_factor : (r - phi) * (r + phi - 1) = 0 := by
 224    ring_nf
 225    nlinarith [sq_nonneg r, sq_nonneg phi]
 226  rcases mul_eq_zero.mp h_factor with h_diff | h_sum
 227  · linarith
 228  · have : r = 1 - phi := by linarith
 229    have : r < 0 := by linarith [one_lt_phi]
 230    linarith
 231
 232/-! ## Why Closure? The Ledger Completeness Argument -/
 233
 234/-- A ledger is "complete" if any composed event can be posted at
 235    a scale that exists in the scale sequence.
 236
 237Without closure, composing events would create orphan scales that
 238can't be posted, violating the discrete ledger structure. -/
 239def LedgerComplete (S : GeometricScaleSequence) : Prop :=
 240  ∀ n m : ℕ, ∃ k : ℕ, S.scale n + S.scale m = S.scale k
 241
 242/-- Full closure is too strong for arbitrary n, m.
 243    But the MINIMAL closure (n=0, m=1 → k=2) is achievable
 244    and forces the golden ratio. -/