Validate paired machine inputs

pairValidateTM is a total finite-state recognizer for the image of the library's self-delimiting pair codec. It rejects every malformed outer input and runs in exactly the generic scanner budget n + 2.

This complements pairSplitCoreTM: validate first when arbitrary input strings need rejecting semantics, then rewind and use the canonical splitter to stage the two decoded components.

theorem Complexity.mem_validPairEncoding_iff (bits : List Bool) : bits ∈ validPairEncoding ↔ (unpair? bits).isSome = true

Decoder-facing characterization of membership in validPairEncoding.

theorem Complexity.mem_validPairEncoding_iff_exists_pair (bits : List Bool) : bits ∈ validPairEncoding ↔ ∃ (x : List Bool) (y : List Bool), bits = pair x y

Extensional characterization: valid encodings are exactly canonical encodings of some pair of Boolean strings.

theorem Complexity.not_mem_validPairEncoding_iff (bits : List Bool) : bits ∉ validPairEncoding ↔ unpair? bits = none

Failure of the partial decoder is exactly nonmembership in the valid-pair language.

@[simp]

theorem Complexity.pair_mem_validPairEncoding (x y : List Bool) : pair x y ∈ validPairEncoding

Every canonical pair is a valid pair encoding.

theorem Complexity.TM.pairValidateAccept_fold_eq_true_iff (bits : List Bool) : pairValidateAccept (List.foldl pairValidateStep PairValidateState.next bits) = true ↔ (unpair? bits).isSome = true

The pair-validator fold accepts exactly when the canonical decoder succeeds.

theorem Complexity.TM.pairValidateTM_decidesInTime : pairValidateTM.DecidesInTime validPairEncoding fun (n : ℕ) => n + 2

The finite-state pair validator decides validPairEncoding in linear time.

theorem Complexity.TM.pairValidateTM_lift_decidesInTime (workTapes : ℕ) : (pairValidateTM.liftTM workTapes).DecidesInTime validPairEncoding fun (n : ℕ) => n + 2

Adding arbitrary unused work tapes preserves the validator's language and exact linear time bound. This is the form used by larger machine pipelines.

theorem Complexity.TM.pairValidateTM_lift_hoareTime (workTapes : ℕ) (bits : List Bool) : (pairValidateTM.liftTM workTapes).HoareTime (fun (inp : Tape) (work : Fin (0 + workTapes) → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool bits) ∧ (work = fun (x : Fin (0 + workTapes)) => Tape.init []) ∧ out = Tape.init []) (fun (inp : Tape) (work : Fin (0 + workTapes) → Tape) (out : Tape) => AllTapesWF inp work out ∧ inp.cells = (Tape.init (List.map Γ.ofBool bits)).cells ∧ inp.head ≤ bits.length + 2 ∧ (∀ (i : Fin (0 + workTapes)), work i = (Tape.init []).move Dir3.right) ∧ out.head ≤ bits.length + 2 ∧ (bits ∈ validPairEncoding → out.cells 1 = Γ.one) ∧ (bits ∉ validPairEncoding → out.cells 1 = Γ.zero)) (bits.length + 2)

Frame-rich initialized specification for the lifted validator. Besides the verdict, it exposes the read-only input cells, head bounds, well-formedness of all tapes, and the fact that every added work tape is parked and blank. These are the seams needed by ifTM and a subsequent input rewind.