ConflictResolutionCert
plain-language theorem explainer
ConflictResolutionCert bundles a cardinality claim on resolution mechanisms with a canonical J-cost threshold certificate. RS sociologists cite it to formalize how conflicts from recognition imbalance are resolved back to the phi band. The declaration is a bare structure definition whose fields are filled by sibling cardinality and certificate lemmas.
Claim. A structure certifying that the set of resolution mechanisms has cardinality exactly 5 and that the J-cost threshold satisfies the six canonical properties: $J(1)=0$, reciprocity $J(x)=J(1/x)$, $J(phi)>0$, the band $0.11<J(phi)<0.13$, and positivity of recovery $J(1/phi^2)>0$.
background
The module treats social conflict as a recognition-cost imbalance. Pre-conflict states have $J(r)=0$ at mutual recognition $r=1$; tension appears when $J(r)$ enters the $J(phi)$ band; outright conflict occurs for $J(r)>J(phi)$. Resolution returns the system to $J(r)leq J(phi)$ via one of five mechanisms. ResolutionMechanism is the inductive type whose five constructors are negotiation, mediation, arbitration, adjudication and force_. CanonicalCert is the upstream six-clause structure that encodes the J-function properties at the phi threshold.
proof idea
This is a structure definition with no proof body or tactics. The two fields simply package the Fintype.cardinality fact on ResolutionMechanism together with an instance of CanonicalCert; the downstream conflictResolutionCert supplies concrete values for both fields.
why it matters
The structure supplies the certificate used by conflictResolutionCert to witness the five-mechanism resolution model. It directly implements the module's claim that configDim D=5 for conflict mechanisms and anchors the J-cost threshold to the CanonicalJBand properties. It closes the sociology tier of the recognition framework by linking social conflict resolution to the same J-function that governs the phi-ladder and Berry threshold elsewhere in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.