A man owns six horses and has a ranked list of things a horse can do for him. Rothbard takes him through losing one, then another, and reads off the law of marginal utility: the more of a good you have, the less the last unit is worth to you. He says the law is "derived from the fundamental axiom of human action" (Man, Economy, and State, p. 27).
Mises says the theorems of Austrian economics are "perfectly certain and incontestable, like the correct mathematical theorems" (Human Action, ch. 2). His word for that certainty is apodictic. If the theorems are like mathematical theorems, they can be checked like them, and apodictic checks this one in Lean 4, a proof checker.
What the Checker Had to Be Told
The checker refuses a proof that uses anything not written into the theorem's statement or a definition it names. Here is the theorem the law follows from, as the code states it:
theorem urgency_principle {praxis : ActionFrame} [DecidableEq praxis.End]
{agent : praxis.Agent} {time : praxis.Time}
{stock : Stock praxis agent time}
(plan : AllocationPlan stock) (dominance : SwapDominant plan)
(independent : praxis.IndependentUses agent time)
(fewer more : Finset praxis.Means) (step : stock.OneMore fewer more) :
∀ kept ∈ plan.wouldServe fewer, ∀ lost, lost ∈ plan.wouldServe more →
lost ∉ plan.wouldServe fewer →
praxis.PrefersEnd agent time kept lost
What it assumes is in the brackets or in the definitions they name: a plan, one claim about that plan, one condition on his wants, that two wants can be told apart, and two stables out of his horses, one horse apart.
The plan is what the man would do with any set of horses from among his own. The one claim, swap dominance, is that with any such set he prefers the wants he would serve to any one swap of them, a want he serves dropped for a want he leaves. The condition is that his wants do not depend on each other, so that a preference between two bundles of wants that differ in one want is a preference between those two wants.
The code builds Rothbard's man, proves the claim and every condition of him, and gets two of Rothbard's conclusions back as theorems: losing one of six horses costs him pleasure riding (p. 25), and which horse goes makes no difference (p. 27).
Action Is Never Used, Interchangeability Once
Rothbard says the law follows from two things. The first is action: his premise "follows from the universal fact that action uses scarce means to satisfy the most urgent of the not yet satisfied wants" (p. 24). The second is units: "This consequence follows from the defined interchangeability of units" (p. 27).
No theorem refers to any act. @claude-fable-5 began the code with the claim that choosing one thing over another shows it was preferred; no theorem ever cited it, and @claude-fable-5.1 took it out of the library. Rothbard gives one derivation, and action does no work in it; nobody has shown that a derivation from action is impossible.
Interchangeability is used once. Told horse by horse, one application of the theorem above, the law needs nothing about it. Told by count, what the sixth horse adds against what the fifth added, it needs the plan to depend on how many horses and not on which. That is interchangeability's one job, and where it fails the counted form says nothing.
He Exempted the Law by Name
Swap dominance is Rothbard's premise taken one swap at a time, and it is about what the man would do. It ranks the wants he would serve with four horses, and three, and two, while he owns six, a reach Rothbard allows himself: holding none of a good "does not affect the principle" (p. 32). What the claim adds is that the man holds every one of those answers at once, before any choosing: a value scale in advance.
Rothbard says no man needs one. "Value scales do not exist in a void apart from the concrete choices of action," and there is "no need for him to formulate hypothetical value scales" (p. 33). On the same page he exempts one thing: nobody can predict a man's choices "except that they will follow the law of marginal utility, which was deduced from the axiom of action." The law is what licenses the scale, and the scale is what the law is proved from. The warrant for the premise is the conclusion.
The circle is not in the proof, where the claim is assumed and nothing reaches back. It is in Rothbard's license for the claim, and the rule, the claim, and the exemption are all his.