passive_fraction
plain-language theorem explainer
Passive fraction is the steady-state proportion of passive tokens in a Fibonacci lexicon model, defined as 1 minus the active fraction 1/φ and equal to 1/φ². Recognition theorists modeling discrete vocabulary evolution cite it to enforce σ-conservation with the active complement. The definition is a direct algebraic subtraction from the imported phi_inv value.
Claim. The passive fraction is the real number $1 - 1/φ$, equivalently $1/φ²$, where $φ$ is the golden ratio satisfying $φ² = φ + 1$.
background
The module models lexicon evolution with active tokens $a_n$ and passive tokens $p_n$ obeying the recurrence $a_{n+1} = a_n + p_n$, $p_{n+1} = a_n$. Total size grows asymptotically as $φ^n$, so the active fraction converges to the fixed point $1/φ$. Upstream theorems establish that phi_inv equals $1/φ$ and satisfies the identity $1/φ = φ - 1$, which follows from the quadratic $φ² = φ + 1$ proved in Constants.phi_sq_eq and reused across PhiRing, Inequalities, and PhiForcing.
proof idea
One-line definition that subtracts the imported phi_inv from 1. It draws the value of phi_inv directly from the sibling definition in the same module, which itself imports the constant from Constants.phi.
why it matters
This definition supplies the passive complement required by fractions_sum_to_one and the bundled fixed-point statement in lexicon_ratio_one_statement. It completes the derivation that the active:passive ratio equals φ:1 as the unique positive solution to $x + x² = 1$, forced by the recognition cost identity $φ² = φ + 1$. The result sits inside the Recognition Science program that extracts constants from the J-cost functional and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.