OAI/Computability/MaxCut/Encoding/ActualEvents.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The two full-table events used in the projected-witness transfer. Their sample space contains actual occurrence tuples and complete affine tables, but no projection choice. The selected witness depends on row advice only.

  1. abbrev OAI.MaxCutGames.Decoder.ActualEvents.Context line 26
  2. abbrev OAI.MaxCutGames.Decoder.ActualEvents.Sample line 29
  3. abbrev OAI.MaxCutGames.Decoder.ActualEvents.FullTableSample line 32
  4. def OAI.MaxCutGames.Decoder.ActualEvents.fullTableEquiv line 37

    Source documentation

    A bijection merely rearranges the full sampled table and changes its matrix coordinates. It never appends the hidden projection to this law.

    def fullTableEquiv (S : Source) (k s d r : ℕ) :
    FullTableSample S k s d r ≃ Sample S k s d r where
…

    Mentions: OAI.MaxCutGames.Decoder.ActualEvents.FullTableSample, OAI.MaxCutGames.Decoder.ActualEvents.Sample

  5. def OAI.MaxCutGames.Decoder.ActualEvents.unrestricted line 72
  6. def OAI.MaxCutGames.Decoder.ActualEvents.sliceEvent line 75
  7. def OAI.MaxCutGames.Decoder.ActualEvents.targetHit line 81
  8. theorem OAI.MaxCutGames.Decoder.ActualEvents.targetHit_implies_slice line 87
  9. theorem OAI.MaxCutGames.Decoder.ActualEvents.uniform_probability_expect line 95
  10. theorem OAI.MaxCutGames.Decoder.ActualEvents.unrestricted_slice_mass line 102
  11. theorem OAI.MaxCutGames.Decoder.ActualEvents.unrestricted_match_mass line 116
  12. theorem OAI.MaxCutGames.Decoder.ActualEvents.slice_probability_lower line 139

    Source documentation

    The full-table slice event pays exactly one bounded column-fiber factor.

    theorem slice_probability_lower (S : Source) (k s d r : ℕ)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s)) (α g₀ : ℝ)
    (hgood : g₀ ≤ ActualGoodRows.adviceMass S k s d r labeling α) :
    g₀ * (1 / (2 : ℝ) ^ (s * r)) ≤
      (unrestricted S k s d r).probability (sliceEvent S k s d r labeling α) := by
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.ActualGoodRows.adviceMass, OAI.MaxCutGames.Decoder.ActualEvents.unrestricted, OAI.MaxCutGames.Decoder.ActualEvents.sliceEvent

  13. theorem OAI.MaxCutGames.Decoder.ActualEvents.target_probability_lower line 150