IndisputableMonolith.Decision.VotingParadoxesFromJCost

   1import Mathlib
   2import IndisputableMonolith.Common.CanonicalJBand
   3
   4/-!
   5# F10: Voting Paradoxes from J-Cost on Preference-Aggregation Ratio
   6
   7Arrow's Theorem (1951), Condorcet paradox (1785), and Gibbard-
   8Satterthwaite (1973-75) all sit structurally at the same canonical
   9J-cost band on the dimensionless preference-aggregation ratio
  10`r := observed_aggregation_consistency / target_consistency`.
  11
  12The structural prediction: every electoral system that violates
  13Arrow's IIA does so at J-cost above the canonical band on a
  14sufficiently rich preference profile; systems that stay within the
  15band are limited to the trivial dictatorial / random / unanimity
  16classes per Arrow.
  17
  18Falsifier: a non-trivial electoral system that satisfies all four
  19Arrow axioms simultaneously (would falsify Arrow itself, hence the
  20RS-derived band claim).
  21
  22Lean status: 0 sorry, 0 axiom.
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Decision
  27namespace VotingParadoxesFromJCost
  28
  29open Common.CanonicalJBand
  30
  31structure VotingParadoxesCert where
  32  base : CanonicalCert
  33
  34def votingParadoxesCert : VotingParadoxesCert where
  35  base := cert
  36
  37end VotingParadoxesFromJCost
  38end Decision
  39end IndisputableMonolith
  40