OAI/Computability/MaxCut/PCP/LocalEquation.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

The actual global addresses use three input-dependent base registers. Every local query contributes only a fixed finite selector and fixed offset, so a finite control table can select a base and emit its unary offset.

  1. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.LocalKey line 12
  2. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.LocalInput line 13
  3. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.signatureEncoding line 15
  4. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.signatureList line 21
  5. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.mem_signatureList line 23
  6. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.signatureList_nodup line 26
  7. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.signatureList_length line 29
  8. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.localInputEncoding line 33
  9. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.localInputs line 36
  10. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.mem_localInputs line 38
  11. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.localInputs_nodup line 41
  12. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.localInputs_length line 44
  13. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.localKeyEncoding line 48
  14. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.emptyLocalAddress line 52
  15. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.foldedLocalAddress line 56
  16. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.equationFor line 64

    Source documentation

    One local descriptor, reusing the existing folded and empty-context equations. The first-valid search is over the fixed explicit answer encoding.

    def equationFor (u D : ℕ) (valid : J u → Bool) (π : J u → I u)
    (t : SourceTape.TestTape (I u) (J u) D) : Equation (LocalKey u) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceTape.TestTape, OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.LocalKey

  17. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.equation line 72
  18. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.emit line 76
  19. def OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.addressMap line 79
  20. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.mapEquation_comp line 85
  21. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.addressMap_emptyLocalAddress line 88
  22. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.addressMap_foldedLocalAddress line 94
  23. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.contextEquation_eq_map_equationFor line 105

    Source documentation

    A generic factorization first aligns the validity function itself, so no unproved transport of dependent anchor subtypes is needed.

    theorem contextEquation_eq_map_equationFor (F : Formula) (u D : ℕ)
    (c : ClauseContext F u) (v : VariableContext F u)
    (t : SourceTape.TestTape (I u) (J u) D) :
    contextEquation F u D c v t =
      mapEquation (addressMap F u c v) (equationFor u D (validJ F c) (pi F c v) t) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceTape.TestTape, OAI.MaxCutGames.Foundations.Hastad.mapEquation, OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.addressMap, OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.equationFor

  24. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.contextEquation_eq_map line 118
  25. theorem OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.sourceEquation_eq_map_emit line 131
  26. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceAddressDescriptors.Descriptor line 150
  27. def OAI.MaxCutGames.Foundations.Hastad.SourceAddressDescriptors.descriptor line 152
  28. def OAI.MaxCutGames.Foundations.Hastad.SourceAddressDescriptors.baseValue line 159

    Source documentation

    Registers zero and one start the selected left and right query blocks; register two is the single dummy address.

    def baseValue (F : Formula) (u : ℕ) (c : ClauseContext F u)
    (v : VariableContext F u) (side : Fin 3) : ℕ :=
…
  29. def OAI.MaxCutGames.Foundations.Hastad.SourceAddressDescriptors.realize line 166
  30. def OAI.MaxCutGames.Foundations.Hastad.SourceAddressDescriptors.words line 168
  31. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressDescriptors.realize_descriptor line 172
  32. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressDescriptors.descriptor_offset_bound line 189
  33. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressDescriptors.sourceEquation_numeric line 212
  34. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressDescriptors.sourceEquation_words line 221
  35. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressDescriptors.baseValue_lt line 230
  36. theorem OAI.MaxCutGames.Foundations.Hastad.SourceAddressDescriptors.equation_emit_steps_le line 247