SemanticChangeCert
plain-language theorem explainer
The declaration defines a certificate structure for semantic change in linguistics under Recognition Science, requiring exactly five types of semantic shifts and a CanonicalCert threshold based on the J-function. Linguists modeling semantic drift via J-cost would cite this to link historical linguistics to the phi-ladder and D=5. It is realized as a structure definition that bundles the cardinality fact with the upstream canonical certificate.
Claim. A SemanticChangeCert consists of a proof that the set of semantic change types has cardinality 5, together with a CanonicalCert (the six-clause structure asserting $J(1)=0$, $J(x)=J(1/x)$ for $x≠0$, $J(ϕ)>0$, $0.11<J(ϕ)<0.13$, and $J(1/ϕ^2)>0$).
background
In the Recognition Science framework, semantic change is modeled by the J-cost function applied to the ratio of current to original word meaning, with semantic drift occurring as J(r) increases over generations. The module sets the canonical J(ϕ) threshold as the point at which a word is considered semantically lost, and identifies five canonical semantic change types (broadening, narrowing, amelioration, pejoration, metaphorical extension) that match configDim D=5. This structure reuses CanonicalCert from CanonicalJBand, whose doc-comment states it is the canonical six-clause certificate reused by domain certs.
proof idea
This is a structure definition that packages two fields: the Fintype cardinality of the inductive SemanticChangeType equaling 5, and an instance of CanonicalCert. No proof tactics are involved; it is a direct bundling of the inductive type's derived Fintype instance with the imported canonical certificate.
why it matters
This certificate feeds the semanticChangeCert definition, which constructs an explicit instance using semanticChangeCount and cert. It connects the linguistics module to the core J-band properties and the configDim D=5 from the forcing chain (T8). It provides the interface for applying the phi threshold to predict when semantic drift renders a word lost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.