phi_unique_fixed_point
The golden ratio φ is the unique positive real satisfying x² = x + 1. Recognition Science ledger arguments cite this to force the cost fixed point. The proof rewrites the quadratic, factors it over the reals, and discards the negative root via the positivity hypothesis and a zero-divisor lemma.
claimFor every positive real number $x$, if $x^2 = x + 1$ then $x = phi$, where $phi = (1 + sqrt(5))/2$.
background
The Meta.LedgerUniqueness module resolves the objection that other ratios could satisfy the discrete conservative constraints. Here the cost function is the J-cost of a recognition event or the derived comparator cost from a multiplicative recognizer; its fixed-point equation reduces to x² = x + 1. The upstream mul_eq_zero result states that the logic integers have no zero divisors, which is applied after the real factorization to split cases.
proof idea
The tactic proof rewrites the hypothesis to x² - x - 1 = 0 via linarith. It factors the left side as (x - phi)(x - psi) with psi the negative conjugate, using ring_nf and the square-root identity. mul_eq_zero splits the product-zero case; the psi branch is contradicted by showing psi < 0 and invoking linarith on x > 0.
why it matters in Recognition Science
This result is invoked by cost_fixed_point_is_phi and supplies the φ clause of complete_ledger_uniqueness and rs_ledger_is_unique. Those theorems close Gap 9 by showing the RS ledger (φ, Q₃, 8-tick) is the only structure meeting the cost-fixed-point, linking, and Gray-code constraints. It corresponds to the T6 step in the unified forcing chain where φ is forced as the self-similar fixed point of the J-cost.
scope and limits
- Does not prove existence of phi.
- Does not apply when x is not positive.
- Does not derive the quadratic from the J-cost definition.
- Does not treat complex or matrix analogs.
formal statement (Lean)
64theorem phi_unique_fixed_point :
65 ∀ x : ℝ, x > 0 → x^2 = x + 1 → x = phi := by
proof body
Tactic-mode proof.
66 intro x hx hEq
67 -- x² = x + 1 ⟹ x² - x - 1 = 0
68 have h1 : x^2 - x - 1 = 0 := by linarith
69
70 -- Factorization: x^2 - x - 1 = (x - phi) * (x - psi)
71 let psi := (1 - Real.sqrt 5) / 2
72 have h_factor : x^2 - x - 1 = (x - phi) * (x - psi) := by
73 unfold phi psi
74 ring_nf
75 rw [Real.sq_sqrt (by norm_num)]
76 ring
77
78 rw [h_factor] at h1
79 cases mul_eq_zero.mp h1 with
80 | inl h => exact sub_eq_zero.mp h
81 | inr h =>
82 have h_psi_neg : psi < 0 := by
83 unfold psi
84 have hsqrt : Real.sqrt 5 > 1 := by
85 rw [← Real.sqrt_one]
86 exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
87 linarith
88 have h_x_psi : x = psi := sub_eq_zero.mp h
89 rw [h_x_psi] at hx
90 linarith -- Contradiction: x > 0 but psi < 0
91
92/-- The cost function fixed point is uniquely φ. -/