2.8. What the law does not rest on🔗

The receipt does not cite an axiom about actual action. This is the main finding to date, and it took two passes to state correctly.

The first pass (2026-08-02) announced that the demonstrated-preference bridge "does no work" and Nozick was vindicated. That was partly an artifact: the urgency principle had been compressed into an axiom that bypassed the bridge. The second pass (2026-09-04) unwound the compression and derived the principle, expecting the bridge to re-enter. It did not. The derivation runs on the subjunctive extension alone. The bridge is parked with its pedigree:

/-- PARKED (2026-09-04): the bridge from actual action to
preference, in the bundle form it would need today. Never cited by
any theorem; lives in the document, not the base. -/
axiom demonstrated_preference (a : Action World) :
    ∀ e ∈ a.forgone, World.Prefers a.agent a.time {a.chosen} {e}

So is the existence axiom, "humans act". Here the archaeology is about the shape of the famous axiom rather than its use. In this encoding it is not one axiom. It decomposes into the definition of action, carried by the fields of Action; the bridge above; and an existence claim that there is action at all. Only the bridge could do deductive work, and nothing has needed it. The existence claim would guard against vacuity under the distinguished frame, and no theorem has an existential conclusion yet, so it too waits.

structure

Apodictic.Action (F : ActionFrame) : Type
Apodictic.Action (F : ActionFrame) : Type

An action: an agent, at a time, employs means in the belief that they conduce to a chosen end, forgoing at least one alternative end.

The fields are jointly constitutive — nothing with fewer components counts as an action — but this is a definition, not an assertion. Shape: our-reconstruction. No theorem yet uses it: the law of marginal utility rests on the counterfactual disposition alone.

Constructor

Apodictic.Action.mk

Fields

agent : F.Agent

The acting person.

time : F.Time

When the action happens.

chosen : F.End

The end aimed at.

means : F.Means

The means employed.

forgone : Set F.End

Ends forgone in acting — the material of opportunity cost. A bare set: "the next-best alternative" would presuppose ranking structure this file does not have.

forgone_nonempty : self.forgone.Nonempty

Action is choice: something is always forgone (at minimum, inaction).

chosen_not_forgone : self.chosen ∉ self.forgone

The chosen end is not among the forgone.

belief : F.Believes self.agent self.time self.means self.chosen

The agent believes the employed means conduce to the chosen end.

The structure is a definition, not an assertion. That split, between the jointly constitutive package and the separable claims about it, is nowhere in Mises. It was adopted (2026-08-02) because the type-checker makes reshaping cheap while little is built on top, and because the asymmetry favours starting split: collapsing separable axioms into one is bundling; prying a monolith apart rewrites every proof that used the conjunction.

2.8.1. Rejected: the urgency principle as an axiom🔗

For the record, the axiom that the theorem replaced. It claimed every supply level and, restated over today's vocabulary, quantifies over every disposition; it almost certainly had the same over-quantification hole as the first swap_dominance, though that was never checked because it was superseded the same day.

/-- SUPERSEDED (2026-09-04, evening): the urgency principle asserted,
over the count-indexed disposition of the time. Compare the theorem
`urgency_principle`, which has the same conclusion under two more
hypotheses. -/
axiom urgency_principle_asserted
    {agent : World.Agent} {t : World.Time} {s : Stock World agent t}
    (A : CountDisposition s) (n : ℕ) :
    ∀ e ∈ A.wouldServe n, ∀ e', e' ∈ A.wouldServe (n + 1) →
      e' ∉ A.wouldServe n → World.PrefersEnd agent t e e'