resolutionMechanismCount
The theorem asserts that the set of canonical conflict resolution mechanisms has cardinality exactly five. Peace studies researchers applying J-cost thresholds to model negotiation and enforcement would cite this count to fix configDim D = 5. The proof is a one-line decision procedure that evaluates the finite type cardinality from the inductive enumeration.
claimThe set of canonical conflict resolution mechanisms has cardinality five: $|$negotiation, mediation, arbitration, adjudication, force$| = 5$.
background
The module models social conflict as arising when recognition imbalance J(r) exceeds the J(phi) threshold (0.11-0.13 band). Resolution returns the system to J(r) ≤ J(phi) via one of five mechanisms. Pre-conflict starts at J(r) = 0 (mutual recognition r = 1), tension occupies the J(phi) band, and conflict occurs for J(r) > J(phi).
proof idea
The proof applies the decide tactic to Fintype.card ResolutionMechanism = 5. The inductive type ResolutionMechanism carries a Fintype instance derived from its five constructors, so the decision procedure computes the cardinality by enumeration.
why it matters in Recognition Science
This supplies the five_mechanisms field of the downstream conflictResolutionCert definition. It instantiates the module claim that resolution mechanisms number five and equal configDim D = 5 in Tier F Peace Studies. The result closes the sociological count without reference to the spatial forcing chain T8 or the Recognition Composition Law.
scope and limits
- Does not derive the five mechanisms from the J-cost functional equation.
- Does not prove uniqueness or completeness beyond the given inductive definition.
- Does not address empirical mapping of real conflicts onto these mechanisms.
- Does not connect to the phi-ladder mass formula or eight-tick octave.
Lean usage
five_mechanisms := resolutionMechanismCountformal statement (Lean)
30theorem resolutionMechanismCount : Fintype.card ResolutionMechanism = 5 := by decide
proof body
31