Proof of `Success probability 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
At least two thirds of the finite random tapes make the explicit construction program terminate successfully.
Proof strategy
For each adaptive source round, interpret its exact fresh Boolean block as the literal random-key input. A block outside the graph-dependent bad set produces a collision-free good sample, so the literal verifier accepts and the stored reduction history advances. The finite adaptive protocol counts the bad blocks with a per-round conditional bound; its bit potential fits within the machine tape. Good paths are coupled to actual source executions, including the guarded prefix, every reduction round, and terminal output. The source compiler transfer yields the claimed word-RAM tape count. Empty, singleton, and initial no-round inputs are handled separately.
Attribution
The sampling and contraction argument follows Dreier and Kuske, arXiv:2602.14625v1. The explicit source and word-RAM semantics use Lax808846.