Safety theorems for the HaltMonitor model

Three guarantees are proved:

• run_emitted_preserves_input — when the result is emitted, the emitted tokens equal the projected input tokens.
• run_emitted_implies_all_pass — when the result is emitted, every input item passes the threshold.
• run_any_fail_implies_halted — if any input item fails the threshold, the result is halted, not emitted.

Together these formalise the informal claim "no token whose coherence score falls below hard_limit is ever emitted".

theorem HaltMonitor.run_emitted_preserves_input (hardLimit : Score) (items : List Item) (ts : List Token) : run hardLimit items = Output.emitted ts → ts = List.map Prod.fst items

emitted ts can only come from the input whose token projection is ts.

theorem HaltMonitor.run_emitted_implies_all_pass (hardLimit : Score) (items : List Item) (ts : List Token) : run hardLimit items = Output.emitted ts → ∀ (it : Item), it ∈ items → Item.passes hardLimit it

When the monitor returns emitted, every input item has a score of at least hardLimit.

theorem HaltMonitor.run_any_fail_implies_not_emitted (hardLimit : Score) (items : List Item) (hexists : ∃ (it : Item), it ∈ items ∧ ¬Item.passes hardLimit it) (ts : List Token) : run hardLimit items ≠ Output.emitted ts

The contrapositive: if any input item fails the threshold, the run does not return emitted.

theorem HaltMonitor.run_any_fail_implies_halted (hardLimit : Score) (items : List Item) (hexists : ∃ (it : Item), it ∈ items ∧ ¬Item.passes hardLimit it) : ∃ (ts : List Token), run hardLimit items = Output.halted ts

The stronger phrasing: a failure anywhere in the input forces the monitor into the halted constructor.