OAI/Computability/UniqueGames/Machines/MachineTupleOdometer.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Alphabet line 15
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.digitTapes line 17
3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.increment line 21
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.reset line 30

   Source documentation

   Reset conserves the digit's unary budget, then enters the next coordinate.

   def reset (current remaining : K) (resetLabel carryLabel : Λ) :
       TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Alphabet

5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.incrementPushBound line 35
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.resetPushBound line 40
7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.update_current line 44
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.update_remaining line 55
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.stepAux_increment_succ line 61
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.stepAux_increment_zero line 71
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.incrementStep_succ line 82

    Source documentation

    A non-carrying digit increment is one actual ambient-program transition.

    theorem incrementStep_succ (current remaining : K) (distinct : current ≠ remaining)
        (checkLabel doneLabel resetLabel : Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Alphabet

12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.incrementStep_zero line 95
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.resetTrace line 108
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.carryTrace line 123

    Source documentation

    Exhaustion costs one check plus the actual d + 1-transition reset.

    theorem carryTrace (current remaining : K) (distinct : current ≠ remaining)
        (checkLabel doneLabel resetLabel carryLabel : Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Alphabet

15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.digitSteps line 145

    Source documentation

    The exact step count for one digit, including its possible reset.

    def digitSteps (d r : ℕ) : ℕ := if r = 0 then d + 2 else 1

16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.digitTrace line 149

    Source documentation

    The bounded digit operation follows actual transitions on both branches. It restores an exhausted digit to zero before returning the carry.

    theorem digitTrace (current remaining : K) (distinct : current ≠ remaining)
        (checkLabel doneLabel resetLabel carryLabel : Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Alphabet

17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.digitSteps_le line 174
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.digitBudget line 180
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.digitFrame line 186

    Source documentation

    Every unrelated stack is preserved, including any separate stored radix or input bound. Both digit-stack suffixes are preserved by the trace itself.

    theorem digitFrame (current remaining other : K)
        (notCurrent : other ≠ current) (notRemaining : other ≠ remaining)
        (base : K → List Bool) (d r : ℕ) (currentSuffix remainingSuffix : List Bool) :
        digitTapes current remaining base (if r = 0 then 0 else d + 1)
          (if r = 0 then d else r - 1) currentSuffix remainingSuffix other =
          digitTapes current remaining base d r currentSuffix remainingSuffix other := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.digitTapes

20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.digitInTime line 196

    Source documentation

    A composable actual-time witness for any well-formed positive-radix digit.

    def digitInTime (current remaining : K) (distinct : current ≠ remaining)
        (checkLabel doneLabel resetLabel carryLabel : Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Alphabet

21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.bodyConfiguration line 218
22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.checkConfiguration line 226
23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.cycleExit line 234
24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.VisitTraces line 241
25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.cycleSteps line 252
26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.cycleSteps_zero line 255
27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.cycleSteps_succ line 259
28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.cycleTrace line 265
29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.ascendingCycleInTime line 302

    Source documentation

    A full positive-radix cycle performs n body visits and exactly 2*n counter transitions. This bound comes from the composed actual execution.

    def ascendingCycleInTime (current remaining : K) (distinct : current ≠ remaining)
        (bodyLabel checkLabel resetLabel exitLabel : Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Alphabet

30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.tupleOrder line 340
31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.tupleOrder_length line 343
32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.tupleOrder_dimension_zero line 347

    Source documentation

    Dimension zero visits the unique empty tuple once, even at radix zero.

    theorem tupleOrder_dimension_zero (n : ℕ) :
        tupleOrder n 0 = [fun i => Fin.elim0 i] := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.tupleOrder

33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.tupleOrder_radix_zero line 355

    Source documentation

    A positive-dimensional zero-radix loop has no tuples to visit.

    theorem tupleOrder_radix_zero {q : ℕ} (hq : 0 < q) : tupleOrder 0 q = [] := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.tupleOrder

34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.tupleRank_cons line 361

    Source documentation

    Coordinate zero is the least significant digit. This is the same radix rank used by SourceOccurrences.Encoding.function.

    theorem tupleRank_cons {n q : ℕ} (d : Fin n) (tail : Fin q → Fin n) :
        (finFunctionFinEquiv (Fin.cons d tail)).val =
          d.val + n * (finFunctionFinEquiv tail).val := by
    …

35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.tupleRank_increment_lowest line 372
36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.tupleRank_carry line 381

    Source documentation

    Resetting an exhausted low digit and incrementing the tail advances the same explicit tuple rank by one.

    theorem tupleRank_carry {n q : ℕ} (hn : 0 < n) (d : Fin n)
        (tail tail' : Fin q → Fin n) (hmax : d.val = n - 1)
        (htail : (finFunctionFinEquiv tail').val = (finFunctionFinEquiv tail).val + 1) :
        (finFunctionFinEquiv (Fin.cons (⟨0, hn⟩ : Fin n) tail')).val =
          (finFunctionFinEquiv (Fin.cons d tail)).val + 1 := by
    …

37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.tupleRank_snoc line 390
38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.tupleOrder_snoc line 397
39. structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.CycleSchedule line 423

    Source documentation

    Explicit caller state and tape endpoints for one level of the nested loop. Compatibility with its child schedules is checked by their types.

    structure CycleSchedule (K σ : Type) where
    …

40. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Configuration line 430
41. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle line 437

    Source documentation

    A finite nesting schedule. Only leaves supply actual emitter traces. Internal nodes supply concrete instruction placements and compatible endpoint schedules; their complete execution is derived below. Level q operates coordinate q, so coordinate zero is always the innermost loop.

    inductive NestedCycle (n : ℕ) (current remaining : ℕ → K) (bodyLabel : Λ)
        (checkLabel resetLabel : ℕ → Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool)) :
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Alphabet

42. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.counterOverhead line 469

    Source documentation

    Exact concrete-counter overhead for a complete positive-radix nesting.

    def counterOverhead (n : ℕ) : ℕ → ℕ
      | 0 => 0
      | q + 1 => n * (counterOverhead n q + 2)
    
    namespace NestedCycle
    
    variable {n : ℕ} {current remaining : ℕ → K} {bodyLabel : Λ}
      {checkLabel resetLabel : ℕ → Λ}
      {program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool)}

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Alphabet

43. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps line 479
44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.LeafBound line 490

    Source documentation

    Every supplied emitter leaf obeys its local time allowance. There is no whole-loop runtime premise at any internal node.

    def LeafBound (B : ℕ) {depth : ℕ} {exitLabel : Λ} {start finish : Configuration K Λ σ}
        (tree : NestedCycle n current remaining bodyLabel checkLabel resetLabel program
          depth exitLabel start finish) : Prop :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Configuration, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle

45. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.work line 499

    Source documentation

    Sum of the actual supplied emitter costs, with no counter work included.

    def work {depth : ℕ} {exitLabel : Λ} {start finish : Configuration K Λ σ}
        (tree : NestedCycle n current remaining bodyLabel checkLabel resetLabel program
          depth exitLabel start finish) : ℕ :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Configuration, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle

46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.reverseDigit line 507
47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.reverseDigit_current line 509
48. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.order line 513
49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.order_eq_tupleOrder line 523
50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.order_length line 532
51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps_eq_work_add_overhead line 537
52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.trace line 563

    Source documentation

    The whole nested-loop trace is derived from its actual leaf traces and the concrete increment/reset code.

    theorem trace {depth : ℕ} {exitLabel : Λ} {start finish : Configuration K Λ σ}
        (tree : NestedCycle n current remaining bodyLabel checkLabel resetLabel program
          depth exitLabel start finish) :
        (MachineComposition.advance (TM2.step program))^[tree.steps] (some start) = some finish := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Configuration, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance

53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps_le line 579
54. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.inTime line 609

    Source documentation

    An actual-time certificate for the complete fixed-dimensional schedule.

    def inTime {depth : ℕ} {exitLabel : Λ} {start finish : Configuration K Λ σ}
        (tree : NestedCycle n current remaining bodyLabel checkLabel resetLabel program
          depth exitLabel start finish) (B : ℕ) (bounded : tree.LeafBound B) :
        StateTransition.EvalsToInTime (TM2.step program) start (some finish)
          (n ^ depth * B + counterOverhead n depth) where
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Configuration, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.counterOverhead

55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.counterOverhead_le line 621
56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps_le_power line 642
57. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.entry line 656

    Source documentation

    The actual entry guard bypasses an empty positive-dimensional Cartesian product. Dimension zero always enters its one empty-tuple emitter.

    def entry (q : ℕ) (radix : K) (bodyLabel exitLabel : Λ) :
        TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Alphabet

58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.entryStep_dimension_zero line 666
59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.entryStep_radix_zero line 676
60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.entryStep_radix_positive line 688
61. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Control.Label line 707

    Source documentation

    Two labels per coordinate, plus start, body, and exit labels.

    abbrev Label (q : ℕ) := Fin q ⊕ (Fin q ⊕ Option Bool)

62. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Control.start line 709
63. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Control.body line 710
64. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Control.exit line 711
65. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Control.check line 712
66. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Control.resetLabel line 713
67. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Control.carry line 715
68. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Control.program line 720

    Source documentation

    A fixed finite controller. Its only unspecified instruction is the emitter body, whose actual leaf traces are supplied to NestedCycle.

    def program (q : ℕ) (current remaining : Fin q → K) (radix : K)
        (emitter : TM2.Stmt (Alphabet (K := K)) (Label q) (σ × Option Bool)) :
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Control.Label

69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTupleOdometer.Control.label_card line 730