polarizationDriverCount
plain-language theorem explainer
The declaration fixes the number of polarization drivers at five in the Recognition Science sociology model. Researchers calibrating group cohesion via J-cost thresholds would cite this count when setting the configuration dimension D. The proof is a one-line wrapper that invokes the decide tactic on the Fintype instance derived from the inductive enumeration of the drivers.
Claim. The finite cardinality of the set of polarization drivers equals five: $|$ {economic inequality, identity threat, media fragmentation, political sorting, institutional mistrust} $| = 5$.
background
The module treats polarization as the departure of opinion ratios r from unity, which drives the recognition cost J(r) above J(φ) and produces in-group/out-group dynamics. PolarizationDriver is the inductive type whose five constructors list the canonical drivers: economicInequality, identityThreat, mediaFragmentation, politicalSorting, and institutionalMistrust. The module identifies this enumeration with configDim D and notes that observed polarization growth approximates φ².
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic evaluates Fintype.card directly from the Fintype instance that the inductive definition of PolarizationDriver derives via DecidableEq and BEq.
why it matters
This theorem supplies the driver count to the downstream polarizationCert definition, closing the sociology tier by fixing D = 5. It implements the module statement that the five drivers span configDim D and that polarization scales along the phi-ladder from a recognition-cost crossing. No open scaffolding questions are attached to the result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.