While this submission is a draft, it cannot be used by other submissions.

Environment v4.30.0. The archive's epoch is v4.33.0; only submissions in v4.30.0 can cite this work.

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 66∗T+6∗X+8166*T + 6*X + 81 and width Q+7Q + 7; the native-to-arena translation uses time 18∗T+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.