OAI/Computability/MaxCut/Machines/SelectorMachine.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Reusable inherited-row execution with actual cleanup

Five concrete drain loops remove the query delimiter, unread scan suffix, raw reverse field, computed reverse field, and copied relation. With initially empty work tapes, the only final tape change is the appended output row. The index on tape zero and input table on tape one are both preserved.

  1. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectionSteps_le line 12
  2. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectorMachine line 33
  3. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectionInTime line 44
  4. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes line 65

    Source documentation

    The fixed core rotor roles use the agreed reusable 27-tape frame.

    def coreRotorTapes : Fin 8 → CoreTape := ![3, 7, 10, 11, 12, 9, 13, 14]

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.CoreTape

  5. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes line 68

    Source documentation

    Tail, selected destination, return port, scratch and emitted row fields.

    def coreFinishTapes : Fin 8 → CoreTape := ![1, 15, 14, 9, 24, 25, 26, 8]

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.CoreTape

  6. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectTape line 70
  7. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView line 88
  8. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView_left line 97
  9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView_right line 105
  10. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTape line 110
  11. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorStateEquiv line 112
  12. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectStateEquiv line 121
  13. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreAfterCleanup line 128
  14. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreInstruction line 133

    Source documentation

    The whole internal-row program has only fixed q and p in its code.

    def coreInstruction (q : Nat) (positive : 0 < q) (p : Fin q)
    (labels : CoreLabel q → Λ) (exit : Option Λ) :
    CoreLabel q → TM2.Stmt (fun _ : CoreTape => Bool) Λ (CoreState σ q)
  | .rotor stage => MachineStateEquiv.statement (coreRotorStateEquiv σ q)
      (rotorInstruction q positive p coreRotorTapes
        (fun l => labels (.rotor l)) (some (labels (.select (.inr (.compare .scan))))) stage)
  | .select stage => MachineCloudPadding.Placement.statement coreSelectTape
      (fun l => labels (.select l)) (some (labels (.finish .seedReturn)))
      (MachineStateEquiv.statement (coreSelectStateEquiv σ q) (selectProgram stage))
  | .finish stage => finishInstruction q coreFinishTapes
      (fun l => labels (.finish l)) (some (labels (.cleanup 0))) stage
  | .cleanup i => MachineDrain.drain (coreCleanupTape i) (labels (.cleanup i))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.CoreLabel, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.CoreTape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.CoreState, OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.statement, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorStateEquiv, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.rotorInstruction, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPadding.Placement.statement, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectTape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectStateEquiv, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.finishInstruction, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDrain.drain, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTape

  15. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreInitialState line 147
  16. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreMachine line 151
  17. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreMemory line 162
  18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreMemory_update_output line 168
  19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes_injective line 176
  20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes_injective line 180
  21. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreCleaned line 184
  22. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupSteps line 189
  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTrace line 194
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreCleaned_memory line 271
  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupSteps_memory line 279
  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorFinalFrame line 291
  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTrace line 307
  28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectFrame line 353
  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectionTrace line 362
  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTrace line 397
  31. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreInputTapes line 429
  32. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreSteps line 439
  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreTrace line 456

    Source documentation

    One full actual internal row of the serialized regularization, including the physical rotor lookup, both destination cases, full equality predicate, row append and complete reusable cleanup frame.

    theorem coreTrace (q : Nat) (positive : 0 < q) (p : Fin q)
    (labels : CoreLabel q → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : CoreTape => Bool) Λ (CoreState σ q))
    (code : ∀ l, program (labels l) = coreInstruction q positive p labels exit l)
    (t : GraphTables.Table) (padding : Fin t.vertices → Nat)
    (tables : ∀ v, ExpanderTables.Table (PreprocessingCloudIndex.cloudSize t v + padding v) q)
    (v : Fin t.vertices) (x : PreprocessingCloudIndex.PaddedCloud t padding v)
    (output : List Bool) (ambient : σ) :
    (advance (TM2.step program))^[coreSteps t padding tables v x p output.length]
      (some ⟨some (labels (coreEntry q)), coreInitialState q positive ambient,
        coreInputTapes t padding tables v x output⟩) =
      some ⟨exit, coreInitialState q positive ambient,
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.CoreLabel, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.CoreTape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.CoreState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreInstruction, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreSteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreEntry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreInitialState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreInputTapes

  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectedIndex_le line 505

    Source documentation

    A selected original dart is below the original dart count; a dummy target is the old-dart count plus its physical prefix and local remainder.

    theorem selectedIndex_le (t : GraphTables.Table) (padding : Fin t.vertices → Nat)
    (v : Fin t.vertices) (i : Fin (PreprocessingCloudIndex.cloudSize t v + padding v)) :
    PreprocessingInternalRows.selectedIndex t padding v i ≤
      t.darts + PreprocessingPaddingOffsets.offset padding v.val + i.val := by
…
  35. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.encodedDrop_length_le line 516
  36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.rotorSize_le_encodedLength line 524

    Source documentation

    Every rotor entry occupies at least its delimiter on the physical tape.

    theorem rotorSize_le_encodedLength {n q : Nat} (positive : 0 < q)
    (table : ExpanderTables.Table n q) :
    n ≤ (encodeWords (ExpanderTableWords.rotationWords table)).length := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWords

  37. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreTimeBound line 534

    Source documentation

    For fixed cloud degree q this is affine in the lengths and unary values on the actual input tapes. All relation/cleanup constants are included.

    def coreTimeBound (q graphLength rotorLength x v i k o m outputLength : Nat) : Nat :=
…
  38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreSteps_le line 538
  39. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreMachineInTime line 604

    Source documentation

    The concrete finite machine executes the actual internal row in the proved affine budget and returns the reusable clean frame.

    def coreMachineInTime (q : Nat) (positive : 0 < q) (t : GraphTables.Table)
    (padding : Fin t.vertices → Nat)
    (tables : ∀ v, ExpanderTables.Table (PreprocessingCloudIndex.cloudSize t v + padding v) q)
    (v : Fin t.vertices) (x : PreprocessingCloudIndex.PaddedCloud t padding v)
    (p : Fin q) (output : List Bool) :
    StateTransition.EvalsToInTime (coreMachine q positive p).step
      ⟨some (coreEntry q), coreInitialState q positive (), coreInputTapes t padding tables v x output⟩
      (some ⟨none, coreInitialState q positive (), coreInputTapes t padding tables v x
        (output ++ encodeWords (GraphTables.rowWords (PreprocessingInternalRows.row t padding tables v x p)))⟩)
      (coreTimeBound q (GraphTables.tableBits t).length
        (encodeWords (ExpanderTableWords.rotationWords (tables v))).length
        (PreprocessingRegularTables.vertexOrder t padding x.val).val v.val
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreMachine, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreEntry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreInitialState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreInputTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreTimeBound

  40. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.Tape line 639
  41. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.Alphabet line 640
  42. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.State line 641
  43. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.Label line 643
  44. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.instruction line 648
  45. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupTapes line 658
  46. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps line 662
  47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.join_trace_inline_MachineRegularOriginalClean line 666
  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupTraceAt line 670
  49. structure OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.Input line 704
  50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.cleanup_frame line 709
  51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.suffix_length_le line 723
  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps_eq line 733
  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps_le line 777
  54. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.steps line 791
  55. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.timeBound line 795
  56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.steps_le line 798
  57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.traceAt line 806
  58. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.machine line 825
  59. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.machineInTime line 837

    Source documentation

    Exact inherited-row emission with all working tapes restored to empty.

    def machineInTime (H : BaseTable) (t : Table) (e : Fin t.darts)
    (base : Tape → List Bool) (input : Input t e base) (register : Option Bool) :
    StateTransition.EvalsToInTime (machine internalDegree).step
      ⟨some (.row (.lookup .seed)), (((), MachineRegularOriginalRow.zeroBuffer), register), base⟩
      (some ⟨none, (((), MachineRegularOriginalRow.zeroBuffer), none),
        Function.update base (9 : Tape)
          (base (9 : Tape) ++ encodeWords (rowWords (MachineRegularOriginalRow.inheritedRow H t e)))⟩)
      (timeBound internalDegree (tableBits t).length (base (9 : Tape)).length) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.Input, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.machine, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.timeBound