Proof of `Native RAM execution of the weight-to-multiplicity reduction`
groundedproofs/Lax263307Proofs/NativeWeightReduction.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
The compiled command consumes the actual encoded input and emits its computed multiplicity buffer. A single explicit magnitude exponent bounds all integer products, source indices, and input words. Layout allowance and instruction counts fit one fixed quadratic polynomial, for every larger word width.