Proof of `Worst-case running time 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
The fixed construction program halts within the claimed word-RAM budget on every admissible tape, including rejected attempts.
Proof strategy
Compose setup, the guarded adaptive loop and both final output branches at source cost . Stored graph histories certify safe reconstruction on accepted paths. The bounded compiler simulation transfers the full execution to the fixed word-RAM program; covers its step cost and workspace bounds. Empty and singleton inputs have separate complete execution proofs.
Attribution
The algorithm and asymptotic target are from Dreier and Kuske, arXiv:2602.14625v1. The source semantics and word-RAM compiler are supplied by Lax808846.