OAI/Computability/MaxCut/Machines/MachineInitialHeaders.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Actual caller-program traces for non-destructive unary-prefix emission and the two headers of the raw initial graph. Unread suffixes are never scanned.

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.Alphabet line 21
  2. def OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.prefixScan line 23
  3. theorem OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.update_source_inline_MachineInitialHeaders line 34
  4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.update_scratch_inline_MachineInitialHeaders line 48
  5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.update_output_inline_MachineInitialHeaders line 59
  6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.prefixStep_true line 65
  7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.prefixStep_false line 76
  8. theorem OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.replicate_append_cons_inline_MachineInitialHeaders line 86
  9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.prefixScanTrace line 92

    Source documentation

    The first loop takes one transition per unary bit and one for the delimiter.

    theorem prefixScanTrace (source scratch output : K)
    (hst : source ≠ scratch) (hso : source ≠ output) (hto : scratch ≠ output)
    (scale : ℕ) (again restore : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.Alphabet

  10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.prefixTrace line 129
  11. def OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.prefixInTime line 179
  12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.prefixScan_pushBound line 198
  13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.literalTrace line 206

    Source documentation

    One transition emits a fixed literal word and enters the caller continuation.

    theorem literalTrace (output : K) (word : List Bool) (label : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.Alphabet

  14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.trace_trans_inline_MachineInitialHeaders line 219
  15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.headerTrace line 225

    Source documentation

    The complete raw initial-graph header phase, in an arbitrary caller program. Only the output tape changes; its old suffix is preserved verbatim.

    theorem headerTrace (nTape mTape scratch output : K)
    (_hnm : nTape ≠ mTape) (hnt : nTape ≠ scratch) (hno : nTape ≠ output)
    (hmt : mTape ≠ scratch) (hmo : mTape ≠ output) (hto : scratch ≠ output)
    (scanN restoreN scanM1 restoreM1 closeFirst scanM6 restoreM6 closeSecond : Λ)
    (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.Alphabet

  16. def OAI.MaxCutGames.Foundations.Complexity.MachineInitialHeaders.headerInTime line 305
  17. abbrev OAI.MaxCutGames.Explicit.MachineProductSeed.Command line 351
  18. abbrev OAI.MaxCutGames.Explicit.MachineProductSeed.LocalLabel line 352
  19. abbrev OAI.MaxCutGames.Explicit.MachineProductSeed.Label line 353
  20. def OAI.MaxCutGames.Explicit.MachineProductSeed.entry line 355
  21. def OAI.MaxCutGames.Explicit.MachineProductSeed.localInstruction line 358
  22. def OAI.MaxCutGames.Explicit.MachineProductSeed.instruction line 362
  23. def OAI.MaxCutGames.Explicit.MachineProductSeed.result line 366
  24. def OAI.MaxCutGames.Explicit.MachineProductSeed.finalTapes line 369
  25. theorem OAI.MaxCutGames.Explicit.MachineProductSeed.sequence_steps line 372
  26. theorem OAI.MaxCutGames.Explicit.MachineProductSeed.seedTrace line 381

    Source documentation

    Each literal has an actual one-transition trace in the ambient machine.

    theorem seedTrace (commands : List (Command K)) (labels : Label commands → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool))
    (atLabels : ∀ l, program (labels l) = instruction commands labels exit l)
    (base : K → List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[commands.length]
      (some ⟨entry commands labels exit, (ambient, register), base⟩) =
      some ⟨exit, (ambient, register), finalTapes commands base⟩ := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductSeed.Command, OAI.MaxCutGames.Explicit.MachineProductSeed.Label, OAI.MaxCutGames.Explicit.MachineProductSeed.instruction, OAI.MaxCutGames.Explicit.MachineProductSeed.entry, OAI.MaxCutGames.Explicit.MachineProductSeed.finalTapes

  27. theorem OAI.MaxCutGames.Explicit.MachineProductSeed.finalTapes_frame line 399
  28. theorem OAI.MaxCutGames.Explicit.MachineProductSeed.finalTapes_field line 409
  29. inductive OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.Tape line 440
  30. inductive OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.Label line 444
  31. def OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.labelAt line 451
  32. def OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.statement line 456

    Source documentation

    Place one of finitely many actual statements into an arbitrary ambient Boolean-tape program, preserving the ambient state component.

    def statement (tape : Tape k → K) (labels : Label k → Λ) (exit : Option Λ) :
    Label k → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool)
  | .seed j => .push (tape (.current j)) (fun _ => false)
      (.goto (fun _ => labels (.copyOut j)))
  | .copyOut j => Reduction.MachineTransfer.loopAt (tape .radix) (tape .scratch)
      id false (labels (.copyOut j)) (some (labels (.copyBack j)))
  | .copyBack j => MachineCopy.forkLoop (tape .scratch) (tape .radix) (tape (.remaining j))
      false (labels (.copyBack j)) (some (labels (.trim j)))
  | .trim j => .pop (tape (.remaining j)) (fun state _ => state)
      (.goto (fun _ => labelAt labels (j.val+1)))
  | .done => .load (fun state => (state.1,none))
      (Reduction.MachineTransfer.exitAt (tape .radix) exit)

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.Label, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkLoop, OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.labelAt, OAI.MaxCutGames.Reduction.MachineTransfer.exitAt

  33. def OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.digitOutput line 469
  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.digitOutput_frame line 474
  35. def OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.digitInTime line 484
  36. def OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.stageTapes line 535
  37. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.stageTapes_frame line 540
  38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.stageTapes_current line 552
  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.stageTapes_remaining line 575
  40. def OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.prefixInTime line 598

    Source documentation

    Place the actual finite initialization prefix inside an ambient program.

    def prefixInTime (m : Nat) (hm : 0 < m) (base : K → List Bool)
    (hradix : base (tape .radix) = encodeWord m)
    (hcurrent : ∀j, base (tape (.current j)) = [])
    (hremaining : ∀j, base (tape (.remaining j)) = [])
    (hscratch : base (tape .scratch) = []) (ambient : σ) (r : Nat) (hr : r ≤ k) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labelAt labels 0),(ambient,none),base⟩
      (some ⟨some (labelAt labels r),(ambient,none),stageTapes tape m base r⟩)
      (r*(2*m+6)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.labelAt, OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.stageTapes

  41. def OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.initializeInTime line 632

    Source documentation

    Complete actual initialization, including width zero and the optional continuation. The radix, scratch, ambient state and unrelated tapes survive.

    def initializeInTime (m : Nat) (hm : 0 < m) (base : K → List Bool)
    (hradix : base (tape .radix) = encodeWord m)
    (hcurrent : ∀j, base (tape (.current j)) = [])
    (hremaining : ∀j, base (tape (.remaining j)) = [])
    (hscratch : base (tape .scratch) = []) (ambient : σ) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labelAt labels 0),(ambient,none),base⟩
      (some ⟨exit,(ambient,none),stageTapes tape m base k⟩)
      (k*(2*m+6)+1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.labelAt, OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.stageTapes

  42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.output_current line 655
  43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.output_remaining line 661
  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.output_radix line 667
  45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOdometerInit.output_scratch line 673