MachineProductGatherBoundsLemmas.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Bounds on the actual work stacks left by the preserving gather. These bounds justify clearing the query/scan remnants after each product field; they are consequences of the exact tape formulas, not runtime assumptions.

theorem OAI.UniqueGamesTheorem.Explicit.MachineProductGather.affine_final_length line 16

theorem OAI.UniqueGamesTheorem.Explicit.MachineProductGather.finalTapes_length line 50

Source documentation

One field query adds at most one table's worth of bits to any tape. A width-fold gather therefore has a uniform linear-in-width space bound.

theorem finalTapes_length (values : List Nat) (coefficient width : Nat)
    (placement : Tape width → K) (distinct : Function.Injective placement)
    (indices offsets fields : Fin width → Nat)
    (selected : ∀ i, values[coefficient * indices i + offsets i]? = some (fields i))
    (base : K → List Bool) (k : K) :
    (finalTapes values coefficient width placement indices offsets fields base k).length ≤
      (base k).length + width * ((encodeWords values).length + 1) := by
…

Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductGather.Tape, OAI.UniqueGamesTheorem.Explicit.MachineProductGather.finalTapes

abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.Alphabet line 84
inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.Label line 86
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.statement line 93
Source documentation
Tape roles: 0 original table, 1 unary index, 2 working copy, 3 output, 4 copy/restore scratch. The embedded halt enters the explicit cleanup loop.
```
def statement (tape : Fin 5 → K) (labels : Label → Λ) (exit : Option Λ) :
    Label → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool)
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.Alphabet
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.program line 99
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.steps line 104
Source documentation
Exact copy, lookup, return, and residual-cleanup transition count.
```
def steps (values : List Nat) (index : Nat) : Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.remaining_length_le line 108
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.steps_le line 115
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.timePolynomial line 123
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.steps_le_timePolynomial line 125
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.traceAt line 134
Source documentation
Actual ambient-program execution. code fixes the concrete instructions at each placed label; it does not assume any execution or semantic behavior. The frame records an empty working copy at both endpoints.
```
theorem traceAt (tape : Fin 5 → K) (distinct : Function.Injective tape)
    (labels : Label → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.Alphabet
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.inTimeAt line 192
Source documentation
A timed certificate for the same actual trace, bounded by a single linear polynomial in the original table encoding length.
```
def inTimeAt (tape : Fin 5 → K) (distinct : Function.Injective tape)
    (labels : Label → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.Alphabet
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.initialTapes_eq line 215
Source documentation
The framing representation is the caller's exact tape state whenever its index and work tape contain the specified index and an empty list.
```
theorem initialTapes_eq (tape : Fin 5 → K) (base : K → List Bool)
    (index : Nat) (indexSuffix : List Bool)
    (counterWord : base (tape 1) = encodeWord index ++ indexSuffix)
    (workEmpty : base (tape 2) = []) :
    MachinePreservingLookup.initialTapes tape base index indexSuffix [] (base (tape 3)) =
      base := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.initialTapes
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.traceAt_fromTapes line 225
Source documentation
A convenience interface starting from the caller's exact configuration.
```
theorem traceAt_fromTapes (tape : Fin 5 → K) (distinct : Function.Injective tape)
    (labels : Label → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.Alphabet
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.machine line 248
Source documentation
The complete construction has five Boolean tapes, nine control labels, and one optional-bit register. No table data appears in its finite state.
```
def machine : FinTM2 where
…
```

def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.machineInTime line 261

Source documentation

The generic trace instantiates the concrete finite machine, with the same linear bound and completely cleaned working copy.

def machineInTime (base : Fin 5 → List Bool) (values : List Nat)
    (tableWord : base 0 = encodeWords values) (scratchEmpty : base 4 = [])
    (index value : Nat) (selected : values[index]? = some value)
    (indexSuffix output : List Bool) (register : Option Bool) :
    StateTransition.EvalsToInTime machine.step
      ⟨some (.run .copyFirst), ((), register),
        MachinePreservingLookup.initialTapes id base index indexSuffix [] output⟩
      (some ⟨none, ((), none),
        MachinePreservingLookup.initialTapes id base 0 indexSuffix []
          (encodeWord value ++ output)⟩)
      (timePolynomial.eval (encodeWords values).length) :=
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookup.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord