OAI/Computability/UniqueGames/PCP/Emitter.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Actual finite TM2 templates for affine unary fields and finite relation bits. Commands write in forward bit order onto a stack, so their concatenated result appears reversed in the accumulator. Every unbounded operand is read from an isolated unary tape and restored by the checked preserving transducer.

  1. inductive OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Command line 20

    Source documentation

    All varying literals are finite: one Boolean or one bounded offset.

    inductive Command (h : Nat) (σ : Type) (bound : Nat)
  | literal (word : List Bool)
  | bit (value : σ → Bool)
  | bounded (value : σ → Fin bound)
  | scaled (source : Fin h) (coefficient : Nat)
  | scaledIf (source : Fin h) (coefficient : Nat) (active : σ → Bool)
  2. inductive OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Phase line 27
  3. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Alphabet line 32
  4. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.State line 33
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.transition line 35
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.payload line 36
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.commandBits line 39
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.commandSteps line 48
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.commandStatement line 59

    Source documentation

    A literal Boolean is emitted by a real finite branch. A bounded offset is dispatched to a finite label, whose push chain has a fixed length.

    def commandStatement (sources : Fin h → K) (scratch output : K)
    (labels : Phase bound → Λ) (next : Λ) (command : Command h σ bound) :
    Phase bound → TM2.Stmt (Alphabet (K := K)) Λ (State σ)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Phase, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Command, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.State

  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.output_encodeWord line 93
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.commandTrace line 109

    Source documentation

    Exact execution of one command of the supplied actual program. The only program hypotheses are equations for its concrete finite statements.

    theorem commandTrace (sources : Fin h → K) (scratch output : K)
    (sourceScratch : ∀ i, sources i ≠ scratch)
    (sourceOutput : ∀ i, sources i ≠ output) (scratchOutput : scratch ≠ output)
    (labels : Phase bound → Λ) (next : Λ) (command : Command h σ bound)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Phase, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Command, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.program, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.State

  12. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Label line 186
  13. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.labelAt line 188
  14. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.commandAt line 191
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.statement line 195
  16. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.program line 205
  17. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.machine line 212

    Source documentation

    Bundling makes the fixed finite tape, control-label, and register sets explicit. Neither the label type nor the state type contains a natural input.

    def machine [Fintype K] [Fintype σ] {count : Nat}
    (commands : Fin count → Command h σ bound) (sources : Fin h → K)
    (scratch output input : K) (ambient : σ) : FinTM2 where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Command

  18. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.prefixBits line 225
  19. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.prefixSteps line 231
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.resultTapes line 236
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.resultTapes_output line 239
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.resultTapes_other line 243
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.prefixTrace line 249

    Source documentation

    Composition of the actual finite command traces, with preserved operand stacks available again at every command boundary.

    theorem prefixTrace {count : Nat} (commands : Fin count → Command h σ bound)
    (sources : Fin h → K) (scratch output : K)
    (sourceScratch : ∀ i, sources i ≠ scratch)
    (sourceOutput : ∀ i, sources i ≠ output) (scratchOutput : scratch ≠ output)
    (labels : Label count bound → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Command, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.State

  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.planTrace line 289

    Source documentation

    The complete callable program, including its actual final jump or halt.

    theorem planTrace {count : Nat} (commands : Fin count → Command h σ bound)
    (sources : Fin h → K) (scratch output : K)
    (sourceScratch : ∀ i, sources i ≠ scratch)
    (sourceOutput : ∀ i, sources i ≠ output) (scratchOutput : scratch ≠ output)
    (labels : Label count bound → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Command, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.State

  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.prefixSteps_le line 310
  26. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.planInTime line 330

    Source documentation

    A linear bound in the largest unary input field; plan size is fixed.

    def planInTime {count : Nat} (commands : Fin count → Command h σ bound)
    (sources : Fin h → K) (scratch output : K)
    (sourceScratch : ∀ i, sources i ≠ scratch)
    (sourceOutput : ∀ i, sources i ≠ output) (scratchOutput : scratch ≠ output)
    (labels : Label count bound → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Command, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.State

  27. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.listCommands line 351
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.prefixBits_listCommands line 354
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.bits_listCommands line 366
  30. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.affineCommands line 372
  31. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.affineValue line 376
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.scaleBits line 379
  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.affineCommands_bits line 389
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.affineCommands_length line 397
  35. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.bitCommands line 402

    Source documentation

    The finite relation table is encoded one actual Boolean branch at a time.

    def bitCommands (bits : List (σ → Bool)) : List (Command h σ bound) := bits.map .bit

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Command

  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.bitCommands_bits line 404
  37. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.affineInTime line 414

    Source documentation

    The affine template itself has an actual composable machine certificate.

    def affineInTime (terms : List (Fin h × Nat)) (offset : σ → Fin bound)
    (sources : Fin h → K) (scratch output : K)
    (sourceScratch : ∀ i, sources i ≠ scratch)
    (sourceOutput : ∀ i, sources i ≠ output) (scratchOutput : scratch ≠ output)
    (labels : Label (affineCommands terms offset).length bound → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.affineCommands, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.State

  38. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Command.mapAmbient line 439

    Source documentation

    Enlarge the finite ambient registers by reading a projection of them.

    def Command.mapAmbient {τ : Type} (view : σ → τ) :
    Command h τ bound → Command h σ bound
  | .literal word => .literal word
  | .bit value => .bit (value ∘ view)
  | .bounded value => .bounded (value ∘ view)
  | .scaled source coefficient => .scaled source coefficient
  | .scaledIf source coefficient active => .scaledIf source coefficient (active ∘ view)

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.Command

  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.commandBits_mapAmbient line 447
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.commandSteps_mapAmbient line 453