constitutionalForm_count
plain-language theorem explainer
The theorem establishes that the inductive type of constitutional forms has cardinality exactly five. Governance modelers in the Recognition Science framework cite it to fix the number of canonical authority allocations at configDim equal to five. The proof is a one-line wrapper invoking the decide tactic on the Fintype instance derived by the inductive definition.
Claim. The finite set of constitutional forms has cardinality five: $|S| = 5$ where $S = $ {presidential, parliamentary, semi-presidential, federal, confederal}.
background
The module defines configDim equal to five and enumerates five canonical constitutional forms as distinct allocations of executive, legislative, and territorial recognition authority. The inductive type ConstitutionalForm lists the constructors presidential, parliamentary, semiPresidential, federal, and confederal, and derives Fintype among other instances. The upstream result is precisely this exhaustive inductive definition, from which the cardinality computation follows directly.
proof idea
The proof is a one-line wrapper that applies the decide tactic. Because ConstitutionalForm derives Fintype, Lean's decision procedure evaluates the cardinality of the finite type as five without additional lemmas or case analysis.
why it matters
This cardinality supplies the five_forms field inside the downstream constitutionalFormsCert definition. It anchors the governance layer of the Recognition Science framework at configDim equal to five, enumerating the five forms listed in the module documentation. No open questions or scaffolding are indicated in the supplied material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.