OAI/Computability/MaxCut/PCP/PoweringDecoding.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Modal decoding is an actual maximum of finite empirical letter masses. Its reciprocal-alphabet lower bound is derived from their total mass one.

  1. def OAI.MaxCutGames.Foundations.PCP.PoweringDecoding.mass line 15
  2. theorem OAI.MaxCutGames.Foundations.PCP.PoweringDecoding.mass_sum line 20
  3. theorem OAI.MaxCutGames.Foundations.PCP.PoweringDecoding.exists_mode line 35
  4. def OAI.MaxCutGames.Foundations.PCP.PoweringDecoding.mode line 41
  5. theorem OAI.MaxCutGames.Foundations.PCP.PoweringDecoding.mode_max line 44
  6. theorem OAI.MaxCutGames.Foundations.PCP.PoweringDecoding.mode_mass_lower line 48
  7. theorem OAI.MaxCutGames.Foundations.PCP.PoweringDecoding.exists_letter_mass_lower line 59
  8. def OAI.MaxCutGames.Foundations.PCP.PoweringMoment.bit line 75
  9. def OAI.MaxCutGames.Foundations.PCP.PoweringMoment.hits line 79
  10. def OAI.MaxCutGames.Foundations.PCP.PoweringMoment.mean line 82
  11. theorem OAI.MaxCutGames.Foundations.PCP.PoweringMoment.bit_nonneg line 84
  12. theorem OAI.MaxCutGames.Foundations.PCP.PoweringMoment.bit_sq line 88
  13. theorem OAI.MaxCutGames.Foundations.PCP.PoweringMoment.bit_mul line 92
  14. theorem OAI.MaxCutGames.Foundations.PCP.PoweringMoment.bit_mono line 96
  15. theorem OAI.MaxCutGames.Foundations.PCP.PoweringMoment.hits_nonneg line 104
  16. theorem OAI.MaxCutGames.Foundations.PCP.PoweringMoment.mean_nonneg line 107
  17. theorem OAI.MaxCutGames.Foundations.PCP.PoweringMoment.mean_hits line 110
  18. theorem OAI.MaxCutGames.Foundations.PCP.PoweringMoment.second_moment_eq line 114
  19. theorem OAI.MaxCutGames.Foundations.PCP.PoweringMoment.mean_witness_sq_le line 122
  20. theorem OAI.MaxCutGames.Foundations.PCP.PoweringMoment.rejection_lower_bound line 154
  21. def OAI.MaxCutGames.Foundations.PCP.PoweringReturn.portConsEquiv line 184
  22. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.mean_word_cons_head line 197
  23. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.mean_word_cons_tail line 205
  24. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.iterateOperator_succ_right line 213
  25. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.mean_wordEnd line 220
  26. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.mean_pivot_endpoints line 242

    Source documentation

    Conditional endpoint factorization at an arbitrary fixed pivot dart.

    theorem mean_pivot_endpoints [Fintype D] [Nonempty D] (G : PortGraph V D) :
    ∀ (n : Nat) (k : Fin (n + 1)) (e : Edge V D) (φ ψ : V → ℝ),
      mean (fun r : Fin n → D =>
        φ (leftFromPivot G n k e.1 r) * ψ (rightFromPivot G n k e r)) =
        iterateOperator G k.val φ e.1 *
          iterateOperator G (n - k.val) ψ (next G e.1 e.2) := by
…
  27. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.mean_edge_endpoints line 285

    Source documentation

    The pivot and both endpoint opinions are averaged over actual walks.

    theorem mean_edge_endpoints [Fintype V] [Fintype D] [Nonempty D]
    (G : PortGraph V D) (n : Nat) (k : Fin (n + 1)) (φ ψ : Edge V D → V → ℝ) :
    mean (fun w : Walk V D (n + 1) =>
      φ (edgeAt G n w k) w.1 * ψ (edgeAt G n w k) (endpoint G w)) =
      mean (fun e : Edge V D =>
        iterateOperator G k.val (φ e) e.1 *
          iterateOperator G (n - k.val) (ψ e) (next G e.1 e.2)) := by
…
  28. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.bit_bool line 309
  29. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.mean_edge_bit line 312
  30. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.mean_marked_bit line 316
  31. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.edgeAt_zero line 326
  32. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.word_first_hit_mean line 330
  33. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.word_hit_mean line 341
  34. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.word_pair_hit_mean line 368
  35. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.hit_mean line 426
  36. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.pair_hit_mean line 442
  37. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReturn.pair_event_mean line 463
  38. def OAI.MaxCutGames.Foundations.PCP.PoweringOpinions.opinionAt line 487

    Source documentation

    Outside the full-radius neighborhood a fixed fallback makes the opinion function total. Actual tested path vertices will be certified inside it.

    def opinionAt (G : PortGraph V D) (t : Nat)
    (selectors : ∀ v, AddressSelector G t v) (labels : V → PaddedLabel D t A)
    (fallback : A) (u v : V) : A := by
…
  39. theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinions.opinionAt_eq_decode line 494
  40. def OAI.MaxCutGames.Foundations.PCP.PoweringOpinions.honestLabels line 502
  41. theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinions.opinionAt_honest line 505
  42. def OAI.MaxCutGames.Foundations.PCP.PoweringOpinions.sampleOpinion line 515
  43. def OAI.MaxCutGames.Foundations.PCP.PoweringOpinions.decoded line 520
  44. def OAI.MaxCutGames.Foundations.PCP.PoweringOpinions.matchFn line 525
  45. theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinions.matchFn_mem_Icc line 531
  46. theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinions.decoded_modal_baseline line 542

    Source documentation

    The reference-length modal lower bound is proved from actual port samples.

    theorem decoded_modal_baseline (G : PortGraph V D) (t N : Nat)
    (selectors : ∀ v, AddressSelector G t v) (labels : V → PaddedLabel D t A)
    (fallback : A) (u : V) :
    1 / (Fintype.card A : ℝ) ≤
      iterateOperator G N (matchFn G t N selectors labels fallback u) u := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringOpinions.matchFn

  47. theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinions.decoded_modal_near line 553

    Source documentation

    Actual decoded letters retain positive mass throughout the middle window.

    theorem decoded_modal_near (G : PortGraph V D) (t M m : Nat)
    (selectors : ∀ v, AddressSelector (lazyGraph G) t v)
    (labels : V → PaddedLabel (Bool × D) t A) (fallback : A)
    (hM : 1 ≤ M)
    (hlo : (4 * Fintype.card A * M) ^ 2 - M ≤ m)
    (hhi : m ≤ (4 * Fintype.card A * M) ^ 2 + M) (u : V) :
    1 / (2 * (Fintype.card A : ℝ)) ≤
      iterateOperator (lazyGraph G) m
        (matchFn (lazyGraph G) t ((4 * Fintype.card A * M) ^ 2)
          selectors labels fallback u) u := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringOpinions.matchFn

  48. def OAI.MaxCutGames.Foundations.PCP.PoweringReach.ReachLE line 588
  49. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReach.reach_refl line 591
  50. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReach.reach_mono line 594
  51. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReach.reach_prepend line 599
  52. def OAI.MaxCutGames.Foundations.PCP.PoweringReach.reversePorts line 607

    Source documentation

    Reversal records each arrival port, not the original outgoing port.

    def reversePorts (G : PortGraph V D) : V → List D → List D
  | _, [] => []
  | v, d :: ds => reversePorts G (next G v d) ds ++ [(G.rot (v, d)).2]
  53. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReach.reversePorts_length line 611
  54. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReach.walkEnd_reversePorts line 617
  55. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReach.wordEnd_eq_walkEnd_ofFn line 628
  56. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReach.reach_reverse line 638
  57. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReach.tail_reach line 651

    Source documentation

    The actual prefix places each traversed edge's tail in the start ball.

    theorem tail_reach (G : PortGraph V D) :
    ∀ (n : Nat) (w : Walk V D (n + 1)) (k : Fin (n + 1)),
      ReachLE G (n + 1) w.1 (edgeAt G n w k).1 := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringReach.ReachLE

  58. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReach.head_reach_endpoint line 666

    Source documentation

    The suffix proceeds from the traversed edge's head to the walk endpoint.

    theorem head_reach_endpoint (G : PortGraph V D) :
    ∀ (n : Nat) (w : Walk V D (n + 1)) (k : Fin (n + 1)),
      ReachLE G (n + 1) (G.rot (edgeAt G n w k)).1 (endpoint G w) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringReach.ReachLE

  59. def OAI.MaxCutGames.Foundations.PCP.PoweringReach.tailFromStart line 680
  60. def OAI.MaxCutGames.Foundations.PCP.PoweringReach.headFromEnd line 684
  61. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReach.tailFromStart_val line 688
  62. theorem OAI.MaxCutGames.Foundations.PCP.PoweringReach.headFromEnd_val line 692
  63. def OAI.MaxCutGames.Foundations.PCP.PoweringTest.baseGraph line 718

    Source documentation

    The base port predicates packaged as a constraint graph.

    def baseGraph (G : PortGraph V D) (accepts : Edge V D → A → A → Bool)
    (reverse_accepts : ∀ e a b, accepts (G.rot e) b a = accepts e a b) :
    ConstraintGraph V (Edge V D) A where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.ConstraintGraph

  64. def OAI.MaxCutGames.Foundations.PCP.PoweringTest.pathAccepts line 729

    Source documentation

    Check all base constraints along the recorded walk. The reach certificates select genuine vertices in the two full-radius neighborhood balls.

    def pathAccepts (G : PortGraph V D) (accepts : Edge V D → A → A → Bool)
    (n : Nat) (selectors : ∀ v, AddressSelector G (n + 1) v)
    (w : Walk V D (n + 1)) (a b : PaddedLabel D (n + 1) A) : Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.accepts

  65. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.pathAccepts_eq_true_iff line 737
  66. abbrev OAI.MaxCutGames.Foundations.PCP.PoweringTest.Dart line 748
  67. def OAI.MaxCutGames.Foundations.PCP.PoweringTest.reverseDart line 751

    Source documentation

    Reversal preserves the recorded walk and changes its direction flag.

    def reverseDart (V D : Type*) (n : Nat) : Dart V D n ≃ Dart V D n where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringTest.Dart

  68. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.reverseDart_involutive line 761
  69. def OAI.MaxCutGames.Foundations.PCP.PoweringTest.poweredGraph line 768

    Source documentation

    An actual powered constraint graph, with a common raw alphabet at all vertices. Its reversal law is witnessed by the orientation bit.

    def poweredGraph (G : PortGraph V D) (accepts : Edge V D → A → A → Bool)
    (n : Nat) (selectors : ∀ v, AddressSelector G (n + 1) v) :
    ConstraintGraph V (Dart V D n) (PaddedLabel D (n + 1) A) where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.PoweringTest.Dart

  70. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.poweredGraph_tail_false line 780
  71. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.poweredGraph_tail_true line 785
  72. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.poweredGraph_edgeSatisfied line 792

    Source documentation

    Both directed copies evaluate the same original-start/original-end path test. Uniformly doubling the darts therefore introduces no change of event.

    theorem poweredGraph_edgeSatisfied (G : PortGraph V D)
    (accepts : Edge V D → A → A → Bool) (n : Nat)
    (selectors : ∀ v, AddressSelector G (n + 1) v)
    (labels : V → PaddedLabel D (n + 1) A)
    (direction : Bool) (w : Walk V D (n + 1)) :
    (poweredGraph G accepts n selectors).edgeSatisfied labels (direction, w) =
      pathAccepts G accepts n selectors w (labels w.1) (labels (endpoint G w)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.PoweringTest.poweredGraph, OAI.MaxCutGames.Foundations.PCP.PoweringTest.pathAccepts

  73. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.rejection_mean_eq_path_mean line 804

    Source documentation

    The actual directed-dart rejection average is exactly the recorded-walk rejection average. Only the orientation-bit average is removed, so the vertex type and the walk type are allowed to be empty.

    theorem rejection_mean_eq_path_mean [Fintype V] [Fintype D]
    (G : PortGraph V D) (accepts : Edge V D → A → A → Bool) (n : Nat)
    (selectors : ∀ v, AddressSelector G (n + 1) v)
    (labels : V → PaddedLabel D (n + 1) A) :
    SpectralReturn.mean (fun d : Dart V D n => PoweringMoment.bit
      ((poweredGraph G accepts n selectors).edgeSatisfied labels d = false)) =
      SpectralReturn.mean (fun w : Walk V D (n + 1) => PoweringMoment.bit
        (pathAccepts G accepts n selectors w (labels w.1) (labels (endpoint G w)) = false)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean, OAI.MaxCutGames.Foundations.PCP.PoweringTest.Dart, OAI.MaxCutGames.Foundations.PCP.PoweringMoment.bit, OAI.MaxCutGames.Foundations.PCP.PoweringTest.poweredGraph, OAI.MaxCutGames.Foundations.PCP.PoweringTest.pathAccepts

  74. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.pathAccepts_honest line 815
  75. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.perfect_completeness line 830

    Source documentation

    Perfect completeness for the actual powered graph and its common alphabet.

    theorem perfect_completeness (G : PortGraph V D)
    (accepts : Edge V D → A → A → Bool) (n : Nat)
    (selectors : ∀ v, AddressSelector G (n + 1) v)
    (assignment : V → A)
    (satisfies : ∀ e, accepts e (assignment e.1) (assignment (G.rot e).1) = true) :
    ∀ d, (poweredGraph G accepts n selectors).edgeSatisfied
      (honestLabels G (n + 1) assignment) d = true := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.PoweringTest.poweredGraph

  76. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.preserves_satisfiability line 841
  77. def OAI.MaxCutGames.Foundations.PCP.PoweringTest.decodedBad line 854

    Source documentation

    Badness is computed from the actual base predicate and the decoded labels.

    def decodedBad (G : PortGraph V D) (accepts : Edge V D → A → A → Bool)
    (assignment : V → A) (e : Edge V D) : Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.accepts

  78. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.decodedBad_eq_true_iff line 858
  79. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.decodedBad_rot line 865

    Source documentation

    The base reversal law makes the decoded bad-edge event rotor-invariant.

    theorem decodedBad_rot (G : PortGraph V D)
    (accepts : Edge V D → A → A → Bool)
    (reverse_accepts : ∀ e a b, accepts (G.rot e) b a = accepts e a b)
    (assignment : V → A) (e : Edge V D) :
    decodedBad G accepts assignment (G.rot e) = decodedBad G accepts assignment e := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.PoweringTest.decodedBad

  80. def OAI.MaxCutGames.Foundations.PCP.PoweringTest.witness line 875

    Source documentation

    A bad decoded edge with matching opinions at its two true endpoints.

    noncomputable def witness (G : PortGraph V D)
    (accepts : Edge V D → A → A → Bool) (n : Nat)
    (selectors : ∀ v, AddressSelector G (n + 1) v)
    (labels : V → PaddedLabel D (n + 1) A) (fallback : A)
    (assignment : V → A) (w : Walk V D (n + 1)) (k : Fin (n + 1)) : Prop :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.accepts

  81. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.witness_bad line 887
  82. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.witness_implies_path_rejection line 897

    Source documentation

    The witness forces failure of the actual kth checked path constraint. The opinion/decode identities use the genuine reach certificates.

    theorem witness_implies_path_rejection (G : PortGraph V D)
    (accepts : Edge V D → A → A → Bool) (n : Nat)
    (selectors : ∀ v, AddressSelector G (n + 1) v)
    (labels : V → PaddedLabel D (n + 1) A) (fallback : A)
    (assignment : V → A) (w : Walk V D (n + 1)) (k : Fin (n + 1))
    (h : witness G accepts n selectors labels fallback assignment w k) :
    pathAccepts G accepts n selectors w (labels w.1) (labels (endpoint G w)) = false := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.PoweringTest.witness, OAI.MaxCutGames.Foundations.PCP.PoweringTest.pathAccepts

  83. theorem OAI.MaxCutGames.Foundations.PCP.PoweringTest.witness_implies_rejection line 925

    Source documentation

    Rejection inclusion for the actual powered graph, derived from its test.

    theorem witness_implies_rejection (G : PortGraph V D)
    (accepts : Edge V D → A → A → Bool) (n : Nat)
    (selectors : ∀ v, AddressSelector G (n + 1) v)
    (labels : V → PaddedLabel D (n + 1) A) (fallback : A)
    (assignment : V → A) (w : Walk V D (n + 1)) (k : Fin (n + 1))
    (h : witness G accepts n selectors labels fallback assignment w k)
    (direction : Bool) :
    (poweredGraph G accepts n selectors).edgeSatisfied labels (direction, w) = false := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.PoweringTest.witness, OAI.MaxCutGames.Foundations.PCP.PoweringTest.poweredGraph