OAI/Computability/UniqueGames/Machines/MachineLazyRows.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.Label line 16
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.State line 17
3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.addressIndex line 21

   Source documentation

   Tape roles: tail, old reverse, relation, scratch, divided copy, quotient, new reverse, accumulated output, row buffer.

   def addressIndex : Fin 5 → Fin 9 := ![1, 3, 4, 5, 6]

4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.addressIndex_injective line 23
5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.fields line 27
6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.reindexInstruction line 31

   Source documentation

   The program depends on the fixed degree and tape placement, never on input-dependent vertices, reverse indices, or predicate values.

   def reindexInstruction (d : Nat) (positive : 0 < d) (c b : Nat) (tape : Fin 9 → K)
       (labels : Label d → Λ) (exit : Option Λ) :
       Label d → TM2.Stmt (fun _ : K => Bool) Λ (State A d)
     | .inl stage => MachinePortReindex.instruction d positive c b
         (tape ∘ addressIndex) (fun stage => labels (.inl stage))
         (some (labels (.inr .relationRead))) stage
     | .inr stage => MachineTableRows.routine (fields tape) (tape 8) (tape 7) (tape 3)
         (fun stage => labels (.inr stage)) exit stage

   Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.addressIndex, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableRows.routine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.fields

7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.instruction line 40
8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.reindexRowBits line 45
9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.reindexMappedTapes line 49
10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.reindexResultTapes line 53
11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.reindexSteps line 58
12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.rowBits line 62
13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.mappedTapes line 65
14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.resultTapes line 68
15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.steps line 73
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.reindexRowTrace line 76
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.rowTrace line 140

    Source documentation

    Lazy specialization of the shared physical mapper/emitter execution.

    theorem rowTrace (d : Nat) (positive : 0 < d) (tape : Fin 9 → K)
        (distinct : Function.Injective tape) (labels : Label d → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State A d))
        (atLabels : ∀ l, program (labels l) = instruction d positive tape labels exit l)
        (base : K → List Bool) (v j : Nat) (relation : RelationTable)
        (tailWord : base (tape 0) = encodeWord v)
        (reverseWord : base (tape 1) = encodeWord j)
        (relationWord : base (tape 2) = encodeWords (relationWords relation))
        (scratchEmpty : base (tape 3) = []) (workEmpty : base (tape 4) = [])
        (quotientEmpty : base (tape 5) = []) (newReverseEmpty : base (tape 6) = [])
        (rowEmpty : base (tape 8) = []) (ambient : A) :
        (advance (TM2.step program))^[steps d v j relation (base (tape 7))]
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.steps

18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.rowBits_eq_moveRow line 162

    Source documentation

    The body emits exactly the moving row of the actual lazy table.

    theorem rowBits_eq_moveRow {n d : Nat} (table : PCP.PortTables.Table n d)
        (v : Fin n) (p : Fin d) :
        rowBits d v.val (PCP.PreprocessingLazyWords.row table v p).reverseIndex.val
            (PCP.PreprocessingLazyWords.row table v p).relation =
          encodeWords (rowWords (moveRow table v p)) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.rowBits, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.row, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.machine line 172

    Source documentation

    A concrete machine for this stored-field phase, with nine Boolean tapes and a finite residue register. It does not assume a whole-row runtime.

    def machine (d : Nat) (positive : 0 < d) : FinTM2 where
    …

20. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.Buffer line 183
21. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.StreamState line 184
22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamClean line 186
23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.relationStateEquiv line 190

    Source documentation

    Only finite register coordinates change; all tapes remain fixed.

    def relationStateEquiv (A : Type) (d : Nat) :
        MachineRegularOriginalRow.State (A × Fin d) ≃ StreamState A d where
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.StreamState

24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamRelationCopy line 197
25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamRelationCopy_step line 202
26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.bodyIndex line 227
27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.bodyIndex_injective line 229
28. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.StreamLabel line 234
29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamInstruction line 240
30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.inputRowBits line 258
31. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamRowSteps line 261
32. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamResultTapes line 266
33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.joinTrace line 271
34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamRowTrace line 275
35. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.VertexLabel line 463
36. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.vertexInstruction line 465
37. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.recordsInput line 475
38. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.recordsOutput line 478
39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamFrame line 481
40. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.vertexSteps line 486
41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.recordsInput_eq_codec line 492
42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamFrame_afterRow line 501
43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.vertexSuffixTrace line 520

    Source documentation

    Every port executes its actual loader, mapper, emitter, and cleanup. The trace is proved from the concrete program, with no per-row run premise.

    theorem vertexSuffixTrace {n m : Nat} (d : Nat) (positive : 0 < d) (c b : Nat)
        (tape : Fin 10 → K) (distinct : Function.Injective tape)
        (labels : VertexLabel d → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (StreamState A d))
        (atLabels : ∀ l, program (labels l) = vertexInstruction d positive c b tape labels exit l)
        (base : K → List Bool) (rows : Fin d → DartRow n m)
        (empty : ∀ i : Fin 10, i ≠ 7 → i ≠ 9 → base (tape i) = []) (ambient : A)
        (remaining : Nat) (i : Fin (d + 1)) (count : i.val + remaining = d) (output : List Bool) :
        (advance (TM2.step program))^[vertexSteps d c b ((List.ofFn rows).drop i.val) output]
          (some ⟨some (labels (i, none)), streamClean d positive ambient,
            streamFrame tape base ((List.ofFn rows).drop i.val) output⟩) =
          some ⟨exit, streamClean d positive ambient,
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.VertexLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.StreamState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.vertexInstruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.vertexSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamClean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamFrame

44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.vertexTrace line 604
45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.encodeWords_flatMap line 620
46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.recordsOutput_lazy line 627

    Source documentation

    The computed moving-row block is exactly the actual lazy table's codec.

    theorem recordsOutput_lazy {n d : Nat} (table : PCP.PortTables.Table n d) (v : Fin n) :
        recordsOutput d (2 * d) d (List.ofFn (PCP.PreprocessingLazyWords.row table v)) =
          encodeWords ((List.ofFn (moveRow table v)).flatMap rowWords) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.recordsOutput, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.row, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

47. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.valueBound line 642
48. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.rowSizeBound line 643
49. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.rowCostBound line 644
50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.reindexValue_le line 647
51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.reindexRowBits_length_le line 656
52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamRowSteps_le line 667

    Source documentation

    The bound comes from all loader, mapper, emitter, and cleanup transitions.

    theorem streamRowSteps_le {n m : Nat} (d c b : Nat) (r : DartRow n m) (output : List Bool) :
        streamRowSteps d c b r.tail.val r.reverseIndex.val r.relation output ≤
          rowCostBound c b n m + 2 * output.length := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamRowSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.rowCostBound

53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.vertexSteps_le_capacity line 679
54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.vertexSteps_le line 704
55. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.vertexInTime line 712

    Source documentation

    Timed execution for the concrete fixed-degree old-row loop. The natural bound is polynomial in vertex count, dart count, and accumulated output size.

    def vertexInTime {n m : Nat} (d : Nat) (positive : 0 < d) (c b : Nat)
        (tape : Fin 10 → K) (distinct : Function.Injective tape)
        (labels : VertexLabel d → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (StreamState A d))
        (atLabels : ∀ l, program (labels l) = vertexInstruction d positive c b tape labels exit l)
        (base : K → List Bool) (rows : Fin d → DartRow n m)
        (empty : ∀ i : Fin 10, i ≠ 7 → i ≠ 9 → base (tape i) = [])
        (ambient : A) (output : List Bool) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some (labels (0, none)), streamClean d positive ambient,
            streamFrame tape base (List.ofFn rows) output⟩
          (some ⟨exit, streamClean d positive ambient,
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.VertexLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.StreamState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.vertexInstruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamClean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.streamFrame

56. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.vertexMachine line 733