constitutionalForm_count
The theorem establishes that the inductive type of constitutional forms has cardinality exactly five. Governance modelers in the Recognition Science framework cite it to fix the number of canonical authority allocations at configDim equal to five. The proof is a one-line wrapper invoking the decide tactic on the Fintype instance derived by the inductive definition.
claimThe finite set of constitutional forms has cardinality five: $|S| = 5$ where $S = $ {presidential, parliamentary, semi-presidential, federal, confederal}.
background
The module defines configDim equal to five and enumerates five canonical constitutional forms as distinct allocations of executive, legislative, and territorial recognition authority. The inductive type ConstitutionalForm lists the constructors presidential, parliamentary, semiPresidential, federal, and confederal, and derives Fintype among other instances. The upstream result is precisely this exhaustive inductive definition, from which the cardinality computation follows directly.
proof idea
The proof is a one-line wrapper that applies the decide tactic. Because ConstitutionalForm derives Fintype, Lean's decision procedure evaluates the cardinality of the finite type as five without additional lemmas or case analysis.
why it matters in Recognition Science
This cardinality supplies the five_forms field inside the downstream constitutionalFormsCert definition. It anchors the governance layer of the Recognition Science framework at configDim equal to five, enumerating the five forms listed in the module documentation. No open questions or scaffolding are indicated in the supplied material.
scope and limits
- Does not derive the five forms from the forcing chain or J-uniqueness.
- Does not address transitions or stability between forms.
- Does not connect the forms to physical constants or the phi-ladder.
- Does not prove these are the only possible forms outside the configDim assumption.
Lean usage
def constitutionalFormsCert : ConstitutionalFormsCert where five_forms := constitutionalForm_countformal statement (Lean)
26theorem constitutionalForm_count : Fintype.card ConstitutionalForm = 5 := by decide
proof body
27