LocalReplay.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

Side-local replay of vanishing advice

The input-reconstruction step reuses the elementary observation-fibre and Boolean-row infrastructure, not a repetition bound or any inverse theorem. The row index may be a disjoint union, so a single row below represents both visible advice maps simultaneously.

We explicitly pass from the three equation bits to the two free homogeneous coordinates. The third position contributes b * d to the intercept and d to both slopes. At a clean position all three contributions vanish. The replay constructors take only the respective prover's clean questions; their correctness is proved as equality of the complete question-and-row input.

def OAI.UniqueGamesTheorem.Clean.LocalReplay.equationBit line 33
Source documentation
The three actual equation coordinates, including the homogeneous term.
```
def equationBit (b t x y : Bool) (i : Fin 3) : Bool :=
…
```
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.equationBit_satisfies line 36
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.equationBit_reconstruct line 43
Source documentation
The two free coordinates parameterize the entire homogeneous equation space, not just its actual-answer slice t = true.
```
theorem equationBit_reconstruct (b t : Bool) (x : Fin 3 → Bool)
    (h : (x 0 ^^ x 1 ^^ x 2) = (b && t)) :
    equationBit b t (x 0) (x 1) = x := by
…
```
Mentions: OAI.UniqueGamesTheorem.Clean.LocalReplay.equationBit
def OAI.UniqueGamesTheorem.Clean.LocalReplay.singletonSlope₀ line 56
Source documentation
Pullback of a singleton column to the first free equation coordinate.
```
def singletonSlope₀ (d : ZeroInformation.Bits R) (i : Fin 3) : ZeroInformation.Bits R :=
…
```
def OAI.UniqueGamesTheorem.Clean.LocalReplay.singletonSlope₁ line 60
Source documentation
Pullback of a singleton column to the second free equation coordinate.
```
def singletonSlope₁ (d : ZeroInformation.Bits R) (i : Fin 3) : ZeroInformation.Bits R :=
…
```
def OAI.UniqueGamesTheorem.Clean.LocalReplay.singletonIntercept line 64
Source documentation
Only the third position changes the homogeneous intercept.
```
def singletonIntercept (d : ZeroInformation.Bits R) (i : Fin 3) (b : Bool) : ZeroInformation.Bits R :=
…
```
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.singleton_pullback line 67
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.singletonSlope₀_zero line 77
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.singletonSlope₁_zero line 81
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.singletonIntercept_zero line 85

theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.third_position_clean line 91

Source documentation

In particular the third-position right-hand side cannot survive a zero singleton slope, even on arbitrary homogeneous vectors.

theorem third_position_clean (b t x y : Bool) :
    ZeroInformation.scale (ZeroInformation.zero : ZeroInformation.Bits R) (equationBit b t x y 2) = ZeroInformation.zero ∧
      singletonIntercept (ZeroInformation.zero : ZeroInformation.Bits R) 2 b = ZeroInformation.zero ∧
      singletonSlope₀ (ZeroInformation.zero : ZeroInformation.Bits R) 2 = ZeroInformation.zero ∧
      singletonSlope₁ (ZeroInformation.zero : ZeroInformation.Bits R) 2 = ZeroInformation.zero := by
…

Mentions: OAI.UniqueGamesTheorem.Clean.LocalReplay.equationBit, OAI.UniqueGamesTheorem.Clean.LocalReplay.singletonIntercept, OAI.UniqueGamesTheorem.Clean.LocalReplay.singletonSlope₀, OAI.UniqueGamesTheorem.Clean.LocalReplay.singletonSlope₁

theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.add_zero line 98
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.zero_add line 103
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.add_assoc line 108
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.add_shuffle line 114
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.scale_add line 120
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.rowSum_add line 126
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.rowSum_scale line 139
def OAI.UniqueGamesTheorem.Clean.LocalReplay.interceptContribution line 150
def OAI.UniqueGamesTheorem.Clean.LocalReplay.paddedIntercept line 154
def OAI.UniqueGamesTheorem.Clean.LocalReplay.paddedSlope₀ line 158
def OAI.UniqueGamesTheorem.Clean.LocalReplay.paddedSlope₁ line 162

theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.full_padded_pullback line 168

Source documentation

The full affine pullback, with the original intercept appearing exactly once and every third-position correction explicitly included.

theorem full_padded_pullback (positions : List P) (single : P → Bool)
    (c : ZeroInformation.Bits R) (f₀ f₁ d : P → ZeroInformation.Bits R) (indices : P → Fin 3)
    (rhs : P → Bool) (t : Bool) (xy : P → Fin 2 → Bool) :
    ZeroInformation.pullbackRow positions single c f₀ f₁ d indices t
        (fun j => equationBit (rhs j) t (xy j 0) (xy j 1)) =
      ZeroInformation.add (ZeroInformation.scale (paddedIntercept positions single c d indices rhs) t)
        (ZeroInformation.rowSum positions fun j =>
          ZeroInformation.add (ZeroInformation.scale (paddedSlope₀ single f₀ d indices j) (xy j 0))
            (ZeroInformation.scale (paddedSlope₁ single f₁ d indices j) (xy j 1))) := by
…

Mentions: OAI.UniqueGamesTheorem.Clean.LocalReplay.equationBit, OAI.UniqueGamesTheorem.Clean.LocalReplay.paddedIntercept, OAI.UniqueGamesTheorem.Clean.LocalReplay.paddedSlope₀, OAI.UniqueGamesTheorem.Clean.LocalReplay.paddedSlope₁

theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.clean_padded_columns line 193
structure OAI.UniqueGamesTheorem.Clean.LocalReplay.EquationInput line 206
Source documentation
The equation player's canonical two-free-coordinate advice input.
```
structure EquationInput (P R O : Type) where
…
```
structure OAI.UniqueGamesTheorem.Clean.LocalReplay.VariableInput line 212
Source documentation
The variable player's input contains full occurrences or variable names, with no occurrence attached to a singleton name.
```
structure VariableInput (P R O N : Type) where
…
```
def OAI.UniqueGamesTheorem.Clean.LocalReplay.EquationInput.ofAmbient line 216
def OAI.UniqueGamesTheorem.Clean.LocalReplay.VariableInput.ofAmbient line 221
def OAI.UniqueGamesTheorem.Clean.LocalReplay.actualEquationInput line 233
def OAI.UniqueGamesTheorem.Clean.LocalReplay.actualVariableInput line 236
def OAI.UniqueGamesTheorem.Clean.LocalReplay.replayEquationInput line 241
Source documentation
The reference is fixed public advice. The only remaining argument contains the equation player's own clean equations; it contains no selected positions.
```
def replayEquationInput (reference : RawObservationFibre J name gamma observed)
    (insideEquations : PositionInside (zeroSet J gamma) → O) : EquationInput P R O :=
…
```
Mentions: OAI.UniqueGamesTheorem.Clean.LocalReplay.EquationInput
def OAI.UniqueGamesTheorem.Clean.LocalReplay.replayVariableInput line 247
Source documentation
The only remaining argument contains the variable player's own clean names; it contains no clean equation or right-hand side.
```
def replayVariableInput (reference : RawObservationFibre J name gamma observed)
    (insideNames : PositionInside (zeroSet J gamma) → N) : VariableInput P R O N :=
…
```
Mentions: OAI.UniqueGamesTheorem.Clean.LocalReplay.VariableInput
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.replayEquationInput_correct line 251
theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.replayVariableInput_correct line 261

theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.equation_input_independent_of_clean_positions line 271

Source documentation

Equality of the equation player's own remaining questions implies equality of its complete actual input, regardless of the clean selected positions.

theorem equation_input_independent_of_clean_positions
    (distinct : ∀ o i i', name o i = name o i' → i = i')
    (reference sample sample' : RawObservationFibre J name gamma observed)
    (sameEquations : ∀ j : PositionInside (zeroSet J gamma),
      (sample.val.2 j.val).1 = (sample'.val.2 j.val).1) :
    actualEquationInput J rhs gamma sample.val.2 =
      actualEquationInput J rhs gamma sample'.val.2 := by
…

Mentions: OAI.UniqueGamesTheorem.Clean.LocalReplay.actualEquationInput

theorem OAI.UniqueGamesTheorem.Clean.LocalReplay.variable_input_independent_of_clean_equations line 286

Source documentation

Equality of the variable player's own remaining questions implies equality of its complete actual input, regardless of the clean equations.

theorem variable_input_independent_of_clean_equations
    (reference sample sample' : RawObservationFibre J name gamma observed)
    (sameNames : ∀ j : PositionInside (zeroSet J gamma),
      name (sample.val.2 j.val).1 (sample.val.2 j.val).2 =
        name (sample'.val.2 j.val).1 (sample'.val.2 j.val).2) :
    actualVariableInput J name gamma sample.val.2 =
      actualVariableInput J name gamma sample'.val.2 := by
…

Mentions: OAI.UniqueGamesTheorem.Clean.LocalReplay.actualVariableInput