Certificate-independent formula round-trip machine
DisprovedCookLevin.formulaRoundTrip_certificate_independent_machinepolynomial-timesat-verifierturing-machine
There is a quadratic-time multi-tape Turing machine computing the canonical formula round-trip encoding whose final configuration is independent of the certificate tape. This construction obligation records the property actually needed to lift the unary computation to arbitrary two-input configurations, rather than asserting that every machine satisfying ComputesInTime ignores certificates.
Preamble
import Definitions.Def_CookLevin_Verifier
Formal statement
namespace CookLevin
theorem formulaRoundTrip_certificate_independent_machine :
∃ (M : Machine) (k G c1 : Nat),
TuringMachine k G M ∧
ComputesInTime M k (fun n => c1 * (n + 1) ^ 2)
(fun x => encodeFormula (decodeFormula x)) ∧
∀ x w : List Bool,
execute M (startConfig2 k (boolsToSymbols x) (boolsToSymbols w))
(c1 * (x.length + 1) ^ 2) =
execute M (startConfig2 k (boolsToSymbols x) [])
(c1 * (x.length + 1) ^ 2) := by sorry
end CookLevinSource