constitutionalFormsCert
plain-language theorem explainer
The definition supplies a concrete certificate that the finite type of constitutional forms has cardinality exactly 5 under the configDim = 5 constraint. Governance modelers in the Recognition Science program cite it to fix the enumeration of executive, legislative, and territorial authority allocations. It is realized as a direct structure instantiation that pulls the pre-established cardinality result.
Claim. Let ConstitutionalFormsCert be the structure whose field requires that the finite cardinality of ConstitutionalForm equals 5. The definition constitutionalFormsCert is the witness obtained by setting this field to the value of the theorem that establishes the cardinality of the enumerated ConstitutionalForm type.
background
The module defines five canonical constitutional forms—presidential, parliamentary, semi-presidential, federal, and confederal—each a distinct allocation of executive, legislative, and territorial recognition authority when the configuration dimension equals 5. The upstream theorem constitutionalForm_count proves that the finite cardinality of the ConstitutionalForm type is exactly 5 by exhaustive enumeration via the decide tactic. This definition packages that result into the certificate structure for use in higher-level governance arguments.
proof idea
The definition is a one-line wrapper that directly instantiates the ConstitutionalFormsCert structure by assigning its five_forms field to the result of the constitutionalForm_count theorem.
why it matters
This definition completes the basic enumeration step in the governance layer, linking the configDim parameter to the five-form classification. It supplies the concrete object required by any downstream theorem that assumes the existence of exactly five constitutional forms. The construction is fully discharged by the upstream cardinality proof with no open questions remaining.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.