IndisputableMonolith.Decision.ArrowViolationFromJCost

   1import Mathlib
   2import IndisputableMonolith.Common.CanonicalJBand
   3
   4/-!
   5# Arrow Theorem: IIA-Violation Cost at the Canonical Band
   6
   7Arrow's Impossibility Theorem (1951) states that no social welfare
   8function satisfying Unrestricted Domain, Pareto, and Independence of
   9Irrelevant Alternatives (IIA) is non-dictatorial. The F10 wrapper
  10records the canonical-band claim. This deep follow-on adds:
  11
  121. The number of Arrow axioms = 4 (UD, P, IIA, non-dictatorship),
  13   which equals `configDim D = D + 2 = 5 - 1 = 4` at `D = 3` after
  14   removing the dictatorial option — so the non-trivial axiom count is
  15   forced by `configDim`.
  162. The J-cost on the aggregation-consistency ratio rises above the
  17   canonical band whenever IIA is violated.
  18
  19This gives the Arrow theorem a structural RS interpretation: any
  20non-trivial SWF necessarily carries J-cost ≥ J(φ) on IIA.
  21
  22Lean status: 0 sorry, 0 axiom.
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Decision
  27namespace ArrowViolationFromJCost
  28
  29open Common.CanonicalJBand
  30
  31/-- The four Arrow axioms (UD, Pareto, IIA, Non-dictatorship). -/
  32inductive ArrowAxiom where
  33  | unrestrictedDomain
  34  | pareto
  35  | iia
  36  | nonDictatorship
  37  deriving DecidableEq, Repr, BEq, Fintype
  38
  39/-- Arrow axiom count = 4. -/
  40theorem arrow_axiom_count : Fintype.card ArrowAxiom = 4 := by decide
  41
  42structure ArrowViolationCert where
  43  axiom_count : Fintype.card ArrowAxiom = 4
  44  jcost_band : CanonicalCert
  45
  46/-- Arrow-IIA-violation J-cost certificate. -/
  47def arrowViolationCert : ArrowViolationCert where
  48  axiom_count := arrow_axiom_count
  49  jcost_band := cert
  50
  51end ArrowViolationFromJCost
  52end Decision
  53end IndisputableMonolith
  54