lexicalDecayCert
plain-language theorem explainer
Lexical half-lives scale by the golden ratio φ per frequency rung in language corpora, with the five-rung span satisfying 10 < φ^5 < 12. Corpus linguists and Recognition Science modelers cite the certificate to connect observed 8-fold ratios to the phi-ladder. The definition is a direct record construction that assembles the ratio theorem halfLifeRatio with the bounding lemmas phi5_gt_10 and phi5_lt_12.
Claim. The definition supplies a certificate asserting that halfLife(k+1)/halfLife(k) = φ for every natural number k, together with the inequalities 10 < φ^5 < 12.
background
The module derives lexical decay half-lives from the phi-ladder. Half-life at rung k is T(k) = T₀ · φ^k, so the ratio per rung equals φ. The structure LexicalDecayCert requires a proof that this ratio holds for all k, plus bounds 10 < φ^5 < 12 to place the top-five frequency classes inside the canonical J(φ) band. Upstream, halfLifeRatio proves the ratio equality by unfolding halfLife and applying algebraic simplification with pow_succ and ring. The bounds phi5_gt_10 and phi5_lt_12 are obtained by iterated use of the minimal polynomial φ² = φ + 1 together with linarith.
proof idea
The definition is a direct record construction. It supplies the phi_ratio field by the theorem halfLifeRatio, the phi5_lower field by phi5_gt_10, and the phi5_upper field by phi5_lt_12.
why it matters
This certificate is consumed by the JCost variant of lexicalDecayCert, bridging the phi-ladder derivation to the J-cost formulation. It fills the F4 linguistics step by showing that the empirical frequency span lies inside the J(φ) band (10,12). The construction closes the phi-ladder application for word persistence and feeds the eight-tick octave and D=3 landmarks via the shared phi constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.