Documentation

Complexitylib.SAT.Tseitin.Machine.Internal.PolynomialTime

Polynomial-time correctness of the Tseitin reduction machine #

This module combines the typed valid-input controller proof with the fixed malformed-input fallback. The decoder decides which execution theorem applies, and both branches fit one explicit quartic budget depending only on the input bit length.

Main results #

source
def Complexity.SAT.ThreeSAT.Machine.reductionMachineTime (n : ℕ) :
ℕ

One uniform time allowance for validation, branching, and the streaming Tseitin controller.

Equations
Instances For
    source
    theorem Complexity.SAT.ThreeSAT.Machine.reductionMachineTime_le_quartic_internal (n : ℕ) :
    reductionMachineTime n ≤ 16439 * (n + 2) ^ 4

    The explicit running-time allowance is bounded pointwise by one shifted quartic monomial.

    source
    theorem Complexity.SAT.ThreeSAT.Machine.reductionMachineTime_bigO_quartic_internal :
    BigO reductionMachineTime fun (x : ℕ) => x ^ 4

    In the standard asymptotic convention, the uniform allowance is O(n⁴).

    source
    theorem Complexity.SAT.ThreeSAT.Machine.reductionTM_computesInTime_internal :
    reductionTM.ComputesInTime reduction reductionMachineTime

    The concrete machine computes the total encoded Tseitin reduction within the uniform quartic allowance on every bit string.