OAI/Computability/MaxCut/Machines/PoweringMachineRelation.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

A concrete relation-field producer: execute a fixed word from the live start vertex, then read the predicate at the reached vertex and fixed port. All instructions use the shared tape layout and preserve the finite row buffer. No execution premise is supplied by the caller.

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelation.Alphabet line 15
  2. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelation.address line 17
  3. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelation.value line 20
  4. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelation.selected line 24
  5. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelation.instruction line 36
  6. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelation.relationTrace line 43

    Source documentation

    Actual predicate access, with serialization selection discharged.

    theorem relationTrace (source : K) (tape : Fin 5 → K)
    (distinct : Function.Injective tape) (outside : ∀ i, source ≠ tape i)
    (port : Fin d) (position : Fin 4096)
    (labels : MachineAffineLookup.Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

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

  7. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelation.steps_le line 63
  8. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelation.value_eq_accepts line 74

    Source documentation

    The semantic two-label predicate is the field used by the row producer.

    theorem value_eq_accepts (table : PortTables.Table n d) (vertex : Fin n) (port : Fin d)
    (left right : PortTables.Label) :
    value table vertex port (GraphTables.relationIndex (left, right)) =
      GraphTables.bitWord (PortTables.accepts table (vertex, port) left right) := rfl

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelation.value

  9. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelation.machine line 79
  10. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.Alphabet line 98
  11. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.State line 99
  12. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.Label line 100
  13. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.lookupTapes line 102
  14. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.lookupTapes_injective line 106
  15. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.source_outside_lookup line 112
  16. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.endpoint line 122
  17. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.endpoint_eq_wordEnd line 125
  18. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.bit line 132
  19. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.instruction line 136
  20. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.afterWord line 145
  21. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes line 151
  22. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.steps line 159
  23. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.afterWord_frame line 165
  24. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes_frame line 182

    Source documentation

    Table, start, scratch and both comparison stacks satisfy these numerical inequalities, so their contents are preserved without an emptiness premise.

    theorem finalTapes_frame (placement : PoweringMachineTapes.Tape max → K) (distinct : Function.Injective placement)
    (path : List (Fin d)) (lengthBound : path.length ≤ max)
    (port : Fin d) (left right : PortTables.Label)
    (table : PortTables.Table n d) (vertex : Fin n) (base : K → List Bool)
    (role : Fin 11) (h₂ : role ≠ 2) (h₃ : role ≠ 3) (h₄ : role ≠ 4)
    (h₆ : role ≠ 6) (h₁₀ : role ≠ 10) :
    finalTapes placement path lengthBound port left right table vertex base (placement (.inl role)) =
      base (placement (.inl role)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes

  25. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes_other line 201

    Source documentation

    Any caller tape outside the shared placement is preserved, including a separate accumulator for already completed output rows.

    theorem finalTapes_other (placement : PoweringMachineTapes.Tape max → K)
    (path : List (Fin d)) (lengthBound : path.length ≤ max)
    (port : Fin d) (left right : PortTables.Label)
    (table : PortTables.Table n d) (vertex : Fin n) (base : K → List Bool)
    (k : K) (outside : ∀ i, k ≠ placement i) :
    finalTapes placement path lengthBound port left right table vertex base k = base k := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes

  26. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.fieldTrace line 214
  27. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRelationField.steps_le line 271
  28. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.Alphabet line 305
  29. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.Tape line 306
  30. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.State line 307
  31. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.Label line 308
  32. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.entry line 311
  33. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.instruction line 313
  34. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.endpoint line 329
  35. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.resultBit line 333
  36. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes line 337
  37. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes line 343
  38. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.steps line 353
  39. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.steps_le line 360
  40. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes_other line 378

    Source documentation

    The only variable-size work areas changed by a word are the declared query, scan, reverse, selected endpoint, and trajectory tapes.

    theorem wordTapes_other (graph : PortTables.Table n d) {t : Nat} (h : t ≤ max)
    (placement : Tape max → K) (target : Bool) (vertex : Fin n)
    (ports : Fin t → Fin d) (base : K → List Bool) (k : K)
    (hquery : k ≠ placement (.inl 2)) (hscan : k ≠ placement (.inl 3))
    (hreverse : k ≠ placement (.inl 4))
    (houtput : k ≠ placement (PoweringMachineTapes.endpoint max target))
    (hpositions : ∀ i : Fin max, k ≠ placement (.inr i)) :
    wordTapes graph h placement target vertex ports base k = base k := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.Tape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.endpoint, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes

  41. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes_role line 398
  42. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_other line 419
  43. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_role line 435

    Source documentation

    This single statement covers table 0, start 1, scratch 5, and copies 8/9.

    theorem finalTapes_role (graph : PortTables.Table n d) (hl : l ≤ max) (hr : r ≤ max)
    (placement : Tape max → K) (distinct : Function.Injective placement) (vertex : Fin n)
    (left : Fin l → Fin d) (right : Fin r → Fin d) (base : K → List Bool)
    (j : Fin 11) (hrole : j = 0 ∨ j = 1 ∨ j = 5 ∨ j = 8 ∨ j = 9) :
    finalTapes graph hl hr placement vertex left right base (placement (.inl j)) =
      base (placement (.inl j)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.Tape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes

  44. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_output line 446
  45. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.joinTrace_inline_PoweringMachineEqualityField line 459
  46. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.fieldTrace line 463
  47. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.fieldInTime line 565
  48. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineEqualityField.machine line 588