OAI/Computability/MaxCut/Machines/MachineTuple.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MaxCutGames.Reduction.MachineSourceTuple.Tape line 12
2. inductive OAI.MaxCutGames.Reduction.MachineSourceTuple.Label line 19
3. def OAI.MaxCutGames.Reduction.MachineSourceTuple.place line 28
4. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.place_injective line 32
5. def OAI.MaxCutGames.Reduction.MachineSourceTuple.fill line 36
6. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.fill_place line 43
7. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.fill_self line 48
8. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.fill_update line 58
9. def OAI.MaxCutGames.Reduction.MachineSourceTuple.placedLabel line 67
10. def OAI.MaxCutGames.Reduction.MachineSourceTuple.placedConfiguration line 71
11. def OAI.MaxCutGames.Reduction.MachineSourceTuple.placedStatement line 77
12. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.placed_stepAux line 89
13. def OAI.MaxCutGames.Reduction.MachineSourceTuple.nextLabel line 114
14. def OAI.MaxCutGames.Reduction.MachineSourceTuple.program line 117
15. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.placed_step line 128
16. def OAI.MaxCutGames.Reduction.MachineSourceTuple.lookupOutput line 145
17. def OAI.MaxCutGames.Reduction.MachineSourceTuple.placedLookupInTime line 150
18. def OAI.MaxCutGames.Reduction.MachineSourceTuple.copiedTapes line 166
19. def OAI.MaxCutGames.Reduction.MachineSourceTuple.coordinateOutput line 169
20. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.cleanup_lookupOutput line 177
21. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.coordinateOutput_savedIndex line 205
22. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.coordinateOutput_field line 210
23. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.coordinateOutput_other_field line 217
24. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.suffix_length_le_input line 222
25. def OAI.MaxCutGames.Reduction.MachineSourceTuple.coordinateInTime line 234
26. def OAI.MaxCutGames.Reduction.MachineSourceTuple.labelAt line 279
27. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.nextLabel_eq line 282
28. def OAI.MaxCutGames.Reduction.MachineSourceTuple.stageTapes line 284
29. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.stageTapes_frame line 292
30. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.stageTapes_clean line 305
31. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.stageTapes_field line 317
32. def OAI.MaxCutGames.Reduction.MachineSourceTuple.prefixInTime line 342
33. def OAI.MaxCutGames.Reduction.MachineSourceTuple.loadInTime line 385
34. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.equations_length_le_input line 408
35. def OAI.MaxCutGames.Reduction.MachineSourceTuple.loadUnaryInTime line 415

    Source documentation

    Actual odometer digits have empty suffixes. The resulting complete loader runs in a polynomial whose coefficients depend only on the fixed repetition k.

    noncomputable def loadUnaryInTime (F : SourceEncoding.Input) (tuple : Fin width → Fin F.equations.length)
        (base : Tape width Extra → List Bool)
        (hsource : base .source = inputBits F)
        (hsavedIndex : ∀ j, base (.savedIndex j) = encodeWord (tuple j).val)
        (hindex : base .index = []) (hwork : base .work = [])
        (hscratch : base .scratch = []) (hcopy : base .copyScratch = []) (ambient : σ) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some (labelAt 0), ((ambient, ()), none), base⟩
          (some ⟨none, ((ambient, ()), none), stageTapes F tuple base width⟩)
          (width * (10 * (inputBits F).length + 20) + 1) := by
    …

    Mentions: OAI.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.MachineSourceTuple.Tape, OAI.MaxCutGames.Reduction.MachineSourceTuple.program, OAI.MaxCutGames.Reduction.MachineSourceTuple.labelAt, OAI.MaxCutGames.Reduction.MachineSourceTuple.stageTapes

36. def OAI.MaxCutGames.Reduction.MachineSourceTuple.timePolynomial line 438
37. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.timePolynomial_eval line 441
38. def OAI.MaxCutGames.Reduction.MachineSourceTuple.tupleBitLength line 448

    Source documentation

    Total physical length of the saved occurrence-ID tapes.

    def tupleBitLength (base : Tape width Extra → List Bool) : Nat :=
    …

    Mentions: OAI.MaxCutGames.Reduction.MachineSourceTuple.Tape

39. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.savedIndex_length_le_tupleBitLength line 452
40. def OAI.MaxCutGames.Reduction.MachineSourceTuple.loadTupleInTime line 457
41. def OAI.MaxCutGames.Reduction.MachineSourceTuple.loadTuplePolynomialInTime line 472

    Source documentation

    The same concrete run with a univariate polynomial in the combined size.

    noncomputable def loadTuplePolynomialInTime (F : SourceEncoding.Input)
        (tuple : Fin width → Fin F.equations.length) (base : Tape width Extra → List Bool)
        (hsource : base .source = inputBits F)
        (hsaved : ∀ j, base (.savedIndex j) = encodeWord (tuple j).val)
        (hindex : base .index = []) (hwork : base .work = [])
        (hscratch : base .scratch = []) (hcopy : base .copyScratch = []) (ambient : σ) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some (labelAt 0), ((ambient, ()), none), base⟩
          (some ⟨none, ((ambient, ()), none), stageTapes F tuple base width⟩)
          ((timePolynomial width).eval ((inputBits F).length + tupleBitLength base)) := by
    …

    Mentions: OAI.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.MachineSourceTuple.Tape, OAI.MaxCutGames.Reduction.MachineSourceTuple.program, OAI.MaxCutGames.Reduction.MachineSourceTuple.labelAt, OAI.MaxCutGames.Reduction.MachineSourceTuple.stageTapes, OAI.MaxCutGames.Reduction.MachineSourceTuple.timePolynomial, OAI.MaxCutGames.Reduction.MachineSourceTuple.tupleBitLength

42. def OAI.MaxCutGames.Reduction.MachineSourceTuple.nameSlot line 490
43. def OAI.MaxCutGames.Reduction.MachineSourceTuple.nameField line 491
44. def OAI.MaxCutGames.Reduction.MachineSourceTuple.rhsField line 492
45. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.nameField_ne_rhsField line 495
46. def OAI.MaxCutGames.Reduction.MachineSourceTuple.equationName line 504
47. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.equationWords_name line 510
48. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.output_name line 517
49. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.output_rhs line 524
50. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.output_savedIndex line 532
51. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.output_savedIndex_unary line 538
52. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.output_source line 545
53. def OAI.MaxCutGames.Reduction.MachineSourceTuple.canonicalFields line 552

    Source documentation

    The fourth canonical record field is the saved occurrence ID. The equation RHS remains separately available on rhsField j.

    def canonicalFields (tapes : Tape width Extra → List Bool) (j : Fin width) : List (List Bool) :=
    …

    Mentions: OAI.MaxCutGames.Reduction.MachineSourceTuple.Tape

54. def OAI.MaxCutGames.Reduction.MachineSourceTuple.canonicalWords line 555
55. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.output_canonicalFields line 559
56. theorem OAI.MaxCutGames.Reduction.MachineSourceTuple.zeroWidthStep line 569

    Source documentation

    Width zero executes its actual done statement in one transition.

    theorem zeroWidthStep (base : Tape 0 Extra → List Bool) (ambient : σ) :
        TM2.step program ⟨some (labelAt 0), ((ambient, ()), none), base⟩ =
          some ⟨none, ((ambient, ()), none), base⟩ := rfl

    Mentions: OAI.MaxCutGames.Reduction.MachineSourceTuple.Tape, OAI.MaxCutGames.Reduction.MachineSourceTuple.program, OAI.MaxCutGames.Reduction.MachineSourceTuple.labelAt

57. def OAI.MaxCutGames.Reduction.MachineSourceTuple.placedLoadUnaryInTime line 575

    Source documentation

    A caller shares this complete tape arena and state, mapping only labels and the final continuation. All saved occurrence IDs remain available to its body.

    noncomputable def placedLoadUnaryInTime {Λ : Type}
        (labels : Label width → Λ) (exit : Option Λ)
        (target : Λ → TM2.Stmt (fun _ : Tape width Extra => Bool) Λ ((σ × Unit) × Option Bool))
        (atLabels : ∀ l, target (labels l) = MachineSubroutine.statement labels exit (program l))
        (F : SourceEncoding.Input) (tuple : Fin width → Fin F.equations.length)
        (base : Tape width Extra → List Bool)
        (hsource : base .source = inputBits F)
        (hsaved : ∀ j, base (.savedIndex j) = encodeWord (tuple j).val)
        (hindex : base .index = []) (hwork : base .work = [])
        (hscratch : base .scratch = []) (hcopy : base .copyScratch = []) (ambient : σ) :
        StateTransition.EvalsToInTime (TM2.step target)
          ⟨some (labels (labelAt 0)), ((ambient, ()), none), base⟩
    …

    Mentions: OAI.MaxCutGames.Reduction.MachineSourceTuple.Label, OAI.MaxCutGames.Reduction.MachineSourceTuple.Tape, OAI.MaxCutGames.Reduction.MachineSourceTuple.program, OAI.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.MachineSourceTuple.labelAt

58. def OAI.MaxCutGames.Reduction.MachineSourceTuple.machine line 592