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

Proof of `Two polynomial-time conventions, and their separation` (1st statement)

groundedproofs/Lax58Proofs/RamPolynomialComparison.lean · lax-58

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.

Read the Lean proof on GitHub

Description

The two tape presentations are compiled into one another. If TT and QQ are the source time and sufficient-width polynomials, the arena-to-native translation uses time 66T+6X+8166*T + 6*X + 81 and width Q+7Q + 7; the native-to-arena translation uses time 18T+2618*T + 26 and width Q+7Q + 7.

Thus a nonconstant time degree is preserved, while arena-to-native conversion can raise degree zero to degree one because the current adapter buffers the input in linear startup time. Width degree is unchanged for nonconstant QQ. Each implication chooses its own witnesses: this theorem neither states nor uses equality of polynomial degrees across the two directions.