lexicalDecayCert
plain-language theorem explainer
The definition constructs the lexical decay certificate in the J-cost formulation for word-frequency persistence. Linguists analyzing lexical replacement rates in basic vocabulary would cite it to connect observed half-lives to the canonical J-band on the persistence ratio. It is realized as a one-line structure wrapper that populates the base field with the canonical certificate.
Claim. The certificate for lexical decay from J-cost is the structure whose base field equals the canonical certificate.
background
The module treats lexical decay rates via per-word J-cost on the persistence ratio r, defined as observed frequency divided by expected frequency under Zipf's law. The J-cost is the recognition cost J(x) = (x + x^{-1})/2 - 1. LexicalDecayCert is the structure containing a base canonical certificate, which supplies the J-cost version of the decay certificate. This sits alongside the phi-ladder formulation and compounds with phoneme inventory bounds and lexicon ratios.
proof idea
The definition is a one-line wrapper that constructs the LexicalDecayCert structure by assigning its base field to the canonical certificate cert.
why it matters
This certificate supplies the J-cost anchor for lexical decay, supporting the phi-ladder version that places the half-life on the phi-ladder with phi^5 bounds between 10 and 12. It fills the F4 claim by linking Pagel-style replacement rates to the canonical band, consistent with J-uniqueness and the phi fixed point. It is referenced by the phi-ladder certificate definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.