passive_fraction_pos
plain-language theorem explainer
The passive fraction in the lexicon model, defined as one minus the inverse golden ratio, is shown to be strictly positive. Researchers deriving vacuum energy bounds or modeling lexical evolution via Fibonacci recurrences in Recognition Science would cite it to bound phase-lock contributions. The proof is a one-line wrapper that unfolds the definition and applies the upstream inequality phi_inv < 1 via linear arithmetic.
Claim. $0 < 1 - 1/φ$ where $φ$ is the golden ratio and the passive fraction equals $1/φ²$ from the fixed-point condition $φ² = φ + 1$.
background
In the LexiconRatio module the lexicon evolves by the σ-conserving recurrence a_{n+1} = a_n + p_n and p_{n+1} = a_n, which is the Fibonacci recurrence forced by the active-edge budget A = 1. The total size grows as L_n ∼ φ^n, so the active fraction converges to the unique fixed point phi_inv := 1/φ and the passive fraction is defined as passive_fraction := 1 - phi_inv = 1/φ². The module also records that phi_inv satisfies phi_inv + phi_inv² = 1, which is the steady-state conservation identity equivalent to φ² = φ + 1. This result depends on the upstream theorem phi_inv_lt_one (both the local copy and the one imported from PhiEmergence) that establishes 1/φ < 1 from the positivity and ordering properties of φ.
proof idea
The proof is a one-line wrapper. It unfolds the definition passive_fraction := 1 - phi_inv, invokes the sibling theorem phi_inv_lt_one that phi_inv < 1, and applies linarith to conclude that the difference is positive.
why it matters
This theorem supplies the strict positivity required by vacuum_energy_pos in Cosmology.VacuumUniformity, where phaseLockEnergy is obtained by multiplying passive_fraction_pos by the positive coherence energy E_coh. It completes the linguistic derivation of the passive fraction 1/φ² that follows from the Recognition Composition Law and the eight-tick octave forcing D = 3. The result touches the open question of whether lexical fixed points directly constrain the vacuum-energy scale in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.