theorem
proved
tactic proof
phi_forcing_complete
show as:
view Lean formalization →
formal statement (Lean)
214theorem phi_forcing_complete :
215 ∀ r : ℝ, r > 0 → r ≠ 1 →
216 (1 + r = r^2) → -- Closure condition
217 r = phi := by
proof body
Tactic-mode proof.
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. -/