2.4. actual_disposition: which plan is the agent's🔗

The agent's actual disposition — which allocation plan is the one the agent would follow. AllocationDisposition s is a type, inhabited by every function from sub-stock to served ends that meets the bookkeeping conditions; this predicate names the agent's own plan, so that an axiom can be restricted to it instead of speaking of every conceivable plan.

Source: tacit. Rothbard's argument presupposes ONE value scale and ONE allocation per actor ("the" marginal unit, "the" least urgent want, MES pp. 24–27); the tradition never contemplates rival plans for the same actor because it never quantifies over plans.

Status: our-reconstruction. Opaque, Prop-valued, on the receipt. It asserts a fact of the matter about WHICH plan is the agent's.

Does not say: that such a plan exists for every stock, or that it is unique. On Nozick's subjunctive account of preference the subjunctive may be undetermined (1977, p. 373), so whether a complete counterfactual table exists is left open. Theorems about dispositions take actual_disposition A as a hypothesis.

A stock of a good, for one agent at one time: finitely many unit-means the agent believes equally serviceable. Homogeneity is serviceability-homogeneity: each unit is believed to conduce to exactly the ends in serves — a BELIEF notion, not a preference notion. No indifference between units is asserted anywhere, so the strict-only Prefers stands and Rothbard's denial that indifference is demonstrable in action is not contradicted. Whether serviceability-homogeneity suffices for the law — Nozick (1977, p. 371) says the law needs indifference — stays checkable rather than assumed away.

What a unit IS is not fixed here: units lists whatever enters the action as one thing. Rothbard: the law holds "regardless of the size of the unit considered. The size of the unit will be the one that enters into concrete human action" (MES p. 28) — pairs of horses are a different stock with a "new and shorter scale of ends", and a good that "cannot be divided into homogeneous units for purposes of action" is a stock of one unit.

Apodictic.Stock.mk

units : Finset F.Means

serves : Set F.End

homog : ∀ u ∈ self.units, ∀ (e : F.End), F.Believes agent t u e ↔ e ∈ self.serves

The agent's counterfactual allocation disposition over a stock: for each sub-stock U — each set of units the agent might have — the ends the agent would serve with exactly those units, at the stock's single time. A NEW PRIMITIVE beyond Action, because a single actual allocation action cannot discriminate among the served ends (they are all inside the chosen package); whatever the law of marginal utility rests on, it is not actual action alone.

Indexed by WHICH units, not how many: that the plan depends only on the count is interchangeability of units, and it is not built in — it is the named condition Homogeneous, hypothesized where a theorem needs it.

Field-shape commitment (audit): card_eq is the one-unit-per-end idealization — with the units U (within the stock on hand), exactly as many ends would be served as there are units; units are not split, pooled, or left idle. Rothbard: "each unit of means is capable of serving one of the ends" — "We assume for simplicity" (MES p. 26). The definitional shape is our-reconstruction.

Apodictic.AllocationDisposition.mk

wouldServe : Finset F.Means → Finset F.End

serves_subset : ∀ (U : Finset F.Means), ∀ e ∈ self.wouldServe U, e ∈ s.serves

card_eq : ∀ U ⊆ s.units, (self.wouldServe U).card = U.card