OAI/Computability/UniqueGames/PCP/SourceDescriptorEmissionLemmas.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

Emit one fixed descriptor equation from three preserved unary base registers. The output order is first address, second address, third address, RHS. The actual stack program emits those fields in reverse order.

  1. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.codedEquation line 24
  2. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.descriptorWords line 28
  3. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.descriptorBits line 31
  4. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.descriptorWords_length line 34
  5. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.descriptorBits_length_le line 38
  6. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.decode_descriptorBits line 42
  7. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.parse_descriptorWords line 46
  8. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.decode_codedEquation line 54

    Source documentation

    Decoding the finite address suffixes recovers the exact local equation, including all repeated occurrences and the Boolean correction.

    theorem decode_codedEquation (u D : ℕ) (state : LocalInput u D) :
    mapEquation (localKeyEncoding u).code.symm (codedEquation u D state) =
      SourceLocalEquation.emit u D state := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.mapEquation, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.codedEquation, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.emit

  9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.codedEquation_global line 65
  10. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.descriptorPushBound line 74
  11. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.descriptorPushBound_le line 77
  12. instance OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.localInputDecidableEq line 94

    Source documentation

    Executable state equality is obtained from the explicit radix code.

    instance localInputDecidableEq (u D : ℕ) : DecidableEq (LocalInput u D) :=
…
  13. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.emitDescriptor line 102

    Source documentation

    Concrete finite-table statement. Its state is the finite signature/tape pair; every branch leaf contains a fixed finite push chain.

    def emitDescriptor (u D : ℕ) (dst : K)
    (next : TM2.Stmt (fun _ : K => Bool) Λ (LocalInput u D)) :
    TM2.Stmt (fun _ : K => Bool) Λ (LocalInput u D) :=
…
  14. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.stepAux_emitDescriptor line 108
  15. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.emitDescriptor_push_bound line 119
  16. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.emitDescriptorInTime line 128

    Source documentation

    One actual TM2 transition emits the descriptor and enters the chosen continuation label. Only a program-definition equation is required.

    def emitDescriptorInTime (u D : ℕ) (dst : K)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (LocalInput u D))
    (label exitLabel : Λ)
    (atLabel : program label = emitDescriptor u D dst (.goto (fun _ => exitLabel)))
    (state : LocalInput u D) (tapes : K → List Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some label, state, tapes⟩
      (some ⟨some exitLabel, state,
        Function.update tapes dst (descriptorBits u D state ++ tapes dst)⟩) 1 :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.emitDescriptor, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.descriptorBits

  17. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceDescriptorEmission.descriptor_output_frame line 141
  18. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.Label line 160
  19. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.Label.enumList line 165
  20. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.Label.enumList_getElem?_ctorIdx_eq line 168
  21. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.Label.enumList_nodup line 172
  22. instance OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.(instance at line 174) line 174
  23. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.Alphabet line 178
  24. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.State line 179
  25. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.rhsBit line 181
  26. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.steps line 183
  27. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.statement line 188
  28. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.program line 211
  29. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.prefixTapes line 215
  30. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.prefixTapes_other line 218
  31. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.equationTrace line 222
  32. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.equationInTime line 293
  33. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.programInTime line 312
  34. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.Tape line 327
  35. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.machine line 329
  36. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.machineInTime line 340
  37. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceProfileBridge.positionEncoding line 358
  38. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceProfileBridge.names line 361
  39. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceProfileBridge.nameWords line 365
  40. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceProfileBridge.reindexProfile line 369
  41. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceProfileBridge.computed_profile_eq line 373
  42. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceProfileBridge.prepared_signature_eq line 381
  43. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceProfileBridge.nameWords_length_le_input line 391

    Source documentation

    Every isolated unary variable-name field is bounded by the true CNF input encoding, including formulas with unused declared variable names.

    theorem nameWords_length_le_input (F : Formula) {u : ℕ} (c : ClauseContext F u)
    (i : Fin (positionEncoding u).size) :
    (nameWords F c i).length ≤ (formulaBits F).length := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceProfileBridge.positionEncoding, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceProfileBridge.nameWords

  44. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.rank line 407
  45. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.reverseDigits line 410
  46. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.reverseDigits_apply line 413
  47. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.horner_value_sum line 417
  48. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.horner_reverse_eq_rank line 432
  49. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.reverseSlots line 452

    Source documentation

    Reverse only digit positions. All six fixed work/control roles stay put.

    def reverseSlots (slots : MachineHorner.Layout width ↪ K) : MachineHorner.Layout width ↪ K :=
…
  50. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.reverseSlots_control line 455
  51. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.reverseSlots_digit line 458
  52. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.clean_reverseSlots line 464
  53. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.statement line 471
  54. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.program line 476
  55. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.rankTrace line 482

    Source documentation

    Exact execution using existing digit fields; only the destination changes.

    theorem rankTrace (slots : MachineHorner.Layout width ↪ K)
    (labels : MachineHorner.Label width → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ label, p (labels label) = statement slots labels exit label)
    (base : K → List Bool) (radix : Nat) (digits : Fin width → Nat)
    (operandRadix : base (slots (.inl 0)) = encodeWord radix)
    (operandDigits : ∀ i, base (slots (.inr i)) = encodeWord (digits i))
    (clean : MachineHorner.Clean slots base) (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step p))^[
      MachineHorner.steps radix (reverseDigits digits) width]
      (some ⟨some (labels .start), ((ambient, ()), register), base⟩) =
      some ⟨exit, ((ambient, ()), none), MachineHorner.resultTapes slots base (rank radix digits)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.statement, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.reverseDigits, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.rank

  56. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.rankInTime line 501
  57. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.rankInPolynomialTime line 518
  58. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.variableRankInTime line 537
  59. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.clauseRankInTime line 553
  60. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.programInTime line 569
  61. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.machine line 581
  62. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.machineInTime line 592
  63. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.clauseSlots line 607

    Source documentation

    Control roles may include preserved headers and dedicated protected extras.

    def clauseSlots (controls : Fin 6 ↪ Extra) :
    MachineHorner.Layout u ↪ SourceContextLoad.Tape u Extra where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.Tape

  64. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.variableSlots line 625

    Source documentation

    Each coordinate selects its own loaded variable field, even if names repeat.

    def variableSlots (controls : Fin 6 ↪ Extra) (selected : SlotContext u) :
    MachineHorner.Layout u ↪ SourceContextLoad.Tape u Extra where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.Tape

  65. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.clauseSlots_control line 642
  66. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.clauseSlots_digit line 645
  67. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.variableSlots_control line 648
  68. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.variableSlots_digit line 651
  69. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRankPhase.selectedDigits_loaded line 655
  70. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.positions line 676

    Source documentation

    An explicit computable enumeration, without an arbitrary finite-type equivalence. Slots occur first, second, third within each clause coordinate.

    def positions (u : ℕ) : List (Position u) :=
…
  71. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.mem_positions line 679
  72. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.fillSigns line 683

    Source documentation

    The mathematical result of the individual finite sign-register writes.

    def fillSigns {u : ℕ} (values initial : Position u → Bool)
    (cells : List (Position u)) : Position u → Bool :=
…
  73. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.fillSigns_apply line 687
  74. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.fillSigns_positions line 701
  75. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.State line 709
  76. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.Alphabet line 710
  77. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.finish line 712
  78. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.peekChain line 719

    Source documentation

    Each statement reads only the head of one supplied polarity field. The other signature fields and the entire ambient-register component are copied.

    def peekChain (field : Position u → K) (exit : Option Λ) :
    List (Position u) → TM2.Stmt (Alphabet (K := K)) Λ (State u τ)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.Alphabet, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.State

  79. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.statement line 727
  80. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.readSigns line 733

    Source documentation

    The head defaults make the finite program total on malformed tapes too; the correctness theorem below supplies the actual unary-field representation.

    def readSigns (field : Position u → K) (tapes : K → List Bool) : Position u → Bool :=
…
  81. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.stepAux_peekChain line 736
  82. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.stepAux_statement line 749
  83. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.peekChain_pushBound line 756
  84. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.statement_pushBound line 764
  85. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.readSigns_of_unary line 769
  86. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.loadStep line 779

    Source documentation

    Exact actual caller-program step. Every stored field and unread suffix is preserved, as are sameName, selected, and all ambient registers.

    theorem loadStep (field : Position u → K) (entryLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State u τ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.Alphabet, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.State

  87. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.loadInTime line 790
  88. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.loaded_ofContext line 809

    Source documentation

    The actual context signature is recovered when equality and selected-slot data have already been loaded by their separate verified preparation stages.

    theorem loaded_ofContext (F : Target.Formula) (c : SourceContexts.ClauseContext F u)
    (selected : SourceContexts.SlotContext u) (initial : Signature u)
    (hnames : initial.sameName = contextNameProfile F c)
    (hselected : initial.selected = selected) :
    {initial with signs := (ofContext F c selected).signs} = ofContext F c selected := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.ClauseContext, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContexts.SlotContext

  89. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.loadContextInTime line 821