GraphTableComplexity.lean`

59 declarations, 0 contain sorry, 0 declared as axioms

Concrete bridges between graph cardinality and the length of the validated unary table encoding. These bounds supply the input-length and intermediate encoding estimates used by actual machine trace composition; they are not themselves a machine execution certificate.

def OAI.MaxCutGames.Foundations.PCP.GraphTableComplexity.encodingPolynomial line 18
theorem OAI.MaxCutGames.Foundations.PCP.GraphTableComplexity.encodingPolynomial_eval line 21
theorem OAI.MaxCutGames.Foundations.PCP.GraphTableComplexity.encodingPolynomial_mono line 25
theorem OAI.MaxCutGames.Foundations.PCP.GraphTableComplexity.rowBound_le_polynomial line 31
theorem OAI.MaxCutGames.Foundations.PCP.GraphTableComplexity.generic_size_add_two_le_bits line 41
theorem OAI.MaxCutGames.Foundations.PCP.GraphTableComplexity.generic_bits_le_polynomial line 47
theorem OAI.MaxCutGames.Foundations.PCP.GraphTableComplexity.generic_bits_le_of_size_le line 53
theorem OAI.MaxCutGames.Foundations.PCP.GraphTableComplexity.size_add_two_le_bits line 58
theorem OAI.MaxCutGames.Foundations.PCP.GraphTableComplexity.bits_le_polynomial line 64
theorem OAI.MaxCutGames.Foundations.PCP.GraphTableComplexity.bits_le_of_size_le line 70
abbrev OAI.MaxCutGames.Foundations.PCP.AmplificationRound.Label line 88
abbrev OAI.MaxCutGames.Foundations.PCP.AmplificationRound.Addresses line 89
abbrev OAI.MaxCutGames.Foundations.PCP.AmplificationRound.PoweredAlphabet line 90
instance OAI.MaxCutGames.Foundations.PCP.AmplificationRound.(instance at line 93) line 93
instance OAI.MaxCutGames.Foundations.PCP.AmplificationRound.(instance at line 94) line 94
abbrev OAI.MaxCutGames.Foundations.PCP.AmplificationRound.PoweredDart line 99
instance OAI.MaxCutGames.Foundations.PCP.AmplificationRound.(instance at line 103) line 103
def OAI.MaxCutGames.Foundations.PCP.AmplificationRound.selectors line 105
def OAI.MaxCutGames.Foundations.PCP.AmplificationRound.powered line 112
abbrev OAI.MaxCutGames.Foundations.PCP.AmplificationRound.Vertex line 118
abbrev OAI.MaxCutGames.Foundations.PCP.AmplificationRound.Dart line 123
instance OAI.MaxCutGames.Foundations.PCP.AmplificationRound.(instance at line 126) line 126
instance OAI.MaxCutGames.Foundations.PCP.AmplificationRound.(instance at line 135) line 135
instance OAI.MaxCutGames.Foundations.PCP.AmplificationRound.(instance at line 138) line 138
def OAI.MaxCutGames.Foundations.PCP.AmplificationRound.graph line 140
theorem OAI.MaxCutGames.Foundations.PCP.AmplificationRound.powered_completeness line 145
theorem OAI.MaxCutGames.Foundations.PCP.AmplificationRound.completeness line 158

theorem OAI.MaxCutGames.Foundations.PCP.PoweringWitness.iterate_mul_const line 183

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
…

def OAI.MaxCutGames.Foundations.PCP.PoweringWitness.endpointWitness line 198
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)) : ℝ :=
…
```

def OAI.MaxCutGames.Foundations.PCP.PoweringWitness.vertexWitness line 205

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) → ℝ :=
…

theorem OAI.MaxCutGames.Foundations.PCP.PoweringWitness.endpoint_lower_bound line 212

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.MaxCutGames.Foundations.PCP.PoweringWitness.endpointWitness

theorem OAI.MaxCutGames.Foundations.PCP.PoweringWitness.lazy_middle_witness_mean line 254

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.MaxCutGames.Foundations.PCP.PoweringWitness.vertexWitness

theorem OAI.MaxCutGames.Foundations.PCP.PoweringMomentBound.symmetric_gap_matrix_sum line 297
def OAI.MaxCutGames.Foundations.PCP.PoweringMomentBound.windowIndex line 352
def OAI.MaxCutGames.Foundations.PCP.PoweringMomentBound.windowEvent line 357
theorem OAI.MaxCutGames.Foundations.PCP.PoweringMomentBound.window_second_moment_eq line 361

theorem OAI.MaxCutGames.Foundations.PCP.PoweringMomentBound.window_second_moment_le line 387

Source documentation

All moment terms come from actual walk events; the only analytic input is the stated spectral contraction certificate of the given graph.

theorem window_second_moment_le (G : PortGraph V D) (lambda : ℝ)
    (certificate : SpectralCertificate G lambda) (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e)
    (n start m : Nat) (h : start + m ≤ n + 1) :
    mean (fun w => hits (windowEvent G bad n start m h) w ^ 2) ≤
      (m : ℝ) * edgeDensity bad *
        (1 + 2 / (1 - lambda) + ((m : ℝ) - 1) * edgeDensity bad) := by
…

Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringMomentBound.windowEvent

theorem OAI.MaxCutGames.Foundations.PCP.PoweringNumeric.min_density_ratio line 411
Source documentation
A bounded nonnegative coefficient gives the required ratio bound both below and above the cutoff 1/t.
```
theorem min_density_ratio (ε C k t : ℝ)
    (hε : 0 < ε) (hC : 0 < C) (hk : 0 ≤ k)
    (ht : 0 < t) (hkt : k ≤ t) :
    min ε (1 / t) / (C + 1) ≤ ε / (C + k * ε) := by
…
```

theorem OAI.MaxCutGames.Foundations.PCP.PoweringNumeric.count_moment_ratio_lower line 440

Source documentation

A positive natural count supplies 0 ≤ m - 1. After cancelling the positive mass m*ε, the ratio of moments dominates a constant times min ε (1/t). No sign condition on α is needed for its fourth power.

theorem count_moment_ratio_lower (α ε C t : ℝ) (m : ℕ)
    (hm : 0 < m) (hε : 0 < ε) (hC : 0 < C) (ht : 0 < t)
    (hmt : (m : ℝ) - 1 ≤ t) :
    (α ^ 4 * (m : ℝ) / (C + 1)) * min ε (1 / t) ≤
      (α ^ 2 * (m : ℝ) * ε) ^ 2 /
        ((m : ℝ) * ε * (C + ((m : ℝ) - 1) * ε)) := by
…

def OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.center line 480
theorem OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.le_center line 482
def OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.gain line 490
def OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.decodedError line 497
def OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.poweredRejection line 502
theorem OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.witness_bit_eq line 509
theorem OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.modal_witness_mean line 522

theorem OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.rejection_lower_bound line 549

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.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.center, OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.decodedError, OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.gain

theorem OAI.MaxCutGames.Foundations.PCP.PoweringGap.gain_nonneg line 651
theorem OAI.MaxCutGames.Foundations.PCP.PoweringGap.uniform_count_gap line 660
abbrev OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.Alphabet line 728
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.card_alphabet line 730
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.card_alphabet_eq_final line 733
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.center_eq line 737
Source documentation
The actual six-bit alphabet gives the endpoint length fixed for the round.
```
theorem center_eq :
    PoweringSoundness.center (Fintype.card Alphabet) FinalConstants.windowHalf =
      FinalConstants.endpointLength := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.center, OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.Alphabet, OAI.MaxCutGames.Foundations.PCP.FinalConstants.windowHalf, OAI.MaxCutGames.Foundations.PCP.FinalConstants.endpointLength
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.walkLength_eq line 744
Source documentation
Prefix, pivot and suffix together have the fixed odd walk length.
```
theorem walkLength_eq :
    2 * PoweringSoundness.center (Fintype.card Alphabet) FinalConstants.windowHalf + 1 =
      FinalConstants.walkLength := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.center, OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.Alphabet, OAI.MaxCutGames.Foundations.PCP.FinalConstants.windowHalf, OAI.MaxCutGames.Foundations.PCP.FinalConstants.walkLength
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.spectral_denominator_eq line 751
Source documentation
The spectral denominator is exactly 66 at the fixed return parameter.
```
theorem spectral_denominator_eq :
    (1 + 2 / (1 - (31 / 32 : ℝ))) + 1 = 66 := by
…
```
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.gain_eq line 757
Source documentation
Dividing the actual powering coefficient by the composition loss gives the round coefficient exactly. The large window parameter is not evaluated.
```
theorem gain_eq :
    PoweringSoundness.gain 64 FinalConstants.windowHalf (31 / 32) / 12288 =
      FinalConstants.gain := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.gain, OAI.MaxCutGames.Foundations.PCP.FinalConstants.windowHalf, OAI.MaxCutGames.Foundations.PCP.FinalConstants.gain
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.gain_card_eq line 775
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.scaled_bound_eq line 783
Source documentation
Both the coefficient and cap in the actual estimate match the fixed round constants, for every real error parameter.
```
theorem scaled_bound_eq (ε : ℝ) :
    (PoweringSoundness.gain (Fintype.card Alphabet) FinalConstants.windowHalf (31 / 32) *
        min ε
          (1 / ((2 * PoweringSoundness.center (Fintype.card Alphabet)
            FinalConstants.windowHalf + 1 : Nat) : ℝ))) / 12288 =
      FinalConstants.gain * min ε FinalConstants.cap := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.gain, OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.Alphabet, OAI.MaxCutGames.Foundations.PCP.FinalConstants.windowHalf, OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.center, OAI.MaxCutGames.Foundations.PCP.FinalConstants.gain, OAI.MaxCutGames.Foundations.PCP.FinalConstants.cap
theorem OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.composed_scaled_gap line 795
Source documentation
The composed powering and alphabet-reduction coefficient yields the fixed doubling bound after the checked preprocessing loss.
```
theorem composed_scaled_gap (ε : ℝ) (hε : 0 ≤ ε) :
    min (2 * ε) FinalConstants.cap ≤
      (PoweringSoundness.gain (Fintype.card Alphabet) FinalConstants.windowHalf (31 / 32) *
        min (ε / (Preprocessing.sizeFactor : ℝ))
          (1 / ((2 * PoweringSoundness.center (Fintype.card Alphabet)
            FinalConstants.windowHalf + 1 : Nat) : ℝ))) / 12288 := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.FinalConstants.cap, OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.gain, OAI.MaxCutGames.Foundations.PCP.PoweringFinalConstants.Alphabet, OAI.MaxCutGames.Foundations.PCP.FinalConstants.windowHalf, OAI.MaxCutGames.Foundations.PCP.Preprocessing.sizeFactor, OAI.MaxCutGames.Foundations.PCP.PoweringSoundness.center