Valid-input assembly for the Tseitin reduction machine

This file isolates the machine-combinator proof needed to plug a valid-input emitter into reductionTMWith. The emitter starts only after validation has succeeded, the validator verdict has been cleared, and the source input has been rewound to cell one.

The principal theorem is generic in the emitter's postcondition. Its sole framing requirement is stability under the standard combinator transition, which is exactly the final transition performed by ifTM.

Main results

• reductionTMWith_valid_hoareTime_internal
• reductionTMWith_valid_emit_hoareTime_internal
• reductionTMWith_valid_emit_reachesIn_internal

Branch-local contract

Validation routing

Full valid path

theorem Complexity.SAT.ThreeSAT.Machine.reductionTMWith_valid_hoareTime_internal (validEmitter : TM workTapeCount) (z : List Bool) {emitterPost : TapePred workTapeCount} {emitterTime : ℕ} (hvalid : validEncoding z = true) (hEmitter : validEmitter.HoareTime (validEmitterPre z) emitterPost emitterTime) (hpostTransition : ∀ (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape), emitterPost inp work out → emitterPost (TM.transitionInput inp) (fun (i : Fin workTapeCount) => TM.transitionTape (work i)) (TM.transitionTape out)) : (reductionTMWith validEmitter).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 []) emitterPost (6 * z.length + emitterTime + 25)

Generic valid branch of the total reduction. A valid input reaches the supplied emitter only after the exact validEmitterPre frame has been established. The result is returned under any emitter postcondition stable under the final ifTM combinator transition.

theorem Complexity.SAT.ThreeSAT.Machine.reductionTMWith_valid_emit_hoareTime_internal (validEmitter : TM workTapeCount) (z ys : List Bool) (emitterTime : ℕ) (hvalid : validEncoding z = true) (hEmitter : validEmitter.HoareTime (validEmitterPre z) (TM.EmitPred { head := 1, cells := (Tape.init (List.map Γ.ofBool z)).cells } (frontEndWork z) ys) emitterTime) : (reductionTMWith validEmitter).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 } (frontEndWork z) ys) (6 * z.length + emitterTime + 25)

Specialization for an emitter that preserves the source and initialized work frame while accumulating an exact bit string.

theorem Complexity.SAT.ThreeSAT.Machine.reductionTMWith_valid_emit_reachesIn_internal (validEmitter : TM workTapeCount) (z ys : List Bool) (emitterTime : ℕ) (hvalid : validEncoding z = true) (hEmitter : validEmitter.HoareTime (validEmitterPre z) (TM.EmitPred { head := 1, cells := (Tape.init (List.map Γ.ofBool z)).cells } (frontEndWork z) ys) emitterTime) : ∃ (c' : Cfg workTapeCount (reductionTMWith validEmitter).Q), ∃ t ≤ 6 * z.length + emitterTime + 25, (reductionTMWith validEmitter).reachesIn t ((reductionTMWith validEmitter).initCfg z) c' ∧ (reductionTMWith validEmitter).halted c' ∧ c'.output.HasOutput ys

Execution-level corollary for an exact-output valid emitter.