AddressMachineLoopLemmas.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

The complete addressed outer-reduction machine

The fixed finite machine reads an encoded nonempty E3LIN occurrence list and writes the exact encoded addressed Unique Games instance. Its execution covers all headers, all occurrence tuples, every fixed noise/coefficient outcome, every permutation image, reversal, and complete tape cleanup.

def OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.bits line 18
def OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.stateTapes line 23
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.stateTapes_frame line 29
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.stateTapes_savedIndex line 39
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.stateTapes_private line 44
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.stateTapes_header line 52
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.stateTapes_ready line 63
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.stateTapes_clean line 90
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.stateTapes_base line 106
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.stateTapes_capacity line 115
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.appended_stateTapes line 128
Source documentation
Appending actual tuple bytes is exactly the schedule's accumulator update.
```
theorem appended_stateTapes (F : SourceEncoding.Input)
    (digits : Fin k → Fin F.equations.length) (output payload : List Bool) :
    MachineAddressEdge.appended (AddressMachineSpace.addressEdgeSlots k s d T.vectors.length)
      (stateTapes k T F digits output) payload =
      stateTapes k T F digits (payload.reverse ++ output) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.appended, OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressEdgeSlots, OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.stateTapes
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.bodyTrace line 142
Source documentation
The local-body premise of the odometer theorem is derived from the actual placed tuple-body implementation and its actual uniform budget theorem.
```
theorem bodyTrace (F : SourceEncoding.Input) :
    AddressOdometerSchedule.BodyTrace (AddressMachineProgram.program k T) (AddressMachineProgram.bodyStart k T)
      (AddressMachineProgram.next k T 0) (AddressMachineSpace.initialState k).1 (AddressMachineInitial.initialized k T F)
      (bits k T F) ((AddressTupleBudget.timePolynomial k T).eval (SourceEncoding.inputBits F).length) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.BodyTrace, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.program, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.bodyStart, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.next, OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.initialState, OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized, OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.bits, OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputBits
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.setDigits_initialized_zero line 165
Source documentation
The all-zero assignment is already physically present after initialization.
```
theorem setDigits_initialized_zero (F : SourceEncoding.Input) :
    AddressOdometerSchedule.setDigits F.equations.length (fun _ : Fin k => 0)
      (AddressMachineInitial.initialized k T F) = AddressMachineInitial.initialized k T F := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setDigits, OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized
def OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.finalTapes line 185
def OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.traversal line 190
Source documentation
Actual complete tuple traversal, before the final output reversal.
```
def traversal (F : SourceEncoding.Input) :
    StateTransition.EvalsToInTime (TM2.step (AddressMachineProgram.program k T))
      ⟨some (AddressMachineProgram.bodyStart k T), AddressMachineSpace.initialState k, AddressMachineInitial.initialized k T F⟩
      (some ⟨some (AddressMachineProgram.finishStart k T), AddressMachineSpace.initialState k, finalTapes k T F⟩)
      (((AddressTupleBudget.timePolynomial k T).eval (SourceEncoding.inputBits F).length + 2*k) *
        F.equations.length^k) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.program, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.bodyStart, OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.initialState, OAI.UniqueGamesTheorem.Reduction.AddressMachineInitial.initialized, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.finishStart, OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.finalTapes, OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputBits
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.allBits_eq line 227
Source documentation
Exact output order, including repeated constraints and the original header.
```
theorem allBits_eq (F : SourceEncoding.Input) :
    AddressOdometerSchedule.allBits (bits k T F) =
      (FixedOutcomes.occurrenceTuples F.equations.length k).flatMap
        (AddressOutcomeSpecs.tupleBits (AddressTupleBody.source F) k T) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.allBits, OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.bits, OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.occurrenceTuples, OAI.UniqueGamesTheorem.Reduction.AddressOutcomeSpecs.tupleBits
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.final_reversed line 233
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.headerBits_eq line 247
Source documentation
The actual header machine emits exactly the target instance's three headers.
```
theorem headerBits_eq (F : SourceEncoding.Input) :
    MachineAddressHeaders.Arithmetic.headerBits k s d T.vectors.length
      F.variables F.equations.length =
      encodeWords [(AddressGame.tableOutput (AddressTupleBody.source F) k T).vertices, 2^s,
        (AddressGame.tableOutput (AddressTupleBody.source F) k T).constraints.length] := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.headerBits, OAI.UniqueGamesTheorem.Reduction.AddressGame.tableOutput
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.final_accumulator line 270
Source documentation
The final reversed tape is exactly the complete encoded actual instance.
```
theorem final_accumulator (F : SourceEncoding.Input) :
    finalTapes k T F (AddressMachineProgram.accumulator k T) =
      (gameBits (AddressGame.tableOutput (AddressTupleBody.source F) k T)).reverse := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.finalTapes, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.accumulator, OAI.UniqueGamesTheorem.Reduction.AddressGame.tableOutput
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.final_other line 276
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.final_outputEmpty line 283
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.final_current line 293
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.final_remaining line 297
def OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.timePolynomial line 303
Source documentation
The exponent and coefficients depend only on fixed reduction parameters.
```
def timePolynomial : Polynomial Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.timePolynomial_eval line 306
def OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.inPolynomialTime line 311
def OAI.UniqueGamesTheorem.Reduction.MachineAddressGame.output line 345
def OAI.UniqueGamesTheorem.Reduction.MachineAddressGame.prefixPolynomial line 349
def OAI.UniqueGamesTheorem.Reduction.MachineAddressGame.timePolynomial line 352
def OAI.UniqueGamesTheorem.Reduction.MachineAddressGame.prefixInTime line 357
Source documentation
The complete actual prefix, with both initialization and every tuple body supplied by their constructed finite programs.
```
def prefixInTime (input : SourceEncoding.Input) :
    StateTransition.EvalsToInTime (AddressMachineProgram.machine k T).step
      (initList (AddressMachineProgram.machine k T) (SourceEncoding.inputBits input))
      (some ⟨some (AddressMachineProgram.finishStart k T), AddressMachineSpace.initialState k,
        AddressMachineLoop.finalTapes k T input⟩)
      ((prefixPolynomial k T).eval (SourceEncoding.inputBits input).length) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.machine, OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputBits, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.finishStart, OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.initialState, OAI.UniqueGamesTheorem.Reduction.AddressMachineLoop.finalTapes, OAI.UniqueGamesTheorem.Reduction.MachineAddressGame.prefixPolynomial
def OAI.UniqueGamesTheorem.Reduction.MachineAddressGame.fullRunInTime line 371
Source documentation
Literal initList to literal haltList, including all private tape and finite-state cleanup. This theorem has no runtime premise.
```
def fullRunInTime (input : SourceEncoding.Input) :
    TM2OutputsInTime (AddressMachineProgram.machine k T) (SourceEncoding.inputBits input)
      (some (gameBits (output k T input)))
      ((timePolynomial k T).eval (SourceEncoding.inputBits input).length) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.AddressMachineProgram.machine, OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputBits, OAI.UniqueGamesTheorem.Reduction.MachineAddressGame.output, OAI.UniqueGamesTheorem.Reduction.MachineAddressGame.timePolynomial
def OAI.UniqueGamesTheorem.Reduction.MachineAddressGame.computableInPolyTime line 381
theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressGame.workAlphabetFinite line 404
Source documentation
Every working tape of the actual certificate uses the finite Bool alphabet.
```
theorem workAlphabetFinite (tape : (computableInPolyTime k T).tm.K) :
    Finite ((computableInPolyTime k T).tm.Γ tape) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressGame.computableInPolyTime