Proof of `Reconstruction yields a graph Welzl order`
groundedproofs/Lax235315Proofs/ReconstructionBridge.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 public reconstruction certificate has exactly the same content as the proof-side certificate, so the established crossing induction proves its encoded graph Welzl order.
Proof strategy
Convert each public twin expansion, checked reduction, and run to the corresponding proof-side certificate by induction on the constructors. The lists, sets, and checks agree directly; then apply the existing certified-run correctness theorem.
Attribution
This bridge carries the reconstruction correctness proof of Theorem 3.2 in Dreier and Kuske, Near-Linear Time Computation of Welzl Orders on Graphs with Linear Neighborhood Complexity, into the submitted certificate types.