MachineRegularTableTrace.lean`

72 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds for the actual regularization subcalls. These lemmas bound the established step counts; they do not assume any machine execution.

theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.joinTraceRegularTableTrace_inline_MachineRegularTableTrace line 11
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.normalizeEmptyAppend_inline_MachineRegularTableTrace line 15
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerStartTrace line 19
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerOldTrace line 31
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.beforeCleanupTrace line 47
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.cleanupFinalTrace line 63
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.fullTrace line 71
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_output line 79
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.input_stacks_eq line 92
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.initial_cfg_eq line 114
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.trace line 125
Source documentation
Complete execution from the actual serialized input. All header reads, metadata, geometric rotors, rows, counters and cleanup are run by this one finite machine. No body trace or target-table computation is supplied as a premise.
```
theorem trace (H : BaseTable) (t : GraphTables.Table) :
    (advance (TM2.step (program H)))^[totalTime H t]
      (some (Turing.initList (machine H) (GraphTables.tableBits t))) =
      some ⟨none, readyState H,
        Function.update (Turing.initList (machine H) (GraphTables.tableBits t)).stk
          (coreTape 8) (PortTables.tableBits (PreprocessingRegularTables.regularize H t))⟩ := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.totalTime, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.machine, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.readyState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.coreTape
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularExecutionBounds.coreTimeBound_mono line 158
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularExecutionBounds.corePolynomial line 165
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularExecutionBounds.corePolynomial_eval line 173
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularExecutionBounds.internal_steps_le line 182
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularExecutionBounds.familyPolynomial line 201

theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularExecutionBounds.family_budget_le line 206

Source documentation

The completed reusable family call includes the three actual drains.

theorem family_budget_le (t : GraphTables.Table) (v : Fin t.vertices) :
    MachinePaddedExpanderFamilyBounds.timePolynomial.eval (cloudSize t v + 1) +
      2 * ExpanderFamily.growth * (cloudSize t v + 1) + 7 ≤
        familyPolynomial.eval (inputLength t) := by
…

def OAI.MaxCutGames.Foundations.Complexity.MachineRegularExecutionBounds.rowPolynomial line 219
Source documentation
A generous serialized-row bound evaluated at the actual linear vertex cap.
```
noncomputable def rowPolynomial (q : Nat) : Polynomial Nat :=
…
```
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularExecutionBounds.rowPolynomial_eval line 223
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularExecutionBounds.actual_row_bound_le line 229
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularExecutionBounds.blockCorePolynomial line 237
Source documentation
The inner port loop can grow the old prefix by at most q complete rows.
```
noncomputable def blockCorePolynomial (q : Nat) : Polynomial Nat :=
…
```
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularExecutionBounds.coreTimeBound_add_output line 240

theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularExecutionBounds.block_core_bound_le line 248

Source documentation

Uniform cap for the actual affine bound used by the port-loop wrapper, including all rows it may already have appended during this vertex.

theorem block_core_bound_le (q : Nat) (t : GraphTables.Table)
    (tables : ∀ v, ExpanderTables.Table (cloudSize t v + padding t v) q)
    (v : Fin t.vertices) (x : PaddedCloud t (padding t) v)
    (initialOutput : Nat) (houtput : initialOutput ≤ regularPolynomial.eval (inputLength t)) :
    coreTimeBound q (GraphTables.tableBits t).length
      (encodeWords (ExpanderTableWords.rotationWords (tables v))).length
      (vertexOrder t (padding t) x.val).val v.val (paddedCloudRank t (padding t) v x).val
      (cloudSize t v) (PreprocessingPaddingOffsets.offset (padding t) v.val) t.darts
      (initialOutput + q *
        (vertexCount t (padding t) + vertexCount t (padding t) * (q + 1) + 8192)) ≤
      (blockCorePolynomial q).eval (inputLength t) := by
…

Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineRegularExecutionBounds.blockCorePolynomial

def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.wide line 286
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.rowPolynomial line 287
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.outputPolynomial line 289
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.corePolynomial line 291
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.blockPolynomial line 295
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.cleanupPolynomial line 298
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.timePolynomial line 299
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.bodySize line 303
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.blockPolynomial_eval line 306
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.originalTimeBound_le line 321
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.wide_le line 332
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.vertexSteps_le line 342
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.clearSteps_frame line 368
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.cleanupSteps_le line 375
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.totalSteps_le line 406
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.originalInTime line 424
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.bodySize line 449
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.wide line 452
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.rowPolynomial line 454
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.outputPolynomial line 457
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.corePolynomial line 460
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial line 465
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial_eval line 469
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.dummyTimeBound_le line 485
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.wide_le line 496
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerPrefix_length_le line 508
Source documentation
Any finite prefix inside this owner is a part of the actual output table, including when the supplied prefix length is larger than the number of blocks.
```
theorem ownerPrefix_length_le (H : BaseTable) (t : GraphTables.Table)
    (v : Fin t.vertices) (n : Nat) :
    (blocksPrefix (PreprocessingRegularWords.dummyVertexBits t (padding t)
      (familyCloudTable H t) v) n).length ≤ regularPolynomial.eval (inputLength t) := by
…
```
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.growingOutput_length_le line 516
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.dummySteps_le line 529
Source documentation
One actual dummy block has a uniform polynomial cost at every prefix of the owner loop. The only inputs are the real table, indices, and old output.
```
theorem dummySteps_le (H : BaseTable) (t : GraphTables.Table) (v : Fin t.vertices)
    (j : Fin (padding t v)) (n : Nat) (output : List Bool) :
    MachineRegularVertexBlock.dummySteps t (padding t) (familyCloudTable H t) v j
      (output ++ blocksPrefix (PreprocessingRegularWords.dummyVertexBits t (padding t)
        (familyCloudTable H t) v) n).length ≤
      (blockPolynomial internalDegree).eval (bodySize t output) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummySteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.bodySize
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.prePolynomial line 560
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.loopPolynomial line 563
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupPolynomial line 566
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.timePolynomial line 569
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.preSteps_le line 573
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.loopSteps_le line 592
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.allLoopSteps_le line 609
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupSteps_working line 622
Source documentation
Exact cost of the six physical drain loops and the prefix addition, expressed through the actual entry stack lengths.
```
theorem cleanupSteps_working (data : MachineRegularOwnerBody.Data)
    (fuel saved : List Bool) (d : Nat) :
    MachineRegularOwnerCleanup.steps (MachineRegularOwnerBody.working data fuel saved) d =
      2*(d+1) + data.localRank.length + data.count.length + data.rotor.length +
        data.padding.length + data.level.length + fuel.length + 6 := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.Data, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.steps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.working
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupCost_le line 632
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerTime_le line 671
Source documentation
The whole owner budget follows from the real recurrence and its separately proved stage bounds. The zero-padding branch performs no family or vertex work.
```
theorem ownerTime_le (H : BaseTable) (t : GraphTables.Table) (v : Fin t.vertices)
    (output : List Bool) :
    MachineRegularOwnerBody.ownerTime H t v output ≤ timePolynomial.eval (bodySize t output) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.ownerTime, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.bodySize
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.totalSteps_le line 688
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerInTime line 693
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldLoopPolynomial line 715
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerLoopPolynomial line 720
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.timePolynomial line 725
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed_prefix_le line 731
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed_le line 753
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed_prefix_le line 761
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed_le line 785
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.totalTime_le line 794
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.machineInTime line 810