Proof of `Linear-Time Construction on the Word RAM`
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
Compile one fixed structured program that initializes the deterministic seed, materializes successive rotation tables, and prints the complete final table.
Proof strategy
Each new row uses the exact zig-zag recurrence with indexed accesses to the fixed seed and preceding table. The old tables occupy disjoint consecutive memory blocks. A geometric potential pays for every growth stage. A final linear scan writes one word per vertex and the order header. The verified Lax808846 compiler bounds actual machine instructions and all physical addresses at every sufficiently large word width.