OAI/Computability/UniqueGames/PCP/SourceHonestLemmas.lean

GitHub source file

82 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. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.taggedAssignment line 18

    Source documentation

    Padded query tables are evaluated at one coordinate per context. Left and right tables have disjoint tags, and the unused dummy bit is fixed to false.

    def taggedAssignment {V C I J : Type} (left : V → I) (right : C → J) :
    (V × Cube I) ⊕ ((C × Cube J) ⊕ Unit) → Bool
  | .inl (v, f) => f (left v)
  | .inr (.inl (c, g)) => g (right c)
  | .inr (.inr _) => false

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube

  2. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.taggedAssignment_left line 24
  3. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.taggedAssignment_right line 28
  4. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.taggedAssignment_right_restriction line 34

    Source documentation

    Extending a conditioned half-table into padded ambient storage does not change its honest bit. Only correctness on valid coordinates is required.

    theorem taggedAssignment_right_restriction {V C I J : Type}
    (left : V → I) (right : C → J) (c : C) (valid : J → Bool)
    (honest : {j : J // valid j = true}) (hright : right c = honest.val)
    (extend : Cube {j : J // valid j = true} → Cube J)
    (hextend : ∀ (g : Cube {j : J // valid j = true})
      (j : {j : J // valid j = true}), extend g j.val = g j)
    (j₀ : {j : J // valid j = true}) (h : HalfCube j₀) :
    taggedAssignment left right (.inr (.inl (c, extend h.val))) = h.val honest := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.HalfCube, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.taggedAssignment

  5. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.conditioned_equation_honest_satisfied line 53

    Source documentation

    Each honest emitted equation fails exactly when its selected noise bit is true. This is a pointwise statement, before averaging any random tape.

    theorem conditioned_equation_honest_satisfied
    (valid : J → Bool) (π : J → I) (i₀ i : I)
    (j₀ j : {j : J // valid j = true}) (hπ : π j.val = i)
    (f : Cube I) (g μ : Cube J) :
    satisfied (FoldedEquation.conditionedEquation valid π i₀ j₀ f g μ)
        (FoldedEquation.storedAssignment (fun h => h.val i) (fun h => h.val j)) =
      !(μ j.val) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.conditionedEquation, OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.storedAssignment

  6. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.mapped_conditioned_equation_honest_satisfied line 67

    Source documentation

    Local table equalities are enough to reuse the same assignment even when different occurrences, contexts, or query positions name the same proof bit.

    theorem mapped_conditioned_equation_honest_satisfied {Name : Type}
    (valid : J → Bool) (π : J → I) (i₀ i : I)
    (j₀ j : {j : J // valid j = true}) (hπ : π j.val = i)
    (rename : FoldedEquation.Address i₀ j₀ → Name) (assignment : Name → Bool)
    (hleft : ∀ h, assignment (rename (.inl h)) = h.val i)
    (hright : ∀ h, assignment (rename (.inr h)) = h.val j)
    (f : Cube I) (g μ : Cube J) :
    satisfied (mapEquation rename
        (FoldedEquation.conditionedEquation valid π i₀ j₀ f g μ)) assignment =
      !(μ j.val) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.Address, OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.mapEquation, OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.conditionedEquation

  7. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.tapeAcceptance_conditioned_dictators line 88

    Source documentation

    The exact finite noise law gives honest acceptance for a conditioned right table and an unconditioned left table, with arbitrary fixed folding bases.

    theorem tapeAcceptance_conditioned_dictators {D : ℕ} (positive : 0 < D)
    (valid : J → Bool) (π : J → I) (i₀ i : I)
    (j₀ j : {j : J // valid j = true}) (hπ : π j.val = i) :
    SourceTape.tapeAcceptance D π
      (foldedAnswer i₀ (fun h => h.val i))
      (conditionedFoldedAnswer valid j₀ (fun h => h.val j)) =
        1 - (D : ℝ)⁻¹ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.tapeAcceptance, OAI.UniqueGamesTheorem.Foundations.Hastad.foldedAnswer, OAI.UniqueGamesTheorem.Foundations.Hastad.conditionedFoldedAnswer

  8. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.numbered_assignment_restriction line 108

    Source documentation

    Numbering the global proof and then restricting it to one local table recovers exactly the local honest half-tables.

    theorem numbered_assignment_restriction
    (vE : Encoding V) (cE : Encoding C) (iE : Encoding I) (jE : Encoding J)
    (left : V → I) (right : C → J) (v : V) (c : C)
    (valid : J → Bool) (i₀ : I) (j₀ j : {j : J // valid j = true})
    (hright : right c = j.val) :
    assignmentOfKey vE cE iE jE (taggedAssignment left right) ∘
      localAddress vE cE iE jE v c valid i₀ j₀ =
      FoldedEquation.storedAssignment (fun h => h.val (left v)) (fun h => h.val j) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.taggedAssignment, OAI.UniqueGamesTheorem.Foundations.Hastad.FoldedEquation.storedAssignment

  9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.conditionedOccurrence_honest_satisfied line 131

    Source documentation

    The globally numbered honest proof satisfies each actual occurrence precisely when the corresponding noise bit is false.

    theorem conditionedOccurrence_honest_satisfied
    (vE : Encoding V) (cE : Encoding C) (iE : Encoding I) (jE : Encoding J)
    (left : V → I) (right : C → J) (v : V) (c : C)
    (valid : J → Bool) (π : J → I) (i₀ : I)
    (j₀ j : {j : J // valid j = true})
    (hright : right c = j.val) (hπ : π j.val = left v)
    (f : Cube I) (g μ : Cube J) :
    satisfied (conditionedOccurrence vE cE iE jE v c valid π i₀ j₀ f g μ)
      (assignmentOfKey vE cE iE jE (taggedAssignment left right)) = !(μ j.val) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.taggedAssignment

  10. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.conditionedOccurrenceList_honest_acceptance line 146

    Source documentation

    Exact normalized accepted count for the actual ordered random-tape list at one incidence context. Equal equations remain separate occurrences.

    theorem conditionedOccurrenceList_honest_acceptance {D : ℕ} (positive : 0 < D)
    (vE : Encoding V) (cE : Encoding C) (iE : Encoding I) (jE : Encoding J)
    (left : V → I) (right : C → J) (v : V) (c : C)
    (valid : J → Bool) (π : J → I) (i₀ : I)
    (j₀ j : {j : J // valid j = true})
    (hright : right c = j.val) (hπ : π j.val = left v)
    (tape : Encoding (SourceTape.TestTape I J D)) :
    let equations := occurrenceList tape (fun t =>
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.TestTape

  11. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.honestGlobal line 180

    Source documentation

    A single assignment to the globally tagged padded tables. It is defined from the input assignment alone, before any incidence or test is sampled.

    def honestGlobal (F : Target.Formula) (u : ℕ)
    (assignment : Fin F.variables → Bool) :
    (VariableContext F u × Cube (I u)) ⊕
      ((ClauseContext F u × Cube (J u)) ⊕ Unit) → Bool :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.Cube

  12. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.honestBits line 187

    Source documentation

    The same global proof in the construction's explicit radix numbering.

    def honestBits (F : Target.Formula) (u : ℕ)
    (assignment : Fin F.variables → Bool) : Fin (nBits F u) → Bool :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula

  13. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.honestBits_code line 192
  14. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.honestBits_dummy line 200
  15. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.honestValidJ line 208

    Source documentation

    Satisfiability supplies one consistent valid right coordinate in every clause tuple, including tuples with repeated clauses or variable names.

    def honestValidJ (F : Target.Formula) {u : ℕ} (c : ClauseContext F u)
    (assignment : Fin F.variables → Bool)
    (hs : ∀ clause ∈ F.clauses, clause.eval assignment = true) :
    {j : J u // validJ F c j = true} :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula

  16. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.validJ_nonempty_of_satisfying line 214
  17. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.leftResponse_honest line 220
  18. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.rightResponse_honest line 228
  19. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.context_tapeAcceptance line 253

    Source documentation

    Actual sampled incidence contexts attain the same honest finite-noise acceptance. Folding bases may be chosen independently of the assignment.

    theorem context_tapeAcceptance {D : ℕ} (positive : 0 < D)
    (F : Target.Formula) {u : ℕ} (c : ClauseContext F u) (s : SlotContext u)
    (assignment : Fin F.variables → Bool)
    (hs : ∀ clause ∈ F.clauses, clause.eval assignment = true)
    (i₀ : I u) (j₀ : {j : J u // validJ F c j = true}) :
    SourceTape.tapeAcceptance D (pi F c (sampledVariables F c s))
      (foldedAnswer i₀ (fun h => h.val (honestI F (sampledVariables F c s) assignment)))
      (conditionedFoldedAnswer (validJ F c) j₀
        (fun h => h.val (honestValidJ F c assignment hs))) =
      1 - (D : ℝ)⁻¹ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.tapeAcceptance, OAI.UniqueGamesTheorem.Foundations.Hastad.foldedAnswer, OAI.UniqueGamesTheorem.Foundations.Hastad.conditionedFoldedAnswer, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.honestValidJ

  20. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.sourceEquation_honest_satisfied line 269

    Source documentation

    The emitted equation, under the one global honest assignment, reads the noise coordinate corresponding to the honest tuple of clause answers.

    theorem sourceEquation_honest_satisfied (F : Target.Formula) (u D : ℕ)
    (assignment : Fin F.variables → Bool)
    (hs : ∀ clause ∈ F.clauses, clause.eval assignment = true)
    (p : SourceIndex F u D) :
    satisfied (sourceEquation F u D p) (honestBits F u assignment) =
      !(realizedNoise p.2.2.1 (honestJ F p.1.1 assignment)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.honestBits

  21. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.rawSourceList_honest_acceptance line 281

    Source documentation

    Every actual occurrence is counted, even when its visible context, equation, or one of its three addresses repeats.

    theorem rawSourceList_honest_acceptance (F : Target.Formula) (u D : ℕ)
    (hD : 0 < D) (hF : F.clauses ≠ [])
    (assignment : Fin F.variables → Bool)
    (hs : ∀ clause ∈ F.clauses, clause.eval assignment = true) :
    ((rawSourceList F u D).countP
      (fun e => satisfied e (honestBits F u assignment)) : ℝ) /
        (rawSourceList F u D).length = 1 - (D : ℝ)⁻¹ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.honestBits

  22. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty line 300
  23. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance line 310
  24. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_rat line 325

    Source documentation

    Rational acceptance form used by the finite reduction interface.

    theorem sourceList_honest_acceptance_rat (F : Target.Formula) (u D : ℕ)
    (hD : 0 < D) (assignment : Fin F.variables → Bool)
    (hs : ∀ clause ∈ F.clauses, clause.eval assignment = true) :
    1 - (D : ℚ)⁻¹ ≤ ((sourceList F u D).countP
      (fun e => satisfied e (honestBits F u assignment)) : ℚ) /
        (sourceList F u D).length := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.honestBits

  25. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty_rat line 335
  26. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.LocalKey line 354
  27. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.LocalInput line 355
  28. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.signatureEncoding line 357
  29. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.signatureList line 363
  30. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.mem_signatureList line 365
  31. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.signatureList_nodup line 368
  32. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.signatureList_length line 371
  33. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.localInputEncoding line 375
  34. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.localInputs line 378
  35. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.mem_localInputs line 380
  36. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.localInputs_nodup line 383
  37. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.localInputs_length line 386
  38. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.localKeyEncoding line 390
  39. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.emptyLocalAddress line 394
  40. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.foldedLocalAddress line 398
  41. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.equationFor line 406

    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.UniqueGamesTheorem.Foundations.Hastad.SourceTape.TestTape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.LocalKey

  42. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.equation line 414
  43. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.emit line 418
  44. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.addressMap line 421
  45. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.mapEquation_comp line 427
  46. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.addressMap_emptyLocalAddress line 430
  47. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.addressMap_foldedLocalAddress line 436
  48. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.contextEquation_eq_map_equationFor line 447

    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.UniqueGamesTheorem.Foundations.Hastad.SourceTape.TestTape, OAI.UniqueGamesTheorem.Foundations.Hastad.mapEquation, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.addressMap, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.equationFor

  49. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.contextEquation_eq_map line 460
  50. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLocalEquation.sourceEquation_eq_map_emit line 473
  51. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressDescriptors.Descriptor line 492
  52. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressDescriptors.descriptor line 494
  53. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressDescriptors.baseValue line 501

    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) : ℕ :=
…
  54. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressDescriptors.realize line 508
  55. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressDescriptors.words line 510
  56. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressDescriptors.realize_descriptor line 514
  57. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressDescriptors.descriptor_offset_bound line 531
  58. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressDescriptors.sourceEquation_numeric line 554
  59. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressDescriptors.sourceEquation_words line 563
  60. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressDescriptors.baseValue_lt line 572
  61. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceAddressDescriptors.equation_emit_steps_le line 589
  62. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.Label line 611
  63. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.Layout line 617
  64. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.digits line 619
  65. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.horner_value line 622
  66. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.steps line 626
  67. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.operandLength line 629
  68. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.timePolynomial line 632
  69. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.timePolynomial_eval line 636
  70. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.steps_le_timePolynomial line 641
  71. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.statement line 658
  72. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.program line 666
  73. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.coefficientTapes line 670
  74. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.affineTrace line 674

    Source documentation

    Exact affine execution, including coefficient initialization and cleanup.

    theorem affineTrace (slots : Layout ↪ K) (coefficient : Nat) (labels : Label → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ label, p (labels label) = statement slots coefficient labels exit label)
    (base : K → List Bool) (rank offset : Nat)
    (rankWord : base (slots (.inl 0)) = encodeWord rank)
    (offsetWord : base (slots (.inr 1)) = encodeWord offset)
    (coefficientEmpty : base (slots (.inr 0)) = [])
    (clean : MachineHorner.Clean slots base) (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step p))^[steps coefficient rank offset]
      (some ⟨some (labels .seed), ((ambient, ()), register), base⟩) =
      some ⟨exit, ((ambient, ()), none),
        MachineHorner.resultTapes slots base (coefficient * rank + offset)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.Layout, OAI.UniqueGamesTheorem.Foundations.Hastad.coefficient, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.statement, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.steps

  75. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.affineInTime line 742
  76. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.affineInPolynomialTime line 759
  77. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.programInTime line 776
  78. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.leftBaseInTime line 789

    Source documentation

    Left query-block base from the preserved variable tuple rank and a zero offset field.

    def leftBaseInTime (F : Formula) (u : Nat) (c : ClauseContext F u) (v : VariableContext F u)
    (slots : Layout ↪ K) (labels : Label → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ label, p (labels label) = statement slots (2 ^ (2 ^ u)) labels exit label)
    (base : K → List Bool)
    (rankWord : base (slots (.inl 0)) = encodeWord (((variableEncoding F u).code v).val))
    (zeroWord : base (slots (.inr 1)) = encodeWord 0)
    (coefficientEmpty : base (slots (.inr 0)) = [])
    (clean : MachineHorner.Clean slots base) (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step p)
      ⟨some (labels .seed), ((ambient, ()), register), base⟩
      (some ⟨exit, ((ambient, ()), none), MachineHorner.resultTapes slots base (baseValue F u c v 0)⟩)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.Layout, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.statement

  79. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.rightBaseInTime line 809

    Source documentation

    Right query-block base using the globally retained left-block size.

    def rightBaseInTime (F : Formula) (u : Nat) (c : ClauseContext F u) (v : VariableContext F u)
    (slots : Layout ↪ K) (labels : Label → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
    (atLabels : ∀ label, p (labels label) = statement slots (2 ^ (8 ^ u)) labels exit label)
    (base : K → List Bool)
    (rankWord : base (slots (.inl 0)) = encodeWord (((clauseEncoding F u).code c).val))
    (leftBlockWord : base (slots (.inr 1)) = encodeWord (2 ^ (2 ^ u) * F.variables ^ u))
    (coefficientEmpty : base (slots (.inr 0)) = [])
    (clean : MachineHorner.Clean slots base) (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step p)
      ⟨some (labels .seed), ((ambient, ()), register), base⟩
      (some ⟨exit, ((ambient, ()), none), MachineHorner.resultTapes slots base (baseValue F u c v 1)⟩)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.Layout, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.statement

  80. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.resultTapes_dummy line 832

    Source documentation

    The retained dummy register is among the unchanged external tapes.

    theorem resultTapes_dummy (slots : Layout ↪ K) (base : K → List Bool) (value : Nat)
    (dummy : K) (distinct : dummy ≠ slots (.inl 3)) :
    MachineHorner.resultTapes slots base value dummy = base dummy :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.Layout

  81. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.machine line 837
  82. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceBasePhase.machineInTime line 848