ConstitutionalFormsCert
plain-language theorem explainer
ConstitutionalFormsCert packages the assertion that exactly five constitutional forms exist when configDim equals 5. Governance modelers in Recognition Science cite it to anchor the enumeration of presidential, parliamentary, semi-presidential, federal, and confederal allocations of authority. The declaration is a one-field structure whose field is satisfied by the derived Fintype instance on the five-constructor inductive type.
Claim. The structure ConstitutionalFormsCert consists of the field five_forms asserting that the finite type ConstitutionalForm has cardinality 5, where ConstitutionalForm is the inductive enumeration of presidential, parliamentary, semi-presidential, federal, and confederal forms.
background
The module Constitutional Forms from configDim states that configDim D = 5 produces five canonical constitutional forms: presidential, parliamentary, semi-presidential, federal, and confederal. Each form is defined as a distinct allocation of executive, legislative, and territorial recognition authority. The upstream inductive definition ConstitutionalForm supplies the five constructors and derives the Fintype instance used by the cardinality claim.
proof idea
The declaration is a structure definition whose single field is discharged by the automatically derived Fintype instance on ConstitutionalForm. No tactics or lemmas beyond the inductive construction are required.
why it matters
The structure supplies the type for the downstream definition constitutionalFormsCert, which instantiates the certificate via constitutionalForm_count. It completes the E7 Governance Depth section by fixing the count at five for configDim = 5, paralleling the forcing of D = 3 in the physical T8 step. It leaves open the question of deriving these forms from the J-cost or RCL axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.