LinguisticRole
plain-language theorem explainer
LinguisticRole is an inductive type whose five constructors enumerate the core syntactic positions in a clause. Cross-domain universality arguments cite it when assembling the five-domain product of cardinality 3125. The declaration is a direct inductive definition that derives Fintype, enabling immediate cardinality proofs by decide.
Claim. Let $L$ be the finite set of linguistic roles defined by the five elements subject, verb, object, modifier, complement. Then $|L|=5$ and $L$ carries the structure of a decidable finite type.
background
The ConfigDim Universality module formalizes the repeated appearance of cardinality 5 across independent domains. HasConfigDim5 is the predicate asserting that a type has exactly five inhabitants; it is witnessed for LinguisticRole by the inductive definition below. Parallel witnesses exist for SensoryModality, PrimaryEmotion, BiologicalState and EconomicCycle. The module proves that the product of any three such types has size 125 and that the full five-fold product has size 3125.
proof idea
The declaration is an inductive definition that introduces five distinct constructors and automatically derives DecidableEq, Repr, BEq and Fintype. No tactics are required; the Fintype instance is used directly by downstream decide calls such as linguistic_hasConfigDim5.
why it matters
LinguisticRole supplies the linguistic component of ConfigDimUniversalityCert and is invoked in five_domain_product to obtain the equality Fintype.card (SensoryModality × PrimaryEmotion × BiologicalState × EconomicCycle × LinguisticRole) = 3125. It therefore contributes one of the five independent witnesses for the structural claim that dimension 5 recurs across domains, consistent with the eight-tick octave and the derivation of D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.