Shared branch frame for the Tseitin reduction machine

After validation, both branches of reductionTMWith receive the same tape frame. This module records that frame once: the scanned input, initialized work registers, validator verdict, tape well-formedness, and the standard ifTM transition into the selected branch.

Main results

• validatedInputTape
• validationBranchPre
• validEmitterPre
• validationFramedPost_allTapesWF_internal
• validationFramedPost_to_branchPre_internal

def Complexity.SAT.ThreeSAT.Machine.validatedInputTape (z : List Bool) : Tape

Input tape after the validation scan reaches the first trailing blank.

Equations

• Complexity.SAT.ThreeSAT.Machine.validatedInputTape z = { head := z.length + 1, cells := (Complexity.Tape.init (List.map Complexity.Γ.ofBool z)).cells }

def Complexity.SAT.ThreeSAT.Machine.validationBranchPre (z : List Bool) : TapePred workTapeCount

The common frame received by either branch after ifTM has rewound the validator output head to cell one.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.validEmitterPre (z : List Bool) : TapePred workTapeCount

The exact tape frame handed to a valid-input emitter after the verdict is cleared and the source is rewound to cell one.

Equations

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

theorem Complexity.SAT.ThreeSAT.Machine.validatedInputTape_parked (z : List Bool) : TM.Parked (validatedInputTape z)

The scanned source input is parked.

theorem Complexity.SAT.ThreeSAT.Machine.frontEndWork_cell_zero (z : List Bool) (i : Fin workTapeCount) : (frontEndWork z i).cells 0 = Γ.start

Every initialized work register retains the left-end marker at cell zero.

theorem Complexity.SAT.ThreeSAT.Machine.validationFramedPost_allTapesWF_internal (z : List Bool) {inp out : Tape} {work : Fin workTapeCount → Tape} (h : validationFramedPost z (frontEndWork z) inp work out) : TM.AllTapesWF inp work out

The framed front-end postcondition supplies the tape well-formedness premise required by ifTM.

theorem Complexity.SAT.ThreeSAT.Machine.validationFramedPost_to_branchPre_internal (z : List Bool) {inp out : Tape} {work : Fin workTapeCount → Tape} (h : validationFramedPost z (frontEndWork z) inp work out) : validationBranchPre z (TM.transitionInput inp) (fun (i : Fin workTapeCount) => TM.transitionTape (work i)) { head := 1, cells := out.cells }

The standard ifTM phase transition turns the framed validation result into the common branch frame.