Five formalizations

Parent: stages-and-gates

Same skeleton, five lenses:

1. Automaton / recognizer — stages = states, gates = guarded transitions (advance enabled iff criterion g holds). The machine recognizes trajectories that clear every gate; it doesn't generate them → recognizer-not-generator.
2. Hoare logic / proof obligations (deepest) — {P} S₁ {Q}; {Q} S₂ {R}. The intermediate assertion Q is the gate: the owner writes the assertions, the agent supplies an execution satisfying the triple. Gate = a proof obligation; stage = the (possibly neural) tactic → lcf-for-labor.
3. Options / hierarchical RL (Sutton) — an option ⟨I, π, β⟩: initiation set I, intra-policy π (free execution), termination β = the gate. A stage is an option; HRL = stages-within-stages (recursion).
4. Supervisory control (Ramadge–Wonham) — the gate disables the controllable advance until the completion event is observed: "commit unreachable until green." Veto, not command → ramadge-wonham-supervisory-control.
5. Real options / staged financing — escalating commitment = a compound option; each gate buys the right (not the obligation) to fund the next stage. Turns one big bet into a chain of abortable small options.