TableKeysCompletenessLemmas.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Completeness of the v2 single-orbit matrix game. The generic finite-average calculation is shared with the proved actual completeness calculation. Its reuse is justified below by pointwise equality of restored answers under diagonal labels; the output vertices themselves are never doubled.

No gadget existence, dispersion hypothesis, inverse theorem, or legacy soundness theorem is a premise. The bound includes the exact fair-bit factor 1 / 2, and is a statement about the actual finite edge occurrence list.

def OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.diagonalLabeling line 31
Source documentation
Use a single label function on both auxiliary sides, solely to share the already proved finite-average calculation. This does not change the v2 game.
```
def diagonalLabeling (S : Source) (k s d : Nat)
    (labeling : Fin (vertexCount S k s d) → Fin (2^s)) :
    Fin (ActualGame.vertexCount S k s d) → Fin (2^s) :=
…
```
theorem OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.diagonal_unfolded line 36

theorem OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.acceptanceProbability_eq_diagonal line 45

Source documentation

Pointwise-identical matrix tests have exactly the same acceptance average.

theorem acceptanceProbability_eq_diagonal (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (labeling : Fin (vertexCount S k s d) → Fin (2^s)) :
    acceptanceProbability S k g labeling =
      ActualGame.acceptanceProbability S k g (diagonalLabeling S k s d labeling) := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.diagonalLabeling

def OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.honestLabeling line 52
theorem OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.diagonal_honestLabeling line 56

theorem OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.honest_unfolded line 64

Source documentation

The removed affine intercept is recovered by gadget equivariance.

theorem honest_unfolded (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (A : Fin S.variables → Bool) (q : Query S k s d) :
    unfolded S k s d (honestLabeling S k g A) q =
      g.f (ActualCompleteness.evaluate (ActualGame.names S) (fun n => ofBit (A n))
        (canonical S k s d q)) := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.honestLabeling

theorem OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.honest_unfolded_valid line 74

Source documentation

On a satisfied tuple, every sampled table evaluates the same homogeneous answer with first coordinate one.

theorem honest_unfolded_valid (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (A : Fin S.variables → Bool) (q : Query S k s d)
    (hgood : ∀ j, S.satisfied A (q.1 j) = true) :
    unfolded S k s d (honestLabeling S k g A) q =
      g.f (q.2 (ActualCompleteness.sourcePoint S k A q.1)) := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.honestLabeling

theorem OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.honest_acceptance_bound line 82
theorem OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.honest_acceptance_of_bounds line 89

theorem OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.honest_satisfied_fraction_bound line 99

Source documentation

Completeness is measured on the generated single-orbit edge occurrences.

theorem honest_satisfied_fraction_bound (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (A : Fin S.variables → Bool) :
    1 - (k : ℚ) * S.failure A - g.stabilityError / 2 ≤
      (countSatisfied (honestLabeling S k g A)
        (outputInstance S k g).constraints : ℚ) /
        (outputInstance S k g).constraints.length := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.honestLabeling

theorem OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.completeAt line 108
theorem OAI.UniqueGamesTheorem.Decoder.TableKeysCompleteness.completeAt_withEnumeration line 122
theorem OAI.UniqueGamesTheorem.Decoder.MatrixGap.semantic_acceptance_le_address_value line 156
Source documentation
Every semantic labeling extends to a labeling of the padded address space. The generated edge list retains its exact acceptance fraction.
```
theorem semantic_acceptance_le_address_value (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (en : NoiseEnumeration g)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s)) :
    (TableKeysGame.acceptanceProbability S k g labeling : ℝ) ≤
      InstanceValue.value (TableKeysAddressGame.outputInstance S k g en) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.TableKeysGame.acceptanceProbability, OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.outputInstance

theorem OAI.UniqueGamesTheorem.Decoder.MatrixGap.address_value_ge_of_near_assignment line 183

Source documentation

The exact near-assignment loss and fair-bit factor one half, measured on the generated address instance and then cast to its real optimum value.

theorem address_value_ge_of_near_assignment (S : Source) (k : Nat) {s d : Nat}
    (T : NoiseTables.Table s d) (f : Ambient s d → Alphabet s)
    (hf : ∀ x c, f (x + (c, 0)) = f x + c)
    (assignment : Fin S.variables → Bool) (ξ p : ℚ)
    (hfailure : S.failure assignment ≤ ξ)
    (hstable : (T.gadget f hf).stabilityError ≤ p) :
    (1 : ℝ) - ((k : ℝ) * (ξ : ℝ) + (p : ℝ) / 2) ≤
      InstanceValue.value (TableKeysAddressGame.tableOutput S k T) := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.tableOutput