fib_fn_strict_mono
plain-language theorem explainer
The function f(x) = x + x² is strictly increasing on (0, ∞). Lexicon evolution models cite this to establish uniqueness of the fixed point 1/φ for the active fraction under the Fibonacci recurrence. The proof first obtains x² < y² from mul_lt_mul' on the given positivity and order, then finishes with linarith.
Claim. If $0 < x < y$, then $x + x^2 < y + y^2$.
background
The LexiconRatio module models a lexicon with active tokens a_n and passive tokens p_n obeying the σ-conserving recurrence a_{n+1} = a_n + p_n, p_{n+1} = a_n. This is the Fibonacci recurrence; total size grows asymptotically as φ^n and the active fraction converges to the unique positive solution of x + x² = 1. The module derives this fixed point from the recognition cost and the identity φ² = φ + 1. This theorem supplies the strict monotonicity of f(x) = x + x² on (0, ∞) needed for the uniqueness argument.
proof idea
Tactic proof: rewrite the squares, apply mul_lt_mul' to the hypotheses 0 < x, 0 < y and x < y to obtain x² < y², then invoke linarith to combine the linear and quadratic terms.
why it matters
Used by phi_inv_unique to conclude that 1/φ is the unique positive root of x + x² = 1. This uniqueness identifies the active fraction with 1/φ and the passive fraction with 1/φ² in the lexicon model, consistent with the self-similar fixed point forced by the J-cost and the Recognition Composition Law. It closes an algebraic step linking the linguistic ratio to the same φ-ladder that governs the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.