ConstitutionalFormsCert
plain-language theorem explainer
Defines a structure certifying that the finite type of constitutional forms has cardinality exactly 5, matching the configuration dimension D=5 in the E7 governance model. Governance or constitutional-theory researchers would cite the structure when confirming the enumeration of executive-legislative-territorial allocations. The definition is a direct structure declaration containing only the cardinality field.
Claim. Let $C$ be the finite type whose elements are the five canonical constitutional forms (presidential, parliamentary, semi-presidential, federal, confederal). A $ConstitutionalFormsCert$ is a structure whose single field asserts that the cardinality of $C$ equals 5.
background
The module treats configDim D=5 as the source of five canonical constitutional forms, each a distinct allocation of executive, legislative, and territorial recognition authority. The upstream inductive definition ConstitutionalForm enumerates precisely these five constructors and derives the Fintype instance used for cardinality. The local setting is the Recognition Science claim that governance structures arise from the same dimensional constraints that fix spatial dimension D=3 elsewhere in the framework.
proof idea
The declaration is a structure definition whose body consists of a single field. No lemmas or tactics are invoked; the field directly records the equality Fintype.card ConstitutionalForm = 5 supplied by the derived Fintype instance on the inductive type.
why it matters
The structure supplies the certificate type instantiated by the downstream definition constitutionalFormsCert. It records the governance-depth consequence of configDim D=5 inside the E7 sector of the Recognition Science forcing chain. The declaration therefore closes one link between the dimensional output of the unified forcing chain and the enumeration of constitutional forms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.