MachineLookupDiscard.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Execution of the destructive field-discard loop in an arbitrary ambient TM2 program. The scanner consumes a unary payload and its delimiter, preserves the ambient state and other tapes, and clears its head register on return. At EOF it returns immediately, leaving the tapes unchanged.

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.discard_update_twice line 20
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.discardStep_delimiter line 29
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.discardStep_true line 42
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.discard_empty_step line 56
Source documentation
EOF returns to the guard in one transition, without changing any tape.
```
theorem discard_empty_step (source : K) (loopLabel returnLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.Alphabet
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.discardTrace_update line 73
Source documentation
A normalized tape form for the field-discard trace.
```
theorem discardTrace_update (source : K) (loopLabel returnLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.Alphabet
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.discardTrace line 98
Source documentation
Discard exactly the first encoded field, in one transition per payload bit plus one transition for its delimiter. No condition is imposed on other tapes.
```
theorem discardTrace (source : K) (loopLabel returnLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.Alphabet
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.discardInTime line 118
Source documentation
The same exact trace packaged for composition with ambient machine phases.
```
def discardInTime (source : K) (loopLabel returnLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.Alphabet