AnswerBridge.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.UniqueGamesTheorem.Clean.AnswerBridge.FirstInput line 21
abbrev OAI.UniqueGamesTheorem.Clean.AnswerBridge.SecondInput line 22
abbrev OAI.UniqueGamesTheorem.Clean.AnswerBridge.SourceAnswer line 24
abbrev OAI.UniqueGamesTheorem.Clean.AnswerBridge.TargetAnswer line 25
abbrev OAI.UniqueGamesTheorem.Clean.AnswerBridge.PointStrategies line 27
theorem OAI.UniqueGamesTheorem.Clean.AnswerBridge.firstAnswer_eq_embed line 32
def OAI.UniqueGamesTheorem.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.UniqueGamesTheorem.Clean.AnswerBridge.PointStrategies
theorem OAI.UniqueGamesTheorem.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.UniqueGamesTheorem.Clean.AnswerBridge.PointStrategies
def OAI.UniqueGamesTheorem.Clean.AnswerBridge.finiteCoordinates line 86
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) :=
…
```
def OAI.UniqueGamesTheorem.Clean.AnswerBridge.bitsCoordinatesEquiv line 91
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 :=
…
```
def OAI.UniqueGamesTheorem.Clean.AnswerBridge.encodeCoefficients line 95
def OAI.UniqueGamesTheorem.Clean.AnswerBridge.coefficientsEquiv line 100

theorem OAI.UniqueGamesTheorem.Clean.AnswerBridge.uniform_encoded_coefficients line 106

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.UniqueGamesTheorem.Clean.AnswerBridge.encodeCoefficients

theorem OAI.UniqueGamesTheorem.Clean.AnswerBridge.encoded_map_coefficients line 113

theorem OAI.UniqueGamesTheorem.Clean.AnswerBridge.zeroSet_encodeCoefficients line 119

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.UniqueGamesTheorem.Clean.AnswerBridge.encodeCoefficients

def OAI.UniqueGamesTheorem.Clean.AnswerBridge.rowPointStrategies line 136
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.UniqueGamesTheorem.Clean.AnswerBridge.SourceAnswer, OAI.UniqueGamesTheorem.Clean.AnswerBridge.TargetAnswer, OAI.UniqueGamesTheorem.Clean.AnswerBridge.PointStrategies
theorem OAI.UniqueGamesTheorem.Clean.AnswerBridge.rowPointStrategies_first_actual line 146

theorem OAI.UniqueGamesTheorem.Clean.AnswerBridge.rowPointStrategies_second_actual line 168

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.UniqueGamesTheorem.Clean.AnswerBridge.SourceAnswer, OAI.UniqueGamesTheorem.Clean.AnswerBridge.TargetAnswer, OAI.UniqueGamesTheorem.Clean.AnswerBridge.rowPointStrategies

def OAI.UniqueGamesTheorem.Clean.AnswerBridge.defaultTargetAnswer line 191
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.UniqueGamesTheorem.Clean.AnswerBridge.TargetAnswer
def OAI.UniqueGamesTheorem.Clean.AnswerBridge.extendSupportedPolicy line 196
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.UniqueGamesTheorem.Clean.AnswerBridge.TargetAnswer
theorem OAI.UniqueGamesTheorem.Clean.AnswerBridge.extendSupportedPolicy_apply line 203