LexicalDecayCert
plain-language theorem explainer
LexicalDecayCert packages the assertion that half-lives on the phi-ladder satisfy a constant ratio phi together with bounds 10 < phi^5 < 12. Researchers modeling lexical decay in language corpora cite it to connect observed half-life ratios to the Recognition Science phi-ladder. The declaration is a structure definition that directly assembles the ratio property from the halfLife function and the two phi^5 inequalities.
Claim. A structure certifying that the half-life function $T(k)=phi^k$ obeys $T(k+1)/T(k)=phi$ for every natural number $k$, along with the bounds $10<phi^5<12$.
background
The module models word half-lives in corpora as scaling geometrically with rung number on the phi-ladder. High-frequency words persist roughly eight times longer than low-frequency words, a ratio approximated by phi^5 within the J(phi) band. The upstream halfLife definition sets halfLife(k) to phi raised to k, where phi is the golden ratio from Constants.
proof idea
The declaration is a structure definition with no proof body. It directly packages the ratio property derived from the halfLife definition and the two inequalities on phi^5.
why it matters
This structure is instantiated in lexicalDecayCert within the same module and also used to define lexicalDecayCert in LexicalDecayFromJCost. It fills the F4 step in the linguistics application of Recognition Science, linking the phi-ladder to empirical word decay rates. The bounds on phi^5 place the ratio within the J-cost band, consistent with the self-similar fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.