1.5. The receipt🔗

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

propext and Quot.sound are Lean's logical background; they ride in with mathlib's finite sets. Classical.choice is absent: the library is constructive by default, so that a case split a proof needs is either named praxeological content or absent. The remaining four are the trusted base. The urgency principle and the chain form of the law have the same receipt; the supply-size form differs from the chain form only by the hypothesis A.Homogeneous, which is not an axiom and so does not appear here.