Draft — mutable and not usable as a dependency; its citation marks the draft state.

Proof of `Constructing polynomial space bounds`

groundedproofs/Lax307052Proofs/PolyBounds.lean · lax-307052

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.

Read the Lean proof on GitHub

Description

Count the input, append each polynomial term using nested counters, and scan the output track to halt at position p(n)+n+1p(n)+n+1.