semanticChangeCert
plain-language theorem explainer
The definition supplies a concrete certificate asserting exactly five semantic change types by direct assignment from the enumeration theorem. Linguists modeling semantic drift via the J-cost function in Recognition Science cite it to fix the five canonical types to the configuration dimension. Construction is a one-line field assignment from the upstream count result together with a canonical threshold.
Claim. The semantic change certificate is the structure whose five_types component satisfies $|$SemanticChangeType$| = 5$ and whose threshold component is a canonical certificate.
background
In the Recognition Science treatment of historical linguistics, semantic change is modeled by applying the J-cost function to the recognition ratio r of current to original meaning. Drift occurs as J(r) increases over generations, with loss predicted when J(r) exceeds the canonical threshold. The module equates the five canonical types (broadening, narrowing, amelioration, pejoration, metaphorical extension) to the spatial dimension D = 5 from the forcing chain.
proof idea
This is a definition that constructs the SemanticChangeCert structure by assigning the five_types field directly to the result of the semanticChangeCount theorem and the threshold field to the canonical certificate.
why it matters
This definition supplies the concrete certificate required by the semantic change model in the linguistics module. It closes the link between the five change types and the configuration dimension D = 5 from the forcing chain. No downstream uses are recorded, leaving open whether it feeds into larger theorems on semantic drift rates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.