PolarizationCert
plain-language theorem explainer
PolarizationCert packages a structure asserting exactly five polarization drivers together with an instance of the canonical J-band certificate. Modelers of affective polarization in the Recognition Science sociology tier would cite it to anchor the driver count and threshold in the J-cost framework. The declaration is a bare structure definition whose fields are typed by the Fintype cardinality of the driver inductive and by CanonicalCert.
Claim. A structure requiring that the set of polarization drivers has cardinality five and that the supplied threshold satisfies the six-clause canonical certificate for the J-function (J(1)=0, reciprocity J(x)=J(1/x), J(φ) in (0.11,0.13), and positivity of J(1/φ²)).
background
The module models political polarization as departure of opinion ratios r from 1, with group cohesion lost once J(r) exceeds J(φ). Five drivers are introduced as an inductive type: economic inequality, identity threat, media fragmentation, political sorting, and institutional mistrust, equipped with a Fintype instance so that their count is well-defined. The upstream CanonicalCert structure from CanonicalJBand supplies the six clauses that certify the J-function band around φ, including matched zero at unity, reciprocity, strict positivity at φ, the numerical band (0.11,0.13), and recovery positivity at 1/φ².
proof idea
The declaration is a structure definition with an empty proof body. It simply declares the two fields: the cardinality statement on the driver inductive type and the embedding of an instance of CanonicalCert.
why it matters
The structure supplies the certificate type instantiated by the downstream polarizationCert definition, which populates the driver count via polarizationDriverCount and the threshold via the imported cert. It thereby links the sociology module to the core J-band properties and supports the claim that polarization grows along the phi-ladder from a recognition-cost crossing. In the broader framework the five drivers align with configDim D, closing the interface for further sociological derivations without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.