10. Automation, resources, and open routes

Plain-English statement. The first time an adapted cumulative spending process reaches a fixed budget is a stopping time.

Intuition

Whether the budget has been exhausted by time n can be decided from information available by time n.

Why it is needed

Any rigorous bandits-with-knapsacks route must stop at a random, history-observable exhaustion time.

Place in the proof

This is a compiled foundation leaf, not a BwK model or regret theorem.

Proof idea

Express exhaustion as Mathlib's hittingAfter construction and use adaptedness to prove measurability of each level event.

Lean reading notes

The stopping time takes values in WithTop Nat, allowing the budget never to be reached.

Teaching dependencies

No direct teaching dependency recorded.

theorem isStoppingTime_budgetExhaustionTime_of_adapted {Omega : Type u} [mOmega : MeasurableSpace Omega] {F : Filtration Nat mOmega} {spent : Nat -> Omega -> Nat} (budget : Nat) (hspent : Adapted F spent) : IsStoppingTime F (budgetExhaustionTime spent budget)

Plain-English statement. A harness task records the target, task kind, status, source and scenario cards, profile, required artifacts, and acceptance gates used by the automation system.

Intuition

Proof automation is safer when completion criteria are data that can be inspected, rather than an informal instruction that can drift across runs.

Why it is needed

The website uses the same status discipline: a theorem card, a planned target, and a compiled Lean theorem are visibly different objects.

Place in the proof

This structure belongs to the automation layer rather than the mathematical bandit theory.

Proof idea

It is a structure definition. The default Lean gate later instantiates the acceptance condition with the repository's build command.

Lean reading notes

Inductive TaskStatus and TaskKind values make invalid status strings unrepresentable inside Lean-side harness data.

Teaching dependencies

No direct teaching dependency recorded.

structure HarnessTask where