ActualGoodRows.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MaxCutGames.Decoder.ActualGoodRows.table line 21
theorem OAI.MaxCutGames.Decoder.ActualGoodRows.table_acceptance line 28
def OAI.MaxCutGames.Decoder.ActualGoodRows.adviceMass line 48
Source documentation
The row-advice probability in actual matrix coordinates. In particular, dependent rows of A are sampled with their full multiplicity.
```
def adviceMass (S : Source) (k s d r : ℕ)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s)) (α : ℝ) : ℝ :=
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount
def OAI.MaxCutGames.Decoder.ActualGoodRows.goodRowMass line 55
theorem OAI.MaxCutGames.Decoder.ActualGoodRows.goodRowMass_pos line 58
theorem OAI.MaxCutGames.Decoder.ActualGoodRows.exists_actual_advice_threshold line 63
def OAI.MaxCutGames.Decoder.ConstantSelection.visibleMass line 108
Source documentation
Probability of actual visible data carrying a transferred witness.
```
def visibleMass (α g₀ : ℝ) (ell r : ℕ) : ℝ :=
…
```
def OAI.MaxCutGames.Decoder.ConstantSelection.conditionalMass line 112
Source documentation
Independent private decoding success on a transferred witness.
```
def conditionalMass (α : ℝ) (ell r : ℕ) : ℝ :=
…
```
def OAI.MaxCutGames.Decoder.ConstantSelection.decodingMass line 115
def OAI.MaxCutGames.Decoder.ConstantSelection.variationBudget line 120
Source documentation
The whole-table TV budget includes the coefficient of both compared events in the witness-margin inequality.
```
def variationBudget (α g₀ : ℝ) (ell r : ℕ) : ℝ :=
…
```
theorem OAI.MaxCutGames.Decoder.ConstantSelection.visibleMass_pos line 123
theorem OAI.MaxCutGames.Decoder.ConstantSelection.conditionalMass_pos line 128
theorem OAI.MaxCutGames.Decoder.ConstantSelection.decodingMass_pos line 133
theorem OAI.MaxCutGames.Decoder.ConstantSelection.variationBudget_pos line 137
theorem OAI.MaxCutGames.Decoder.ConstantSelection.variationBudget_suffices line 141

theorem OAI.MaxCutGames.Decoder.ConstantSelection.cube_exponential_antitone line 154

Source documentation

Exponential clean-mask decay persists after increasing the cube root.

theorem cube_exponential_antitone {m n : ℕ} (hmn : m ≤ n)
    {N : ℝ} (hN : 0 < N) :
    Real.exp (-(n : ℝ) / (3600 * N)) ≤
      Real.exp (-(m : ℝ) / (3600 * N)) := by
…

theorem OAI.MaxCutGames.Decoder.ConstantSelection.exists_simultaneous_cube line 164

Source documentation

One tuple length meets the sparse-law and repetition requirements, while exceeding any independent inverse/erasure dimension threshold.

theorem exists_simultaneous_cube (V : Type*) [Fintype V] [Zero V] [DecidableEq V]
    {N ε γ : ℝ} (hN : 1 ≤ N) (hε : 0 < ε) (hγ : 0 < γ) (lower : ℕ) :
    ∃ m : ℕ, lower ≤ m ∧ 0 < m ∧
      totalVariation
        (independentWeights (mixture (1 / (m : ℝ) ^ 2) (singletonPairWeights V)) (m ^ 3))
        (uniformWeights (Fin (m ^ 3) → V × V)) ≤ ε ∧
      (1 - ((1 / (m : ℝ) ^ 2) / N) / 3600) ^ (m ^ 3) < γ := by
…

theorem OAI.MaxCutGames.Decoder.ConstantSelection.exists_matrix_cube line 185

Source documentation

All scalar requirements for the final decoding contradiction can be met after the fixed alphabet and inverse parameters have been chosen.

theorem exists_matrix_cube (V : Type*) [Fintype V] [Zero V] [DecidableEq V]
    {α g₀ : ℝ} (hα : 0 < α) (hg₀ : 0 < g₀)
    (ell r dimW lower : ℕ) :
    ∃ m : ℕ, lower ≤ m ∧ 0 < m ∧
      totalVariation
        (independentWeights (mixture (1 / (m : ℝ) ^ 2) (singletonPairWeights V)) (m ^ 3))
        (uniformWeights (Fin (m ^ 3) → V × V)) ≤ variationBudget α g₀ ell r ∧
      (1 - ((1 / (m : ℝ) ^ 2) / (2 : ℝ) ^ (dimW + r)) / 3600) ^ (m ^ 3) <
        decodingMass α g₀ ell r := by
…

Mentions: OAI.MaxCutGames.Decoder.ConstantSelection.variationBudget, OAI.MaxCutGames.Decoder.ConstantSelection.decodingMass

structure OAI.MaxCutGames.Decoder.MatrixGapChoice.InverseParameters line 209
Source documentation
Fixed dimensions, density and sparse mask for one logical alphabet. The remaining gadget codimension may be arbitrary when choosing the cube.
```
structure InverseParameters (rstar : ℕ) where
…
```
theorem OAI.MaxCutGames.Decoder.MatrixGapChoice.eta_lt_one line 231
theorem OAI.MaxCutGames.Decoder.MatrixGapChoice.exists_inverse_parameters line 239

theorem OAI.MaxCutGames.Decoder.MatrixGapChoice.exists_cube line 278

Source documentation

After all fixed dimensions are known, the cube simultaneously exceeds the inverse threshold, reduces full-table variation, and beats the decoder mass.

theorem exists_cube {rstar : ℕ} (P : InverseParameters rstar) (d : ℕ) :
    ∃ m : ℕ, 0 < m ∧ P.tupleThreshold ≤ m ^ 3 ∧
      0 ≤ 1 / (m : ℝ) ^ 2 ∧ 1 / (m : ℝ) ^ 2 ≤ 1 ∧
      Foundations.Information.totalVariation
        (SparseLaw.independentWeights
          (SparseLaw.mixture (1 / (m : ℝ) ^ 2)
            (SparseLaw.singletonPairWeights (Ambient P.s d))) (m ^ 3))
        (SparseLaw.uniformWeights (Fin (m ^ 3) → Ambient P.s d × Ambient P.s d)) ≤
          ConstantSelection.variationBudget P.α (ActualGoodRows.goodRowMass rstar P.s P.r) P.s P.r ∧
      (1 - ((1 / (m : ℝ) ^ 2) / (2 : ℝ) ^ (d + P.r)) / 3600) ^ (m ^ 3) <
        ConstantSelection.decodingMass P.α (ActualGoodRows.goodRowMass rstar P.s P.r) P.s P.r := by
…

Mentions: OAI.MaxCutGames.Decoder.MatrixGapChoice.InverseParameters, OAI.MaxCutGames.Foundations.Information.totalVariation, OAI.MaxCutGames.Decoder.SparseLaw.independentWeights, OAI.MaxCutGames.Decoder.SparseLaw.mixture, OAI.MaxCutGames.Decoder.SparseLaw.singletonPairWeights, OAI.MaxCutGames.Decoder.SparseLaw.uniformWeights, OAI.MaxCutGames.Decoder.ConstantSelection.variationBudget, OAI.MaxCutGames.Decoder.ActualGoodRows.goodRowMass, OAI.MaxCutGames.Decoder.ConstantSelection.decodingMass