phi_inv_unique
The theorem states that the positive real solution to x + x² = 1 is uniquely the inverse golden ratio 1/φ. Researchers deriving lexicon active-passive ratios from Fibonacci recurrences in linguistic models would cite this result to anchor the steady-state fraction. The proof establishes uniqueness by contradiction, invoking the strict monotonicity of the map y ↦ y + y² on the positive reals together with the known satisfaction of the equation at 1/φ.
claimIf $x > 0$ and $x + x^2 = 1$, then $x = 1/φ$, where $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
In the LexiconRatio module a discrete-time lexicon model is defined with active tokens a_n and passive tokens p_n obeying the recurrence a_{n+1} = a_n + p_n and p_{n+1} = a_n. This is the Fibonacci recurrence, and the active fraction r = a_n / L_n converges to the fixed point of the associated quadratic. The inverse golden ratio phi_inv satisfies phi_inv + phi_inv² = 1 by the identity φ² = φ + 1, which is established in upstream results such as phi_inv_fibonacci_fixed_point from PhiForcing and the algebraic form phi_inv = φ - 1 from PhiRing and Inequalities.
proof idea
The proof proceeds by contradiction. It first recalls that phi_inv + phi_inv² = 1 from phi_inv_fibonacci_fixed_point and that phi_inv > 0 from phi_inv_pos. Assuming x ≠ phi_inv, it cases on whether x < phi_inv or x > phi_inv. In each case fib_fn_strict_mono is applied to derive a strict inequality between f(x) and f(phi_inv), contradicting both equaling 1, which is resolved by linarith.
why it matters in Recognition Science
This uniqueness result is used by lexiconRatioCert to certify the lexicon ratio properties including the fibonacci_identity. It completes the fixed-point derivation in the lexicon model described in the module documentation, linking the linguistic ratio directly to the phi self-similar fixed point (T6 in the forcing chain). The result closes the algebraic step needed for the passive fraction equaling 1/φ² and the sum to one.
scope and limits
- Does not prove the equation holds for the golden ratio inverse without prior algebraic identities.
- Does not extend uniqueness to non-positive reals.
- Does not derive the Fibonacci recurrence from the Recognition cost function.
- Does not provide numerical bounds beyond the algebraic uniqueness.
formal statement (Lean)
122theorem phi_inv_unique {x : ℝ} (hx : 0 < x) (h : x + x ^ 2 = 1) :
123 x = phi_inv := by
proof body
Term-mode proof.
124 -- Use strict monotonicity of f(x) = x + x² on (0, ∞).
125 -- f(phi_inv) = 1 (by phi_inv_fibonacci_fixed_point) and f(x) = 1 (by h).
126 -- So f(x) = f(phi_inv); strict monotonicity forces x = phi_inv.
127 have h_phi : phi_inv + phi_inv ^ 2 = 1 := phi_inv_fibonacci_fixed_point
128 have h_phi_pos : 0 < phi_inv := phi_inv_pos
129 by_contra h_ne
130 rcases lt_or_gt_of_ne h_ne with h_lt | h_gt
131 · have := fib_fn_strict_mono hx h_phi_pos h_lt
132 linarith
133 · have := fib_fn_strict_mono h_phi_pos hx h_gt
134 linarith
135
136/-! ## §4. Active and passive fractions -/
137
138/-- The passive fraction is `1 - phi_inv = 1/φ²`. -/