Setup specifications for the Tseitin reduction machine

This proof-only module establishes the compositional contracts used before the streaming controller starts. The fresh-variable setup first parks every tape, measures the source encoding, and increments the resulting unary register. A separate one-step machine clears the validator verdict, after which the input can be rewound while the initialized registers and empty output accumulator are preserved.

Main results

• seedFreshTM_hoareTime_internal — exact setup state within 4 * |z| + 11 steps
• clearValidationOutputTM_hoareTime_internal — generic one-step clear rule
• clearValidationOutputTM_verdict_hoareTime_internal — clear a Boolean verdict
• rewindInputTM_after_validation_hoareTime_internal — framed input rewind
• fallbackEmitter_hoareTime_internal — emit the fixed fallback from a clear output

theorem Complexity.SAT.ThreeSAT.Machine.seedFreshTM_hoareTime_internal (z : List Bool) : seedFreshTM.HoareTime (fun (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool z) ∧ (∀ (i : Fin workTapeCount), work i = Tape.init []) ∧ out = Tape.init []) (TM.EmitPred { head := 1, cells := (Tape.init (List.map Γ.ofBool z)).cells } (Function.update (fun (x : Fin workTapeCount) => TM.regTape 0) freshReg (TM.regTape (z.length + 1))) []) (4 * z.length + 11)

The three setup phases take linear time. This bound includes both seqTM phase-boundary steps.

theorem Complexity.SAT.ThreeSAT.Machine.seedFreshTime_le_linear_internal (n : ℕ) : 4 * n + 11 ≤ 11 * (n + 1)

The exact setup budget is bounded by a linear polynomial with a convenient single coefficient.

theorem Complexity.SAT.ThreeSAT.Machine.clearValidationOutputTM_hoareTime_internal (inp₀ : Tape) (work₀ : Fin workTapeCount → Tape) (out₀ : Tape) (hinp₀ : TM.Parked inp₀) (hwork₀ : ∀ (i : Fin workTapeCount), TM.Parked (work₀ i)) (hout₀ : TM.Parked out₀) : clearValidationOutputTM.HoareTime (fun (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀.write Γw.blank.toΓ) 1

Blanking the symbol under a parked output head takes one step. The input, all work tapes, and the output head are preserved exactly.

theorem Complexity.SAT.ThreeSAT.Machine.clearValidationOutputTM_verdict_hoareTime_internal (inp₀ : Tape) (work₀ : Fin workTapeCount → Tape) (hinp₀ : TM.Parked inp₀) (hwork₀ : ∀ (i : Fin workTapeCount), TM.Parked (work₀ i)) : clearValidationOutputTM.HoareTime (fun (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out.head = 1 ∧ out.cells 0 = Γ.start ∧ (∃ (verdict : Bool), out.cells 1 = Γ.ofBool verdict) ∧ ∀ (j : ℕ), 2 ≤ j → out.cells j = Γ.blank) (TM.EmitPred inp₀ work₀ []) 1

Clear the Boolean verdict left at output cell one by validationTM. Cells beyond the verdict are assumed blank, as they are in the standard front-end run; the result is the canonical empty output accumulator.

theorem Complexity.SAT.ThreeSAT.Machine.rewindInputTM_after_validation_hoareTime_internal (z : List Bool) (work₀ : Fin workTapeCount → Tape) (hwork₀ : ∀ (i : Fin workTapeCount), TM.Parked (work₀ i)) : TM.rewindInputTM.HoareTime (fun (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool z)).cells ∧ inp.head ≤ z.length + 1 ∧ work = work₀ ∧ TM.OutAcc [] out) (TM.EmitPred { head := 1, cells := (Tape.init (List.map Γ.ofBool z)).cells } work₀ []) (z.length + 3)

Rewind the source input after validation, preserving both the initialized register family and the cleared output accumulator.

theorem Complexity.SAT.ThreeSAT.Machine.rewindInputTime_le_linear_internal (n : ℕ) : n + 3 ≤ 3 * (n + 1)

The framed rewind budget is itself bounded linearly.

theorem Complexity.SAT.ThreeSAT.Machine.fallbackEmitter_hoareTime_internal (inp₀ : Tape) (work₀ : Fin workTapeCount → Tape) (hinp₀ : TM.Parked inp₀) (hwork₀ : ∀ (i : Fin workTapeCount), TM.Parked (work₀ i)) : (TM.emitBitsTM fallbackEncoding).HoareTime (TM.EmitPred inp₀ work₀ []) (TM.EmitPred inp₀ work₀ fallbackEncoding) 28

Once the validator verdict has been cleared, the fixed malformed-input fallback is emitted in its concrete constant length.