OAI/Computability/MaxCut/Machines/MachineTupleOdometer.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Alphabet line 13
2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.digitTapes line 15
3. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.increment line 19
4. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.reset line 28

   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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Alphabet

5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.incrementPushBound line 33
6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.resetPushBound line 38
7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.update_current_inline_MachineTupleOdometer line 42
8. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.update_remaining_inline_MachineTupleOdometer line 53
9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.stepAux_increment_succ line 59
10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.stepAux_increment_zero line 69
11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.incrementStep_succ line 80

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Alphabet

12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.incrementStep_zero line 93
13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.resetTrace line 106
14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.carryTrace line 121

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Alphabet

15. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.digitSteps line 143

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.digitTrace line 147

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Alphabet

17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.digitSteps_le line 172
18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.digitBudget line 178
19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.digitFrame line 184

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.digitTapes

20. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.digitInTime line 194

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Alphabet

21. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.bodyConfiguration line 216
22. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.checkConfiguration line 224
23. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.cycleExit line 232
24. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.VisitTraces line 239
25. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.cycleSteps line 250
26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.cycleSteps_zero_inline_MachineTupleOdometer line 253
27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.cycleSteps_succ_inline_MachineTupleOdometer line 257
28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.cycleTrace line 263
29. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.ascendingCycleInTime line 300

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Alphabet

30. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder line 338
31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder_length line 341
32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder_dimension_zero line 345

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder

33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder_radix_zero line 353

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder

34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.tupleRank_cons line 359

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.tupleRank_increment_lowest line 370
36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.tupleRank_carry line 379

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.tupleRank_snoc line 388
38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder_snoc line 395
39. structure OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.CycleSchedule line 421

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Configuration line 428
41. inductive OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle line 435

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Alphabet

42. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.counterOverhead line 467

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle, OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Alphabet

43. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps line 477
44. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.LeafBound line 488

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Configuration, OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle

45. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.work line 497

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Configuration, OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle

46. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.reverseDigit line 505
47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.reverseDigit_current line 507
48. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.order line 511
49. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.order_eq_tupleOrder line 521
50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.order_length line 530
51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps_eq_work_add_overhead line 535
52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.trace line 561

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Configuration, OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle, OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance

53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps_le line 577
54. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.inTime line 607

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Configuration, OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle, OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.counterOverhead

55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.counterOverhead_le line 619
56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps_le_power line 640
57. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.entry line 654

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Alphabet

58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.entryStep_dimension_zero line 664
59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.entryStep_radix_zero line 674
60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.entryStep_radix_positive line 686
61. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Control.Label line 705

    Source documentation

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

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

62. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Control.start line 707
63. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Control.body line 708
64. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Control.exit line 709
65. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Control.check line 710
66. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Control.resetLabel line 711
67. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Control.carry line 713
68. def OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Control.program line 718

    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.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Control.Label

69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTupleOdometer.Control.label_card line 728