OAI/Computability/UniqueGames/Machines/PoweringMachineRow.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Finite tape program for a powered relation row

The radius, address count, and powered alphabet size are fixed machine parameters. The machine consumes live base predicate bits and endpoint-match bits. Its finite register selects the first matching address, looks up the two fixed powered labels, and conjoins the bounded list of base predicates.

Both input and output bits use the graph-table unary natural-word codec. The theorems below describe actual TM2 transitions, not assumed execution costs. Producing this input block from live graph rotor lookups is a separate frontend composition obligation; no graph table occurs in the machine's finite transition function.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.Field line 29
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.inputSize line 31
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.fieldEquiv line 33
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.inputEquiv line 37
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.packData line 41

    Source documentation

    Proof-level organization of exactly the finite bits physically read.

    def packData {t S : Nat} (data : Fin t → Field S → Bool) : Buffer (inputSize t S) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.Field, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.inputSize

  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.packData_inputEquiv line 44
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.basePredicate line 49
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.leftMatches line 53
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.rightMatches line 57
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.firstMatch line 62

    Source documentation

    The scan order is the fixed increasing finite-index order.

    def firstMatch {S : Nat} (mask : Fin S → Bool) : Option (Fin S) :=
…
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.firstMatch_spec line 65
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.firstMatch_none line 72
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.edgeAccept line 78

    Source documentation

    labelAt is a fixed finite lookup table determined by the reduction parameters, for example decodeLabel a (allAddresses.get i).

    def edgeAccept {t S q : Nat} (labelAt : Fin q → Fin S → GraphTables.Label)
    (bits : Buffer (inputSize t S)) (k : Fin t) (a b : Fin q) : Bool :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.inputSize

  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.edgeAccept_of_matches line 84
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.rowAccept line 92
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.rowAccept_eq_true line 96
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.rowBlock line 103

    Source documentation

    Every powered-label pair is written in the canonical row-major order.

    def rowBlock {t S q : Nat} (labelAt : Fin q → Fin S → GraphTables.Label)
    (bits : Buffer (inputSize t S)) : Buffer (q * q) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.inputSize

  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.rowBlock_at line 109
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.encodeBit line 116
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.encodeBits line 118
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.encodeBits_append line 122
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.encodeBits_graphWords line 128
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.encodeBits_length_le line 135
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.readEncodedSlots line 149

    Source documentation

    Read one zero-delimited unary Boolean field for each fixed register slot. The second pop occurs exactly when the value is one.

    def readEncodedSlots (src : K) : List (Fin N) →
    TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N) →
    TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N)
  | [], next => next
  | i :: slots, next =>
      .pop src (fun state head =>
        (state.1, Function.update state.2 i (head.getD false)))
        (.branch (fun state => state.2 i)
          (.pop src (fun state _ => state) (readEncodedSlots src slots next))
          (readEncodedSlots src slots next))

variable [DecidableEq K]
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.stepAux_readEncodedSlots line 162
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.stepAux_readEncodedAll line 181
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.statementPushBound_readEncodedSlots line 197
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.writeEncodedSlots line 207

    Source documentation

    The delimiter is pushed first, then the optional unary one; writing slots in reverse order gives the canonical field order on the destination stack.

    def writeEncodedSlots {M : Nat} (dst : K) (emit : σ → Buffer M) : List (Fin M) →
    TM2.Stmt (fun _ : K => Bool) Λ σ → TM2.Stmt (fun _ : K => Bool) Λ σ
  | [], next => next
  | i :: slots, next => .push dst (fun _ => false)
      (.branch (fun state => emit state i)
        (.push dst (fun _ => true) (writeEncodedSlots dst emit slots next))
        (writeEncodedSlots dst emit slots next))
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.stepAux_writeEncodedSlots line 215
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.statementPushBound_writeEncodedSlots line 232
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.encodedBlockStmt line 249
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.encodedBlockAt line 256
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.statementPushBound_encodedBlockAt line 260
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.stepAux_encodedBlockStmt line 269
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.stepAux_encodedBlockAt line 284
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.step_encodedBlockAt line 295
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.rowAt line 312
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.machine line 317
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.machine_statementPushBound line 328
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.machineInTime line 336

    Source documentation

    The input predicate/match block is consumed. The exact unary predicate row is prepended; the remaining input, old output, and ambient register are accounted for in the actual transition witness.

    def machineInTime {t S q : Nat} (labelAt : Fin q → Fin S → GraphTables.Label)
    (bits : Buffer (inputSize t S)) (suffix : List Bool)
    (register : Buffer (inputSize t S)) (tapes : Bool → List Bool)
    (hinput : tapes false = encodeBits (List.ofFn bits) ++ suffix) :
    StateTransition.EvalsToInTime (machine (t := t) labelAt).step
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.inputSize, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.encodeBits, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.machine