The reduction emitter, assembled

emitTM N p computes the Cook–Levin reduction: bump the tapes, measure the input, evaluate the time polynomial, initialize the radix and fuel registers, and emit the seven encoded clause families of tableauCNFFlat N (p.eval |x|) x.

The file then proves the running time polynomially bounded (via the PolyBnd closure kit), concluding reductionFn N (p.eval ·) ∈ FP, the Cook–Levin reductions cookLevin_reduction_singleTape / cookLevin_reduction, and the headlines NPHard_language and NPComplete_language for the SAT language language.

def Complexity.SAT.initVals (n steps P Qc tf : ℕ) : Fin Emit.nT → ℕ

The register file after initialization (tf = the row-loop fuel).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.Tape.inits (n steps P Qc tf : ℕ) : Fin Emit.nT → Tape

The corresponding tape file.

Equations

• Complexity.SAT.Tape.inits n steps P Qc tf i = Complexity.TM.regTape (Complexity.SAT.initVals n steps P Qc tf i)

theorem Complexity.SAT.Tape.inits_parked (n steps P Qc tf : ℕ) (i : Fin Emit.nT) : TM.Parked (inits n steps P Qc tf i)

Every tape in the initialized register file is Parked.

noncomputable def Complexity.SAT.emitInitTM (N : NTM 1) (p : Polynomial ℕ) : TM Emit.nT

The register initialization chain: input length, time polynomial, tableau width, radices, and position fuels.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.initBudget (Mp M : ℕ) (p : Polynomial ℕ) : ℕ

Budget of the initialization chain: the polynomial evaluation plus sixteen register operations.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.emitInitTM_hoareTime (N : NTM 1) (p : Polynomial ℕ) (x : List Bool) (steps P Mp M : ℕ) (hsteps : steps = Polynomial.eval x.length p) (hP : P = steps + x.length + 1) (hMp : ∀ k ≤ p.natDegree + 1, TM.hornerFold x.length (List.take k (TM.polyCoeffs p)) 0 ≤ Mp) (hnMp : x.length ≤ Mp) (hM : 4 * (steps + 1) * max (Fintype.card N.Q) 3 * (P + 2) * 4 ≤ M) (ys : List Bool) : (emitInitTM N p).HoareTime (TM.EmitPred { head := 1, cells := (Tape.init (List.map Γ.ofBool x)).cells } (fun (x : Fin Emit.nT) => TM.regTape 0) ys) (TM.EmitPred { head := 1, cells := (Tape.init (List.map Γ.ofBool x)).cells } (Tape.inits x.length steps P (Fintype.card N.Q) 0) ys) (initBudget Mp M p)

emitInitTM Hoare specification. From the bumped all-zero register file, reach the initialized file; Mp caps the Horner evaluation, M the tableau values.

theorem Complexity.SAT.Tape.inits_update_tFuel (n steps P Qc tf tf' : ℕ) : Function.update (inits n steps P Qc tf) Emit.tFuel (TM.regTape tf') = inits n steps P Qc tf'

Overwriting tFuel in an initialized register file just changes the fuel parameter.

theorem Complexity.SAT.scratch_initTapes (n steps P Qc tf : ℕ) : TM.scratch (Tape.inits n steps P Qc tf) Emit.tmp Emit.tmp2 0 = Tape.inits n steps P Qc tf

Zeroing the scratch registers tmp/tmp2 of an initialized register file is a no-op: they already hold 0.

noncomputable def Complexity.SAT.emitBodyTM (N : NTM 1) : TM Emit.nT

The family chain: fuel setups, the seven families, counter resets.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.bodyBudget (N : NTM 1) (M : ℕ) : ℕ

Budget of the family chain.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.emitBodyTM_hoareTime (N : NTM 1) (x : List Bool) (steps P M : ℕ) (hP : P = steps + x.length + 1) (hM : 4 * (steps + 1) * max (Fintype.card N.Q) 3 * (P + 2) * 4 ≤ M) (ys : List Bool) : (emitBodyTM N).HoareTime (TM.EmitPred { head := 1, cells := (Tape.init (List.map Γ.ofBool x)).cells } (Tape.inits x.length steps P (Fintype.card N.Q) 0) ys) (fun (inp : Tape) (_work : Fin Emit.nT → Tape) (out : Tape) => inp = { head := 1, cells := (Tape.init (List.map Γ.ofBool x)).cells } ∧ TM.OutAcc (ys ++ (tableauCNFFlat N steps x).encode) out) (bodyBudget N M)

emitBodyTM Hoare specification: from the initialized register file and empty accumulator, emit the encoded flat tableau.

noncomputable def Complexity.SAT.emitTM (N : NTM 1) (p : Polynomial ℕ) : TM Emit.nT

The Cook–Levin reduction machine: bump, initialize, emit.

Equations

• Complexity.SAT.emitTM N p = Complexity.TM.bumpTM.seqTM ((Complexity.SAT.emitInitTM N p).seqTM (Complexity.SAT.emitBodyTM N))

def Complexity.SAT.emitMp (p : Polynomial ℕ) (n : ℕ) : ℕ

The Horner-evaluation value cap.

Equations

• Complexity.SAT.emitMp p n = ((Complexity.TM.polyCoeffs p).sum + 1) * (n + 1) ^ (p.natDegree + 1) + n

def Complexity.SAT.emitM (N : NTM 1) (p : Polynomial ℕ) (n : ℕ) : ℕ

The tableau value cap.

Equations

• Complexity.SAT.emitM N p n = 4 * (Polynomial.eval n p + 1) * max (Fintype.card N.Q) 3 * (Polynomial.eval n p + n + 1 + 2) * 4

def Complexity.SAT.emitTime (N : NTM 1) (p : Polynomial ℕ) (n : ℕ) : ℕ

The reduction machine's running time.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.emitTM_computesInTime (N : NTM 1) (p : Polynomial ℕ) : (emitTM N p).ComputesInTime (reductionFn N fun (n : ℕ) => Polynomial.eval n p) (emitTime N p)

The reduction machine computes the reduction function.

def Complexity.SAT.PolyBnd (f : ℕ → ℕ) : Prop

Dominated by a Polynomial ℕ evaluation.

Equations

• Complexity.SAT.PolyBnd f = ∃ (q : Polynomial ℕ), ∀ (n : ℕ), f n ≤ Polynomial.eval n q

theorem Complexity.SAT.PolyBnd.const (c : ℕ) : PolyBnd fun (x : ℕ) => c

Constant functions are polynomially bounded.

theorem Complexity.SAT.PolyBnd.id : PolyBnd fun (n : ℕ) => n

The identity function is polynomially bounded.

theorem Complexity.SAT.PolyBnd.add {f g : ℕ → ℕ} (hf : PolyBnd f) (hg : PolyBnd g) : PolyBnd fun (n : ℕ) => f n + g n

Polynomial boundedness is closed under pointwise addition.

theorem Complexity.SAT.PolyBnd.mul {f g : ℕ → ℕ} (hf : PolyBnd f) (hg : PolyBnd g) : PolyBnd fun (n : ℕ) => f n * g n

Polynomial boundedness is closed under pointwise multiplication.

theorem Complexity.SAT.PolyBnd.mono {f g : ℕ → ℕ} (hg : PolyBnd g) (h : ∀ (n : ℕ), f n ≤ g n) : PolyBnd f

A function pointwise below a polynomially bounded one is itself polynomially bounded.

theorem Complexity.SAT.PolyBnd.pow {f : ℕ → ℕ} (hf : PolyBnd f) (k : ℕ) : PolyBnd fun (n : ℕ) => f n ^ k

Polynomial boundedness is closed under a fixed power.

theorem Complexity.SAT.PolyBnd.eval (p : Polynomial ℕ) : PolyBnd fun (n : ℕ) => Polynomial.eval n p

Evaluating a Polynomial ℕ is polynomially bounded (by itself).

theorem Complexity.SAT.PolyBnd.opBudget {f : ℕ → ℕ} (hf : PolyBnd f) : PolyBnd fun (n : ℕ) => TM.opBudget (f n)

Budget compositions preserve polynomial boundedness.

theorem Complexity.SAT.PolyBnd.layerBudget {f : ℕ → ℕ} (hf : PolyBnd f) : PolyBnd fun (n : ℕ) => TM.layerBudget (f n)

layerBudget of a polynomially bounded value cap is polynomially bounded.

theorem Complexity.SAT.PolyBnd.loadBudget {f : ℕ → ℕ} (hf : PolyBnd f) : PolyBnd fun (n : ℕ) => TM.loadBudget (f n)

loadBudget of a polynomially bounded value cap is polynomially bounded.

theorem Complexity.SAT.PolyBnd.emitVarBudget {f : ℕ → ℕ} (hf : PolyBnd f) : PolyBnd fun (n : ℕ) => TM.emitVarBudget (f n)

emitVarBudget of a polynomially bounded value cap is polynomially bounded.

theorem Complexity.SAT.PolyBnd.clauseBudget {L f : ℕ → ℕ} (hL : PolyBnd L) (hf : PolyBnd f) : PolyBnd fun (n : ℕ) => SAT.clauseBudget (L n) (f n)

clauseBudget with polynomially bounded length and value cap is polynomially bounded.

theorem Complexity.SAT.PolyBnd.cnfBudget {K L f : ℕ → ℕ} (hK : PolyBnd K) (hL : PolyBnd L) (hf : PolyBnd f) : PolyBnd fun (n : ℕ) => SAT.cnfBudget (K n) (L n) (f n)

cnfBudget with polynomially bounded clause count, clause length, and value cap is polynomially bounded.

theorem Complexity.SAT.PolyBnd.loopBudget {f inner : ℕ → ℕ} (hf : PolyBnd f) (hinner : PolyBnd inner) : PolyBnd fun (n : ℕ) => SAT.loopBudget (f n) (inner n)

loopBudget with polynomially bounded iteration count and body budget is polynomially bounded.

theorem Complexity.SAT.emitTime_polyBnd (N : NTM 1) (p : Polynomial ℕ) : PolyBnd (emitTime N p)

The running time is polynomially bounded. A mechanical walk over the budget definitions with the PolyBnd closure kit.

theorem Complexity.SAT.reductionFn_mem_FP (N : NTM 1) (p : Polynomial ℕ) : (reductionFn N fun (n : ℕ) => Polynomial.eval n p) ∈ FP

The reduction is polynomial-time computable — for an explicit polynomial time bound n ↦ p.eval n. The tableau has size polynomial in p.eval |x| (hence in |x|), and emitTM emits its encoding in polynomial time.

theorem Complexity.SAT.cookLevin_reduction_singleTape {L : Language} (N : NTM 1) (T : ℕ → ℕ) (c : ℕ) (hdec : N.DecidesInTime L T) (hTO : BigO T fun (x : ℕ) => x ^ c) : L ≤ₚ language

Single-tape Cook–Levin reduction. A single-work-tape machine deciding L in polynomial time yields a polynomial-time many-one reduction to language. The abstract bound T is first replaced by a dominating explicit polynomial (BigO.pow_polynomial_bound), since the reduction function is only computable for explicit bounds; deciding transfers by monotonicity.

theorem Complexity.SAT.cookLevin_reduction {k : ℕ} {L : Language} (N : NTM k) (T : ℕ → ℕ) (c : ℕ) (hdec : N.DecidesInTime L T) (hTO : BigO T fun (x : ℕ) => x ^ c) : L ≤ₚ language

Per-machine Cook–Levin reduction. If a nondeterministic machine N decides L within a polynomial time bound, then L polynomial-time many-one reduces to language. Reduces to the single-work-tape case (NTM.exists_singleTape_decidesInTime) and then builds the tableau formula.

theorem Complexity.SAT.NPHard_language : NPHard language

NP-hardness of SAT. Every language in NP polynomial-time reduces to language.

theorem Complexity.SAT.NPComplete_language : NPComplete language

Cook–Levin theorem: SAT is NP-complete.