Polynomial-time Tseitin reduction machine

This surface module exposes the concrete deterministic machine implementing the total encoded CNF-SAT-to-3SAT reduction. Its explicit quartic time bound includes validation, register initialization, valid-input transformation, and the fixed malformed-input fallback.

Main results

• ThreeSAT.Machine.reductionTM_computesInTime
• ThreeSAT.reduction_mem_FP

theorem Complexity.SAT.ThreeSAT.Machine.reductionTM_computesInTime : reductionTM.ComputesInTime reduction fun (n : ℕ) => 6 * n + 16384 * (n + 2) ^ 4 + 49

The concrete Tseitin reduction machine computes the total encoded reduction within an explicit quartic time bound.

theorem Complexity.SAT.ThreeSAT.reduction_mem_FP : reduction ∈ FP

The total encoded CNF-SAT-to-3SAT reduction is polynomial-time computable.