phi_inv_unique
plain-language theorem explainer
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/φ.
Claim. If $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.