1.8. The horses in Lean🔗

The case from the opening, built. It does a second job at the same time. If Rothbard's own six horses satisfy the claim and every condition at once, then those assumptions can all hold together, and the theorems are not empty.

Wants are ranks on the man's value scale, and the lower rank is the more urgent want:

def

Apodictic.Model.rankPrefers (X Y : Set Model.Want) : Prop
Apodictic.Model.rankPrefers
  (X Y : Set Model.Want) : Prop

Preference between bundles of wants. X is preferred to Y exactly when the two differ by a single swap, and the want X has in place of Y's is the more urgent of the two — which here just means the lower rank.

The man's plan is the obvious one — with any n horses he serves the n most urgent wants — and it satisfies the claim. Wants can be told apart, uses are independent, one-horse steps exist inside the stable, each step has a marginal end, and preference is asymmetric. That last one matters: it means the claim holds somewhere preference is strict, which is how it was meant all along and what no_rival_swap_dominant needs.

Two of the theorems here are conclusions Rothbard reached himself, not bookkeeping. The first is his result at p. 25:

theorem

Apodictic.Model.loss_of_a_horse_ends_pleasure_riding :
  Model.pleasureRiding ∈
    marginalEnds (Model.horsePlan 6) (Finset.range 5) (Finset.range 6)
Apodictic.Model.loss_of_a_horse_ends_pleasure_riding :
  Model.pleasureRiding ∈
    marginalEnds (Model.horsePlan 6)
      (Finset.range 5) (Finset.range 6)

Rothbard's own conclusion, p. 25. With six horses the man serves the six most urgent wants. Lose one, and what he gives up is the sixth-ranked want — pleasure riding, in Rothbard's telling: "the loss of a horse will cause him to give up pleasure riding".

Here it is a calculation about the plan, not a further assumption.

The second is the point he names two horses in order to make, and it is the reason the plan is encoded the way it is:

theorem

Apodictic.Model.which_horse_does_not_matter :
  (Model.horsePlan 6).wouldServe
      ((Finset.range 6).erase Model.manOWar) =
    (Model.horsePlan 6).wouldServe
      ((Finset.range 6).erase Model.seabiscuit)
Apodictic.Model.which_horse_does_not_matter :
  (Model.horsePlan 6).wouldServe
      ((Finset.range 6).erase
        Model.manOWar) =
    (Model.horsePlan 6).wouldServe
      ((Finset.range 6).erase
        Model.seabiscuit)

Rothbard's own conclusion, p. 27 — the one he names two horses to make. Losing Man o' War, who was leading a wagon, leaves the man serving exactly the ends he would serve after losing Seabiscuit, who was out for pleasure riding: he simply moves Seabiscuit to the wagon. Which horse goes makes no difference to which end is surrendered.

This is what interchangeability amounts to, and it is why the plan is indexed by WHICH horses while Homogeneous is a separate named condition: the claim has to be statable before it can be true.

And the last step is the point:

theorem

Apodictic.Model.horses_law_applies (k n : ℕ) (h : n < k)
  (h' : n + 1 < k) (addedFirst : Model.Horses.End) :
  addedFirst ∈
      marginalEnds (Model.horsePlan k) (Finset.range n)
        (Finset.range (n + 1)) →
    ∀
      addedSecond ∈
        marginalEnds (Model.horsePlan k) (Finset.range (n + 1))
          (Finset.range (n + 2)),
      Model.Horses.PrefersEnd () () addedFirst addedSecond
Apodictic.Model.horses_law_applies
  (k n : ℕ) (h : n < k) (h' : n + 1 < k)
  (addedFirst : Model.Horses.End) :
  addedFirst ∈
      marginalEnds (Model.horsePlan k)
        (Finset.range n)
        (Finset.range (n + 1)) →
    ∀
      addedSecond ∈
        marginalEnds (Model.horsePlan k)
          (Finset.range (n + 1))
          (Finset.range (n + 2)),
      Model.Horses.PrefersEnd () ()
        addedFirst addedSecond

The law itself, applied to the horses. Every hypothesis of marginal_utility_chain is met at this frame. So the claim and the conditions on the situation can all hold at once, and the law is not empty. That is the whole consistency argument: this type-checks, therefore they fit together.

That is the law itself, applied to the horses, with every assumption met — every assumption, that is, of the chain form. The size-based form asks for one thing more, interchangeability, and the horses meet that too:

theorem

Apodictic.Model.horses_homogeneous (k : ℕ) :
  (Model.horsePlan k).Homogeneous
Apodictic.Model.horses_homogeneous
  (k : ℕ) :
  (Model.horsePlan k).Homogeneous

Interchangeability holds of the plan: it depends on how many horses there are, never on which.

Nothing was copied across by hand: horses_swapDominant proves exactly the statement the theorem asks for.

theorem

Apodictic.Model.horses_swapDominant (k : ℕ) :
  SwapDominant (Model.horsePlan k)
Apodictic.Model.horses_swapDominant
  (k : ℕ) :
  SwapDominant (Model.horsePlan k)

The man's plan is swap-dominant — the claim itself, proved of this frame and this plan. Serving the n most urgent wants beats any one-swap alternative, because any want swapped in ranks below every want swapped out.

Two places where this departs from Rothbard, both said out loud rather than papered over. His ten ends are "for simplicity", to fit a diagram; putting a ceiling on the scale would drag an extra condition through every theorem and buy nothing, so here the horses can serve any rank. And which of the earlier horses is Man o' War is arbitrary — Rothbard says only that he arrived before Seabiscuit, and nothing about a horse except its identity enters any claim.