ActualCompleteness.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Actual finite-distribution identities for completeness.

theorem OAI.MaxCutGames.Reduction.ActualCompleteness.expect_linear_eval line 19
Source documentation
Evaluation at a point on the homogeneous h = 1 slice sends the uniform law on all linear maps to the uniform law on the target vector space.
```
theorem expect_linear_eval (τ : E →ₗ[F2] F2) (x : E) (hx : τ x = 1)
    (g : R → ℚ) :
    (𝔼 X : E →ₗ[F2] R, g (X x)) = 𝔼 r : R, g r := by
…
```

theorem OAI.MaxCutGames.Reduction.ActualCompleteness.expect_independent_linear_evals line 42

Source documentation

Independent uniform linear maps retain independence after evaluating the same h = 1 point. In particular the second coordinate is a uniform binary bit.

theorem expect_independent_linear_evals [Fintype (E →ₗ[F2] F2)]
    (τ : E →ₗ[F2] F2) (x : E) (hx : τ x = 1) (g : R → F2 → ℚ) :
    (𝔼 X : E →ₗ[F2] R, 𝔼 ell : E →ₗ[F2] F2, g (X x) (ell x)) =
      𝔼 r : R, 𝔼 b : F2, g r b := by
…

def OAI.MaxCutGames.Reduction.ActualCompleteness.localNoiseFailure line 58
Source documentation
The actual honest noise test on a fixed valid homogeneous point.
```
noncomputable def localNoiseFailure (g : SplitGadget s d) (x : E) : ℚ :=
…
```
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.localNoiseFailure_eq_half line 64
Source documentation
The independent random functional makes the conditional noise failure exactly half the gadget's stability error, including indexed noise repetitions.
```
theorem localNoiseFailure_eq_half (g : SplitGadget s d)
    (τ : E →ₗ[F2] F2) (x : E) (hx : τ x = 1) :
    localNoiseFailure g x = g.stabilityError / 2 := by
…
```
Mentions: OAI.MaxCutGames.Reduction.ActualCompleteness.localNoiseFailure
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.localNoiseFailure_le line 93
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.expect_function_apply line 104
def OAI.MaxCutGames.Reduction.ActualCompleteness.tupleFailure line 118
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.tupleFailure_le line 122
def OAI.MaxCutGames.Reduction.ActualCompleteness.evalTriple line 157
def OAI.MaxCutGames.Reduction.ActualCompleteness.evalRecord line 160
def OAI.MaxCutGames.Reduction.ActualCompleteness.evaluate line 166
Source documentation
An assignment is evaluated from retained record data only.
```
def evaluate (names : Id → Fin 3 → Name) (A : Name → F2)
    (d : Data k Name Id R) : R := d.1 + ∑ j, evalRecord names A (d.2 j)
```
Mentions: OAI.MaxCutGames.Reduction.ActualCompleteness.evalRecord
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.record_eval_normalized line 169
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.record_eval_adjustment line 187
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.evaluate_data line 198
def OAI.MaxCutGames.Reduction.ActualCompleteness.honestPoint line 209
Source documentation
The free-coordinate local assignment always has homogeneous coordinate one.
```
def honestPoint (occ : Fin k → Id) (names : Id → Fin 3 → Name) (A : Name → F2) : E k :=
…
```
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.honestPoint_tau line 212
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.canonical_evaluate line 217
Source documentation
Actual canonical evaluation equals linear-map evaluation on every question whose occurrences the assignment satisfies.
```
theorem canonical_evaluate (occ : Fin k → Id) (names : Id → Fin 3 → Name)
    (rhs : Id → F2) (A : Name → F2) (X : E k →ₗ[F2] R)
    (hvalid : ∀ j, ∑ i, A (names (occ j) i) = rhs (occ j)) :
    evaluate names A (canonical occ names rhs X) = X (honestPoint occ names A) := by
…
```
Mentions: OAI.MaxCutGames.Reduction.ActualCompleteness.evaluate, OAI.MaxCutGames.Reduction.ActualCompleteness.honestPoint
def OAI.MaxCutGames.Reduction.ActualCompleteness.honestVertexLabel line 229
def OAI.MaxCutGames.Reduction.ActualCompleteness.honestLabeling line 234
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.honest_unfolded line 240
Source documentation
Equivariance recovers the dropped alphabet component exactly.
```
theorem honest_unfolded (S : Source) (k : Nat) {s d : Nat} (g : SplitGadget s d)
    (A : Fin S.«variables» → Bool) (side : Bool) (q : ActualGame.Query S k s d) :
    ActualGame.unfolded S k s d (honestLabeling S k g A) side q =
      g.f (evaluate (ActualGame.names S) (fun n => ofBit (A n))
        (ActualGame.canonical S k s d q)) := by
…
```
Mentions: OAI.MaxCutGames.Reduction.ActualGame.Query, OAI.MaxCutGames.Reduction.ActualGame.unfolded, OAI.MaxCutGames.Reduction.ActualCompleteness.honestLabeling, OAI.MaxCutGames.Reduction.ActualCompleteness.evaluate, OAI.MaxCutGames.Reduction.ActualGame.names, OAI.MaxCutGames.Reduction.ActualGame.canonical
def OAI.MaxCutGames.Reduction.ActualCompleteness.sourcePoint line 257
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.sourcePoint_tau line 261
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.satisfied_parity line 264
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.honest_unfolded_valid line 274
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.expect_pair_inline_ActualCompleteness line 284
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.honest_acceptance_bound line 288
theorem OAI.MaxCutGames.Reduction.ActualCompleteness.honest_acceptance_of_bounds line 347

theorem OAI.MaxCutGames.Reduction.ActualCompleteness.honest_satisfied_fraction_bound line 357

Source documentation

The probability bound is exactly a bound on the generated unweighted list.

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 ≤
      (Foundations.Target.countSatisfied (honestLabeling S k g A)
        (ActualGame.outputInstance S k g).constraints : ℚ) /
        (ActualGame.outputInstance S k g).constraints.length := by
…

Mentions: OAI.MaxCutGames.Foundations.Target.countSatisfied, OAI.MaxCutGames.Reduction.ActualCompleteness.honestLabeling, OAI.MaxCutGames.Reduction.ActualGame.outputInstance

theorem OAI.MaxCutGames.Reduction.ActualCompleteness.actual_completeAt line 368
Source documentation
The honest labeling witnesses the formal target completeness predicate for the actual generated instance whenever its actual error budget fits the target.
```
theorem actual_completeAt (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (A : Fin S.«variables» → Bool)
    (error : Foundations.Target.RationalError)
    (hbudget : (k : ℚ) * S.failure A + g.stabilityError / 2 ≤
      Integration.GapSemantics.errorValue error) :
    Foundations.Target.CompleteAt error (ActualGame.outputInstance S k g) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Target.RationalError, OAI.MaxCutGames.Integration.GapSemantics.errorValue, OAI.MaxCutGames.Foundations.Target.CompleteAt, OAI.MaxCutGames.Reduction.ActualGame.outputInstance