OAI/Computability/MaxCut/Machines/EmitRows.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

The actual alphabet-reduction row template. The old predicate and the loop flag are finite registers. All unbounded quantities reside in five preserved unary tapes. The fixed event/slot/orientation order is retained without deduplication.

  1. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.Context line 18
  2. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.RowCommand line 19
  3. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.relationBits line 21
  4. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.vector_list_ofFn_inline_EmitRows line 26
  5. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.bitValues_ofFn_inline_EmitRows line 31
  6. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.relationBits_values line 40
  7. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands line 49

    Source documentation

    Two actual affine fields followed by the 4096 stored relation entries.

    def rowCommands (q : Nat) (event : AlphabetGraph.LocalEvent (Fin q))
    (slot : Fin 6) (orientation : Bool) : List (RowCommand q) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.LocalEvent, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.RowCommand

  8. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.rowContext line 58
  9. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.rowValues line 62
  10. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.encodedRow_inline_EmitRows line 68
  11. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands_bits line 76

    Source documentation

    The executable command semantics equals the precise stored row, including the orientation-specific tail, reverse index, and every predicate bit.

    theorem rowCommands_bits {q : Nat} (input : GenericGraphTables.Table q)
    (edge : Fin input.darts) (event : AlphabetGraph.LocalEvent (Fin q))
    (slot : Fin 6) (orientation : Bool) :
    (rowCommands q event slot orientation).flatMap
      (commandBits (rowValues input edge) (rowContext input edge)) =
      encodeWords (GraphTables.rowWords
        (Table.rowFromDart input (((edge, event), slot), orientation))) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.LocalEvent, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.rowValues, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.rowContext, OAI.MaxCutGames.Foundations.PCP.GraphTables.rowWords, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.rowFromDart

  12. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands line 109

    Source documentation

    One old dart emits every local event, then all six slots, false orientation before true. These loops are fixed by q and form part of the finite template.

    def blockCommands (q : Nat) : List (RowCommand q) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.RowCommand

  13. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.blockWords line 114
  14. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.tableWords_eq_blocks line 121
  15. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands line 134

    Source documentation

    Headers use only the preserved n and m tapes; all relation registers may still have their initial values.

    def headerCommands (q : Nat) (σ : Type) : List (Command 2 σ (Addresses.fieldBound q)) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound

  16. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands_bits line 140
  17. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands_length line 154
  18. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.headerInTime line 158
  19. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.encodeWords_flatMap_inline_EmitRows line 183
  20. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands_bits line 189
  21. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands_length_le line 196
  22. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.flatMap_length_le_inline_EmitRows line 204
  23. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands_length_le line 215
  24. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.blockInTime line 229

    Source documentation

    Actual execution of all rows belonging to one old dart. The finite relation register is supplied by the checked row parser; only code equations are assumed about the enclosing program. The trace restores the five operand tapes.

    def blockInTime {K Λ : Type} [DecidableEq K] {q : Nat}
    (input : GenericGraphTables.Table q) (edge : Fin input.darts)
    (sources : Fin 5 → K) (scratch output : K)
    (sourceScratch : ∀ i, sources i ≠ scratch)
    (sourceOutput : ∀ i, sources i ≠ output) (scratchOutput : scratch ≠ output)
    (labels : Label (blockCommands q).length (Addresses.fieldBound q) → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State (Context q)))
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.Context

  25. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommandsIn line 259

    Source documentation

    Preserve additional finite parser/driver registers through a projection.

    def blockCommandsIn {σ : Type} (q : Nat) (context : σ → Context q) :
    List (Command 5 σ (Addresses.fieldBound q)) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.Context, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound

  26. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommandsIn_bits line 263
  27. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.blockInTimeAmbient line 272
  28. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.Alphabet line 316
  29. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.finish line 319

    Source documentation

    Reset both the ambient finite state and the drain register before exiting.

    def finish (initial : σ) (exit : Option Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.Alphabet

  30. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.instruction line 325

    Source documentation

    A concrete instruction for each of the n drain phases and the final reset.

    def instruction {n : Nat} (selected : Fin n → K) (labels : Fin (n + 1) → Λ)
    (initial : σ) (exit : Option Λ) (phase : Fin (n + 1)) :
    TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.Alphabet

  31. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.instruction_drain line 334
  32. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.instruction_finish line 342
  33. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes line 348

    Source documentation

    Actual tape family after the selected stacks have been drained in order.

    def clearTapes : {n : Nat} → (Fin n → K) → (K → List Bool) → K → List Bool
  | 0, _, base => base
  | n + 1, selected, base =>
      clearTapes (fun i : Fin n => selected i.succ) (Function.update base (selected 0) [])

/-- Exact number of transitions, including the final state-reset transition. -/
  34. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.actualCost line 354

    Source documentation

    Exact number of transitions, including the final state-reset transition.

    def actualCost : {n : Nat} → (Fin n → K) → (K → List Bool) → Nat
  | 0, _, _ => 1
  | n + 1, selected, base =>
      actualCost (fun i : Fin n => selected i.succ) (Function.update base (selected 0) []) +
        ((base (selected 0)).length + 1)
  35. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_apply line 360
  36. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_selected line 373
  37. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_unselected line 377
  38. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.actualCost_le line 383
  39. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.cleanupTrace line 401

    Source documentation

    The trace is derived solely from the actual drain instructions and final reset instruction. No execution of the entire cleanup is assumed.

    theorem cleanupTrace {n : Nat} (selected : Fin n → K) (labels : Fin (n + 1) → Λ)
    (initial : σ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.program, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.Alphabet

  40. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.cleanupInTime line 427

    Source documentation

    Actual cleanup execution, bounded using the original selected-stack lengths.

    def cleanupInTime {n : Nat} (selected : Fin n → K) (labels : Fin (n + 1) → Λ)
    (initial : σ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.program, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.Alphabet

  41. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.program line 444

    Source documentation

    Concrete n+1-label program, terminating after resetting the finite state.

    def program {n : Nat} (selected : Fin n → K) (initial : σ) :
    Fin (n + 1) → TM2.Stmt (Alphabet (K := K)) (Fin (n + 1)) (σ × Option Bool) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.Alphabet

  42. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.machine line 449

    Source documentation

    A bundled finite machine. Its input/output tapes are designated explicitly.

    def machine [Fintype K] [Fintype σ] {n : Nat} (selected : Fin n → K)
    (input output : K) (initial : σ) : FinTM2 where
…
  43. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.machineInTime line 461
  44. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_outputOnly line 474

    Source documentation

    Enumerating exactly the nonoutput stacks yields the standard final tape family. Repeated selected stacks are permitted.

    theorem clearTapes_outputOnly {n : Nat} (selected : Fin n → K)
    (output : K) (base : K → List Bool)
    (excludesOutput : ∀ i, selected i ≠ output)
    (coversOther : ∀ k, k ≠ output → ∃ i, selected i = k) :
    clearTapes selected base = fun k => if k = output then base output else [] := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes

  45. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.machineHaltInTime line 488

    Source documentation

    Full cleanup reaches haltList, with all nonoutput stacks empty and the machine's actual initial finite state restored.

    def machineHaltInTime [Fintype K] [Fintype σ] {n : Nat} (selected : Fin n → K)
    (input output : K) (initial : σ) (base : K → List Bool)
    (ambient : σ) (register : Option Bool)
    (excludesOutput : ∀ i, selected i ≠ output)
    (coversOther : ∀ k, k ≠ output → ∃ i, selected i = k) :
    StateTransition.EvalsToInTime (machine selected input output initial).step
      ⟨some (0 : Fin (n + 1)), (ambient, register), base⟩
      (some (haltList (machine selected input output initial) (base output)))
      ((∑ i, (base (selected i)).length) + n + 1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Cleanup.machine

  46. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.headerPlan line 514
  47. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.rowPlan line 515
  48. inductive OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.Label line 517
  49. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.headerEntry line 529
  50. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.rowEntry line 532
  51. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.clearNext line 535
  52. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.program line 538
  53. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.machine line 574

    Source documentation

    Every state component is finite; the q-dependent relation register is enumerated by the explicit vector/function equivalence of the parser.

    def machine (q : Nat) : FinTM2 := by
…
  54. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.program_setup line 587
  55. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.program_guard line 591
  56. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.program_headLookup line 594
  57. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.program_compare line 598
  58. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.program_increment line 601
  59. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.inputBits line 621
  60. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords line 625

    Source documentation

    The output headers are included even before the first old row is read.

    def prefixWords (input : GenericGraphTables.Table q) (e : Nat) : List Nat :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table

  61. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits line 630
  62. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.cursorWords line 633
  63. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits line 636
  64. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_zero line 639
  65. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_zero line 645
  66. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_succ line 651
  67. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_succ line 664
  68. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_reverse_succ line 671
  69. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_full line 678
  70. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_full line 688

    Source documentation

    At the terminal guard the stored prefix is the complete concrete output encoding.

    theorem prefixBits_full (input : GenericGraphTables.Table q) :
    prefixBits input input.darts = GraphTables.tableBits (Table.build input) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits, OAI.MaxCutGames.Foundations.PCP.GraphTables.tableBits, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Table.build

  71. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_zero line 693
  72. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.cursorWords_succ line 698
  73. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_succ line 709
  74. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_full line 717
  75. structure OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.Ready line 726

    Source documentation

    Guard-to-guard tape contract. Only scan and indexScan may contain residues.

    structure Ready (input : GenericGraphTables.Table q) (e : Nat)
    (base : Tape → List Bool) : Prop where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table

  76. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.of_agree line 745

    Source documentation

    Changing only lookup residues preserves the complete loop contract.

    theorem Ready.of_agree {input : GenericGraphTables.Table q} {e : Nat}
    {base next : Tape → List Bool} (ready : Ready input e base)
    (agree : ∀ tape, tape ≠ .scan → tape ≠ .indexScan → next tape = base tape) :
    Ready input e next where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.Ready

  77. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.update_scan line 765
  78. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.update_indexScan line 772
  79. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.counter_succ line 779
  80. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.counter_at_end line 786
  81. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.cursor_at_end line 791
  82. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.Ready.reversed_at_end line 795