OAI/Computability/MaxCut/Machines/PoweringMachineRowHeaders.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement line 17

   Source documentation

   The existing word placement, with its result directed to row-output 10.

   def headerPlacement {t max : Nat} (h : t ≤ max) : PoweringMachineWord.Tape t → Tape max :=
   …

   Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.Tape

2. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_injective line 20
3. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_table line 24
4. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_query line 28
5. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_scan line 32
6. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_reverse line 36
7. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_scratch line 40
8. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_output line 44
9. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_start line 48
10. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_succ line 52
11. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.Label line 56
12. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.entry line 59
13. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.tailEntry line 61
14. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.affineInstruction line 64
15. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.instruction line 72

    Source documentation

    Only the coefficient, word, and direction are built into finite control.

    def instruction (n : Nat) (h : n + 1 ≤ max) (placement : Tape max → K)
        (ports : Fin (n + 1) → Fin d) (direction : Bool)
        (labels : Label n → Λ) (exit : Option Λ) :
        Label n → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool)
      | .inl q => affineInstruction (placement (start max)) (placement (scratch max))
          (placement (rowOutput max)) (blockSize d n) (reverseOffset d n ports direction)
          (fun z => labels (.inl z)) (some (labels (tailEntry n direction))) q
      | .inr (.inl q) => PoweringMachineWord.copyInstruction
          (placement (start max)) (placement (scratch max)) (placement (rowOutput max))
          (fun z => labels (.inr (.inl z))) exit q
      | .inr (.inr q) => PoweringMachineWord.instruction (n + 1)
          (placement ∘ headerPlacement h) ports (fun z => labels (.inr (.inr z))) exit q

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.Label, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.affineInstruction, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.tailEntry, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.copyInstruction, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.instruction, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement

16. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.afterReverse line 85
17. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes line 90
18. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.steps line 99
19. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.headerTrace line 107

    Source documentation

    Compose the actual affine and word/copy instructions. The trace and both header values are derived; the only data premises describe the physical input.

    theorem headerTrace (input : PortTables.Table vertices d) (n : Nat) (h : n + 1 ≤ max)
        (placement : Tape max → K) (distinct : Function.Injective placement)
        (vertex : Fin vertices) (ports : Fin (n + 1) → Fin d) (direction : Bool)
        (labels : Label n → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool))
        (atLabels : ∀ l, program (labels l) = instruction n h placement ports direction labels exit l)
        (base : K → List Bool) (tableWord : base (placement (table max)) = PortTables.tableBits input)
        (scratchEmpty : base (placement (scratch max)) = []) (suffix : List Bool)
        (sourceWord : base (placement (start max)) = encodeWord vertex.val ++ suffix)
        (ambient : σ) (register : Option Bool) :
        (advance (TM2.step program))^[steps input n vertex ports direction]
          (some ⟨some (labels (entry n)), (ambient, register), base⟩) =
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.Label, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.instruction, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.steps, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.entry

20. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes_other line 179
21. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes_shared line 204

    Source documentation

    In particular, table 0, start 1, scratch 5, and saved endpoint/copy tapes 6--9 survive the header phase. Only roles 2, 3, 4, 10 and trajectory tapes may change.

    theorem finalTapes_shared (input : PortTables.Table vertices d) (n : Nat) (h : n + 1 ≤ max)
        (placement : Tape max → K) (distinct : Function.Injective placement)
        (vertex : Fin vertices) (ports : Fin (n + 1) → Fin d)
        (direction : Bool) (base : K → List Bool) (i : Fin 11)
        (hquery : i ≠ 2) (hscan : i ≠ 3) (hreverse : i ≠ 4) (houtput : i ≠ 10) :
        finalTapes input n h placement vertex ports direction base (placement (.inl i)) =
          base (placement (.inl i)) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes

22. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.steps_le line 219

    Source documentation

    Linear in the serialized input length for the fixed word length.

    theorem steps_le (input : PortTables.Table vertices d) (n : Nat) (vertex : Fin vertices)
        (ports : Fin (n + 1) → Fin d) (direction : Bool) :
        steps input n vertex ports direction ≤
          (14 * (n + 1) + 4) * (PortTables.tableBits input).length + 12 * (n + 1) + 6 := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.steps

23. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowHeaders.machine line 237

    Source documentation

    A closed finite-control instance. Embedded uses instantiate instruction on the caller's common tapes and preserve its larger ambient register.

    def machine (degree n : Nat) (ports : Fin (n + 1) → Fin degree) (direction : Bool) : FinTM2 where
    …

24. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.capacity line 257
25. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.bufferSize line 258
26. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.State line 259
27. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.commands line 261
28. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.Label line 264
29. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.planMain line 269

    Source documentation

    A finite main label also exists for an empty command list.

    def planMain {max : Nat} {E : Type}
        (ops : List (PoweringMachinePlan.Command d max)) (fallback : E) :
        PoweringMachinePlan.Label ops ⊕ E :=
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.Command, OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.Label

30. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.plan_entry_eq line 276
31. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.entry line 283
32. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement line 287

    Source documentation

    Only the header phase directs shared output role 10 to the external output.

    def headerPlacement {max : Nat} (placement : PoweringMachineTapes.Tape max → K)
        (output : K) (i : PoweringMachineTapes.Tape max) : K :=
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.Tape

33. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_output line 292
34. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_other line 297
35. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_injective line 303
36. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_excludes_data line 319
37. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.instruction line 331
38. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.afterPlan line 342
39. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.rowRelation line 346
40. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.rowWords line 351
41. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit line 356
42. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes line 363
43. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.planSteps line 371
44. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.planSteps_eq line 376
45. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.steps line 389
46. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.Ready line 394
47. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.plan_other_inline_PoweringMachineRowBody line 399
48. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_data line 412
49. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_role line 419
50. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_ready line 429
51. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_data line 451
52. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_ready line 464
53. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_other line 489
54. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.rowBlock_eq_rowRelation line 508
55. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_output line 525

    Source documentation

    The full serialized row is prepended to the caller's existing output.

    theorem finalTapes_output (graph : PortTables.Table vertices d) (n : Nat)
        (placement : PoweringMachineTapes.Tape (capacity n) → K) (distinct : Function.Injective placement)
        (output : K) (outside : ∀ i, output ≠ placement i) (vertex : Fin vertices)
        (ports : Fin (n + 1) → Fin d) (direction : Bool) (base : K → List Bool)
        (suffix : List Bool) (ready : Ready graph n placement vertex suffix base) :
        finalTapes graph n placement output vertex ports direction base output =
          encodeWords (rowWords graph n vertex ports direction) ++ base output := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.capacity, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.Ready, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.rowWords

56. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.rowTrace line 556

    Source documentation

    The complete row producer executes its concrete plan, one row transition, and the concrete two-header writer. No local execution hypothesis is assumed.

    theorem rowTrace (graph : PortTables.Table vertices d) (n : Nat)
        (placement : PoweringMachineTapes.Tape (capacity n) → K) (distinct : Function.Injective placement)
        (output : K) (outside : ∀ i, output ≠ placement i) (vertex : Fin vertices)
        (ports : Fin (n + 1) → Fin d) (direction : Bool)
        (labels : Label n ports direction → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State d n))
        (atLabels : ∀ l, program (labels l) = instruction n placement output ports direction labels exit l)
        (base : K → List Bool) (suffix : List Bool) (ready : Ready graph n placement vertex suffix base) :
        (advance (TM2.step program))^[steps graph vertex n ports direction]
          (some ⟨some (labels (entry n ports direction)), PoweringMasterState.clean (bufferSize d n), base⟩) =
          some ⟨exit, PoweringMasterState.clean (bufferSize d n),
            finalTapes graph n placement output vertex ports direction base⟩ := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.capacity, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.Label, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.State, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.instruction, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.Ready, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.steps, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.entry, OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.clean, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.bufferSize, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes

57. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.budget line 608
58. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.steps_le line 612
59. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.rowInTime line 625

    Source documentation

    The row subroutine's genuine execution certificate has the explicit fixed-parameter affine bound in the serialized graph length.

    def rowInTime (graph : PortTables.Table vertices d) (n : Nat)
        (placement : PoweringMachineTapes.Tape (capacity n) → K) (distinct : Function.Injective placement)
        (output : K) (outside : ∀ i, output ≠ placement i) (vertex : Fin vertices)
        (ports : Fin (n + 1) → Fin d) (direction : Bool)
        (labels : Label n ports direction → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State d n))
        (atLabels : ∀ l, program (labels l) = instruction n placement output ports direction labels exit l)
        (base : K → List Bool) (suffix : List Bool) (ready : Ready graph n placement vertex suffix base) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some (labels (entry n ports direction)), PoweringMasterState.clean (bufferSize d n), base⟩
          (some ⟨exit, PoweringMasterState.clean (bufferSize d n),
            finalTapes graph n placement output vertex ports direction base⟩)
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.capacity, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.Label, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.State, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.instruction, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.Ready, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.entry, OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.clean, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.bufferSize, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes