test(computability): prove pair-first transitions

[windsornguyen]

Explain what this changes, why it is needed, and anything reviewers should
verify. Link an issue when one exists.

What does this change?

Proves each primitive transition of the pair-first wrapper: duplicated-bit decoding, delimiter recognition, witness consumption, decoded-input restoration, and transfer into the embedded source program.

The lemmas expose one operational fact per parser state and provide the local proof steps used by the recursive execution certificates above this layer. This is stack layer 4 of 8.

How was it tested?

• lake build --wfail passes
• lake lint passes
• No sorry or new axioms, or this PR does not change Lean proofs

[chatgpt-codex-connector]

💡 Codex Review

https://github.com/windsornguyen/ComplexityTheory/blob/4e16e979d6079fb666dc876313fd4b84a1a3aa01/Computability/PairFirstComposition/Transitions.lean#L12-L14
Cite the borrowed TM2 semantics

This new transition module unfolds Turing.TM2.step, Turing.TM2.stepAux, and Turing.initList throughout its public proofs, but the module provenance only describes the parser. Because this repo requires every borrowed definition/result to be cited with authors, title, year/version, and a precise definition/theorem/section/page, add the Mathlib source details here before these transition theorems depend on them.

---

https://github.com/windsornguyen/ComplexityTheory/blob/4e16e979d6079fb666dc876313fd4b84a1a3aa01/Computability/PairFirstComposition/Transitions.lean#L24-L27
Document the inputAlphabet wrapper

This new public helper is just certificate.inputAlphabet.invFun specialized to the source input stack, but its docstring does not name that underlying operation or say what certificate-specific guarantee the wrapper adds. Since later transition proofs expose this as API rather than using the equivalence directly, please either keep it private or document the inputAlphabet.invFun lift and why the certificate wrapper is useful.

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".