MachineProductLoop.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

Whole tuple traversal of the concrete product program. The odometer theorem is instantiated by the proved actual row trace, not by an assumed row machine.

structure OAI.MaxCutGames.Explicit.MachineProductLoop.BaseReady line 22
def OAI.MaxCutGames.Explicit.MachineProductLoop.tupleTapes line 28
theorem OAI.MaxCutGames.Explicit.MachineProductLoop.tupleTapes_frame line 33
theorem OAI.MaxCutGames.Explicit.MachineProductLoop.tupleTapes_current line 45
theorem OAI.MaxCutGames.Explicit.MachineProductLoop.tupleTapes_accumulator line 50
theorem OAI.MaxCutGames.Explicit.MachineProductLoop.tupleTapes_ready line 55
def OAI.MaxCutGames.Explicit.MachineProductLoop.rowBits line 106
theorem OAI.MaxCutGames.Explicit.MachineProductLoop.input_length line 110
def OAI.MaxCutGames.Explicit.MachineProductLoop.bodyBound line 116
theorem OAI.MaxCutGames.Explicit.MachineProductLoop.bodyTrace line 121
Source documentation
The actual row execution supplies the local obligation of the generic odometer schedule. Its cost is uniformly polynomial in the original bits.
```
theorem bodyTrace (H : Target.Instance q) (base : Tape t → List Bool) (ready : BaseReady H base) :
    SourceOdometerSchedule.BodyTrace (program q t) (rowMain q t) (nextCheck q t 0)
      ((), ()) (Sum.inl (6 : Fin 10)) base (rowBits (t := t) H) (bodyBound H t) := by
…
```
Mentions: OAI.MaxCutGames.Explicit.MachineProductLoop.BaseReady, OAI.MaxCutGames.Explicit.MachineProductLoop.rowBits, OAI.MaxCutGames.Explicit.MachineProductLoop.bodyBound

theorem OAI.MaxCutGames.Explicit.MachineProductLoop.traversalInTime line 174

Source documentation

Complete positive-radix tuple traversal with actual row bodies discharged.

theorem traversalInTime (H : Target.Instance q) (base : Tape t → List Bool) (ready : BaseReady H base) :
    Nonempty (StateTransition.EvalsToInTime (TM2.step (program q t))
      (SourceOdometerSchedule.initialConfiguration (m := H.constraints.length) t (rowMain q t) ((), ()) base)
…

Mentions: OAI.MaxCutGames.Explicit.MachineProductLoop.BaseReady

theorem OAI.MaxCutGames.Explicit.MachineProductFinish.base_ready line 210
def OAI.MaxCutGames.Explicit.MachineProductFinish.afterRows line 220
theorem OAI.MaxCutGames.Explicit.MachineProductFinish.afterRows_output line 224
theorem OAI.MaxCutGames.Explicit.MachineProductFinish.allRows_eq line 231
theorem OAI.MaxCutGames.Explicit.MachineProductFinish.afterRows_accumulator line 237

def OAI.MaxCutGames.Explicit.MachineProductFinish.finishInTime line 250

Source documentation

The entry hop reaches the actual cleanup list, then all work is drained, the accumulator is reversed, and the final finite register is reset.

def finishInTime (base : Tape t → List Bool) (emptyOutput : base (output t) = []) :
    StateTransition.EvalsToInTime (TM2.step (program q t))
      ⟨some .finishStart, (((), ()), none), base⟩
      (some ⟨none, (((), ()), none),
        SourceRuntimeFinish.canonicalTapes (output t) (base (accumulator t)).reverse⟩)
      (1 + SourceRuntimeFinish.finishCost (clearKeys t) (accumulator t) base) := by
…

theorem OAI.MaxCutGames.Explicit.MachineProductFinish.finishCost_le_uniform line 272

Source documentation

A uniform bound on the real cleanup work, from bounds on actual stacks.

theorem finishCost_le_uniform (base : Tape t → List Bool) (bound : Nat)
    (bounded : ∀ k, (base k).length ≤ bound) :
    SourceRuntimeFinish.finishCost (clearKeys t) (accumulator t) base ≤
      ((clearKeys t).length + 1) * bound + (clearKeys t).length + 2 := by
…

theorem OAI.MaxCutGames.Explicit.MachineProductFinish.finish_afterRows line 283
def OAI.MaxCutGames.Explicit.MachineProductRuntime.loopPolynomial line 328
theorem OAI.MaxCutGames.Explicit.MachineProductRuntime.loop_budget line 332
def OAI.MaxCutGames.Explicit.MachineProductRuntime.prefixPolynomial line 341
def OAI.MaxCutGames.Explicit.MachineProductRuntime.prefixInTime line 345
Source documentation
Actual header initialization followed by every product row and odometer step.
```
def prefixInTime {q : Nat} (H : Instance q) (t : Nat) :
    StateTransition.EvalsToInTime (machine q t).step
      (initList (machine q t) (gameBits H))
      (some (MachineProductFinish.afterRows H t))
      ((prefixPolynomial q t).eval (gameBits H).length) := by
…
```
Mentions: OAI.MaxCutGames.Explicit.MachineProductFinish.afterRows, OAI.MaxCutGames.Explicit.MachineProductRuntime.prefixPolynomial
def OAI.MaxCutGames.Explicit.MachineProductRuntime.timePolynomial line 367
def OAI.MaxCutGames.Explicit.MachineProductRuntime.outputInTime line 373
Source documentation
The complete run produces the literal full-table target code, clears all private stacks, resets its finite state, and halts.
```
def outputInTime {q : Nat} (H : Instance q)
    (presentation : MachineOutputContract.SimpleBipartite H) (t : Nat) (ht : 0 < t) :
    TM2OutputsInTime (machine q t) (gameBits H)
      (some (gameBits (ProductPaddedOutput.output H presentation t ht)))
      ((timePolynomial q t).eval (gameBits H).length) := by
…
```
Mentions: OAI.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite, OAI.MaxCutGames.Explicit.ProductPaddedOutput.output, OAI.MaxCutGames.Explicit.MachineProductRuntime.timePolynomial
abbrev OAI.MaxCutGames.Explicit.MachineProductRuntime.Input line 404
Source documentation
The bipartition is proof-side data. Its codec is exactly the underlying instance code and the fixed program does not inspect it.
```
abbrev Input (q : Nat) := Σ H : Instance q, MachineOutputContract.SimpleBipartite H
```
Mentions: OAI.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite
def OAI.MaxCutGames.Explicit.MachineProductRuntime.construct line 406
def OAI.MaxCutGames.Explicit.MachineProductRuntime.computation line 409
theorem OAI.MaxCutGames.Explicit.MachineProductRuntime.finiteAlphabet line 424
def OAI.MaxCutGames.Explicit.MachineProductRuntime.certify line 430

def OAI.MaxCutGames.Explicit.MachineProductRuntime.compose line 441

Source documentation

Direct composition with an actual preceding simple-bipartite producer.

def compose (upstream : TM2ComputableInPolyTime encode gameBits f)
    (presentation : ∀ a, MachineOutputContract.SimpleBipartite (f a))
    (t : Nat) (ht : 0 < t) :
    TM2ComputableInPolyTime encode gameBits
      (fun a => ProductPaddedOutput.output (f a) (presentation a) t ht) :=
…

Mentions: OAI.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite, OAI.MaxCutGames.Explicit.ProductPaddedOutput.output

theorem OAI.MaxCutGames.Explicit.MachineProductRuntime.compose_finiteAlphabet line 448