2.1. The receipt🔗

Lean can list the axioms a proof depends on. For the law of marginal utility the list is this:

'Apodictic.marginal_utility' depends on axioms: [propext,
 World,
 actual_disposition,
 ends_distinguishable,
 swap_dominance,
 Quot.sound]

Two of the six are Lean's logical background, not praxeology: propext and Quot.sound ride in with mathlib's finite sets. Classical.choice is absent, by decision (2026-09-04): the library is constructive by default, so that when a proof needs a case split we are forced to ask whether the split is praxeological content, and if so to name it. The remaining four are the trusted base. The urgency principle, which Rothbard offers as the premise, has the same receipt, because it is derived rather than asserted.

Every axiom carries a docstring with two required fields. Source is a citation or "tacit". Status is one of three verdicts: explicit-in-tradition (Rothbard or Mises say it), suppressed-premise (they use it without saying it), or our-reconstruction (a formalization decision the tradition never faced). The docstrings below are the axiom-by-axiom catalogue; there is no other.

One rule governs what appears in the base at all. An axiom enters at the point of first use: it lives in the base only while some theorem's receipt cites it. Two doctrinally central axioms are therefore not here, and the last section says why that is the main finding so far.

A second rule governs what is an axiom and what is not. The aim of the audit is diagnostic: Austrian conclusions fail to match reality in known cases, so some assumption is off, and we want to point at which one. So claimed-universal facts about action are axioms, on the receipt, and if one is false praxeology is wrong. Situational conditions under which a law applies are named hypotheses in the theorem statement, and where they fail the law is silent rather than refuted. The Austrian reply "the conditions did not hold" then names a checkable hypothesis instead of an escape hatch.