constitutionalForm_count
plain-language theorem explainer
The theorem states that exactly five constitutional forms exist when configDim equals 5. Governance analysts cite it to fix the enumeration of executive, legislative, and territorial authority allocations. The proof is a one-line decision procedure on the derived Fintype instance of the five-constructor inductive.
Claim. The set of constitutional forms has cardinality five, consisting of the presidential, parliamentary, semi-presidential, federal, and confederal forms.
background
The module introduces five constitutional forms as distinct allocations of executive, legislative, and territorial recognition authority, each tied to configDim equal to 5. The inductive definition enumerates them explicitly and derives DecidableEq, Repr, BEq, and Fintype instances. This construction sits inside the Governance section of Recognition Science, which extends the core functional equation and forcing chain to constitutional structures via the dimensional parameter.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype.card computation, which succeeds automatically from the inductive definition with five constructors.
why it matters
The result supplies the five_forms field required by the downstream constitutionalFormsCert definition. It directly instantiates the configDim equals 5 claim in the module title, linking the governance enumeration to the Recognition Science framework's use of dimensional parameters (cf. T8 for spatial D equals 3). No open questions or scaffolding are indicated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.