Threshold monotonicity for the HaltMonitor model

The safety theorems in HaltMonitor.Properties fix the threshold and reason about a single run. This file proves how the monitor behaves as the threshold moves — the formal counterpart of "approved() is monotone with respect to the threshold" (Verified-AI FVGK programme, phase 1):

• passes_antitone — passing a stricter (higher) threshold implies passing any looser (lower) one.
• run_all_pass_emitted — the converse of run_emitted_implies_all_pass: if every item passes, the run emits the whole input.
• run_threshold_monotone — lowering the threshold can never turn an emitting stream into a halting one. Equivalently, raising the threshold is the only way to introduce a halt: tightening is safe-by-construction.

theorem HaltMonitor.passes_antitone {h1 h2 : Score} (hle : h1 ≤ h2) {it : Item} (h : Item.passes h2 it) : Item.passes h1 it

Passing a stricter (higher) threshold implies passing any looser one.

theorem HaltMonitor.run_all_pass_emitted (hardLimit : Score) (items : List Item) : (∀ (it : Item), it ∈ items → Item.passes hardLimit it) → run hardLimit items = Output.emitted (List.map Prod.fst items)

Converse of run_emitted_implies_all_pass: when every item passes the threshold, the monitor emits the whole input unchanged.

theorem HaltMonitor.run_threshold_monotone {h1 h2 : Score} (hle : h1 ≤ h2) (items : List Item) (hemit : (run h2 items).isEmitted = true) : (run h1 items).isEmitted = true

Threshold monotonicity. If the stricter limit h2 emits the whole stream, then the looser limit h1 ≤ h2 does too — lowering the threshold cannot introduce a halt.