PoweringOpinionsLemmas.lean`

43 declarations, 0 contain sorry, 0 declared as axioms

Actual local-label opinions, modal decoding at the reference length, and its proved persistence at nearby lazy-walk lengths.

def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinions.opinionAt line 23
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
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinions.opinionAt_eq_decode line 30
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinions.honestLabels line 38
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinions.opinionAt_honest line 41
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinions.sampleOpinion line 51
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinions.decoded line 56
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinions.matchFn line 61
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinions.matchFn_mem_Icc line 67

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinions.decoded_modal_baseline line 78

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.UniqueGamesTheorem.Foundations.PCP.PoweringOpinions.matchFn

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringOpinions.decoded_modal_near line 89

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.UniqueGamesTheorem.Foundations.PCP.PoweringOpinions.matchFn

def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.baseGraph line 134
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.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.pathAccepts line 145
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.UniqueGamesTheorem.Foundations.PCP.accepts
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.pathAccepts_eq_true_iff line 153
abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.Dart line 164
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.reverseDart line 167
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.UniqueGamesTheorem.Foundations.PCP.PoweringTest.Dart
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.reverseDart_involutive line 177
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.poweredGraph line 184
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.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.Dart
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.poweredGraph_tail_false line 196
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.poweredGraph_tail_true line 201
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.poweredGraph_edgeSatisfied line 208
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.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.poweredGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.pathAccepts
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.rejection_mean_eq_path_mean line 220
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.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.Dart, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.bit, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.poweredGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.pathAccepts
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.pathAccepts_honest line 231

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.perfect_completeness line 246

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.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.poweredGraph

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.preserves_satisfiability line 257
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.decodedBad line 270
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.UniqueGamesTheorem.Foundations.PCP.accepts
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.decodedBad_eq_true_iff line 274

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.decodedBad_rot line 281

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.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.decodedBad

def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.witness line 291

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.UniqueGamesTheorem.Foundations.PCP.accepts

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.witness_bad line 303

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.witness_implies_path_rejection line 313

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.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.witness, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.pathAccepts

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.witness_implies_rejection line 341

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.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.witness, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.poweredGraph

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringCounting.constraint_rejection_mean_eq_count line 377
Source documentation
An arbitrary constraint graph's rejection probability is its actual rejected-dart cardinal ratio, including the empty-dart case.
```
theorem constraint_rejection_mean_eq_count [Fintype E]
    (H : ConstraintGraph V E A) (labels : V → A) :
    SpectralReturn.mean (fun e : E => PoweringMoment.bit
      (H.edgeSatisfied labels e = false)) =
      (H.rejectionCount labels : ℝ) / (Fintype.card E : ℝ) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.bit
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringCounting.constraint_rejection_lower_iff line 393
Source documentation
Multiplying a normalized lower bound by the actual positive dart count.
```
theorem constraint_rejection_lower_iff [Fintype E]
    (H : ConstraintGraph V E A) (labels : V → A)
    (hcard : 0 < Fintype.card E) (ε : ℝ) :
    ε ≤ SpectralReturn.mean (fun e : E => PoweringMoment.bit
      (H.edgeSatisfied labels e = false)) ↔
      ε * (Fintype.card E : ℝ) ≤ (H.rejectionCount labels : ℝ) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.bit
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringCounting.edgeDensity_eq_bit_mean line 404
Source documentation
The edge-profile definition equals its actual directed-edge indicator mean without any nonemptiness assumption on vertices or ports.
```
theorem edgeDensity_eq_bit_mean [Fintype V] [Fintype D]
    (bad : Edge V D → Bool) :
    SpectralReturn.edgeDensity bad =
      SpectralReturn.mean (fun e : Edge V D => PoweringMoment.bit (bad e = true)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.bit

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringCounting.base_edgeDensity_eq_rejection_count line 419

Source documentation

Decoded badness is exactly rejection in the actual base constraint graph.

theorem base_edgeDensity_eq_rejection_count [Fintype V] [Fintype D]
    (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) :
    SpectralReturn.edgeDensity (decodedBad G accepts assignment) =
      ((baseGraph G accepts reverse_accepts).rejectionCount assignment : ℝ) /
        (Fintype.card (Edge V D) : ℝ) := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringCounting.base_count_lower_to_density line 437

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringCounting.powered_rejection_mean_eq_count line 449

Source documentation

The actual powered graph's directed-dart average is its rejected-dart fraction. No nonemptiness premise is needed for this identity.

theorem powered_rejection_mean_eq_count [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)) =
      ((poweredGraph G accepts n selectors).rejectionCount labels : ℝ) /
        (Fintype.card (Dart V D n) : ℝ) :=
…

Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.bit

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringCounting.path_rejection_mean_eq_count line 461

Source documentation

The recorded-walk rejection average used in soundness is the actual powered graph's rejected-dart fraction.

theorem path_rejection_mean_eq_count [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 w : Walk V D (n + 1) => PoweringMoment.bit
      (pathAccepts G accepts n selectors w (labels w.1) (labels (endpoint G w)) = false)) =
      ((poweredGraph G accepts n selectors).rejectionCount labels : ℝ) /
        (Fintype.card (Dart V D n) : ℝ) := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.bit

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringCounting.powered_density_lower_to_count line 474

Source documentation

Convert a proved path-test rejection lower bound into the actual powered constraint graph's rejected-dart count inequality.

theorem powered_density_lower_to_count [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)
    (hcard : 0 < Fintype.card (Dart V D n)) (ε : ℝ)
    (hlower : ε ≤ 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))) :
    ε * (Fintype.card (Dart V D n) : ℝ) ≤
      ((poweredGraph G accepts n selectors).rejectionCount labels : ℝ) := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.bit

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringCounting.natCard_dart line 488
Source documentation
Exact size of the powered dart type, retaining both direction flags and all recorded port words, including repeated vertices and edges.
```
theorem natCard_dart [Finite V] [Finite D] (n : Nat) :
    Nat.card (Dart V D n) = 2 * Nat.card V * Nat.card D ^ (n + 1) := by
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringCounting.fintypeCard_dart line 492
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringCounting.natCard_poweredAlphabet line 499
Source documentation
The common powered alphabet size depends only on degree, radius, and the base alphabet. The ambient vertex cardinality does not occur.
```
theorem natCard_poweredAlphabet [Finite D] [Finite A] (n : Nat) :
    Nat.card (PaddedLabel D (n + 1) A) =
      Nat.card A ^ (∑ j : Fin (n + 2), Nat.card D ^ j.val) :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringCounting.natCard_finitePortAlphabet line 506
Source documentation
With finite numbered ports, the same exponent is the length of the already constructed executable address enumeration.
```
theorem natCard_finitePortAlphabet [Finite A] (d n : Nat) :
    Nat.card (PaddedLabel (Fin d) (n + 1) A) =
      Nat.card A ^ (PoweringAddresses.allAddresses d (n + 1)).length := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringAddresses.allAddresses