LexiconRatioCert
plain-language theorem explainer
LexiconRatioCert bundles six properties of the lexicon active fraction r: positivity, r < 1, membership in (0.6, 0.7), the relation r + r² = 1, the identity φ² = φ + 1, and uniqueness of r as the positive solution to x + x² = 1. Researchers modeling lexical dynamics via Fibonacci recurrences cite this certificate when invoking the steady-state fraction derived from recognition cost. The structure aggregates lemmas already established in sibling declarations without additional steps.
Claim. Let $r$ be the active fraction of a lexicon evolving under the Fibonacci recurrence. Then $r > 0$, $r < 1$, $0.6 < r < 0.7$, $r + r^2 = 1$, $φ^2 = φ + 1$, and $r$ is the unique positive real satisfying $x + x^2 = 1$.
background
The module derives the lexicon active/passive ratio from a discrete-time recurrence on active and passive tokens. With $a_{n+1} = a_n + p_n$ and $p_{n+1} = a_n$, the total size grows as $φ^n$ and the active fraction converges to $1/φ$. lexicon_ratio is defined as phi_inv, the reciprocal of the golden ratio. The Constants structure supplies φ along with other CPM parameters. The band definition from PreLogicalCost provides arithmetic conjunctions on stable states, while phi_sq_identity asserts the defining relation φ² = φ + 1.
proof idea
LexiconRatioCert is a structure definition that collects six fields. Each field is populated by a separate lemma: positivity and bounds from direct properties of phi_inv, the Fibonacci identity from algebraic rearrangement of φ² = φ + 1, and uniqueness from the quadratic equation. No additional tactics are required beyond referencing the upstream phi_sq_identity theorem.
why it matters
This certificate supplies the master properties for the lexiconRatioCert definition, which constructs the full theorem. It completes the derivation of the active fraction as the unique fixed point of the σ-conserving recurrence, linking directly to the φ fixed point in the forcing chain (T6). The result replaces an earlier literal definition with a derivation from the recognition cost equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.