TableKeysLemmas.lean`

73 declarations, 0 contain sorry, 0 declared as axioms

Exact affine-table keys for outer questions

The retained data has one entry at every original block position. A full entry contains the equation occurrence ID, a singleton entry contains the actual variable ID, and the first component is the entire reduced affine intercept. The common coefficient-normalization implementation below is independent of every latent-gadget existence or inverse theorem.

The explicit binary slope cases justify its use for the rank-zero, rank-one, and rank-two rule. In particular, the third-position pullback adds the parity intercept twice, so exact sharing preserves the intercept as well as the slopes.

def OAI.UniqueGamesTheorem.Decoder.TableKeys.slope line 43
Source documentation
The free-coordinate block slope (x,y) ↦ x • a + y • d.
```
def slope (a d : R) : (F2 × F2) →ₗ[F2] R :=
…
```
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.slope_apply line 48
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.slope_zero_iff line 52
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.slope_injective line 66
Source documentation
Over the binary field, the remaining case really is a rank-two slope: the two-coordinate map is injective, rather than merely syntactically full.
```
theorem slope_injective (a d : R) (ha : a ≠ 0) (hd : d ≠ 0) (had : a ≠ d) :
    Function.Injective (slope a d) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeys.slope
def OAI.UniqueGamesTheorem.Decoder.TableKeys.freeTriple line 86
def OAI.UniqueGamesTheorem.Decoder.TableKeys.reduceBlock line 89
Source documentation
A single block's intercept correction and tagged retained record.
```
def reduceBlock (names : Id → Fin 3 → Name) (rhs : Id → F2)
    (e : Id) (a d : R) : R × ActualCanonical.Record Name Id R :=
…
```
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.reduceBlock_zero line 94
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.reduceBlock_first line 99
Source documentation
The first rank-one direction uses the actual first variable.
```
theorem reduceBlock_first (names : Id → Fin 3 → Name) (rhs : Id → F2)
    (e : Id) (a : R) (ha : a ≠ 0) :
    reduceBlock names rhs e a 0 = (0, .single (names e 0) a) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeys.reduceBlock
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.reduceBlock_second line 105
Source documentation
The second rank-one direction uses the actual second variable.
```
theorem reduceBlock_second (names : Id → Fin 3 → Name) (rhs : Id → F2)
    (e : Id) (d : R) (hd : d ≠ 0) :
    reduceBlock names rhs e 0 d = (0, .single (names e 1) d) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeys.reduceBlock
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.reduceBlock_third line 113
Source documentation
The third rank-one direction uses the actual third bit and adjusts the homogeneous intercept by the parity bit times the nonzero slope.
```
theorem reduceBlock_third (names : Id → Fin 3 → Name) (rhs : Id → F2)
    (e : Id) (a : R) (ha : a ≠ 0) :
    reduceBlock names rhs e a a = (rhs e • a, .single (names e 2) a) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeys.reduceBlock
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.reduceBlock_full line 119
Source documentation
A genuine rank-two block retains its occurrence ID and both ordered slopes.
```
theorem reduceBlock_full (names : Id → Fin 3 → Name) (rhs : Id → F2)
    (e : Id) (a d : R) (ha : a ≠ 0) (hd : d ≠ 0) (had : a ≠ d) :
    reduceBlock names rhs e a d = (0, .full e (freeTriple a d)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeys.reduceBlock, OAI.UniqueGamesTheorem.Decoder.TableKeys.freeTriple
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.third_intercept_cancels line 130
Source documentation
Pulling an actual third-bit table back adds b • a to its intercept; reducing the rank-one slope adds exactly the same quantity a second time.
```
theorem third_intercept_cancels (z a : R) (b : F2) :
    (z + b • a) + b • a = z := by
…
```
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.third_key_cancels line 134
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.full_record_occurrence_injective line 144
Source documentation
The reduced representation never merges two distinct occurrence IDs in the full-block case.
```
theorem full_record_occurrence_injective {e e' : Id} {a a' : Fin 3 → R}
    (h : (ActualCanonical.Record.full e a : ActualCanonical.Record Name Id R) =
      .full e' a') : e = e' := by
…
```
abbrev OAI.UniqueGamesTheorem.Decoder.TableKeys.Key line 157
def OAI.UniqueGamesTheorem.Decoder.TableKeys.key line 159
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.key_data_ext_iff line 165
Source documentation
Key equality includes the affine intercept and every original position.
```
theorem key_data_ext_iff (a b : Key k Name Id R) :
    a = b ↔ a.1 = b.1 ∧ ∀ j : Fin k, a.2 j = b.2 j := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeys.Key
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.key_shift line 173

theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.key_shift_free line 180

Source documentation

Translation of the entire reduced affine table is a free action.

theorem key_shift_free (occ : Fin k → Id) (names : Id → Fin 3 → Name) (rhs : Id → F2)
    (P : ActualHomogeneous.E k →ₗ[F2] R) (c : R)
    (h : key occ names rhs (P + ActualHomogeneous.tau.smulRight c) =
      key occ names rhs P) : c = 0 := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeys.key

theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.projected_key_sharing line 193

Source documentation

Every displayed singleton is its actual bit, including the affine parity intercept in position three. Hidden occurrence IDs are forgotten precisely at singleton positions and retained at full positions.

theorem projected_key_sharing
    (J : Finset (Fin k)) (names : Id → Fin 3 → Name) (rhs : Id → F2)
    (occ occ' : Fin k → Id) (slot slot' : Fin k → PartnerProjection.Slot)
    (Y : RawPartnerTarget.RawPoint J →ₗ[F2] R)
    (h : RawPrivateTable.displayed J names occ slot =
      RawPrivateTable.displayed J names occ' slot') :
    key occ names rhs (Y.comp (RawPrivateTable.projection J rhs occ slot)) =
      key occ' names rhs (Y.comp (RawPrivateTable.projection J rhs occ' slot')) :=
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeys.key

def OAI.UniqueGamesTheorem.Decoder.TableKeys.projectedKey line 205
Source documentation
The reduced table attached to visible data is independent of the compatible full question used to realize it. This is equality of the entire key.
```
noncomputable def projectedKey (J : Finset (Fin k)) (names : Id → Fin 3 → Name) (rhs : Id → F2)
    (Q : RawPrivateTable.SupportedV J names) (Y : RawPartnerTarget.RawPoint J →ₗ[F2] R) :
    Key k Name Id R :=
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeys.Key
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.projectedKey_pullback line 212
def OAI.UniqueGamesTheorem.Decoder.TableKeys.visibleTau line 239
Source documentation
Read the shared homogeneous coordinate in the visible coordinate system.
```
def visibleTau (J : Finset (Fin k)) : RawPartnerTarget.RawPoint J →ₗ[F2] F2 :=
…
```
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.projection_surjective line 244
Source documentation
Every visible valid answer extends to an answer of each compatible full question. This proves surjectivity of the actual affine-coordinate projection.
```
theorem projection_surjective (J : Finset (Fin k)) (rhs : Id → F2)
    (occ : Fin k → Id) (slot : Fin k → PartnerProjection.Slot) :
    Function.Surjective (RawPrivateTable.projection J rhs occ slot) := by
…
```
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.projection_preserves_homogeneous line 252

theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.visible_table_unique line 261

Source documentation

Equality after pullback is equality of the entire visible linear extension, so no affine intercept or hidden coefficient can be lost by sharing.

theorem visible_table_unique (J : Finset (Fin k)) (rhs : Id → F2)
    (occ : Fin k → Id) (slot : Fin k → PartnerProjection.Slot)
    (Y Z : RawPartnerTarget.RawPoint J →ₗ[F2] R)
    (h : Y.comp (RawPrivateTable.projection J rhs occ slot) =
      Z.comp (RawPrivateTable.projection J rhs occ slot)) : Y = Z := by
…

theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.pullback_shift line 271

theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.projectedKey_shift line 287

Source documentation

Constant translation commutes with exact sharing at the level of whole reduced keys, including the removed alphabet component of the intercept.

theorem projectedKey_shift (J : Finset (Fin k)) (names : Id → Fin 3 → Name)
    (rhs : Id → F2) (Q : RawPrivateTable.SupportedV J names)
    (Y : RawPartnerTarget.RawPoint J →ₗ[F2] R) (c : R) :
    projectedKey J names rhs Q (Y + (visibleTau J).smulRight c) =
      ((projectedKey J names rhs Q Y).1 + c, (projectedKey J names rhs Q Y).2) := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeys.projectedKey, OAI.UniqueGamesTheorem.Decoder.TableKeys.visibleTau

structure OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.FullAdvice line 326
Source documentation
The first prover's entire information; no singleton-choice or private matrix field is present.
```
structure FullAdvice where
…
```
structure OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw line 333
Source documentation
The actual draw before forgetting the hidden projection and private map.
```
structure Draw where
…
```
structure OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.ProjectedAdvice line 347
Source documentation
The second prover sees actual equation/variable tags, retaining ordered block positions but omitting every hidden singleton occurrence ID.
```
structure ProjectedAdvice (J : Finset (Fin k)) where
…
```
def OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.projection line 355
def OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.leftObservation line 359
def OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.rightObservation line 365
def OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.paddedMatrix line 375
Source documentation
The same full sampled table used in the unconditional variation comparison. Its projection choices have not been supplied as extra compared coordinates.
```
def paddedMatrix (d : Draw k Id K W R) : ActualHomogeneous.E k →ₗ[F2] K :=
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw
def OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.paddedComplement line 378
theorem OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.left_rows_eq line 381
theorem OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.left_rows_attainable line 384
theorem OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.right_rows_attainable line 389
def OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.changeHidden line 396
Source documentation
Replace the entire hidden matrix once, consistently across all overlapping column events; the row advice remains fixed.
```
def changeHidden (d : Draw k Id K W R)
    (N : RawPartnerTarget.RawPoint d.singletons →ₗ[F2] d.rowMap.ker) : Draw k Id K W R :=
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw
theorem OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.leftObservation_changeHidden line 400
theorem OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.rightObservation_changeHidden line 405
theorem OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.selectedWitness_changeHidden line 412
Source documentation
A selected affine witness is fixed by the first player's observation, before any hidden matrix on its row fiber is sampled.
```
theorem selectedWitness_changeHidden {Witness : Type*}
    (choose : FullAdvice k Id K W R → Witness) (d : Draw k Id K W R)
    (N : RawPartnerTarget.RawPoint d.singletons →ₗ[F2] d.rowMap.ker) :
    choose (leftObservation rhs (changeHidden d N)) = choose (leftObservation rhs d) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.FullAdvice, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.leftObservation, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.changeHidden
theorem OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.projection_actual_answer line 419
Source documentation
Every projected answer keeps the actual homogeneous bit.
```
theorem projection_actual_answer (d : Draw k Id K W R)
    (z : ActualHomogeneous.E k) (hz : ActualHomogeneous.tau z = 1) :
    TableKeys.visibleTau d.singletons (projection rhs d z) = 1 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw, OAI.UniqueGamesTheorem.Decoder.TableKeys.visibleTau, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.projection
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.slope_rank_zero line 439
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.slope_rank_first line 444
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.slope_rank_second line 458
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.slope_rank_third line 472
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.slope_rank_two line 487
theorem OAI.UniqueGamesTheorem.Decoder.TableKeys.slope_rank_one_iff line 494
Source documentation
These cases exhaust all slopes; no unexamined binary rank-one direction can accidentally be retained as a full equation block.
```
theorem slope_rank_one_iff (a d : R) :
    Module.finrank F2 (slope a d).range = 1 ↔
      (a ≠ 0 ∧ d = 0) ∨ (a = 0 ∧ d ≠ 0) ∨ (a = d ∧ a ≠ 0) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeys.slope
def OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.extendedLabel line 539
theorem OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.extendedLabel_actual line 543
def OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.restoredData line 550
Source documentation
Restore the full affine intercept after labeling the orbit body.
```
def restoredData (can : Q → Ambient s d × T)
    (label : ActualOrbit.Vertex can → Alphabet s) (D : Ambient s d × T) : Alphabet s :=
…
```
theorem OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.restoredData_actual line 554
theorem OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.restoredData_shift line 561
def OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.keyAnswer line 570
Source documentation
The actual verifier labeling, viewed as a function of exact affine keys.
```
def keyAnswer (S : Source) (k s d : Nat)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2^s))
    (D : TableKeys.Key k (Fin S.variables) (Fin S.occurrences) (Ambient s d)) : Alphabet s :=
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.TableKeys.Key
theorem OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.keyAnswer_actual line 576
theorem OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.keyAnswer_shift line 583
def OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.projectedAnswer line 590

theorem OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.projectedAnswer_pullback line 600

Source documentation

No extra consistency predicate: projected answers equal full-query answers for every table and every compatible hidden extension.

theorem projectedAnswer_pullback (S : Source) (k s d : Nat)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2^s))
    (J : Finset (Fin k)) (occ : Fin k → Fin S.occurrences)
    (slot : Fin k → PartnerProjection.Slot)
    (Y : RawPartnerTarget.RawPoint J →ₗ[F2] Ambient s d) :
    projectedAnswer S k s d labeling J
        (RawPrivateTable.supported J (ActualGame.names S) occ slot) Y =
      TableKeysGame.unfolded S k s d labeling
        (occ, Y.comp (RawPrivateTable.projection J (ActualGame.rhs S) occ slot)) := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.projectedAnswer, OAI.UniqueGamesTheorem.Decoder.TableKeysGame.unfolded

theorem OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.projectedAnswer_fold line 616

Source documentation

The visible table has the exact same affine folding law, with its genuine homogeneous coordinate rather than an assumed or reconstructed first bit.

theorem projectedAnswer_fold (S : Source) (k s d : Nat)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2^s))
    (J : Finset (Fin k)) (O : RawPrivateTable.SupportedV J (ActualGame.names S))
    (Y : RawPartnerTarget.RawPoint J →ₗ[F2] Ambient s d) (c : Alphabet s) :
    projectedAnswer S k s d labeling J O
        (Y + (TableKeys.visibleTau J).smulRight (c, (0 : Vector d))) =
      projectedAnswer S k s d labeling J O Y + c := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.projectedAnswer, OAI.UniqueGamesTheorem.Decoder.TableKeys.visibleTau

theorem OAI.UniqueGamesTheorem.Decoder.TableKeysPrivateRow.assemble_prod_shift line 654

def OAI.UniqueGamesTheorem.Decoder.TableKeysPrivateRow.rowAnswer line 671

Source documentation

The right player's actual private table, formed from visible row advice.

def rowAnswer (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2^s))
    (J : Finset (Fin k))
    (Q : RawPrivateTable.SupportedV J (ActualGame.names S))
    (A : Alphabet s →ₗ[F2] R)
    (rows : AdviceFibers.ObservedRow (E := RawPartnerTarget.RawPoint J) A)
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.AdviceFibers.ObservedRow

theorem OAI.UniqueGamesTheorem.Decoder.TableKeysPrivateRow.rowAnswer_fold line 683

Source documentation

Folding on the hidden kernel is a consequence of the exact key action.

theorem rowAnswer_fold (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2^s))
    (J : Finset (Fin k)) (Q : RawPrivateTable.SupportedV J (ActualGame.names S))
    (A : Alphabet s →ₗ[F2] R)
    (rows : AdviceFibers.ObservedRow (E := RawPartnerTarget.RawPoint J) A)
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.AdviceFibers.ObservedRow

theorem OAI.UniqueGamesTheorem.Decoder.TableKeysPrivateRow.rowAnswer_actual line 697
Source documentation
At the actual hidden matrix this row table is exactly the projected table used by the verifier, with the same complement and the same complete key.
```
theorem rowAnswer_actual (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2^s))
    (J : Finset (Fin k)) (Q : RawPrivateTable.SupportedV J (ActualGame.names S))
    (A : Alphabet s →ₗ[F2] R)
    (M : RawPartnerTarget.RawPoint J →ₗ[F2] Alphabet s)
    (T : RawPartnerTarget.RawPoint J →ₗ[F2] Vector d) :
    rowAnswer S labeling J Q A (AdviceFibers.observe A M) T
        (AdviceFibers.hiddenCoordinate A M) =
      TableKeysRestoration.projectedAnswer S k s d labeling J Q (M.prod T) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.TableKeysPrivateRow.rowAnswer, OAI.UniqueGamesTheorem.Decoder.AdviceFibers.observe, OAI.UniqueGamesTheorem.Decoder.AdviceFibers.hiddenCoordinate, OAI.UniqueGamesTheorem.Decoder.TableKeysRestoration.projectedAnswer
def OAI.UniqueGamesTheorem.Decoder.TableKeysPrivateRow.targetIntercept line 714
Source documentation
This intercept is determined once the visible base and affine witness are fixed; it is not silently erased when decoding from a row fiber.
```
def targetIntercept (J : Finset (Fin k)) (A : Alphabet s →ₗ[F2] R)
    (rows : AdviceFibers.ObservedRow (E := RawPartnerTarget.RawPoint J) A)
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceFibers.ObservedRow
theorem OAI.UniqueGamesTheorem.Decoder.TableKeysPrivateRow.affine_target_on_row line 719
theorem OAI.UniqueGamesTheorem.Decoder.TransferredDecoding.indicator_congr line 767
Source documentation
Equality indicators depend on their propositions, not on the chosen computable or classical decision procedures. Both deciders are explicit.
```
theorem indicator_congr (P Q : Prop) (dP : Decidable P) (dQ : Decidable Q)
    (h : P ↔ Q) : @ite ℝ P dP 1 0 = @ite ℝ Q dQ 1 0 := by
…
```
def OAI.UniqueGamesTheorem.Decoder.TransferredDecoding.privateOrigin line 779
Source documentation
The slice origin, expressed relative to the fixed visible row base.
```
def privateOrigin (A : K →ₗ[F2] R) (rows : AdviceFibers.ObservedRow (E := E) A)
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceFibers.ObservedRow
theorem OAI.UniqueGamesTheorem.Decoder.TransferredDecoding.assemble_privateOrigin line 785
Source documentation
Rebase the complete quotient parametrization without changing its matrices.
```
theorem assemble_privateOrigin (A : K →ₗ[F2] R)
    (rows : AdviceFibers.ObservedRow (E := E) A)
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceFibers.ObservedRow
def OAI.UniqueGamesTheorem.Decoder.TransferredDecoding.visibleFallback line 808
Source documentation
A default actual projected answer depends only on the displayed positions.
```
def visibleFallback (J : Finset (Fin k)) : ActualAnswer (TableKeys.visibleTau J) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeys.visibleTau
theorem OAI.UniqueGamesTheorem.Decoder.TransferredDecoding.actual_slice_agreement_eq_private line 813
Source documentation
Exact transport from the actual conditional matrix slice to the private Fourier coordinates. targetIntercept uses the visible base, not Mstar.
```
theorem actual_slice_agreement_eq_private (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (J : Finset (Fin k)) (O : RawPrivateTable.SupportedV J (ActualGame.names S))
    (A : Alphabet s →ₗ[F2] R)
    (rows : AdviceFibers.ObservedRow (E := RawPartnerTarget.RawPoint J) A)
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.AdviceFibers.ObservedRow
theorem OAI.UniqueGamesTheorem.Decoder.TransferredDecoding.actual_transferred_decoding line 850
Source documentation
Private policies for an actual restored labeling satisfy the conditional decoding bound on every transferred good slice. Folding and first-bit preservation come from their concrete constructions, not additional premises.
```
theorem actual_transferred_decoding (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (J : Finset (Fin k)) (occ : Fin k → Fin S.occurrences)
    (slot : Fin k → PartnerProjection.Slot)
    (A : Alphabet s →ₗ[F2] R)
    (rows : AdviceFibers.ObservedRow (E := RawPartnerTarget.RawPoint J) A)
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.AdviceFibers.ObservedRow