OAI/Computability/MaxCut/Games/AnswerBridge.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Explicit hidden-coordinate enumeration in the actual conditional law.

  1. abbrev OAI.MaxCutGames.Clean.AnswerBridge.FirstInput line 21
  2. abbrev OAI.MaxCutGames.Clean.AnswerBridge.SecondInput line 22
  3. abbrev OAI.MaxCutGames.Clean.AnswerBridge.SourceAnswer line 24
  4. abbrev OAI.MaxCutGames.Clean.AnswerBridge.TargetAnswer line 25
  5. abbrev OAI.MaxCutGames.Clean.AnswerBridge.PointStrategies line 27
  6. theorem OAI.MaxCutGames.Clean.AnswerBridge.firstAnswer_eq_embed line 32
  7. def OAI.MaxCutGames.Clean.AnswerBridge.toOuterStrategy line 50

    Source documentation

    Convert a pair of genuine local point strategies into the ordinary answer type used by the clean-coordinate local simulation.

    def toOuterStrategy (J : Finset (Fin k)) (g : IncidenceExtraction.Incidence Id Name)
    (strategy : PointStrategies (Q := Q) (Id := Id) (Name := Name) J) :
…

    Mentions: OAI.MaxCutGames.Clean.AnswerBridge.PointStrategies

  8. theorem OAI.MaxCutGames.Clean.AnswerBridge.toOuterStrategy_wins line 63

    Source documentation

    Projection agreement of matrix answers implies the named verifier accepts. No question-law or value assumption occurs in this pointwise bridge.

    theorem toOuterStrategy_wins (J : Finset (Fin k))
    (g : IncidenceExtraction.Incidence Id Name)
    (strategy : PointStrategies (Q := Q) (Id := Id) (Name := Name) J)
…

    Mentions: OAI.MaxCutGames.Clean.AnswerBridge.PointStrategies

  9. def OAI.MaxCutGames.Clean.AnswerBridge.finiteCoordinates line 84

    Source documentation

    A basis supplies the required coordinates for every finite-dimensional combined advice space; this choice is independent of the equation questions.

    def finiteCoordinates [FiniteDimensional F2 D] :
    D ≃ₗ[F2] (Fin (Module.finrank F2 D) → F2) :=
…
  10. def OAI.MaxCutGames.Clean.AnswerBridge.bitsCoordinatesEquiv line 89

    Source documentation

    The coordinate map is a bijection all the way to the actual bit-row type.

    def bitsCoordinatesEquiv (coordinates : D ≃ₗ[F2] (Q → F2)) :
    D ≃ ZeroInformation.Bits Q :=
…
  11. def OAI.MaxCutGames.Clean.AnswerBridge.encodeCoefficients line 93
  12. def OAI.MaxCutGames.Clean.AnswerBridge.coefficientsEquiv line 98
  13. theorem OAI.MaxCutGames.Clean.AnswerBridge.uniform_encoded_coefficients line 104

    Source documentation

    The encoding sends the actual uniform coefficient law to the uniform bit coefficient law, counting every intercept and slope exactly once.

    theorem uniform_encoded_coefficients [Fintype D] [Fintype Q]
    (coordinates : D ≃ₗ[F2] (Q → F2)) (J : Finset (Fin k))
    (F : RawCoefficients J (ZeroInformation.Bits Q) → ℝ) :
    (𝔼 gamma : RawCoefficients J D, F (encodeCoefficients coordinates J gamma)) =
      𝔼 bits : RawCoefficients J (ZeroInformation.Bits Q), F bits :=
…

    Mentions: OAI.MaxCutGames.Clean.AnswerBridge.encodeCoefficients

  14. theorem OAI.MaxCutGames.Clean.AnswerBridge.encoded_map_coefficients line 111
  15. theorem OAI.MaxCutGames.Clean.AnswerBridge.zeroSet_encodeCoefficients line 117

    Source documentation

    Encoding the advice preserves exactly the zero-slope clean set.

    theorem zeroSet_encodeCoefficients [Fintype Q] [DecidableEq Q] [DecidableEq D]
    (coordinates : D ≃ₗ[F2] (Q → F2))
    (J : Finset (Fin k)) (gamma : RawCoefficients J D) :
    zeroSet J (encodeCoefficients coordinates J gamma) = zeroSet J gamma := by
…

    Mentions: OAI.MaxCutGames.Clean.AnswerBridge.encodeCoefficients

  16. def OAI.MaxCutGames.Clean.AnswerBridge.rowPointStrategies line 134

    Source documentation

    Transport a local strategy on genuine row maps to the complete bit-row input type. The same fixed public data may be closed over in both policies. All remaining inputs are private to the respective prover.

    def rowPointStrategies (coordinates : D ≃ₗ[F2] (Q → F2))
    (J : Finset (Fin k)) (rhs : Id → Bool)
    (first : (Fin k → Id) → (ActualHomogeneous.E k →ₗ[F2] D) → SourceAnswer k)
    (second : (Fin k → Sum Id Name) → (RawPoint J →ₗ[F2] D) → TargetAnswer J) :
    PointStrategies (Q := Q) (Id := Id) (Name := Name) J where
…

    Mentions: OAI.MaxCutGames.Clean.AnswerBridge.SourceAnswer, OAI.MaxCutGames.Clean.AnswerBridge.TargetAnswer, OAI.MaxCutGames.Clean.AnswerBridge.PointStrategies

  17. theorem OAI.MaxCutGames.Clean.AnswerBridge.rowPointStrategies_first_actual line 144
  18. theorem OAI.MaxCutGames.Clean.AnswerBridge.rowPointStrategies_second_actual line 166

    Source documentation

    The target policy receives the original target map and displayed question, without an occurrence or selected slot supplied at a singleton coordinate.

    theorem rowPointStrategies_second_actual [Fintype Q] [DecidableEq Q]
    (coordinates : D ≃ₗ[F2] (Q → F2))
    (J : Finset (Fin k)) (rhs : Id → Bool) (names : Id → Fin 3 → Name)
    (first : (Fin k → Id) → (ActualHomogeneous.E k →ₗ[F2] D) → SourceAnswer k)
    (second : (Fin k → Sum Id Name) → (RawPoint J →ₗ[F2] D) → TargetAnswer J)
    (draw : Draw (Fin k) Id) (Y : RawPoint J →ₗ[F2] D) :
    (rowPointStrategies coordinates J rhs first second).second
      (actualSecond J names
        (rowCoefficients J (gammaOfRawMap J (coordinates.toLinearMap.comp Y))) draw) =
      second
        (actualSecond J names
          (rowCoefficients J (gammaOfRawMap J (coordinates.toLinearMap.comp Y))) draw).question
…

    Mentions: OAI.MaxCutGames.Clean.AnswerBridge.SourceAnswer, OAI.MaxCutGames.Clean.AnswerBridge.TargetAnswer, OAI.MaxCutGames.Clean.AnswerBridge.rowPointStrategies

  19. def OAI.MaxCutGames.Clean.AnswerBridge.defaultTargetAnswer line 189

    Source documentation

    A default actual target answer is used only for unsupported displayed questions, which never occur in the experiment.

    def defaultTargetAnswer (J : Finset (Fin k)) : TargetAnswer J :=
…

    Mentions: OAI.MaxCutGames.Clean.AnswerBridge.TargetAnswer

  20. def OAI.MaxCutGames.Clean.AnswerBridge.extendSupportedPolicy line 194

    Source documentation

    Extend a policy defined on supported private questions to a total local answer function. The support decision uses only the displayed question.

    def extendSupportedPolicy (J : Finset (Fin k)) (names : Id → Fin 3 → Name)
    (policy : RawPrivateTable.SupportedV J names → (RawPoint J →ₗ[F2] D) → TargetAnswer J)
    (question : Fin k → Sum Id Name) (Y : RawPoint J →ₗ[F2] D) : TargetAnswer J :=
…

    Mentions: OAI.MaxCutGames.Clean.AnswerBridge.TargetAnswer

  21. theorem OAI.MaxCutGames.Clean.AnswerBridge.extendSupportedPolicy_apply line 201
  22. def OAI.MaxCutGames.Soundness.ConditionalIncidences.coordinateReindex line 217
  23. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.raw_conditional_incidence_reindex line 227
  24. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.raw_conditional_event_reindex_real line 247
  25. def OAI.MaxCutGames.Clean.ProductLaw.splitCoordinates line 292

    Source documentation

    Restriction to the clean and nonclean coordinates is a genuine bijection.

    def splitCoordinates (K : Finset P) :
    (P → Q) ≃ (PositionInside K → Q) × (PositionOutside K → Q) :=
…
  26. theorem OAI.MaxCutGames.Clean.ProductLaw.table_split line 298

    Source documentation

    Independent weighted sampling splits into independent clean and nonclean parts. This identity proves, rather than assumes, their independence.

    theorem table_split (μ : P → FiniteDistribution Q) (K : Finset P) :
    (FiniteDistribution.table μ).transport (splitCoordinates K) =
      (FiniteDistribution.table (fun i : PositionInside K => μ i.val)).product
        (FiniteDistribution.table (fun i : PositionOutside K => μ i.val)) := by
…

    Mentions: OAI.MaxCutGames.Clean.ProductLaw.splitCoordinates

  27. theorem OAI.MaxCutGames.Clean.ProductLaw.probability_product_and line 322
  28. theorem OAI.MaxCutGames.Clean.ProductLaw.probability_product_right line 339
  29. theorem OAI.MaxCutGames.Clean.ProductLaw.table_inside_outside line 346

    Source documentation

    Exact factorization for an arbitrary joint event of clean coordinates and an arbitrary observation/event depending only on the nonclean coordinates.

    theorem table_inside_outside (μ : P → FiniteDistribution Q) (K : Finset P)
    (event : (PositionInside K → Q) → Bool)
    (given : (PositionOutside K → Q) → Bool) :
    (FiniteDistribution.table μ).probability
        (fun x => event (fun i => x i.val) && given (fun i => x i.val)) =
      (FiniteDistribution.table (fun i : PositionInside K => μ i.val)).probability event *
        (FiniteDistribution.table (fun i : PositionOutside K => μ i.val)).probability given := by
…
  30. theorem OAI.MaxCutGames.Clean.ProductLaw.table_outside line 357
  31. theorem OAI.MaxCutGames.Clean.ProductLaw.conditioned_inside line 365

    Source documentation

    The normalized conditional law is the ordinary independent product law. The only hypothesis is that the observed outside event has positive mass.

    theorem conditioned_inside (μ : P → FiniteDistribution Q) (K : Finset P)
    (given : (PositionOutside K → Q) → Bool)
    (positive : 0 < (FiniteDistribution.table μ).probability
      (fun x => given (fun i => x i.val)))
    (event : (PositionInside K → Q) → Bool) :
    ((FiniteDistribution.table μ).condition
      (fun x => given (fun i => x i.val)) positive).probability
        (fun x => event (fun i => x i.val)) =
      (FiniteDistribution.table (fun i : PositionInside K => μ i.val)).probability event := by
…
  32. theorem OAI.MaxCutGames.Clean.ProductLaw.seeded_inside_outside line 386

    Source documentation

    Fixing an independently sampled seed additionally exposes the intercept and all slope data, without exposing any of the clean questions. The seed's mass and the outside-observation mass factor off from every clean event.

    theorem seeded_inside_outside (ν : FiniteDistribution S)
    (μ : P → FiniteDistribution Q) (seed : S) (K : Finset P)
    (given : (PositionOutside K → Q) → Bool)
    (event : (PositionInside K → Q) → Bool) :
    (ν.product (FiniteDistribution.table μ)).probability
      (fun x => (decide (x.1 = seed) && given (fun i => x.2 i.val)) &&
        event (fun i => x.2 i.val)) =
      (FiniteDistribution.table (fun i : PositionInside K => μ i.val)).probability event *
        (ν.weight seed *
          (FiniteDistribution.table (fun i : PositionOutside K => μ i.val)).probability given) := by
…
  33. theorem OAI.MaxCutGames.Clean.ProductLaw.conditioned_seed_inside line 410

    Source documentation

    Public conditioning on the independently generated advice, including its intercept, and on arbitrary nonclean question data leaves the weighted clean product law unchanged. K may be any function of seed; it is fixed here after the public seed has been exposed.

    theorem conditioned_seed_inside (ν : FiniteDistribution S)
    (μ : P → FiniteDistribution Q) (seed : S) (K : Finset P)
    (given : (PositionOutside K → Q) → Bool)
    (positive : 0 < (ν.product (FiniteDistribution.table μ)).probability
      (fun x => decide (x.1 = seed) && given (fun i => x.2 i.val)))
    (event : (PositionInside K → Q) → Bool) :
    ((ν.product (FiniteDistribution.table μ)).condition
      (fun x => decide (x.1 = seed) && given (fun i => x.2 i.val)) positive).probability
        (fun x => event (fun i => x.2 i.val)) =
      (FiniteDistribution.table (fun i : PositionInside K => μ i.val)).probability event := by
…
  34. theorem OAI.MaxCutGames.Clean.ProductLaw.table_reindex line 426

    Source documentation

    Reindexing a finite coordinate set gives the usual iid law on Fin r.

    theorem table_reindex (μ : FiniteDistribution Q) {A : Type} [Fintype A] [DecidableEq A]
    {r : ℕ} (e : Fin r ≃ A) :
    (FiniteDistribution.table (fun _ : A => μ)).transport (coordinateReindex e) =
      μ.iid r := by
…
  35. theorem OAI.MaxCutGames.Clean.ProductLaw.conditioned_incidence_reindex line 437

    Source documentation

    Fixed advice, intercept and nonclean data preserve precisely the repeated incidence law for arbitrary occurrence weights. Repeated IDs are permitted.

    theorem conditioned_incidence_reindex
    {O N D : Type} [Fintype O] [DecidableEq O] [Fintype N] [DecidableEq N]
    [Zero D] [DecidableEq D]
    (μ : FiniteDistribution (O × Fin 3))
    (J : Finset P) (name : O → Fin 3 → N) (gamma : RawCoefficients J D)
    (observed : PositionOutside (zeroSet J gamma) → O × N)
    (positive : 0 < (FiniteDistribution.table (fun _ : P => μ)).probability
      (fun x => decide (outsideRecord (zeroSet J gamma) name x = observed)))
    {r : ℕ} (e : Fin r ≃ PositionInside (zeroSet J gamma))
    (event : (Fin r → O × N) → Bool) :
    ((FiniteDistribution.table (fun _ : P => μ)).condition
      (fun x => decide (outsideRecord (zeroSet J gamma) name x = observed))
…
  36. theorem OAI.MaxCutGames.Clean.ProductLaw.conditioned_incidence_distribution line 466

    Source documentation

    Equality of the complete conditional question distribution, not only its individual marginals. The target is the ordinary repeated incidence law.

    theorem conditioned_incidence_distribution
    {O N D : Type} [Fintype O] [DecidableEq O] [Fintype N] [DecidableEq N]
    [Zero D] [DecidableEq D]
    (μ : FiniteDistribution (O × Fin 3))
    (J : Finset P) (name : O → Fin 3 → N) (gamma : RawCoefficients J D)
    (observed : PositionOutside (zeroSet J gamma) → O × N)
    (positive : 0 < (FiniteDistribution.table (fun _ : P => μ)).probability
      (fun x => decide (outsideRecord (zeroSet J gamma) name x = observed)))
    {r : ℕ} (e : Fin r ≃ PositionInside (zeroSet J gamma)) :
    (((FiniteDistribution.table (fun _ : P => μ)).condition
      (fun x => decide (outsideRecord (zeroSet J gamma) name x = observed))
        positive).pushforward
…
  37. theorem OAI.MaxCutGames.Clean.ProductLaw.clean_mask_independent line 500

    Source documentation

    A clean-mask rule reads only the independent advice seed. Thus even after fixing the entire question tuple, its distribution is unchanged. The seed may include the projection mask, all slope columns, and the independent intercept.

    theorem clean_mask_independent (ν : FiniteDistribution S)
    (μ : FiniteDistribution Q) (clean : S → Finset P) (K : Finset P)
    (questionEvent : Q → Bool) :
    (ν.product μ).probability (fun x => decide (clean x.1 = K) && questionEvent x.2) =
      ν.probability (fun s => decide (clean s = K)) * μ.probability questionEvent := by
…
  38. def OAI.MaxCutGames.Clean.WeightedPartition.fibre line 525
  39. theorem OAI.MaxCutGames.Clean.WeightedPartition.sum_fibre_inter line 528
  40. theorem OAI.MaxCutGames.Clean.WeightedPartition.sum_fibre_bound line 539
  41. theorem OAI.MaxCutGames.Clean.WeightedPartition.probability_le_conditional_bounds line 554

    Source documentation

    The averaging step for a genuine weighted observation. No conditional independence or law-of-total-probability equality is supplied as a premise.

    theorem probability_le_conditional_bounds (μ : FiniteDistribution Ω)
    (observe : Ω → H) (event : Ω → Bool) (bound : H → ℝ)
    (conditional : ∀ h (positive : 0 < μ.probability (fibre observe h)),
      (μ.condition (fibre observe h) positive).probability event ≤ bound h) :
    μ.probability event ≤ μ.expectation (fun x => bound (observe x)) := by
…

    Mentions: OAI.MaxCutGames.Clean.WeightedPartition.fibre

  42. theorem OAI.MaxCutGames.Clean.WeightedPartition.probability_le_of_conditional_le line 571

    Source documentation

    A constant bound survives arbitrary public outside observations.

    theorem probability_le_of_conditional_le (μ : FiniteDistribution Ω)
    (observe : Ω → H) (event : Ω → Bool) (bound : ℝ)
    (conditional : ∀ h (positive : 0 < μ.probability (fibre observe h)),
      (μ.condition (fibre observe h) positive).probability event ≤ bound) :
    μ.probability event ≤ bound := by
…

    Mentions: OAI.MaxCutGames.Clean.WeightedPartition.fibre

  43. instance OAI.MaxCutGames.Soundness.ConditionalSimulation.firstInputFintype line 599
  44. instance OAI.MaxCutGames.Soundness.ConditionalSimulation.secondInputFintype line 608
  45. def OAI.MaxCutGames.Soundness.ConditionalSimulation.incidenceGame line 618
  46. def OAI.MaxCutGames.Soundness.ConditionalSimulation.actualLocalSimulation line 623
  47. theorem OAI.MaxCutGames.Soundness.ConditionalSimulation.actual_conditioned_strategy_success_le_repeated_value line 661
  48. theorem OAI.MaxCutGames.Soundness.ConditionalGameLaw.uniform_probability_decide line 698
  49. abbrev OAI.MaxCutGames.Soundness.ConditionalGameLaw.OuterStrategy line 716
  50. def OAI.MaxCutGames.Soundness.ConditionalGameLaw.actualWin line 720
  51. def OAI.MaxCutGames.Soundness.ConditionalGameLaw.conditionedWinProbability line 726
  52. def OAI.MaxCutGames.Soundness.ConditionalGameLaw.reconstructedEvent line 736
  53. theorem OAI.MaxCutGames.Soundness.ConditionalGameLaw.actualWin_iff_reconstructedEvent line 748
  54. theorem OAI.MaxCutGames.Soundness.ConditionalGameLaw.conditionedWinProbability_eq_fresh line 765
  55. def OAI.MaxCutGames.Soundness.ConditionalGameLaw.incidenceLaw line 787
  56. theorem OAI.MaxCutGames.Soundness.ConditionalGameLaw.reconstructed_success_eq_fresh_average line 790
  57. theorem OAI.MaxCutGames.Soundness.ConditionalGameLaw.conditioned_probability_le_repeated_value line 827

    Source documentation

    The actual finite observation-fibre probability is bounded by the genuine repeated incidence-game value. The sampling identity is proved internally.

    theorem conditioned_probability_le_repeated_value [Nonempty O]
    (J : Finset P) (g : Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R))
    (observed : PositionOutside (zeroSet J gamma) → O × N)
    (reference : RawObservationFibre J g.name gamma observed)
    (e : Fin (zeroSet J gamma).card ≃ PositionInside (zeroSet J gamma))
    (strategy : OuterStrategy (P := P) (R := R) (O := O) (N := N))
…

    Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.Bits, OAI.MaxCutGames.Soundness.ConditionalGameLaw.OuterStrategy