OAI/Computability/MaxCut/Machines/MachineSubroutine.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Actual lookup from a preserved table. A fresh copy is prefixed to the scan stack before each access. The old scan suffix is retained and need not be cleared between accesses. No graph/table data occurs in finite control.

  1. def OAI.MaxCutGames.Foundations.Complexity.MachineSubroutine.label line 12
  2. def OAI.MaxCutGames.Foundations.Complexity.MachineSubroutine.configuration line 16
  3. def OAI.MaxCutGames.Foundations.Complexity.MachineSubroutine.statement line 19
  4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineSubroutine.stepAux_simulation line 33
  5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineSubroutine.step_simulation line 54
  6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineSubroutine.trace line 70
  7. def OAI.MaxCutGames.Foundations.Complexity.MachineSubroutine.execution line 80
  8. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.Alphabet line 103
  9. def OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.initialTapes line 106

    Source documentation

    Tape roles: original table, unary query, scan work, output, copy scratch.

    def initialTapes (tape : Fin 5 → K) (base : K → List Bool)
    (index : Nat) (indexSuffix workSuffix output : List Bool) : K → List Bool :=
…
  10. def OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.finalTapes line 111
  11. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.lookupFramedHaltTrace_some line 118
  12. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.preservingLookupTrace line 138

    Source documentation

    Code-level interfaces specify the actual two copy loops and six lookup instructions in the caller's program. No execution premise is supplied.

    theorem preservingLookupTrace (tape : Fin 5 → K) (distinct : Function.Injective tape)
    (firstLabel secondLabel : Λ) (lookupLabels : MachineLookup.Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLookup.Label, OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.program, OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.Alphabet

  13. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.preservingLookup_steps_le line 188
  14. def OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.preservingLookupInTime line 196
  15. inductive OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.Label line 218
  16. def OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.program line 222
  17. def OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.machine line 229
  18. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.Alphabet line 249
  19. inductive OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.Label line 251
  20. def OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.instruction line 256
  21. def OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.steps line 271
  22. def OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.finalTapes line 276
  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.initialTapes_eq_update line 281
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.affineLookupTrace line 303

    Source documentation

    An exact trace for the actual composite instructions. atLabels specifies the caller's finite program; there is no execution or runtime premise.

    theorem affineLookupTrace (source : K) (tape : Fin 5 → K)
    (distinct : Function.Injective tape) (outside : ∀ i, source ≠ tape i)
    (coefficient offset : Nat) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.Label, OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.Alphabet

  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.steps_le line 331
  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.steps_le_table line 339
  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.finalTapes_other line 346
  28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.finalTapes_output line 352
  29. def OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.machine line 357
  30. abbrev OAI.MaxCutGames.Explicit.MachineProductGather.Tape line 388

    Source documentation

    Shared original table, query, scan and copy scratch, then input coordinate fields and the corresponding gathered output fields.

    abbrev Tape (width : Nat) := Fin 4 ⊕ (Fin width ⊕ Fin width)
  31. def OAI.MaxCutGames.Explicit.MachineProductGather.shift line 390
  32. theorem OAI.MaxCutGames.Explicit.MachineProductGather.shift_injective line 393
  33. def OAI.MaxCutGames.Explicit.MachineProductGather.lookupRole line 397
  34. theorem OAI.MaxCutGames.Explicit.MachineProductGather.lookupRole_injective line 404
  35. def OAI.MaxCutGames.Explicit.MachineProductGather.Label line 408
  36. instance OAI.MaxCutGames.Explicit.MachineProductGather.labelFintype line 412
  37. instance OAI.MaxCutGames.Explicit.MachineProductGather.labelDecidableEq line 419
  38. def OAI.MaxCutGames.Explicit.MachineProductGather.entry line 426
  39. def OAI.MaxCutGames.Explicit.MachineProductGather.instruction line 430
  40. def OAI.MaxCutGames.Explicit.MachineProductGather.steps line 444
  41. def OAI.MaxCutGames.Explicit.MachineProductGather.finalTapes line 451
  42. theorem OAI.MaxCutGames.Explicit.MachineProductGather.finalTapes_other line 461
  43. theorem OAI.MaxCutGames.Explicit.MachineProductGather.gatherTrace line 476
  44. theorem OAI.MaxCutGames.Explicit.MachineProductGather.finalTapes_field line 538

    Source documentation

    Every output is the physically gathered unary field, with its old suffix preserved. This identifies the operands consumed by the Horner phase.

    theorem finalTapes_field (values : List Nat) (coefficient width : Nat)
    (placement : Tape width → K) (distinct : Function.Injective placement)
    (indices offsets fields : Fin width → Nat) (base : K → List Bool) (i : Fin width) :
    finalTapes values coefficient width placement indices offsets fields base
      (placement (.inr (.inr i))) =
      encodeWord (fields i) ++ base (placement (.inr (.inr i))) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductGather.Tape, OAI.MaxCutGames.Explicit.MachineProductGather.finalTapes

  45. theorem OAI.MaxCutGames.Explicit.MachineProductGather.steps_le line 573

    Source documentation

    For fixed width, gather time is linear in the encoded table size plus coordinate magnitudes. Query and scan debris is never rescanned.

    theorem steps_le (values : List Nat) (coefficient width magnitude : Nat)
    (indices offsets fields : Fin width → Nat)
    (selected : ∀ i, values[coefficient * indices i + offsets i]? = some (fields i))
    (bounded : ∀ i, indices i ≤ magnitude) :
    steps values coefficient width indices offsets ≤
      width * (2 * magnitude + 5 * (encodeWords values).length + 6) + 1 := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductGather.steps

  46. def OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.guardConfiguration line 610
  47. def OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.bodyConfiguration line 616
  48. def OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.exitConfiguration line 621
  49. def OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.BodyTraces line 628

    Source documentation

    The hypotheses are actual traces of the caller's body in the same program. Both endpoints have the same unary remainder and unread suffix.

    def BodyTraces (counter : K) (guardLabel bodyLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
  50. def OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.totalSteps line 638

    Source documentation

    Exactly n supplied body blocks and n + 1 concrete guard transitions.

    def totalSteps (cost : Nat → Nat) (n : Nat) : Nat :=
…
  51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.totalSteps_zero line 641
  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.totalSteps_succ line 644
  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.loopTrace line 651

    Source documentation

    The loop trace is derived by composing each actual unary guard transition with one supplied body trace. No whole-loop execution is assumed.

    theorem loopTrace (counter : K) (guardLabel bodyLabel exitLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.totalSteps_le line 684
  55. def OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.loopInTime line 696

    Source documentation

    An actual timed execution witness with the exact composed step count.

    def loopInTime (counter : K) (guardLabel bodyLabel exitLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
  56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.baseFrame line 717

    Source documentation

    Chaining the caller's declared per-body frame equalities.

    theorem baseFrame (base : Nat → K → List Bool) (frame : K → Prop) (n : Nat)
    (bodyFrame : ∀ r, r < n → ∀ k, frame k → base (r + 1) k = base r k) :
    ∀ k, frame k → base n k = base 0 k := by
…
  57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.counterFrame line 730

    Source documentation

    Protected tapes are unchanged by the complete loop, including its guard steps. The counter itself is explicitly excluded from this frame.

    theorem counterFrame (counter : K) (suffix : List Bool)
    (base : Nat → K → List Bool) (frame : K → Prop) (n : Nat)
    (counterOutside : ∀ k, frame k → k ≠ counter)
    (bodyFrame : ∀ r, r < n → ∀ k, frame k → base (r + 1) k = base r k) :
    ∀ k, frame k →
      counterTapes counter (base n) n suffix k = counterTapes counter (base 0) 0 suffix k := by
…
  58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.loopTrace_framed line 742

    Source documentation

    Actual loop execution and preservation of an arbitrary declared tape frame.

    theorem loopTrace_framed (counter : K) (guardLabel bodyLabel exitLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…