lexiconRatioCert
plain-language theorem explainer
The lexiconRatioCert constructs a certificate asserting that the active lexicon fraction equals 1/φ and satisfies positivity, the band (0.6, 0.7), the fixed-point equation r + r² = 1, and uniqueness as the positive solution to x + x² = 1. Cognitive scientists modeling discrete-time language evolution cite it for the derived active/passive split forced by σ-conservation. The definition is a direct construction that assembles six supporting lemmas on the φ-ladder without further reduction.
Claim. Let r denote the active lexicon fraction. Then r > 0, r < 1, 0.6 < r < 0.7, r + r² = 1, φ² = φ + 1, and r is the unique positive real satisfying x + x² = 1.
background
In the Recognition Science lexicon model a discrete-time process tracks active tokens a_n and passive tokens p_n under the σ-conserving recurrence a_{n+1} = a_n + p_n, p_{n+1} = a_n. This is the Fibonacci recurrence whose total size L_n grows asymptotically as φ^n; the active fraction r = a_n / L_n converges to the unique fixed point of r + r² = 1. The structure LexiconRatioCert bundles the six derived properties: positivity, strict inequality below 1, the numerical band, the Fibonacci identity, the quadratic relation φ² = φ + 1, and uniqueness among positive solutions.
proof idea
The definition constructs the LexiconRatioCert instance by direct field assignment from six pre-proved lemmas: lexicon_ratio_pos supplies positivity, lexicon_ratio_lt_one the bound below 1, lexicon_ratio_band the interval (0.6, 0.7), lexicon_ratio_derivation the identity r + r² = 1, phi_sq the relation φ² = φ + 1, and phi_inv_unique the uniqueness clause. No additional tactics or reductions are performed.
why it matters
This definition replaces the v4 skeleton literal with a derivation that closes the σ-conservation loop between the recognition cost (via Constants.phi_sq_eq) and the steady-state lexicon split on Track A2/E2. The module one-statement summary presents it as unifying the active fraction 1/φ with the Fibonacci recurrence and the φ² = φ + 1 identity. No downstream uses are recorded, leaving open whether further linguistic or cognitive derivations will invoke the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.