TableKeys.lean`

44 declarations, 0 contain sorry, 0 declared as axioms

Exact affine-table keys for the v2 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 v2 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.MaxCutGames.Decoder.TableKeys.slope line 38
Source documentation
The free-coordinate block slope (x,y) ↦ x • a + y • d.
```
def slope (a d : R) : (F2 × F2) →ₗ[F2] R :=
…
```
theorem OAI.MaxCutGames.Decoder.TableKeys.slope_apply line 43
theorem OAI.MaxCutGames.Decoder.TableKeys.slope_zero_iff line 47
theorem OAI.MaxCutGames.Decoder.TableKeys.slope_injective line 61
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.MaxCutGames.Decoder.TableKeys.slope
def OAI.MaxCutGames.Decoder.TableKeys.freeTriple line 81
def OAI.MaxCutGames.Decoder.TableKeys.reduceBlock line 84
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.MaxCutGames.Decoder.TableKeys.reduceBlock_zero line 89
theorem OAI.MaxCutGames.Decoder.TableKeys.reduceBlock_first line 94
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.MaxCutGames.Decoder.TableKeys.reduceBlock
theorem OAI.MaxCutGames.Decoder.TableKeys.reduceBlock_second line 100
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.MaxCutGames.Decoder.TableKeys.reduceBlock
theorem OAI.MaxCutGames.Decoder.TableKeys.reduceBlock_third line 108
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.MaxCutGames.Decoder.TableKeys.reduceBlock
theorem OAI.MaxCutGames.Decoder.TableKeys.reduceBlock_full line 114
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.MaxCutGames.Decoder.TableKeys.reduceBlock, OAI.MaxCutGames.Decoder.TableKeys.freeTriple
theorem OAI.MaxCutGames.Decoder.TableKeys.third_intercept_cancels line 125
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.MaxCutGames.Decoder.TableKeys.third_key_cancels line 129
theorem OAI.MaxCutGames.Decoder.TableKeys.full_record_occurrence_injective line 139
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.MaxCutGames.Decoder.TableKeys.Key line 150
def OAI.MaxCutGames.Decoder.TableKeys.key line 152
theorem OAI.MaxCutGames.Decoder.TableKeys.key_data_ext_iff line 158
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.MaxCutGames.Decoder.TableKeys.Key
theorem OAI.MaxCutGames.Decoder.TableKeys.key_shift line 166

theorem OAI.MaxCutGames.Decoder.TableKeys.key_shift_free line 173

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.MaxCutGames.Decoder.TableKeys.key

theorem OAI.MaxCutGames.Decoder.TableKeys.projected_key_sharing line 186

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.MaxCutGames.Decoder.TableKeys.key

def OAI.MaxCutGames.Decoder.TableKeys.projectedKey line 198
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.MaxCutGames.Decoder.TableKeys.Key
theorem OAI.MaxCutGames.Decoder.TableKeys.projectedKey_pullback line 205
def OAI.MaxCutGames.Decoder.TableKeys.visibleTau line 226
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.MaxCutGames.Decoder.TableKeys.projection_surjective line 231
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.MaxCutGames.Decoder.TableKeys.projection_preserves_homogeneous line 239

theorem OAI.MaxCutGames.Decoder.TableKeys.visible_table_unique line 248

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.MaxCutGames.Decoder.TableKeys.pullback_shift line 258

theorem OAI.MaxCutGames.Decoder.TableKeys.projectedKey_shift line 274

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.MaxCutGames.Decoder.TableKeys.projectedKey, OAI.MaxCutGames.Decoder.TableKeys.visibleTau

structure OAI.MaxCutGames.Decoder.AdviceExperiment.FullAdvice line 309
Source documentation
The first prover's entire information; no singleton-choice or private matrix field is present.
```
structure FullAdvice where
…
```
structure OAI.MaxCutGames.Decoder.AdviceExperiment.Draw line 316
Source documentation
The actual draw before forgetting the hidden projection and private map.
```
structure Draw where
…
```
structure OAI.MaxCutGames.Decoder.AdviceExperiment.ProjectedAdvice line 330
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.MaxCutGames.Decoder.AdviceExperiment.projection line 338
def OAI.MaxCutGames.Decoder.AdviceExperiment.leftObservation line 342
def OAI.MaxCutGames.Decoder.AdviceExperiment.rightObservation line 348
def OAI.MaxCutGames.Decoder.AdviceExperiment.paddedMatrix line 358
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.MaxCutGames.Decoder.AdviceExperiment.Draw
def OAI.MaxCutGames.Decoder.AdviceExperiment.paddedComplement line 361
theorem OAI.MaxCutGames.Decoder.AdviceExperiment.left_rows_eq line 364
theorem OAI.MaxCutGames.Decoder.AdviceExperiment.left_rows_attainable line 367
theorem OAI.MaxCutGames.Decoder.AdviceExperiment.right_rows_attainable line 372
def OAI.MaxCutGames.Decoder.AdviceExperiment.changeHidden line 379
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.MaxCutGames.Decoder.AdviceExperiment.Draw
theorem OAI.MaxCutGames.Decoder.AdviceExperiment.leftObservation_changeHidden line 383
theorem OAI.MaxCutGames.Decoder.AdviceExperiment.rightObservation_changeHidden line 388
theorem OAI.MaxCutGames.Decoder.AdviceExperiment.selectedWitness_changeHidden line 395
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.MaxCutGames.Decoder.AdviceExperiment.FullAdvice, OAI.MaxCutGames.Decoder.AdviceExperiment.Draw, OAI.MaxCutGames.Decoder.AdviceExperiment.leftObservation, OAI.MaxCutGames.Decoder.AdviceExperiment.changeHidden
theorem OAI.MaxCutGames.Decoder.AdviceExperiment.projection_actual_answer line 402
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.MaxCutGames.Decoder.AdviceExperiment.Draw, OAI.MaxCutGames.Decoder.TableKeys.visibleTau, OAI.MaxCutGames.Decoder.AdviceExperiment.projection