SelectedFiberLaw.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Actual conditional selected-fiber agreement

The selected event is the full-table event used by the total-variation comparison. On a positive complete-data fiber it becomes the uniform actual affine row/column slice. The selector is fixed by the left observation; the extra complete data and a supporting matrix occur only in this analysis.

theorem OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.univ_congr line 34
Source documentation
The universe finset is independent of the chosen finite enumeration. The instances are explicit so elaboration need not unfold either enumeration.
```
private theorem univ_congr {X : Type*} (i j : Fintype X) :
    @Finset.univ X i = @Finset.univ X j := by
…
```
def OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.datumLeft line 41
def OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.datumMatrix line 44
def OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.datumProjection line 47
theorem OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.datumLeft_eq line 50
theorem OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.datumMatrix_rows line 56
theorem OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.datumMatrix_rowAdvice line 60

theorem OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.slice_assemble_iff line 73

Source documentation

Every event membership uses the same selected normalized witness on the entire complete-data fiber.

theorem slice_assemble_iff (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (data : Datum S k s d r) (hgood : GoodAdvice S labeling α (datumLeft S data))
    (N : AdviceLaw.PrivateMap data) :
    slice S k s d r labeling α (AdviceLaw.completeAssemble data N) = true ↔
      mapEquiv k s ((datumMatrix S data N).comp (datumProjection S data)) ∈
        (normalizedDescription S labeling α hα hsmall (datumLeft S data) hgood).toSlice.points := by
…

theorem OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.target_assemble_iff line 92

Source documentation

On the selected event, the actual full-table target-hit predicate equals projected affine equality with the very same normalized coefficient/intercept.

theorem target_assemble_iff (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (data : Datum S k s d r) (hgood : GoodAdvice S labeling α (datumLeft S data))
    (N : AdviceLaw.PrivateMap data)
    (hN : slice S k s d r labeling α (AdviceLaw.completeAssemble data N) = true) :
    targetHit S k s d r labeling α (AdviceLaw.completeAssemble data N) = true ↔
      TableKeysRestoration.projectedAnswer S k s d labeling (PaddedLaw.choiceMask data.2.1)
        (RawPrivateTable.supported (PaddedLaw.choiceMask data.2.1) (ActualGame.names S)
          data.1.1 (PaddedLaw.choiceSlots data.2.1)) ((datumMatrix S data N).prod data.2.2.1) =
        datumMatrix S data N (datumProjection S data
          (normalizedResponse S labeling α hα hsmall (datumLeft S data) hgood).coefficient) +
…

theorem OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.exists_selected_private line 128
Source documentation
Positive mass supplies a supporting private coordinate in the selected fiber; neither a hidden matrix nor good advice is an additional premise.
```
theorem exists_selected_private (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) (data : Datum S k s d r)
    (positive : 0 < (law S k s d r β hβ hβ').probability
      (VisibleTransfer.fiberEvent AdviceLaw.completeObserve data (slice S k s d r labeling α))) :
    ∃ N : AdviceLaw.PrivateMap data,
      slice S k s d r labeling α (AdviceLaw.completeAssemble data N) = true := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.fiberEvent, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeObserve, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.PrivateMap, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeAssemble
theorem OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.good_of_selected_private line 154

def OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.selectedPrivateEquiv line 168

Source documentation

The actual selected private coordinates are in bijection with the complete projected affine slice. The supporting point is used only to state its column equations; the canonical visible base still defines the private coordinates.

def selectedPrivateEquiv (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (data : Datum S k s d r) (hgood : GoodAdvice S labeling α (datumLeft S data))
    (Nstar : AdviceLaw.PrivateMap data)
    (hstar : slice S k s d r labeling α (AdviceLaw.completeAssemble data Nstar) = true) :
    {N : AdviceLaw.PrivateMap data //
      slice S k s d r labeling α (AdviceLaw.completeAssemble data N) = true} ≃
      RowErasureSliceQuotient.AffineSlice data.1.2
        ((normalizedResponse S labeling α hα hsmall (datumLeft S data) hgood).columns.map
          (datumProjection S data)) (datumMatrix S data Nstar) := by
…

theorem OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.selectedPrivateEquiv_val line 216

theorem OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.conditional_eq_transferred line 227

Source documentation

Exact conditional target probability, with no assumed uniformity premise.

theorem conditional_eq_transferred (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1)
    (data : Datum S k s d r) (hgood : GoodAdvice S labeling α (datumLeft S data))
    (Nstar : AdviceLaw.PrivateMap data)
    (hstar : slice S k s d r labeling α (AdviceLaw.completeAssemble data Nstar) = true)
    (positive : 0 < (law S k s d r β hβ hβ').probability
      (VisibleTransfer.fiberEvent AdviceLaw.completeObserve data (slice S k s d r labeling α))) :
    ((law S k s d r β hβ hβ').condition
      (VisibleTransfer.fiberEvent AdviceLaw.completeObserve data (slice S k s d r labeling α))
        positive).probability (targetHit S k s d r labeling α) =
…

theorem OAI.UniqueGamesTheorem.Decoder.SelectedFiberLaw.visibleWitness_decoding line 300

Source documentation

Every complete visible datum selected by the actual witness event pays the private-decoding success constant. Good advice and a nonempty transferred slice follow from positivity and are not additional hypotheses.

theorem visibleWitness_decoding (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) (data : Datum S k s d r)
    (hvisible : VisibleTransfer.visibleWitness (law S k s d r β hβ hβ')
      AdviceLaw.completeObserve (slice S k s d r labeling α)
      (targetHit S k s d r labeling α) (α / 4) data = true) :
    (α / 8) ^ 2 / (2 : ℝ) ^ (s * r) / (2 : ℝ) ^ r ≤
      ActualConditionalLaw.datumAgreement S labeling (goodPredicate S labeling α hα hsmall) data := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.visibleWitness, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeObserve, OAI.UniqueGamesTheorem.Decoder.ActualConditionalLaw.datumAgreement