Proof of `A fixed RAM program constructing the complete moment LP`
groundedproofs/Lax263307Proofs/NativeMomentProgram.lean · lax-263307
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
Compile the actual catalog, metadata, matrix and vector loops. Every written word is bounded by the guarded RAM semantics, and output is exactly the registered LP encoding. The same program works for all graphs and parameters, with one quartic time/word-width bound, including empty graphs.