Proof of `Two polynomial-time conventions, and their separation` (1st statement)
groundedproofs/Lax58Proofs/RamPolynomialComparison.lean · lax-58
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 two tape presentations are compiled into one another. If and are the source time and sufficient-width polynomials, the arena-to-native translation uses time and width ; the native-to-arena translation uses time and width .
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 . Each implication chooses its own witnesses: this theorem neither states nor uses equality of polynomial degrees across the two directions.