apodictic machine-checked praxeology

2.7. The units: where interchangeability is used๐Ÿ”—

The brief named this the known trap: the law needs homogeneous units, and Rothbard denies that indifference is demonstrable in action. The count-indexed disposition above had walked around it by putting interchangeability into a type: a plan that is a function of a number cannot depend on which units. The receipt could not see that.

On 2026-09-05 the index became the sub-stock, the set of units the agent would have, and interchangeability became a named condition.

๐Ÿ”—def
Apodictic.AllocationDisposition.Homogeneous {F : ActionFrame} {agent : F.Agent} {t : F.Time} {s : Stock F agent t} (A : AllocationDisposition s) : Prop
Apodictic.AllocationDisposition.Homogeneous {F : ActionFrame} {agent : F.Agent} {t : F.Time} {s : Stock F agent t} (A : AllocationDisposition s) : Prop

Interchangeability of units โ€” a situational applicability condition, NOT an axiom: the plan depends only on how many units, not which. Two sub-stocks of the same size would serve the same ends. This is what makes "the plan at n units" โ€” and so the marginal utility of a supply of n โ€” a function of n. Rothbard makes it definitional of a supply: "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 law in its supply-size form does not apply to them as one. Subjunctive, like the disposition it constrains.

The sub-stocks are hypothesized, never constructed: "one unit more" is inclusion plus a count, so no decidable equality on units was forced, though an erase-based statement would have forced one.

๐Ÿ”—def
Apodictic.Stock.OneMore {F : ActionFrame} {agent : F.Agent} {t : F.Time} (s : Stock F agent t) (U V : Finset F.Means) : Prop
Apodictic.Stock.OneMore {F : ActionFrame} {agent : F.Agent} {t : F.Time} (s : Stock F agent t) (U V : Finset F.Means) : Prop

V is U plus one unit, within the stock. Stated by inclusion and cardinality, so that the sub-stocks are hypothesized, never constructed โ€” no decidable equality on units is needed anywhere.

The prototype compiled at the first attempt, which by the project's rule is a warning, and the examination is the finding. Served over unserved, the urgency principle, and the law along a chain of named units need no interchangeability: each is about one sub-stock, and none compares two of the same size. Rothbard's wording, by supply size, uses it exactly once, to identify the plan at one sub-stock of size n with the plan at another. Without it "the marginal utility of a supply of n units" is not a function of n, so the supply-size form cannot be stated. That is Nozick's p. 371, "without the notion of a unit ... we have no way to state the law", located: a condition on stating the law by size, not a premise of the ordering.

๐Ÿ”—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).

Three notions of homogeneity were in play, and the text has all three. Equal serviceability, Stock.homog, is p. 22, "equally capable of rendering the same service", a belief notion; it does no formal work in either form of the law. Indifference in value between units is p. 23, "Cow A and cow B were valued equally", "regards horses B and C indifferently", and it is withdrawn on p. 24: interchangeability "does not mean that the concrete units are actually valued equally." It is needed nowhere. What the supply-size form needs is the third, that the plan ignores which units, and that is subjunctive, what the agent would serve with horses A and B against B and C. It is the same kind of commitment the base already carries in swap_dominance, so the trap is one collision, not two.

Where the condition lives was the human's decision. An axiom bridging equal serviceability to a homogeneous plan would have put a fifth line on the receipt and made Stock.homog do work; it would also claim a universal fact about action where the text gives a definition. Rothbard: "If a specific unit is differently evaluated from all other units, then the supply of that good is only one unit" (p. 23). Interchangeability is what makes units one supply, so where it fails the law's supply-size form is silent about them as one good, and a hypothesis says exactly that. The other premise Rothbard names for the reallocation, "disregard of past events" (p. 27), has nothing to bite on in a one-instant frame, and waits for time to do work.