OAI/Computability/UniqueGames/PCP/PoweringTableSemanticsLemmas.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Exact semantics of the executable powering tables

The explicit label and dart bijections preserve every actual edge test and every rejected directed occurrence. The inverse label map covers all encoded assignments, so satisfiability and uniform rejection-count bounds transport without any consistency restriction on padded labels.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.RawLabeling line 32
  2. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.EncodedLabeling line 35
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.encodeLabeling line 38
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.decodeLabeling line 42
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.decodeLabeling_encodeLabeling line 46
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.encodeLabeling_decodeLabeling line 52
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_encoded line 59

    Source documentation

    Each enumerated directed occurrence evaluates its actual powering test.

    theorem edgeSatisfied_encoded {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (labels : RawLabeling vertices d n)
    (e : PoweringTest.Dart (Fin vertices) (Fin d) n) :
    (GenericGraphTables.semantics (table input n)).edgeSatisfied
      (encodeLabeling d n labels) (encodeDart vertices d n e) =
        (mathematicalGraph input n).edgeSatisfied labels e := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.RawLabeling, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.Dart, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.encodeLabeling

  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_decoded line 72

    Source documentation

    The equality also holds for every encoded assignment and every stored row.

    theorem edgeSatisfied_decoded {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (labels : EncodedLabeling vertices d n) (i : Fin (dartCount vertices d n)) :
    (GenericGraphTables.semantics (table input n)).edgeSatisfied labels i =
      (mathematicalGraph input n).edgeSatisfied (decodeLabeling d n labels)
        (decodeDart vertices d n i) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.EncodedLabeling, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.decodeLabeling

  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_eq_path line 84

    Source documentation

    The stored Boolean test is exactly the path test at the recorded endpoints.

    theorem edgeSatisfied_eq_path {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (labels : EncodedLabeling vertices d n) (direction : Bool)
    (w : Walk (Fin vertices) (Fin d) (n + 1)) :
    (GenericGraphTables.semantics (table input n)).edgeSatisfied labels
      (encodeDart vertices d n (direction, w)) =
    PoweringTest.pathAccepts (PortTables.portGraph input) (PortTables.accepts input) n
      (finitePortSelector (PortTables.portGraph input) (n + 1)) w
      (decodeLabeling d n labels w.1)
      (decodeLabeling d n labels (endpoint (PortTables.portGraph input) w)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.EncodedLabeling, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.pathAccepts, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.portGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.decodeLabeling

  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.rejectionCount_encoded line 100

    Source documentation

    Exact rejected-dart counting, retaining both orientations and repeated walks.

    theorem rejectionCount_encoded {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (labels : RawLabeling vertices d n) :
    (GenericGraphTables.semantics (table input n)).rejectionCount
      (encodeLabeling d n labels) = (mathematicalGraph input n).rejectionCount labels := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.RawLabeling, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.encodeLabeling

  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.rejectionCount_decoded line 110
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.card_darts_eq_table line 119

    Source documentation

    The denominator equality comes from the same explicit dart bijection.

    theorem card_darts_eq_table {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) :
    Fintype.card (PoweringTest.Dart (Fin vertices) (Fin d) n) = (table input n).darts := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.Dart

  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.satisfiable_iff line 127

    Source documentation

    The table has a satisfying encoded assignment exactly when the powered graph does.

    theorem satisfiable_iff {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat) :
    (GenericGraphTables.semantics (table input n)).Satisfiable ↔
      (mathematicalGraph input n).Satisfiable := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics

  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.preserves_satisfiability line 145

    Source documentation

    Perfect completeness from the actual stored base predicates.

    theorem preserves_satisfiability {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (h : (PortTables.baseGraph input).Satisfiable) :
    (GenericGraphTables.semantics (table input n)).Satisfiable := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.baseGraph, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics

  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.path_rejection_mean_eq_table_fraction line 154

    Source documentation

    The path rejection average equals the encoded table's actual rejection fraction.

    theorem path_rejection_mean_eq_table_fraction {vertices d : Nat}
    (input : PortTables.Table vertices d) (n : Nat) (labels : EncodedLabeling vertices d n) :
    SpectralReturn.mean (fun w : Walk (Fin vertices) (Fin d) (n + 1) =>
      PoweringMoment.bit
        (PoweringTest.pathAccepts (PortTables.portGraph input) (PortTables.accepts input) n
          (finitePortSelector (PortTables.portGraph input) (n + 1)) w
          (decodeLabeling d n labels w.1)
          (decodeLabeling d n labels (endpoint (PortTables.portGraph input) w)) = false)) =
      ((GenericGraphTables.semantics (table input n)).rejectionCount labels : ℝ) /
        ((table input n).darts : ℝ) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.EncodedLabeling, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.bit, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.pathAccepts, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.portGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.decodeLabeling, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics

  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.uniform_count_gap_iff line 170

    Source documentation

    Uniform actual rejection-count gaps are invariant under the executable encoding.

    theorem uniform_count_gap_iff {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (epsilon : ℝ) :
    (∀ labels : EncodedLabeling vertices d n,
      epsilon * ((table input n).darts : ℝ) ≤
        ((GenericGraphTables.semantics (table input n)).rejectionCount labels : ℝ)) ↔
    (∀ labels : RawLabeling vertices d n,
      epsilon * (Fintype.card (PoweringTest.Dart (Fin vertices) (Fin d) n) : ℝ) ≤
        ((mathematicalGraph input n).rejectionCount labels : ℝ)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.EncodedLabeling, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.RawLabeling, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.Dart

  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.uniform_count_gap line 190

    Source documentation

    Apply an established powering count bound to every encoded table labeling.

    theorem uniform_count_gap {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (epsilon : ℝ)
    (hgap : ∀ labels : RawLabeling vertices d n,
      epsilon * (Fintype.card (PoweringTest.Dart (Fin vertices) (Fin d) n) : ℝ) ≤
        ((mathematicalGraph input n).rejectionCount labels : ℝ)) :
    ∀ labels : EncodedLabeling vertices d n,
      epsilon * ((table input n).darts : ℝ) ≤
        ((GenericGraphTables.semantics (table input n)).rejectionCount labels : ℝ) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.RawLabeling, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.Dart, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.EncodedLabeling, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics

  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWitness.iterate_mul_const line 218

    Source documentation

    A constant scalar passes through every iterate of the actual graph mean.

    theorem iterate_mul_const [Fintype D] (G : PortGraph V D)
    (n : Nat) (c : ℝ) (h : V → ℝ) :
    iterateOperator G n (fun x => c * h x) =
      fun x => c * iterateOperator G n h x := by
…
  19. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWitness.endpointWitness line 233

    Source documentation

    The actual pivot dart is marked and both endpoint opinions pass their tests. For indicator opinions this is the indicator of their conjunction.

    noncomputable def endpointWitness (G : PortGraph V D) (bad : Edge V D → Bool)
    (φ ψ : Edge V D → V → ℝ) (n : Nat) (k : Fin (n + 1))
    (w : Walk V D (n + 1)) : ℝ :=
…
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWitness.vertexWitness line 240

    Source documentation

    Vertex-indexed opinions are tested at the two endpoints of the pivot dart.

    noncomputable def vertexWitness (G : PortGraph V D) (bad : Edge V D → Bool)
    (f : V → V → ℝ) (n : Nat) (k : Fin (n + 1)) :
    Walk V D (n + 1) → ℝ :=
…
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWitness.endpoint_lower_bound line 247

    Source documentation

    Pointwise bounds on the two genuine earlier-length graph iterates give the witness first moment. The hypotheses are only needed on marked darts.

    theorem endpoint_lower_bound [Fintype V] [Fintype D] [Nonempty D]
    (G : PortGraph V D) (n : Nat) (k : Fin (n + 1)) (bad : Edge V D → Bool)
    (φ ψ : Edge V D → V → ℝ) (a : ℝ) (ha : 0 ≤ a)
    (hL : ∀ e, bad e = true → a ≤ iterateOperator G k.val (φ e) e.1)
    (hR : ∀ e, bad e = true →
      a ≤ iterateOperator G (n - k.val) (ψ e) (next G e.1 e.2)) :
    edgeDensity bad * a ^ 2 ≤ mean (endpointWitness G bad φ ψ n k) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWitness.endpointWitness

  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWitness.lazy_middle_witness_mean line 289

    Source documentation

    The two endpoint-opinion tests each retain probability at least 1/(2q) at every middle pivot. The walk has 2N+1 edges, with N=(4qM)^2, so the prefix and suffix lengths are exactly k and 2N-k.

    The only modal input is the actual centered lazy iterate at each vertex. It will be supplied by the finite modal-opinion decoder, not by a witness law.

    theorem lazy_middle_witness_mean [Fintype V] [Fintype D] [Nonempty D]
    (G : PortGraph V D) (q M : Nat) (hq : 1 ≤ q) (hM : 1 ≤ M)
    (k : Fin (2 * (4 * q * M) ^ 2 + 1))
    (hlo : (4 * q * M) ^ 2 - M ≤ k.val)
    (hhi : k.val ≤ (4 * q * M) ^ 2 + M)
    (bad : Edge V (Bool × D) → Bool) (f : V → V → ℝ)
    (hf : ∀ u w, f u w ∈ Set.Icc (0 : ℝ) 1)
    (hmodal : ∀ u, 1 / (q : ℝ) ≤
      iterateOperator (lazyGraph G) ((4 * q * M) ^ 2) (f u) u) :
    edgeDensity bad / (4 * (q : ℝ) ^ 2) ≤
      mean (vertexWitness (lazyGraph G) bad f (2 * (4 * q * M) ^ 2) k) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWitness.vertexWitness

  23. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.center line 336
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.le_center line 338
  25. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.gain line 346
  26. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.decodedError line 353
  27. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.poweredRejection line 358
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.witness_bit_eq line 364
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.modal_witness_mean line 377
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.rejection_lower_bound line 404

    Source documentation

    Positive decoded error forces rejection of the actual powered graph. The cap and amplification coefficient are explicit constants.

    theorem rejection_lower_bound (G : PortGraph V D) (lambda : ℝ)
    (certificate : SpectralCertificate (lazyGraph G) lambda)
    (accepts : Edge V (Bool × D) → A → A → Bool)
    (reverse_accepts : ∀ e a b, accepts ((lazyGraph G).rot e) b a = accepts e a b)
    (M : Nat) (hM : 1 ≤ M)
    (selectors : ∀ v, AddressSelector (lazyGraph G) (2 * center (Fintype.card A) M + 1) v)
    (labels : V → PaddedLabel (Bool × D) (2 * center (Fintype.card A) M + 1) A)
    (fallback : A)
    (hε : 0 < decodedError (lazyGraph G) accepts (2 * center (Fintype.card A) M)
      (center (Fintype.card A) M) selectors labels fallback) :
    gain (Fintype.card A) M lambda *
        min (decodedError (lazyGraph G) accepts (2 * center (Fintype.card A) M)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.center, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.decodedError, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.gain

  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringGap.gain_nonneg line 505
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringGap.uniform_count_gap line 514
  33. def OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.indicator line 581
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.mean_indicator line 583
  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.energy_indicator line 591
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.indicator_nonnegative line 599
  37. def OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.cut line 606
  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.cut_density_eq line 614

    Source documentation

    The normalized cut count is exactly mean minus one-step correlation.

    theorem cut_density_eq (S : Finset V) :
    ((cut G S).card : ℝ) / (Fintype.card (V × D) : ℝ) =
      mean (indicator S) - correlation (indicator S) (averagingOperator G (indicator S)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.cut, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.indicator

  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.cut_density_ge_variance line 636
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.cut_density_ge_quarter line 655
  41. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.cut_card_ge_quarter_degree line 672

    Source documentation

    The real cardinal estimate before removing denominators.

    theorem cut_card_ge_quarter_degree
    (certificate : SpectralCertificate G (1/2)) (S : Finset V)
    (hsmall : 2 * S.card ≤ Fintype.card V) :
    (Fintype.card D : ℝ) * (S.card : ℝ) / 4 ≤ ((cut G S).card : ℝ) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.cut

  42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.degree_mul_card_le_four_cut line 689
  43. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.cut_card_ge_quarter_degree_of_card_le_half line 698
  44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.cut_card_ge_twice line 707

    Source documentation

    The natural-number expansion used in cloud rounding. Empty vertex sets are included; a degree of at least eight supplies the nonempty port type.

    theorem cut_card_ge_twice (G : PortGraph V D)
    (certificate : SpectralCertificate G (1/2)) (hdegree : 8 ≤ Fintype.card D)
    (S : Finset V) (hsmall : 2 * S.card ≤ Fintype.card V) :
    2 * S.card ≤ (cut G S).card := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralCut.cut

  45. def OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.restrict line 740

    Source documentation

    The values of a full Boolean tape on the legal coordinates.

    def restrict (f : B → Bool) : {b // p b} → Bool := fun b => f b.1
…
  46. def OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.extend line 745

    Source documentation

    Extend a tape on legal coordinates by false on every other coordinate.

    def extend (g : {b // p b} → Bool) : B → Bool :=
…
  47. def OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.canonicalize line 749

    Source documentation

    Replace the values outside the legal coordinates by false.

    def canonicalize (f : B → Bool) : B → Bool := extend p (restrict p f)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.extend, OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.restrict

  48. theorem OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.restrict_apply line 752
  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.extend_apply_of_mem line 755
  50. theorem OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.extend_apply_of_not_mem line 759
  51. theorem OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.restrict_extend line 763
  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.canonicalize_apply_of_mem line 768
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.canonicalize_apply_of_not_mem line 772
  54. theorem OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.restrict_canonicalize line 776
  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.canonicalize_idempotent line 780
  56. theorem OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.canonicalize_eq_iff line 784
  57. theorem OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.expect_restrict line 795

    Source documentation

    Uniform full tapes induce exactly uniform legal-coordinate tapes.

    theorem expect_restrict (h : ({b // p b} → Bool) → ℝ) :
    (𝔼 f : B → Bool, h (restrict p f)) = 𝔼 g : {b // p b} → Bool, h g := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.restrict

  58. theorem OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.expect_canonicalize line 812

    Source documentation

    The same law after choosing the canonical full-domain oracle address.

    theorem expect_canonicalize (h : (B → Bool) → ℝ) :
    (𝔼 f : B → Bool, h (canonicalize p f)) =
      𝔼 g : {b // p b} → Bool, h (extend p g) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.canonicalize, OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.extend

  59. theorem OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.expect_restrict_pair line 818

    Source documentation

    Two independent full tapes restrict to two independent uniform legal tapes.

    theorem expect_restrict_pair (h : ({b // p b} → Bool) → ({b // p b} → Bool) → ℝ) :
    (𝔼 f : B → Bool, 𝔼 g : B → Bool, h (restrict p f) (restrict p g)) =
      𝔼 f : {b // p b} → Bool, 𝔼 g : {b // p b} → Bool, h f g := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.restrict