Proof of `Near-linear-time computation of Welzl orders`
conditional — 3 open assumptionsproofs/Lax235315Proofs/Assembly.lean · lax-235315
What this proof establishes
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
Conditional assembly for the near-linear Welzl-order algorithm. This proof assembles the construction's three independent contracts. It is conditional on their runtime, output-correctness, and finite-tape probability claims; it does not discharge those claims.
Proof strategy
Take the sum of the three eventual resource thresholds. The runtime contract gives total halting on every tape. Every tape in the successful-final-state set yields a witness, and the output contract makes that output acceptable. Monotonicity of finite cardinality transfers the probability lower bound from successful tapes to accepted tapes.
Attribution
The conditional contracts are the three separate theorem concepts in this submission. The assembled target is the registered claim of Lax195003; the graph result is Theorem 1.4 in the supplied arXiv v1 PDF.