apodictic machine-checked praxeology

1.3. Hypotheses🔗

The theorems take four hypotheses. Each is a situational condition, not a universal claim, and each is in the statement so that it can be pointed at when it fails. Where one fails the law is silent, not refuted.

  • actual_disposition A: the plan under discussion is the agent's.

  • s.OneMore U V: the sub-stocks compared are on hand, and differ by one unit. The disposition is data only there, and the law holds only there.

  • IndependentUses agent t: the value of an end does not depend on which other ends are served.

  • A.Homogeneous: the plan depends only on how many units, not which. Needed only by the supply-size form of the law.

🔗def
Apodictic.ActionFrame.IndependentUses (F : ActionFrame) (a : F.Agent) (t : F.Time) : Prop
Apodictic.ActionFrame.IndependentUses (F : ActionFrame) (a : F.Agent) (t : F.Time) : Prop

Independence of uses — a situational applicability condition, NOT an axiom: bundle preference between two bundles that differ in one slot transfers to the two ends in that slot. Fails under complementarity (B valuable only together with A). Named here so it can be a hypothesis of the theorems that need it and be pointed at when it does not hold. Rothbard's "we assume for simplicity" (MES p. 26) covers one-unit-one-end; this is the further tacit assumption his derivation spends.