ActualSeedSamplingLemmas.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The complete seed used for the lower-bound conditioning argument and the mask/slot/map experiment used for the clean upper bound have exactly the same actual decoder success. Unused positions are removed only by the pointwise observation equality; occurrence IDs and their ordered local copies remain.

theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedSampling.uniform_occurrence_slots line 30

def OAI.UniqueGamesTheorem.Decoder.ActualSeedSampling.drawAgreement line 44

Source documentation

A named pointwise observable makes the finite expectation permutations explicit without changing the actual sampled draw.

def drawAgreement (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector rs) →
      VisiblePolicies.ResponseWitness k → Prop)
    (A : Alphabet s →ₗ[F2] Vector rs) (mask : Fin k → Bool)
    (occ : Fin k → Fin S.occurrences) (slots : Fin k → Fin 3)
    (TM :
      (RawPartnerTarget.RawPoint (Clean.NativeExperiment.maskSet mask) →ₗ[F2] Vector d) ×
      (RawPartnerTarget.RawPoint (Clean.NativeExperiment.maskSet mask) →ₗ[F2] Alphabet s)) : ℝ :=
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness, OAI.UniqueGamesTheorem.Clean.NativeExperiment.maskSet

theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedSampling.sampledAgreement_eq_separated line 57
theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedSampling.fullSeedLaw_eq_sampledAgreement line 95
Source documentation
Exact sampler join: the complete hidden seed used by conditioning has the same success as the genuine local-policy experiment used by the upper bound, with no extra hidden-data conditioning on either side.
```
theorem fullSeedLaw_eq_sampledAgreement (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector rs) →
      VisiblePolicies.ResponseWitness k → Prop)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1) :
    (AdviceLaw.fullSeedLaw (V := Alphabet s × Vector d)
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.fullSeedLaw
theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedSampling.fullSeedLaw_upper line 133
theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedVariation.uniform_pushforward_equiv line 175
theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedVariation.totalVariation_pushforward_equiv line 184

theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedVariation.ideal_full_uniform line 193

Source documentation

Three independent uniform samples are uniform on their full product.

theorem ideal_full_uniform (S : Source) (k s d r : ℕ) :
    AdviceLaw.withKernel
      ((FiniteDistribution.uniform (ActualGame.Question S k)).product
        (FiniteDistribution.uniform (Alphabet s →ₗ[F2] Vector r)))
      (fun _ => FiniteDistribution.uniform (ActualGame.Map k s d)) =
        FiniteDistribution.uniform (ActualEvents.FullTableSample S k s d r) := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceLaw.withKernel, OAI.UniqueGamesTheorem.Decoder.ActualEvents.FullTableSample

theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedVariation.ideal_pad_coordinates line 205
theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedVariation.actual_totalVariation_le_slope line 214
structure OAI.UniqueGamesTheorem.Decoder.MatrixGap.Parameters line 255
Source documentation
Fixed matrix-test parameters, before the separate bipartite subdivision and repetition. Existence is proved by the spectral/decoding argument.
```
structure Parameters (p : ℚ) where
…
```
theorem OAI.UniqueGamesTheorem.Decoder.MatrixGap.semantic_rate_le_address_value line 272
Source documentation
The rate of any semantic vertex labeling is realized on the direct address output. Isolated unused addresses receive an arbitrary valid label.
```
theorem semantic_rate_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)) :
    (GapSemantics.satisfactionRate (TableKeysGame.outputInstance S k g) labeling : ℝ) ≤
      InstanceValue.value (TableKeysAddressGame.outputInstance S k g en) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.TableKeysGame.outputInstance, OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.outputInstance
def OAI.UniqueGamesTheorem.Decoder.MatrixGap.Parameters.output line 287
Source documentation
The actual output constructor depends only on finite tables, not on the correcting map or its equivariance proof.
```
def output (P : Parameters p) (S : Source) : Instance (2 ^ P.s) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.MatrixGap.Parameters
theorem OAI.UniqueGamesTheorem.Decoder.MatrixGap.Parameters.completeness line 290
theorem OAI.UniqueGamesTheorem.Decoder.MatrixGap.Parameters.output_translations line 298