ConstitutionalForm
plain-language theorem explainer
The inductive type enumerates five canonical constitutional forms as distinct allocations of executive, legislative, and territorial authority at configDim depth 5. Governance modelers in the Recognition framework cite this enumeration when counting or certifying constitutional structures. The declaration is a direct inductive listing that automatically derives finite type and equality instances.
Claim. Let $C$ be the finite set of constitutional forms consisting of the presidential, parliamentary, semi-presidential, federal, and confederal systems, equipped with decidable equality.
background
The module states that five canonical constitutional forms arise at configDim $D=5$, each a distinct allocation of executive, legislative, and territorial recognition authority. The inductive type supplies the enumeration for this governance depth in the E7 setting. No upstream lemmas are required; the definition stands alone and feeds the cardinality theorem and certificate structure in the same file.
proof idea
The declaration is an inductive type definition that introduces the five named constructors directly and derives DecidableEq, Repr, BEq, and Fintype instances via the deriving clause.
why it matters
This definition supplies the base type for constitutionalForm_count (which proves cardinality exactly 5) and ConstitutionalFormsCert (the structure carrying the cardinality fact). It realizes the module claim that configDim $D=5$ corresponds to these five forms. The enumeration anchors governance models to the Recognition framework's configDim parameter without reference to the forcing chain or physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.