1.4. Theorems🔗

Rothbard's urgency principle, that the loss of a unit falls on the least urgent want, is a theorem here rather than a premise. What the axiom delivers is stronger than the principle, so the workhorse is stated first.

theorem

Apodictic.served_over_unserved {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t} (A : AllocationDisposition s)
  (hA : actual_disposition A) (hI : World.IndependentUses agent t)
  (U : Finset World.Means) (hU : U ⊆ s.units) (e : World.End) :
  e ∈ A.wouldServe U →
    ∀ e' ∈ s.serves, e' ∉ A.wouldServe U → World.PrefersEnd agent t e e'
Apodictic.served_over_unserved
  {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t}
  (A : AllocationDisposition s)
  (hA : actual_disposition A)
  (hI : World.IndependentUses agent t)
  (U : Finset World.Means)
  (hU : U ⊆ s.units) (e : World.End) :
  e ∈ A.wouldServe U →
    ∀ e' ∈ s.serves,
      e' ∉ A.wouldServe U →
        World.PrefersEnd agent t e e'

Served over unserved — the workhorse: with any sub-stock on hand, every end the agent would serve is preferred to every serviceable end the agent would not. This is all swap_dominance delivers, and it is more than Rothbard states: it compares a served end with ANY unserved serviceable end, not only with the one the next unit would reach. Derived under the hypothesis that uses are independent (module docstring).

Proof shape: swapping the served e for the unserved e' is dominated (swap_dominance); the served bundle is e plus the rest (insert_sdiff_self_of_mem); the two bundles now differ in one slot, and independence reads off e ≻ e'.

theorem

Apodictic.urgency_principle {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t} (A : AllocationDisposition s)
  (hA : actual_disposition A) (hI : World.IndependentUses agent t)
  (U V : Finset World.Means) (hUV : s.OneMore U V) (e : World.End) :
  e ∈ A.wouldServe U →
    ∀ e' ∈ A.wouldServe V,
      e' ∉ A.wouldServe U → World.PrefersEnd agent t e e'
Apodictic.urgency_principle
  {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t}
  (A : AllocationDisposition s)
  (hA : actual_disposition A)
  (hI : World.IndependentUses agent t)
  (U V : Finset World.Means)
  (hUV : s.OneMore U V) (e : World.End) :
  e ∈ A.wouldServe U →
    ∀ e' ∈ A.wouldServe V,
      e' ∉ A.wouldServe U →
        World.PrefersEnd agent t e e'

The urgency principle (Rothbard), in counterfactual-loss form: for an agent's allocation disposition over a stock, every end that would still be served with the units U is preferred to every end that would be abandoned in the step down from V, one unit more — the loss falls on the least urgent want. One application of served_over_unserved: the abandoned end is serviceable and unserved at U; that V is U plus one unit is not used beyond that.

The law is stated over Rothbard's own definition of the marginal utility of a supply: the ends that would be given up on the loss of one unit. It comes in two forms. Along a chain of named units it needs no interchangeability; in Rothbard's wording, by supply size, it does.

def

Apodictic.marginalEnds {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t} (A : AllocationDisposition s)
  (U V : Finset World.Means) : Set World.End
Apodictic.marginalEnds
  {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t}
  (A : AllocationDisposition s)
  (U V : Finset World.Means) :
  Set World.End

Marginal utility of the step U → V (one more unit), Rothbard's sense: the ends the extra unit adds — equivalently, the ends that would be given up on its loss. "The marginal utility of the supply is the end that must be given up as the result of a loss of the unit" (MES p. 27); "he gives up the least urgent of the wants which the larger stock would have satisfied" (p. 25). A set rather than a single end: determinacy of the drop is not assumed (see module docstring). A Set, not a Finset: set difference on Finset needs decidable equality on World.End, which the opaque world does not supply, and reaching for Classical would put Classical.choice on the receipt for no praxeological reason. Definition, not axiom — Rothbard introduces it as a definition ("is called", "is known as"). Imputation of value from ends to units — "actors value means strictly in accordance with their valuation of the ends that they believe the means can serve" (p. 19) — is what licenses calling this the utility of the unit. Indexed by the step, not by a size: which ends a unit adds may depend on which units are already on hand unless the plan is Homogeneous.

theorem

Apodictic.marginal_utility_chain {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t} (A : AllocationDisposition s)
  (hA : actual_disposition A) (hI : World.IndependentUses agent t)
  (U V W : Finset World.Means) (_hUV : s.OneMore U V)
  (hVW : s.OneMore V W) (e : World.End) :
  e ∈ marginalEnds A U V →
    ∀ e' ∈ marginalEnds A V W, World.PrefersEnd agent t e e'
Apodictic.marginal_utility_chain
  {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t}
  (A : AllocationDisposition s)
  (hA : actual_disposition A)
  (hI : World.IndependentUses agent t)
  (U V W : Finset World.Means)
  (_hUV : s.OneMore U V)
  (hVW : s.OneMore V W) (e : World.End) :
  e ∈ marginalEnds A U V →
    ∀ e' ∈ marginalEnds A V W,
      World.PrefersEnd agent t e e'

The law of marginal utility, along a chain of specific units: for U ⊂ V ⊂ W each one unit more, every end the step U → V adds is preferred to every end the step V → W adds. No interchangeability of units is needed: the chain names which units. One application of urgency_principle; the marginality of e at the first step is unused (_h_marg).

theorem

Apodictic.marginal_utility {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t} (A : AllocationDisposition s)
  (hA : actual_disposition A) (hI : World.IndependentUses agent t)
  (hH : A.Homogeneous) (U V U' V' : Finset World.Means)
  (hUV : s.OneMore U V) (hU'V' : s.OneMore U' V') (n : ℕ)
  (hn : V.card = n) (hn' : V'.card = n + 1) (e : World.End) :
  e ∈ marginalEnds A U V →
    ∀ e' ∈ marginalEnds A U' V', World.PrefersEnd agent t e e'
Apodictic.marginal_utility
  {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t}
  (A : AllocationDisposition s)
  (hA : actual_disposition A)
  (hI : World.IndependentUses agent t)
  (hH : A.Homogeneous)
  (U V U' V' : Finset World.Means)
  (hUV : s.OneMore U V)
  (hU'V' : s.OneMore U' V') (n : ℕ)
  (hn : V.card = n)
  (hn' : V'.card = n + 1)
  (e : World.End) :
  e ∈ marginalEnds A U V →
    ∀ e' ∈ marginalEnds A U' V',
      World.PrefersEnd agent t e e'

The law of marginal utility (Rothbard, MES, ch. 1, p. 27): "The greater the supply of a good, the lower the marginal utility; the smaller the supply, the higher the marginal utility." By supply SIZE: every end marginal at a supply of n units is preferred to every end marginal at a supply of n + 1 — for ANY two one-unit steps reaching those sizes; the steps need not share a unit.

Needs Homogeneous A, exactly once: the plan with the n units below the second step is the plan with the n units of the first. The marginality of e at n is unused (_h_marg).