Axioms.lean

View source on GitHub

Modeling assumptions (definitional choices in Auction.lean)

These are assumptions of the model, but they're encoded as definitions rather than axioms — reject any and you'd need different definitions, not a different axiom file:

• Quasilinear utility — utility is defined as value minus payment
• Positive bids and sigmas — carried as fields on Report and Valuation
• Independent private values — withReport changes reports, not valuations
• Free disposal — empty player set means zero welfare
• Gaussian valuation decay — trueVal is an exponential in squared distance

Typeclass constraints (structural requirements)

• Finite nonempty advertisers — [Fintype ι] [Nonempty ι]
• Inner product space — [NormedAddCommGroup E] [InnerProductSpace ℝ E]

QueryMeasure

The sole axiom: there exists a monotone functional from (E → ℝ) to ℝ. If f(x) ≥ g(x) everywhere, then integrate f ≥ integrate g.

Note what this does not assume: normalization, linearity, additivity, or even nontriviality. It is weaker than a probability measure — any monotone functional satisfies it. An economist might interpret it as an expected-value operator, but the proof only uses monotonicity.

structure QueryMeasure (E : Type*) where
  integrate : (E → ℝ) → ℝ
  integral_mono : ∀ (f g : E → ℝ),
    (∀ x, f x ≥ g x) → integrate f ≥ integrate g

Monotonicity holds for any finite positive measure and any standard notion of integration. It replaces Mathlib's full measure theory stack with the one property the proof actually uses.

; Four monotone functionals — all satisfy integral_mono
(define xs (let loop ((i 0) (acc '()))
  (if (> i 100) (reverse acc) (loop (+ i 1) (cons (/ i 100.0) acc)))))

(define (f x) (exp (- x)))
(define (g x) (exp (* -2 x)))

(define (mu-sum h) (apply + (map h xs)))
(define (mu-max h) (apply max (map h xs)))
(define (mu-min h) (apply min (map h xs)))
(define (mu-pt h) (h 1.0))

(define (check name mu)
  (let ((mf (mu f)) (mg (mu g)))
    (display name) (display ": f=")
    (display (round (* mf 1000) )) (display "/1000  g=")
    (display (round (* mg 1000))) (display "/1000  mono=")
    (display (>= mf mg)) (newline)))

(check "sum  " mu-sum)
(check "max  " mu-max)
(check "min  " mu-min)
(check "point" mu-pt)

import math

xs = [i / 100 for i in range(101)]

def f(x): return math.exp(-x)      # slower decay
def g(x): return math.exp(-2*x)    # faster decay; f >= g everywhere

# Four very different "integrals" — all monotone
def mu_sum(h):  return sum(h(x) for x in xs)
def mu_max(h):  return max(h(x) for x in xs)
def mu_min(h):  return min(h(x) for x in xs)
def mu_pt(h):   return h(xs[-1])  # point evaluation

print("if f(x) >= g(x) everywhere, does integrate(f) >= integrate(g)?")
print()
for name, mu in [("sum", mu_sum), ("max", mu_max), ("min", mu_min), ("point", mu_pt)]:
    mf, mg = mu(f), mu(g)
    print(f"  {name:6s}  f={mf:.4f}  g={mg:.4f}  mono={mf >= mg}")

print()
print("All four satisfy integral_mono.")
print("The proof needs nothing more.")

What's a hypothesis on theorems (not axiomatized)

• isTruthful — player i reports honestly. Precondition on the DSIC theorem: only player i needs to be truthful.
• allTruthful — all players report honestly. Used for efficiency theorems and the Nash equilibrium corollary.

Connections

• IntegralEfficiency.lean — uses integral_mono to lift pointwise welfare to integrated welfare
• GaussianOptimality.lean — composes everything through QueryMeasure