OAI/Computability/UniqueGames/Machines/MachineExpanderRowEmitLemmas.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Actual lookup and reversal phases of the expander row program

The Boolean phase selector chooses the first or second occurrence of the same preserving lookup. The selected word is proved to be the actual stored reverse index of the supplied graph row. All execution facts follow from the concrete program statements; no phase execution is assumed.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.emitSteps line 13

    Source documentation

    One scaled scan/restore, one bounded offset, the delimiter, and final jump.

    def emitSteps (n : Nat) : Nat := 3 * (n + 1) + 6
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.affinePlan_bits line 15
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.affinePlan_steps line 26
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.emittedWord line 34

    Source documentation

    Every tape except the accumulator is literally retained.

    def emittedWord {K : Type} [DecidableEq K]
    (target : K) (base : K → List Bool) (value : Nat) : K → List Bool :=
…
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.emittedWord_target line 38
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.emittedWord_other line 43
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.program_firstEmit line 51
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.program_secondEmit line 57
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.program_outputEmit line 63
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.firstEmitTraceAt line 75

    Source documentation

    The code premise identifies concrete statements in a caller's program; it does not assume any phase execution.

    theorem firstEmitTraceAt (positive : 0 < d) (H : Table (cloudSize d) d)
    (ports : Tape → K) (portsInjective : Function.Injective ports)
    (labels : Label d → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ d))
    (atLabels : ∀ l, target (labels l) = statement positive H ports labels exit l)
    (n : Nat) (base : K → List Bool)
    (source : base (ports .inputVertex) = encodeWord n)
    (scratch : base (ports .emitScratch) = [])
    (ambient : Ambient ρ d × Fin (degree d)) :
    (MachineComposition.advance (TM2.step target))^[emitSteps n]
      (some ⟨some (labels (.firstEmit (Emitter.labelAt 3 _ 0 .entry))),
        ((ambient, ()), none), base⟩) =
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Ambient, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.emitSteps

  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.secondEmitTraceAt line 106
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.outputEmitTraceAt line 137
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.firstEmitInTimeAt line 168
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.secondEmitInTimeAt line 186
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.outputEmitInTimeAt line 204
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.firstEmitTrace line 224
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.secondEmitTrace line 236
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.outputEmitTrace line 248
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.firstEmitInTime line 260
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.secondEmitInTime line 272
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.outputEmitInTime line 284
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel line 311
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.scanPhaseLabel line 315
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.reversePhaseLabel line 318
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupPhasePort line 321
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupPhaseAddress line 324
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupPhaseAddress_eq_rowIndex line 327
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupTape_injective line 335
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupResultTapes line 340

    Source documentation

    The exact cleaned tape state produced by either lookup.

    def lookupResultTapes (ports : Tape → K) (base : K → List Bool)
    (value : Nat) (indexSuffix : List Bool) : K → List Bool :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape

  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_index line 345
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_work line 353
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_output line 359
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_other line 366

    Source documentation

    Every tape outside the query, work, and lookup-output roles is retained.

    theorem lookupResultTapes_other (ports : Tape → K) (base : K → List Bool)
    (value : Nat) (indexSuffix : List Bool) (p : K)
    (hi : p ≠ ports .queryIndex) (hw : p ≠ ports .lookupWork)
    (ho : p ≠ ports .lookupOutput) :
    lookupResultTapes ports base value indexSuffix p = base p := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupResultTapes

  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_table line 373
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_restore line 379
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupPhaseTrace line 406

    Source documentation

    Actual first/second lookup execution on a stored graph row. The selected reverse index is obtained from rotationWords_getElem?, not a caller premise.

    theorem lookupPhaseTrace :
    (advance (TM2.step target))^[MachinePreservingLookupClean.steps
        (rotationWords G) (rowIndex v (degree d) x).val]
      (some ⟨some (labels (lookupPhaseLabel second (.run .copyFirst))),
        (ambient, register), base⟩) =
      some ⟨some (labels (scanPhaseLabel second)), (ambient, none),
        lookupResultTapes ports base (reverseIndex G (rowIndex v (degree d) x)).val
          indexSuffix⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePreservingLookupClean.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.scanPhaseLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupResultTapes

  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupPhaseInTime line 430

    Source documentation

    A linear bound in the original encoded table length for the same actual phase. This includes the copy, restore, lookup, and residual cleanup.

    def lookupPhaseInTime :
    StateTransition.EvalsToInTime (TM2.step target)
      ⟨some (labels (lookupPhaseLabel second (.run .copyFirst))),
        (ambient, register), base⟩
      (some ⟨some (labels (scanPhaseLabel second)), (ambient, none),
        lookupResultTapes ports base (reverseIndex G (rowIndex v (degree d) x)).val
          indexSuffix⟩)
      (6 * (encodeWords (rotationWords G)).length + 4) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.scanPhaseLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupResultTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.reversePhaseTrace line 458

    Source documentation

    The reversal consumes the reverse query word and prepends its forward encoding to the index tape, retaining every other tape and finite state.

    theorem reversePhaseTrace :
    (advance (TM2.step target))^[(base (ports .queryReverse)).length + 1]
      (some ⟨some (labels (reversePhaseLabel second)), (ambient, register), base⟩) =
      some ⟨some (labels (lookupPhaseLabel second (.run .copyFirst))), (ambient, none),
        Reduction.MachineTransfer.tapesAt (ports .queryReverse) (ports .queryIndex) base []
          ((base (ports .queryReverse)).reverse ++ base (ports .queryIndex))⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.reversePhaseLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.tapesAt

  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.reversePhaseInTime line 474
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.reversePhaseTrace_unary line 488

    Source documentation

    Reversing an actual emitted unary field takes exactly index + 2 steps. This includes consuming the field's delimiter and leaving the reversal loop.

    theorem reversePhaseTrace_unary (index : Nat) (suffix : List Bool)
    (queryWord : base (ports .queryReverse) = (encodeWord index).reverse)
    (indexWord : base (ports .queryIndex) = suffix) :
    (advance (TM2.step target))^[index + 2]
      (some ⟨some (labels (reversePhaseLabel second)), (ambient, register), base⟩) =
      some ⟨some (labels (lookupPhaseLabel second (.run .copyFirst))), (ambient, none),
        Reduction.MachineTransfer.tapesAt (ports .queryReverse) (ports .queryIndex) base []
          (encodeWord index ++ suffix)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.reversePhaseLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.tapesAt