OAI/Computability/UniqueGames/Soundness/RawTargetLawLemmas.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Exact partner-map laws in shared raw target coordinates

Inactive positions do not use a retained slot. Replacing their slots leaves both the concrete partner projection and the shared raw projection unchanged.

The row/column expectation identity below transports the two actual uniform map samples through the target coordinate equivalence independently. It is an exact identity for every observable of the pulled-back maps; it requires no trace, character, or naturality hypotheses.

  1. theorem OAI.UniqueGamesTheorem.Soundness.RawTargetLaw.partnerProjection_congr_slots line 36

    Source documentation

    The genuine partner projection reads retained slots only at active positions.

    theorem partnerProjection_congr_slots {k : Nat} (rhs : Fin k → Bool)
    (J : Finset (Fin k)) (slot slot' : Fin k → Slot)
    (agree : ∀ j ∈ J, slot j = slot' j) :
    PartnerLinear.projection rhs (activeOf J) slot =
      PartnerLinear.projection rhs (activeOf J) slot' := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerLinear.projection

  2. theorem OAI.UniqueGamesTheorem.Soundness.RawTargetLaw.rawProjection_congr_slots line 46

    Source documentation

    The shared raw target also ignores every inactive retained-slot choice.

    theorem rawProjection_congr_slots {k : Nat} (rhs : Fin k → Bool)
    (J : Finset (Fin k)) (slot slot' : Fin k → Slot)
    (agree : ∀ j ∈ J, slot j = slot' j) :
    RawPartnerTarget.rawProjection rhs J slot =
      RawPartnerTarget.rawProjection rhs J slot' := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RawPartnerTarget.rawProjection

  3. theorem OAI.UniqueGamesTheorem.Soundness.RawTargetLaw.precompose_rawProjection line 54
  4. theorem OAI.UniqueGamesTheorem.Soundness.RawTargetLaw.partner_row_column_expectation line 66

    Source documentation

    Exact nested uniform expectations in partner versus raw coordinates. Any finite enumerations of the four map spaces may be used.

    theorem partner_row_column_expectation {k : Nat} (rhs : Fin k → Bool)
    (J : Finset (Fin k)) (slot : Fin k → Slot)
    {D C : Type} [AddCommGroup D] [Module F2 D] [AddCommGroup C] [Module F2 C]
    [Fintype (PartnerPoint rhs (activeOf J) →ₗ[F2] D)]
    [Fintype (PartnerPoint rhs (activeOf J) →ₗ[F2] C)]
    [Fintype (RawPoint J →ₗ[F2] D)] [Fintype (RawPoint J →ₗ[F2] C)]
    (H : (ActualHomogeneous.E k →ₗ[F2] D) →
      (ActualHomogeneous.E k →ₗ[F2] C) → ℝ) :
    (𝔼 Z : PartnerPoint rhs (activeOf J) →ₗ[F2] D,
      𝔼 X : PartnerPoint rhs (activeOf J) →ₗ[F2] C,
        let pi := (PartnerLinear.projection rhs (activeOf J) slot).comp
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerLinear.projection

  5. def OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage line 121

    Source documentation

    The normalized uniform sum on a concrete finite outcome space.

    def uniformAverage {Ω K : Type*} [Fintype Ω] [Field K] (f : Ω → K) : K :=
…
  6. def OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.zeroCount line 125

    Source documentation

    Number of zero columns in an actual coefficient vector.

    def zeroCount {I C : Type*} [Fintype I] [Zero C] [DecidableEq C]
    (omega : I → C) : Nat :=
…
  7. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.power_zeroCount_eq_prod line 129
  8. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.sum_one_zero_weight line 135
  9. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.sum_power_zeroCount line 148

    Source documentation

    The unnormalized count identity, on the actual full product space.

    theorem sum_power_zeroCount {C K : Type*} [Fintype C] [Zero C]
    [DecidableEq C] [Field K] (a : K) (t : Nat) :
    (∑ omega : Fin t → C, a ^ zeroCount omega) =
      ((Fintype.card C : K) + a - 1) ^ t := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.zeroCount

  10. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage_power_zeroCount line 158

    Source documentation

    Exact moment identity for independent uniform coefficients in any finite nonempty zero-pointed space, proved by enumeration and product expansion.

    theorem uniformAverage_power_zeroCount {C K : Type*} [Fintype C] [Zero C]
    [DecidableEq C] [Field K] [CharZero K] (a : K) (t : Nat) :
    uniformAverage (fun omega : Fin t → C => a ^ zeroCount omega) =
      (1 - (1 / (Fintype.card C : K)) * (1 - a)) ^ t := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.zeroCount

  11. abbrev OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.BinaryCoefficient line 173

    Source documentation

    Binary vectors of length m, the actual coefficient alphabet.

    abbrev BinaryCoefficient (m : Nat) := Fin m → ZMod 2
  12. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.card_binaryCoefficient line 175
  13. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniform_binary_coefficient_moment line 180

    Source documentation

    The precise averaging identity from Lemma 6.8, including zero-dimensional coefficient spaces and zero trials.

    theorem uniform_binary_coefficient_moment {K : Type*} [Field K] [CharZero K]
    (a : K) (m t : Nat) :
    uniformAverage (fun omega : Fin t → BinaryCoefficient m => a ^ zeroCount omega) =
      (1 - (1 / 2 : K) ^ m * (1 - a)) ^ t := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.BinaryCoefficient, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.zeroCount

  14. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage_mono line 187
  15. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage_const line 193
  16. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage_prod line 199

    Source documentation

    Iterated averaging equals a single average on the actual product space.

    theorem uniformAverage_prod {Ω Γ K : Type*} [Fintype Ω] [Fintype Γ]
    [Field K] (f : Ω × Γ → K) :
    uniformAverage f = uniformAverage (fun ω => uniformAverage fun γ => f (ω, γ)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage

  17. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage_equiv line 206
  18. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage_product_left line 212
  19. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage_coordinate_product line 218
  20. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage_power_zeroCount_indexed line 228
  21. def OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.splitRawCoefficients line 241
  22. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.zeroSet_card_eq_zeroCount line 262
  23. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniform_raw_coefficient_moment line 272

    Source documentation

    The full raw coefficient tuple includes ζ₀ and both coefficients at every full position. Their uniform averaging cancels exactly; no ignored-coordinate independence premise is needed.

    theorem uniform_raw_coefficient_moment {P C K : Type} [Fintype P] [DecidableEq P]
    [Fintype C] [Zero C] [DecidableEq C] [Field K] [CharZero K]
    (J : Finset P) (a : K) :
    uniformAverage (fun gamma : ConditionalIncidences.RawCoefficients J C =>
      a ^ (ConditionalIncidences.zeroSet J gamma).card) =
      (1 - (1 / (Fintype.card C : K)) * (1 - a)) ^ J.card := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawCoefficients, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.zeroSet

  24. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniform_binary_coefficient_upper line 288

    Source documentation

    Averages an actual pointwise coefficient-dependent upper bound over the uniform product law. No binomial distribution is assumed.

    theorem uniform_binary_coefficient_upper {K : Type*}
    [Field K] [LinearOrder K] [IsStrictOrderedRing K]
    (a : K) (m t : Nat) (success : (Fin t → BinaryCoefficient m) → K)
    (bound : ∀ omega, success omega ≤ a ^ zeroCount omega) :
    uniformAverage success ≤ (1 - (1 / 2 : K) ^ m * (1 - a)) ^ t := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.BinaryCoefficient, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.zeroCount, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.uniformAverage

  25. abbrev OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.PredicateGame line 305
  26. abbrev OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.PredicateStrategies line 306
  27. def OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.predicateGame line 314

    Source documentation

    Pass a Boolean verifier predicate to the already checked deterministic local-reconstruction and incidence-extraction interface.

    def predicateGame (G : Game QA QB A B) : PredicateGame QA QB A B :=
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.PredicateGame

  28. def OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.strategyPair line 317
  29. def OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.weightedGame line 322

    Source documentation

    Interpret a concrete predicate and a normalized finite question law as a game with the common foundation interface.

    def weightedGame (G : PredicateGame QA QB A B)
    (questions : FiniteDistribution (QA × QB)) : Game QA QB A B := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.PredicateGame

  30. def OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.reconstructedGame line 329

    Source documentation

    The reconstructed outer question law is the actual pushforward of the inner question law under the separate local reconstruction functions.

    def reconstructedGame (inner : Game QA QB A B) (outer : PredicateGame OA OB X Y)
    (r : IncidenceExtraction.LocalSimulation (predicateGame inner) outer) :
    Game OA OB X Y :=
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.PredicateGame, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.LocalSimulation, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.predicateGame

  31. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.reconstructedGame_success_le line 337

    Source documentation

    Event containment from IncidenceExtraction becomes an inequality of the actual normalized winning sums. The outer law is constructed, not assumed.

    theorem reconstructedGame_success_le
    (inner : Game QA QB A B) (outer : PredicateGame OA OB X Y)
    (r : IncidenceExtraction.LocalSimulation (predicateGame inner) outer)
    (s : PredicateStrategies OA OB X Y) :
    (reconstructedGame inner outer r).success (strategyPair s) ≤
      inner.success (strategyPair (r.induced s)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.PredicateGame, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.LocalSimulation, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.predicateGame, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.PredicateStrategies, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.reconstructedGame, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.strategyPair

  32. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.reconstructed_repetition_success_le line 356

    Source documentation

    Specialization to the actual parallel game. Its strategy receives each entire question tuple, preserving cross-coordinate local dependence.

    theorem reconstructed_repetition_success_le
    (G : Game QA QB A B) (n : Nat) (outer : PredicateGame OA OB X Y)
    (r : IncidenceExtraction.LocalSimulation (predicateGame (G.repetition n)) outer)
    (s : PredicateStrategies OA OB X Y) :
    (reconstructedGame (G.repetition n) outer r).success (strategyPair s) ≤
      (G.repetition n).success (strategyPair (r.induced s)) :=
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.PredicateGame, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.LocalSimulation, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.predicateGame, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.PredicateStrategies, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.reconstructedGame, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.Simulation.strategyPair

  33. abbrev OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.FirstAnswer line 372
  34. abbrev OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.SecondAnswer line 373
  35. def OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.project line 376

    Source documentation

    Ambient coordinate form of the actual retained-coordinate projection.

    def project {P : Type} (single : P → Bool) (indices : P → Fin 3)
    (answer : FirstAnswer P) : SecondAnswer P :=
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.FirstAnswer, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.SecondAnswer

  36. def OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.accepts line 384

    Source documentation

    A verifier using only the two displayed questions. The retained indices are verifier witnesses compatible with the displayed names, never player inputs. The output equality is the actual projection on all ambient coordinates.

    def accepts {P R O N : Type} (g : Incidence O N) (single : P → Bool)
    (qa : ZeroInformation.FirstInput P R O)
    (qb : ZeroInformation.SecondInput P R O N)
    (answerA : FirstAnswer P) (answerB : SecondAnswer P) : Prop :=
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.ZeroInformation.FirstInput, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.SecondInput, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.FirstAnswer, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.SecondAnswer

  37. def OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.predicateGame line 394
  38. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.actual_partnerProjection_accepts line 403

    Source documentation

    Points satisfying (6.17) satisfy this named verifier: validity comes from the actual first-question equation subspace and agreement from the actual partnerProjection map.

    theorem actual_partnerProjection_accepts
    {P R O N : Type} (g : Incidence O N) (positions : List P)
    (single : P → Bool) (zeta0 : ZeroInformation.Bits R)
    (zeta1 zeta2 omega : P → ZeroInformation.Bits R)
    (occurrences : P → O) (indices : P → Fin 3)
    (point : ZeroInformation.FirstPoint g.rhs occurrences)
    (hone : point.val.1 = true) :
    accepts g single
      (ZeroInformation.firstInput positions single zeta0 zeta1 zeta2 omega
        occurrences indices)
      (ZeroInformation.secondInput positions single zeta0 zeta1 zeta2 omega
        occurrences (fun j => g.name (occurrences j) (indices j)))
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.ZeroInformation.Bits, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.FirstPoint, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.accepts, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.firstInput, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.secondInput

  39. theorem OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.accepts_implies_named_incidence line 422

    Source documentation

    At a single coordinate, actual projection acceptance supplies an accepted named-incidence answer with no access to the retained index.

    theorem accepts_implies_named_incidence
    {P R O N : Type} (g : Incidence O N) (single : P → Bool)
    (qa : ZeroInformation.FirstInput P R O)
    (qb : ZeroInformation.SecondInput P R O N)
    (answerA : FirstAnswer P) (answerB : SecondAnswer P)
    (h : accepts g single qa qb answerA answerB)
    (j : P) (hj : single j = true) (name : N)
    (hname : qb.question j = Sum.inr name) :
    g.namedAccepts (qa.question j) name (answerA.2 j) (answerB.2.2 j) := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.ZeroInformation.FirstInput, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.SecondInput, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.FirstAnswer, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.SecondAnswer, OAI.UniqueGamesTheorem.Soundness.RepeatedGameBounds.ActualProjection.accepts