OAI/Computability/MaxCut/PCP/PoweringRowHeaderSemantics.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact tail and reverse-index fields of the actual powering-table rows. The reverse address is affine in the live starting vertex; the coefficient and offset depend only on the fixed degree, word, and orientation.

  1. def OAI.MaxCutGames.Foundations.PCP.PoweringRowHeaderSemantics.blockSize line 17
  2. def OAI.MaxCutGames.Foundations.PCP.PoweringRowHeaderSemantics.reverseOffset line 19
  3. def OAI.MaxCutGames.Foundations.PCP.PoweringRowHeaderSemantics.reverseValue line 22
  4. def OAI.MaxCutGames.Foundations.PCP.PoweringRowHeaderSemantics.tailVertex line 26
  5. def OAI.MaxCutGames.Foundations.PCP.PoweringRowHeaderSemantics.headerWords line 30
  6. theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowHeaderSemantics.table_tail line 35

    Source documentation

    The stored tail is the recorded start or endpoint according to direction.

    theorem table_tail (input : PortTables.Table vertices d) (n : Nat) (vertex : Fin vertices)
    (ports : Fin (n + 1) → Fin d) (direction : Bool) :
    (PoweringTables.table input n).rows[encodeDart vertices d n (direction, vertex, ports)].tail =
      tailVertex input n vertex ports direction := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTables.table, OAI.MaxCutGames.Foundations.PCP.PoweringRowHeaderSemantics.tailVertex

  7. theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowHeaderSemantics.table_reverseValue line 48

    Source documentation

    The reverse address retains the word and changes only its direction bit.

    theorem table_reverseValue (input : PortTables.Table vertices d) (n : Nat)
    (vertex : Fin vertices) (ports : Fin (n + 1) → Fin d) (direction : Bool) :
    (PoweringTables.table input n).rows[encodeDart vertices d n
      (direction, vertex, ports)].reverseIndex.val = reverseValue d n vertex ports direction := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTables.table, OAI.MaxCutGames.Foundations.PCP.PoweringRowHeaderSemantics.reverseValue

  8. theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowHeaderSemantics.headerWords_eq line 58
  9. theorem OAI.MaxCutGames.Foundations.PCP.PoweringRowHeaderSemantics.header_relation_bits line 70

    Source documentation

    Prepending these two fields to the existing relation yields the exact serialized row, preserving the rest of the output tape.

    theorem header_relation_bits (input : PortTables.Table vertices d) (n : Nat)
    (vertex : Fin vertices) (ports : Fin (n + 1) → Fin d) (direction : Bool)
    (suffix : List Bool) :
    encodeWords (headerWords input n vertex ports direction) ++
      (encodeWords (GenericGraphTables.relationWords
        (PoweringTables.table input n).rows[encodeDart vertices d n
          (direction, vertex, ports)].relation) ++ suffix) =
      encodeWords (GenericGraphTables.rowWords
        (PoweringTables.table input n).rows[encodeDart vertices d n
          (direction, vertex, ports)]) ++ suffix := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringRowHeaderSemantics.headerWords, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.relationWords, OAI.MaxCutGames.Foundations.PCP.PoweringTables.table, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.rowWords