1.5. The conditions🔗

The theorems take five assumptions besides the claims. Each says something about the situation rather than about action as such, and each is written into the statement, so a reader can point at it and say: that is the one that did not hold. Where one fails, the law says nothing — it is silent, not wrong.

stock.OneMore fewer more: the two piles compared are both on hand and differ by exactly one unit. The plan says nothing about piles the man does not hold, and neither does the law.
IndependentUses agent time: what one want is worth does not depend on which other wants are being served.
plan.Homogeneous: the plan depends only on how many units there are, not on which ones. Only the size-based form of the law needs it.
stock.ComparableServiceable: any two wants the good can serve are ranked one way or the other. Mises's route and the ladder read as a history need it; Rothbard's never does.
earlier.NoNewUses later: the good is believed to serve no use at the later moment that it was not believed to serve at the earlier one. Only the ladder read as a history needs it, and it is the one condition there that spans two moments. It is about belief in what the good can do, not about the scale, and it runs one way: the man learns no new use, though he may drop an old one.

Nothing here has to say which plan is the man's. A theorem is handed a plan and makes its claim about that one, so there is no rival plan anyone could build to refute it.

All five are given in full here, in the order they are listed above, because these are the assumptions a reader has to judge. Exchange takes conditions of its own, about trades rather than stocks; they are given in full under Exchange. Time preference takes its own too, about dated ends, given in full under Time preference. The regression theorem's are about a record of exchanges, given in full under The regression theorem.

def

Apodictic.Stock.OneMore {praxis : ActionFrame} {agent : praxis.Agent}
  {time : praxis.Time} (stock : Stock praxis agent time)
  (fewer more : Finset praxis.Means) : Prop
Apodictic.Stock.OneMore
  {praxis : ActionFrame}
  {agent : praxis.Agent}
  {time : praxis.Time}
  (stock : Stock praxis agent time)
  (fewer more : Finset praxis.Means) :
  Prop

more is fewer plus one unit, both inside the stock. It is said with an inclusion and a count rather than by naming the extra unit, so that sub-stocks are only ever supposed and never constructed — which is why nothing here needs to decide when two units are the same unit.

def

Apodictic.ActionFrame.IndependentUses (praxis : ActionFrame)
  (agent : praxis.Agent) (time : praxis.Time) : Prop
Apodictic.ActionFrame.IndependentUses
  (praxis : ActionFrame)
  (agent : praxis.Agent)
  (time : praxis.Time) : Prop

Independence of uses — a condition on the situation, NOT a universal claim. If two bundles differ in exactly one slot, then preferring one bundle to the other carries down to preferring the one end to the other. It fails where uses are complementary: where B is worth having only alongside A. It is named here so that the theorems that need it carry it as a hypothesis, and so a reader can point at it where it does not hold.

This is NOT a premise Rothbard spends. He ranks wants against each other directly, off a scale that is already ranked (MES pp. 25–26, Figure 3), and never argues from bundles at all. It is what OUR decomposition costs. Where he makes one fused claim, we make a claim about bundles plus this condition — and complementarity, which his wording never has to face, lands here once the pieces are pulled apart. To assert this rather than hypothesize it would be to assert that complementarity never happens.

def

Apodictic.AllocationPlan.Homogeneous {praxis : ActionFrame}
  {agent : praxis.Agent} {time : praxis.Time}
  {stock : Stock praxis agent time} (plan : AllocationPlan stock) : Prop
Apodictic.AllocationPlan.Homogeneous
  {praxis : ActionFrame}
  {agent : praxis.Agent}
  {time : praxis.Time}
  {stock : Stock praxis agent time}
  (plan : AllocationPlan stock) : Prop

Interchangeability of units — a condition on the situation, NOT a praxeological claim. The plan depends only on how many units there are, not on which ones: any two sub-stocks of the same size would serve the same ends.

Without it, the phrase "the plan at n units" — and so the marginal utility of a supply of n — picks out nothing in particular. Rothbard makes interchangeability part of what a supply IS: "If a specific unit is differently evaluated from all other units, then the supply of that good is only one unit" (MES p. 23). Where it fails, the units are not one good, and the supply-size form of the law does not treat them as one. Like the plan it constrains, it speaks of sub-stocks the agent may not hold.

def

Apodictic.Stock.ComparableServiceable {praxis : ActionFrame}
  {agent : praxis.Agent} {time : praxis.Time}
  (stock : Stock praxis agent time) : Prop
Apodictic.Stock.ComparableServiceable
  {praxis : ActionFrame}
  {agent : praxis.Agent}
  {time : praxis.Time}
  (stock : Stock praxis agent time) : Prop

Comparability of the ends a good can serve — a condition on the situation, NOT a praxeological claim.

Any two ends the good can serve are ranked one way or the other. It is confined to one stock's serviceable ends, not asserted of every pair of ends in the frame, because that is all any theorem needs.

Where it fails, a theorem carrying it is SILENT rather than false: an agent may simply never have had occasion to rank two ends against each other, and Rothbard's own doctrine — that scales are revealed in action and nowhere else — makes such agents the normal case rather than the exotic one. Mises says the same thing in almost the same words: "the scale of values or wants manifests itself only in the reality of action. These scales have no independent existence apart from the actual behavior of individuals" (Human Action, ch. IV, §2).

Carried by the Mises route (Apodictic.Mises.ladder_from_order), by the ladder read as a history (Apodictic.Temporal.ladder_judged_earlier), and by no theorem on the Rothbard route. That asymmetry is a finding: swap dominance forces a comparison between every served end and every unserved serviceable one, so this condition can only fail for a pair that never straddles a margin — see Apodictic.Model.rothbard_applies_where_mises_is_silent.

def

Apodictic.Stock.NoNewUses {praxis : ActionFrame} {agent : praxis.Agent}
  {earlierTime laterTime : praxis.Time}
  (earlier : Stock praxis agent earlierTime)
  (later : Stock praxis agent laterTime) : Prop
Apodictic.Stock.NoNewUses
  {praxis : ActionFrame}
  {agent : praxis.Agent}
  {earlierTime laterTime : praxis.Time}
  (earlier :
    Stock praxis agent earlierTime)
  (later : Stock praxis agent laterTime) :
  Prop

The good is believed to serve no new use — whatever the good is believed to serve at the later moment, it was believed to serve at the earlier one: the later stock's serviceable ends are among the earlier stock's.

A situational condition, and the one condition on the history reading that spans two moments. It runs one way, and it is about BELIEF about the good, not about the scale of values: between the two moments the man learns no new use for the good. It is there so that the want the added unit goes to was on the earlier scale at all. Where he does learn one, the earlier-judged ladder is silent.

Does not say that the good's uses stay the same: a use believed in earlier may be dropped later. Says nothing about the scale at either moment, about which units are held, or about the order of the two times. Carried by Apodictic.Temporal.ladder_judged_earlier and by nothing else.