AddressMachineLoop.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

The actual address machine's final bridge, cleanup, reversal, and halt. The polynomial cleanup bound follows from space used by the supplied actual prefix execution. The complete reduction supplies that prefix in MachineAddressGame.

def OAI.MaxCutGames.Reduction.AddressMachineLoop.bits line 17
def OAI.MaxCutGames.Reduction.AddressMachineLoop.stateTapes line 22
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.stateTapes_frame line 28
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.stateTapes_savedIndex line 38
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.stateTapes_private line 43
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.stateTapes_header line 51
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.stateTapes_ready line 62
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.stateTapes_clean line 89
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.stateTapes_base line 105
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.stateTapes_capacity line 114
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.appended_stateTapes line 127
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.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.MachineAddressEdge.appended, OAI.MaxCutGames.Reduction.AddressMachineSpace.addressEdgeSlots, OAI.MaxCutGames.Reduction.AddressMachineLoop.stateTapes
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.bodyTrace line 141
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.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.AddressOdometerSchedule.BodyTrace, OAI.MaxCutGames.Reduction.AddressMachineProgram.program, OAI.MaxCutGames.Reduction.AddressMachineProgram.bodyStart, OAI.MaxCutGames.Reduction.AddressMachineProgram.next, OAI.MaxCutGames.Reduction.AddressMachineSpace.initialState, OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized, OAI.MaxCutGames.Reduction.AddressMachineLoop.bits, OAI.MaxCutGames.Reduction.SourceEncoding.inputBits
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.setDigits_initialized_zero line 164
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.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setDigits, OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized
def OAI.MaxCutGames.Reduction.AddressMachineLoop.finalTapes line 184
def OAI.MaxCutGames.Reduction.AddressMachineLoop.traversal line 189
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.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.AddressMachineProgram.program, OAI.MaxCutGames.Reduction.AddressMachineProgram.bodyStart, OAI.MaxCutGames.Reduction.AddressMachineSpace.initialState, OAI.MaxCutGames.Reduction.AddressMachineInitial.initialized, OAI.MaxCutGames.Reduction.AddressMachineProgram.finishStart, OAI.MaxCutGames.Reduction.AddressMachineLoop.finalTapes, OAI.MaxCutGames.Reduction.SourceEncoding.inputBits
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.allBits_eq line 226
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.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.AddressOdometerSchedule.allBits, OAI.MaxCutGames.Reduction.AddressMachineLoop.bits, OAI.MaxCutGames.Reduction.FixedOutcomes.occurrenceTuples, OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.tupleBits
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.final_reversed line 232

theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.headerBits_eq line 246

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.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.MachineAddressHeaders.Arithmetic.headerBits, OAI.MaxCutGames.Reduction.AddressGame.tableOutput

theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.final_accumulator line 269
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.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.AddressMachineLoop.finalTapes, OAI.MaxCutGames.Reduction.AddressMachineProgram.accumulator, OAI.MaxCutGames.Reduction.AddressGame.tableOutput
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.final_other line 275
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.final_outputEmpty line 282
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.final_current line 292
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.final_remaining line 296
def OAI.MaxCutGames.Reduction.AddressMachineLoop.timePolynomial line 302
Source documentation
The exponent and coefficients depend only on fixed reduction parameters.
```
def timePolynomial : Polynomial Nat :=
…
```
theorem OAI.MaxCutGames.Reduction.AddressMachineLoop.timePolynomial_eval line 305
def OAI.MaxCutGames.Reduction.AddressMachineLoop.inPolynomialTime line 310
def OAI.MaxCutGames.Reduction.AddressMachineFinish.timePolynomial line 338

def OAI.MaxCutGames.Reduction.AddressMachineFinish.completePrefix line 345

Source documentation

Finish the concrete program, including its one-step finalizer entry bridge. The runtime bound uses all actual intermediate tapes, with no output-size or private-space assumption.

def completePrefix (input : List Bool) (prefixTime : Polynomial Nat)
    (base : AddressMachineProgram.Tape k T → List Bool)
    (execution : StateTransition.EvalsToInTime (AddressMachineProgram.machine k T).step
      (initList (AddressMachineProgram.machine k T) input)
      (some ⟨some (AddressMachineProgram.finishStart k T),
        AddressMachineSpace.initialState k, base⟩) (prefixTime.eval input.length))
    (outputEmpty : base (AddressMachineProgram.output k T) = []) :
    TM2OutputsInTime (AddressMachineProgram.machine k T) input
      (some (base (AddressMachineProgram.accumulator k T)).reverse)
      ((timePolynomial k T prefixTime).eval input.length) := by
…

Mentions: OAI.MaxCutGames.Reduction.AddressMachineProgram.Tape, OAI.MaxCutGames.Reduction.AddressMachineProgram.machine, OAI.MaxCutGames.Reduction.AddressMachineProgram.finishStart, OAI.MaxCutGames.Reduction.AddressMachineSpace.initialState, OAI.MaxCutGames.Reduction.AddressMachineProgram.output, OAI.MaxCutGames.Reduction.AddressMachineProgram.accumulator, OAI.MaxCutGames.Reduction.AddressMachineFinish.timePolynomial

def OAI.MaxCutGames.Reduction.MachineAddressGame.output line 411
def OAI.MaxCutGames.Reduction.MachineAddressGame.prefixPolynomial line 415
def OAI.MaxCutGames.Reduction.MachineAddressGame.timePolynomial line 418
def OAI.MaxCutGames.Reduction.MachineAddressGame.prefixInTime line 423
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.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.AddressMachineProgram.machine, OAI.MaxCutGames.Reduction.SourceEncoding.inputBits, OAI.MaxCutGames.Reduction.AddressMachineProgram.finishStart, OAI.MaxCutGames.Reduction.AddressMachineSpace.initialState, OAI.MaxCutGames.Reduction.AddressMachineLoop.finalTapes, OAI.MaxCutGames.Reduction.MachineAddressGame.prefixPolynomial
def OAI.MaxCutGames.Reduction.MachineAddressGame.fullRunInTime line 437
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.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.AddressMachineProgram.machine, OAI.MaxCutGames.Reduction.SourceEncoding.inputBits, OAI.MaxCutGames.Reduction.MachineAddressGame.output, OAI.MaxCutGames.Reduction.MachineAddressGame.timePolynomial
def OAI.MaxCutGames.Reduction.MachineAddressGame.computableInPolyTime line 447
theorem OAI.MaxCutGames.Reduction.MachineAddressGame.workAlphabetFinite line 466
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.MaxCutGames.Reduction.MachineAddressGame.computableInPolyTime
abbrev OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.SingleAddress.vertexCount line 488
abbrev OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.SingleAddress.queryAddress line 489
abbrev OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.SingleAddress.addressEdge line 490
abbrev OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.SingleAddress.outputInstance line 491
abbrev OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.SingleAddress.tableOutput line 492
theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.old_addressEdge_eq_double line 496
theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.old_outputInstance_eq_double line 506
Source documentation
Exact equality of the ordered, fully serialized constraint data.
```
theorem old_outputInstance_eq_double (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (en : NoiseEnumeration g) :
    AddressGame.outputInstance S k g en = doubleInstance (SingleAddress.outputInstance S k g en) := by
…
```
Mentions: OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.SingleAddress.outputInstance
theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.old_tableOutput_eq_double line 515
def OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.output line 520
theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.old_output_eq_double line 524
def OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.doubledComputableInPolyTime line 532
Source documentation
Reinterpret the existing producer using the proved exact codec equality.
```
def doubledComputableInPolyTime (k : Nat) {s d : Nat}
    (T : MaxCutGames.Integration.NoiseTables.Table s d) :
    TM2ComputableInPolyTime SourceEncoding.inputBits
      (fun I => gameBits (doubleInstance I)) (output k T) := by
…
```
Mentions: OAI.MaxCutGames.Integration.NoiseTables.Table, OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.output
def OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.computableInPolyTime line 547
theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitBridge.workAlphabetFinite line 559