1.6. Not in the base
Two doctrinally central claims are not cited by any theorem and are therefore not axioms. The bridge from actual action to preference, demonstrated preference in Rothbard's sense, is stated here in the form it would take, and it is parked:
/-- PARKED: the bridge from actual action to preference. Not 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 claim that there is action at all. The structure of action itself is a definition, and no theorem uses it yet.
Apodictic.Action (F : ActionFrame) : TypeApodictic.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.mkFields
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.