ConstitutionalForm
plain-language theorem explainer
The declaration defines an inductive type enumerating five constitutional forms tied to configDim equal to 5 in the Recognition Science governance model. Each form represents a distinct allocation of executive, legislative, and territorial authority. Governance researchers formalizing constitutional completeness would cite this enumeration. The definition is self-contained, directly listing the constructors and deriving finiteness and equality instances.
Claim. Let $C$ be the inductive type generated by five constructors, each a distinct allocation of executive, legislative, and territorial recognition authority in a configuration space of dimension 5.
background
The module establishes five canonical constitutional forms corresponding to configDim D = 5. These are presidential, parliamentary, semi-presidential, federal, and confederal. The local theoretical setting is the E7 Governance Depth, with the module doc-comment stating zero sorries or axioms and each form as a distinct allocation of authority. No upstream results are required.
proof idea
The declaration consists of the inductive definition itself with zero proof lines. It enumerates the five constructors directly and derives the typeclass instances for decidable equality, representation, boolean equality, and finiteness via the deriving clause.
why it matters
This supplies the enumeration counted by the downstream theorem asserting cardinality exactly 5 and certified by the structure holding that cardinality fact. It fills the E7 Governance Depth step in the module doc-comment, extending configDim beyond the spatial D = 3 forced by T8 in the unified forcing chain. It touches the mapping of recognition authority to the phi-ladder in higher-dimensional settings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.