pragmaticPrincipleCount
plain-language theorem explainer
The declaration asserts that the set of pragmatic principles in the Recognition Science framework has cardinality five. Researchers modeling communication as recognition exchanges would cite this when linking Gricean maxims to the configDim parameter. The proof reduces to a decision procedure on the finite inductive type.
Claim. The cardinality of the set of pragmatic principles is five: $|$relevance, quantity, quality, manner, politeness$| = 5$.
background
The module derives pragmatic principles from Recognition Science by equating successful communication with zero J-cost, where J is the recognition cost function. The five principles are relevance, quantity, quality, manner, and politeness, extending Grice's four maxims by adding politeness to reach configDim D = 5. The upstream inductive definition PragmaticPrinciple enumerates these five cases and derives Fintype for cardinality computation.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype.card expression. This works because the inductive type PragmaticPrinciple derives DecidableEq and Fintype, allowing the kernel to compute the exact count of five constructors.
why it matters
This count populates the pragmaticsCert definition, which certifies the five principles as the basis for RS pragmatics. It directly implements the module's claim that five principles equal configDim D = 5, connecting linguistic structure to the Recognition Science forcing chain via the J-uniqueness property. No open questions are flagged in the declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.