passive_fraction_eq_phi_sq_inv
plain-language theorem explainer
The passive fraction in the two-state lexicon model equals the square of the inverse golden ratio. Researchers working on Fibonacci-driven vocabulary evolution would cite this to confirm the steady-state split under sigma conservation. The proof is a one-line wrapper that unfolds the definition and reduces the claim via the Fibonacci fixed-point identity.
Claim. The passive fraction equals $1/φ^2$, where $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The module models a lexicon evolving in discrete time with active tokens $a_n$ and passive tokens $p_n$. The recurrence $a_{n+1} = a_n + p_n$ and $p_{n+1} = a_n$ is the Fibonacci recurrence; total size $L_n$ grows as $φ^n$. The active fraction converges to the fixed point $φ^{-1}$, so the passive fraction is defined as $1 - φ^{-1}$ and must equal $φ^{-2}$ once the fixed-point equation holds.
proof idea
The proof unfolds the definition of passive_fraction as $1 - φ^{-1}$ and invokes the upstream theorem phi_inv_fibonacci_fixed_point, which states $φ^{-1} + (φ^{-1})^2 = 1$. Linarith then closes the algebraic reduction.
why it matters
This equality completes the derivation of the steady-state fractions for the lexicon model, confirming that active plus passive sums to one via the identity $φ^2 = φ + 1$ from the recognition cost. It directly supports the sigma-conservation statement in the module doc-comment and aligns with the phi-ladder fixed point from the forcing chain (T5-T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.