ConstitutionalForm
plain-language theorem explainer
The inductive definition enumerates five constitutional forms as distinct allocations of executive, legislative, and territorial authority under configDim equal to 5. Governance modelers in Recognition Science cite the enumeration when counting structures or certifying cardinality in downstream results. The declaration is a direct inductive type with no proof obligations, deriving decidable equality and finite cardinality automatically.
Claim. An inductive type whose five constructors are presidential, parliamentary, semi-presidential, federal, and confederal, each representing a distinct allocation of executive, legislative, and territorial recognition authority.
background
The module defines constitutional forms from configDim D = 5. Each form is a distinct allocation of executive, legislative, and territorial recognition authority. The inductive type supplies the enumeration whose cardinality is later certified as exactly five.
proof idea
The declaration is the inductive type itself with five constructors and deriving clauses for DecidableEq, Repr, BEq, and Fintype. No lemmas or tactics are invoked; the structure is introduced directly.
why it matters
The definition supplies the type for constitutionalForm_count, which proves Fintype.card equals 5, and for ConstitutionalFormsCert. It anchors the E7 governance depth by tying the five forms to configDim = 5, consistent with the framework's derivation of discrete structures from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.