Proof of `Correct outputs of the construction program`
groundedproofs/Lax235315Proofs/ProgramContracts.lean · lax-235315
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Every successful machine execution returns each vertex exactly once and satisfies the paper's crossing bound.
Proof strategy
Carry the verifier's concrete partitions and the ordered deletion log through each accepted source round. Replay the actual stored intervals into the terminal active-vertex scan and apply the crossing induction. The final source success test preserves this output guarantee. Source and machine determinism transfer the result to every successful terminal machine state. The proof uses no probability assumption.
Attribution
The graph reduction and crossing argument follow Dreier and Kuske, arXiv:2602.14625v1. Concrete source execution and compiler simulation are formalized using the Lax808846 word-RAM framework.