pith. machine review for the scientific record. sign in
structure definition def or abbrev high

GovernanceFailureCert

show as:
view Lean formalization →

GovernanceFailureCert certifies that the inductive enumeration of governance failure modes has cardinality exactly 5. Researchers modeling institutional stability under configDim = 5 in the Recognition framework cite this structure when fixing the number of canonical modes. The definition supplies a single field that records the Fintype cardinality, with the concrete count supplied by a companion definition in the same module.

claimA structure $C$ equipped with a field asserting that the set of governance failure modes has cardinality 5, where the modes are the five enumerated cases capture, fragmentation, authoritarian drift, corruption, and legitimacy collapse.

background

The module defines five canonical governance failure modes tied to configDim D = 5. These modes are capture, fragmentation, authoritarian drift, corruption, and legitimacy collapse, each corresponding to the failure of one of the five canonical institutions. The inductive type GovernanceFailure enumerates exactly these cases and automatically derives Fintype, DecidableEq, and related instances.

proof idea

The declaration is a bare structure definition containing one field of type Prop. No lemmas or tactics are invoked inside the structure itself; the field is populated by the downstream definition governanceFailureCert, which simply assigns the result of the count function to the five_failures field.

why it matters in Recognition Science

The structure fixes the governance analysis at exactly five modes, matching the configDim = 5 convention stated in the module header. It is used directly by the definition governanceFailureCert that constructs the concrete certificate instance. Within the Recognition framework this supplies a static enumeration for institutional analysis but does not derive the count from the T0-T8 forcing chain, the Recognition Composition Law, or the phi-ladder mass formula.

scope and limits

formal statement (Lean)

  27structure GovernanceFailureCert where
  28  five_failures : Fintype.card GovernanceFailure = 5
  29

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.