2.6. The hypotheses
The theorems take four hypotheses. Each is a situational condition, not a universal claim, and the diagnostic aim puts it in the statement so that it can be pointed at when it fails.
The first is actual_disposition A: the plan under discussion is the
agent's. The second is that the sub-stocks compared are on hand and
differ by one unit, s.OneMore U V; it descends from the supply
bound n โค s.units.card of the count-indexed days. The former axiom
quantified over every supply level, which is more than the
tradition's argument delivers; the disposition is data only within
the stock on hand, and the derivation gives the law only there. The
third is independence of uses. The fourth, interchangeability of
units, has its own section below.
Apodictic.ActionFrame.IndependentUses (F : ActionFrame) (a : F.Agent) (t : F.Time) : PropApodictic.ActionFrame.IndependentUses (F : ActionFrame) (a : F.Agent) (t : F.Time) : Prop
Independence of uses โ a situational applicability condition, NOT an axiom: bundle preference between two bundles that differ in one slot transfers to the two ends in that slot. Fails under complementarity (B valuable only together with A). Named here so it can be a hypothesis of the theorems that need it and be pointed at when it does not hold. Rothbard's "we assume for simplicity" (MES p. 26) covers one-unit-one-end; this is the further tacit assumption his derivation spends.
Independence became statable only when preference moved to bundles (2026-09-04). With preference over single ends there was no way even to write the condition that fails under complementarity. The human's objection that forced the move was "are not all ends composites?", and the answer is yes: "atomic" can only mean "not further divided by this action", the same relativity as the size of a unit (p. 28). So there is one ranking over bundles, and an end in the ordinary sense is a singleton bundle.
Apodictic.ActionFrame.PrefersEnd (F : ActionFrame) (a : F.Agent) (t : F.Time) (e e' : F.End) : PropApodictic.ActionFrame.PrefersEnd (F : ActionFrame) (a : F.Agent) (t : F.Time) (e e' : F.End) : Prop
Preference between ends in the ordinary sense: singleton-bundle preference. Definition, not a second relation.
The law is then 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, and it is strict, as his is.
Apodictic.marginalEnds {agent : World.Agent} {t : World.Time} {s : Stock World agent t} (A : AllocationDisposition s) (U V : Finset World.Means) : Set World.EndApodictic.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.
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.
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).