AdviceImageLaw.lean`

71 declarations, 0 contain sorry, 0 declared as axioms

The exact visible-advice law for a fixed latent map

For every fixed binary-linear map A, including rank-deficient maps, a uniform latent column has a uniform image in range A. An explicit range/kernel bijection proves the assertion simultaneously for every intercept and slope. The final theorem starts with the actual pair of independently uniform linear maps on the partner answer space and pushes it to independent uniform visible coefficients in W × range A. No full-rank or independence premise is assumed.

def OAI.MaxCutGames.Clean.AdviceImageLaw.rangePoint line 33
def OAI.MaxCutGames.Clean.AdviceImageLaw.selectedLift line 36
theorem OAI.MaxCutGames.Clean.AdviceImageLaw.selectedLift_spec line 39
theorem OAI.MaxCutGames.Clean.AdviceImageLaw.rangePoint_lift_add_kernel line 43
def OAI.MaxCutGames.Clean.AdviceImageLaw.imageKernelEquiv line 50
Source documentation
Every range fibre is one translate of the same kernel.
```
def imageKernelEquiv (A : K →ₗ[F2] S) : K ≃ A.range × A.ker where
…
```
def OAI.MaxCutGames.Clean.AdviceImageLaw.columnImage line 69
def OAI.MaxCutGames.Clean.AdviceImageLaw.columnSplitEquiv line 72
def OAI.MaxCutGames.Clean.AdviceImageLaw.visibleCoefficients line 76
def OAI.MaxCutGames.Clean.AdviceImageLaw.coefficientsSplitEquiv line 80
instance OAI.MaxCutGames.Clean.AdviceImageLaw.rangeFintype line 85
instance OAI.MaxCutGames.Clean.AdviceImageLaw.kernelFintype line 88
theorem OAI.MaxCutGames.Clean.AdviceImageLaw.uniform_visible_coefficients line 93
Source documentation
Exact pushforward law for all columns jointly, including the original intercept. This implies every event identity, not just individual marginals.
```
theorem uniform_visible_coefficients {I : Type} [Fintype I] [DecidableEq I]
    [Fintype W] [Fintype K] [Fintype S]
    (A : K →ₗ[F2] S) (F : (I → W × A.range) → ℝ) :
    (𝔼 columns : I → W × K, F (visibleCoefficients A columns)) =
      𝔼 visible : I → W × A.range, F visible := by
…
```
Mentions: OAI.MaxCutGames.Clean.AdviceImageLaw.visibleCoefficients

theorem OAI.MaxCutGames.Clean.AdviceImageLaw.uniform_coordinate_product line 108

Source documentation

The full product law exposes mutual independence of every raw coefficient.

theorem uniform_coordinate_product {I E : Type} [Fintype I] [DecidableEq I] [Fintype E]
    (f : I → E → ℝ) :
    (𝔼 columns : I → E, ∏ i, f i (columns i)) = ∏ i, 𝔼 e : E, f i e := by
…

theorem OAI.MaxCutGames.Clean.AdviceImageLaw.visible_coefficient_product line 116
theorem OAI.MaxCutGames.Clean.AdviceImageLaw.uniform_pushforward_of_expect line 124
theorem OAI.MaxCutGames.Clean.AdviceImageLaw.visible_coefficients_pushforward line 142

theorem OAI.MaxCutGames.Clean.AdviceImageLaw.visible_card_le line 149

Source documentation

The worst-case codomain cardinality suffices; no rank estimate is needed.

theorem visible_card_le [Fintype W] [Fintype K] [Fintype S] (A : K →ₗ[F2] S) :
    Fintype.card (W × A.range) ≤ Fintype.card W * Fintype.card S := by
…

theorem OAI.MaxCutGames.Clean.AdviceImageLaw.visible_card_binary_le line 155
abbrev OAI.MaxCutGames.Clean.AdviceImageLaw.PartnerSpace line 168
theorem OAI.MaxCutGames.Clean.AdviceImageLaw.coefficients_comp line 171
Source documentation
Raw coefficients commute with actual linear-map composition.
```
theorem coefficients_comp (A : K →ₗ[F2] S) (M : PartnerSpace rhs J →ₗ[F2] K) :
    coefficients rhs J S (A.comp M) = fun i => A (coefficients rhs J K M i) := by
…
```
Mentions: OAI.MaxCutGames.Clean.AdviceImageLaw.PartnerSpace
def OAI.MaxCutGames.Clean.AdviceImageLaw.actualVisibleCoefficients line 176
theorem OAI.MaxCutGames.Clean.AdviceImageLaw.actualVisibleCoefficients_second line 182
Source documentation
The displayed second component is precisely the coefficient of S = A M.
```
theorem actualVisibleCoefficients_second (A : K →ₗ[F2] S)
    (T : PartnerSpace rhs J →ₗ[F2] W) (M : PartnerSpace rhs J →ₗ[F2] K)
    (i : RawSlot J) :
    ((actualVisibleCoefficients rhs J A (T, M) i).2 : S) =
      coefficients rhs J S (A.comp M) i := by
…
```
Mentions: OAI.MaxCutGames.Clean.AdviceImageLaw.PartnerSpace, OAI.MaxCutGames.Clean.AdviceImageLaw.actualVisibleCoefficients
def OAI.MaxCutGames.Clean.AdviceImageLaw.actualMapPairEquiv line 190
theorem OAI.MaxCutGames.Clean.AdviceImageLaw.actual_maps_visible_uniform line 198
Source documentation
Sampling the actual independent maps T and M yields the claimed joint uniform coefficient law of (T,A M), for every fixed equation tuple and mask.
```
theorem actual_maps_visible_uniform [Fintype W] [Fintype K] [Fintype S]
    (A : K →ₗ[F2] S) (F : (RawSlot J → W × A.range) → ℝ) :
    (𝔼 maps : (PartnerSpace rhs J →ₗ[F2] W) × (PartnerSpace rhs J →ₗ[F2] K),
        F (actualVisibleCoefficients rhs J A maps)) =
      𝔼 gamma : RawSlot J → W × A.range, F gamma := by
…
```
Mentions: OAI.MaxCutGames.Clean.AdviceImageLaw.PartnerSpace, OAI.MaxCutGames.Clean.AdviceImageLaw.actualVisibleCoefficients
theorem OAI.MaxCutGames.Clean.AdviceImageLaw.actual_maps_visible_product line 210
theorem OAI.MaxCutGames.Clean.AdviceImageLaw.actual_maps_visible_pushforward line 218
def OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage line 243
Source documentation
The normalized uniform sum on a concrete finite outcome space.
```
def uniformAverage {Ω K : Type*} [Fintype Ω] [Field K] (f : Ω → K) : K :=
…
```
def OAI.MaxCutGames.Soundness.RepeatedGameBounds.zeroCount line 247
Source documentation
Number of zero columns in an actual coefficient vector.
```
def zeroCount {I C : Type*} [Fintype I] [Zero C] [DecidableEq C]
    (omega : I → C) : Nat :=
…
```
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.power_zeroCount_eq_prod line 251
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.sum_one_zero_weight line 257
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.sum_power_zeroCount line 270
Source documentation
The unnormalized count identity, on the actual full product space.
```
theorem sum_power_zeroCount {C K : Type*} [Fintype C] [Zero C]
    [DecidableEq C] [Field K] (a : K) (t : Nat) :
    (∑ omega : Fin t → C, a ^ zeroCount omega) =
      ((Fintype.card C : K) + a - 1) ^ t := by
…
```
Mentions: OAI.MaxCutGames.Soundness.RepeatedGameBounds.zeroCount
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage_power_zeroCount line 280
Source documentation
Exact moment identity for independent uniform coefficients in any finite nonempty zero-pointed space, proved by enumeration and product expansion.
```
theorem uniformAverage_power_zeroCount {C K : Type*} [Fintype C] [Zero C]
    [DecidableEq C] [Field K] [CharZero K] (a : K) (t : Nat) :
    uniformAverage (fun omega : Fin t → C => a ^ zeroCount omega) =
      (1 - (1 / (Fintype.card C : K)) * (1 - a)) ^ t := by
…
```
Mentions: OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage, OAI.MaxCutGames.Soundness.RepeatedGameBounds.zeroCount
abbrev OAI.MaxCutGames.Soundness.RepeatedGameBounds.BinaryCoefficient line 295
Source documentation
Binary vectors of length m, the actual coefficient alphabet.
```
abbrev BinaryCoefficient (m : Nat) := Fin m → ZMod 2
```
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.card_binaryCoefficient line 297
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniform_binary_coefficient_moment line 302
Source documentation
The precise averaging identity from Lemma 6.8, including zero-dimensional coefficient spaces and zero trials.
```
theorem uniform_binary_coefficient_moment {K : Type*} [Field K] [CharZero K]
    (a : K) (m t : Nat) :
    uniformAverage (fun omega : Fin t → BinaryCoefficient m => a ^ zeroCount omega) =
      (1 - (1 / 2 : K) ^ m * (1 - a)) ^ t := by
…
```
Mentions: OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage, OAI.MaxCutGames.Soundness.RepeatedGameBounds.BinaryCoefficient, OAI.MaxCutGames.Soundness.RepeatedGameBounds.zeroCount
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage_mono line 309
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage_const line 315
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage_prod line 321
Source documentation
Iterated averaging equals a single average on the actual product space.
```
theorem uniformAverage_prod {Ω Γ K : Type*} [Fintype Ω] [Fintype Γ]
    [Field K] (f : Ω × Γ → K) :
    uniformAverage f = uniformAverage (fun ω => uniformAverage fun γ => f (ω, γ)) := by
…
```
Mentions: OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage_equiv line 328
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage_product_left line 334
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage_coordinate_product line 340
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage_power_zeroCount_indexed line 350
def OAI.MaxCutGames.Soundness.RepeatedGameBounds.splitRawCoefficients line 363
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.zeroSet_card_eq_zeroCount line 384
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniform_raw_coefficient_moment line 394
Source documentation
The full raw coefficient tuple includes ζ₀ and both coefficients at every full position. Their uniform averaging cancels exactly; no ignored-coordinate independence premise is needed.
```
theorem uniform_raw_coefficient_moment {P C K : Type} [Fintype P] [DecidableEq P]
    [Fintype C] [Zero C] [DecidableEq C] [Field K] [CharZero K]
    (J : Finset P) (a : K) :
    uniformAverage (fun gamma : ConditionalIncidences.RawCoefficients J C =>
      a ^ (ConditionalIncidences.zeroSet J gamma).card) =
      (1 - (1 / (Fintype.card C : K)) * (1 - a)) ^ J.card := by
…
```
Mentions: OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage, OAI.MaxCutGames.Soundness.ConditionalIncidences.RawCoefficients, OAI.MaxCutGames.Soundness.ConditionalIncidences.zeroSet
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniform_binary_coefficient_upper line 410
Source documentation
Averages an actual pointwise coefficient-dependent upper bound over the uniform product law. No binomial distribution is assumed.
```
theorem uniform_binary_coefficient_upper {K : Type*}
    [Field K] [LinearOrder K] [IsStrictOrderedRing K]
    (a : K) (m t : Nat) (success : (Fin t → BinaryCoefficient m) → K)
    (bound : ∀ omega, success omega ≤ a ^ zeroCount omega) :
    uniformAverage success ≤ (1 - (1 / 2 : K) ^ m * (1 - a)) ^ t := by
…
```
Mentions: OAI.MaxCutGames.Soundness.RepeatedGameBounds.BinaryCoefficient, OAI.MaxCutGames.Soundness.RepeatedGameBounds.zeroCount, OAI.MaxCutGames.Soundness.RepeatedGameBounds.uniformAverage
abbrev OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.PredicateGame line 427
abbrev OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.PredicateStrategies line 428
def OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.predicateGame line 436
Source documentation
Pass a Boolean verifier predicate to the already checked deterministic local-reconstruction and incidence-extraction interface.
```
def predicateGame (G : Game QA QB A B) : PredicateGame QA QB A B :=
…
```
Mentions: OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.PredicateGame
def OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.strategyPair line 439
def OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.weightedGame line 444
Source documentation
Interpret a concrete predicate and a normalized finite question law as a game with the common foundation interface.
```
def weightedGame (G : PredicateGame QA QB A B)
    (questions : FiniteDistribution (QA × QB)) : Game QA QB A B := by
…
```
Mentions: OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.PredicateGame
def OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.reconstructedGame line 451
Source documentation
The reconstructed outer question law is the actual pushforward of the inner question law under the separate local reconstruction functions.
```
def reconstructedGame (inner : Game QA QB A B) (outer : PredicateGame OA OB X Y)
    (r : IncidenceExtraction.LocalSimulation (predicateGame inner) outer) :
    Game OA OB X Y :=
…
```
Mentions: OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.PredicateGame, OAI.MaxCutGames.Soundness.IncidenceExtraction.LocalSimulation, OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.predicateGame
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.reconstructedGame_success_le line 459
Source documentation
Event containment from IncidenceExtraction becomes an inequality of the actual normalized winning sums. The outer law is constructed, not assumed.
```
theorem reconstructedGame_success_le
    (inner : Game QA QB A B) (outer : PredicateGame OA OB X Y)
    (r : IncidenceExtraction.LocalSimulation (predicateGame inner) outer)
    (s : PredicateStrategies OA OB X Y) :
    (reconstructedGame inner outer r).success (strategyPair s) ≤
      inner.success (strategyPair (r.induced s)) := by
…
```
Mentions: OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.PredicateGame, OAI.MaxCutGames.Soundness.IncidenceExtraction.LocalSimulation, OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.predicateGame, OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.PredicateStrategies, OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.reconstructedGame, OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.strategyPair
theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.reconstructed_repetition_success_le line 478
Source documentation
Specialization to the actual parallel game. Its strategy receives each entire question tuple, preserving cross-coordinate local dependence.
```
theorem reconstructed_repetition_success_le
    (G : Game QA QB A B) (n : Nat) (outer : PredicateGame OA OB X Y)
    (r : IncidenceExtraction.LocalSimulation (predicateGame (G.repetition n)) outer)
    (s : PredicateStrategies OA OB X Y) :
    (reconstructedGame (G.repetition n) outer r).success (strategyPair s) ≤
      (G.repetition n).success (strategyPair (r.induced s)) :=
…
```
Mentions: OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.PredicateGame, OAI.MaxCutGames.Soundness.IncidenceExtraction.LocalSimulation, OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.predicateGame, OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.PredicateStrategies, OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.reconstructedGame, OAI.MaxCutGames.Soundness.RepeatedGameBounds.Simulation.strategyPair
abbrev OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.FirstAnswer line 494
abbrev OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.SecondAnswer line 495
def OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.project line 498
Source documentation
Ambient coordinate form of the actual retained-coordinate projection.
```
def project {P : Type} (single : P → Bool) (indices : P → Fin 3)
    (answer : FirstAnswer P) : SecondAnswer P :=
…
```
Mentions: OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.FirstAnswer, OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.SecondAnswer
def OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.accepts line 506
Source documentation
A verifier using only the two displayed questions. The retained indices are verifier witnesses compatible with the displayed names, never player inputs. The output equality is the actual projection on all ambient coordinates.
```
def accepts {P R O N : Type} (g : Incidence O N) (single : P → Bool)
    (qa : ZeroInformation.FirstInput P R O)
    (qb : ZeroInformation.SecondInput P R O N)
    (answerA : FirstAnswer P) (answerB : SecondAnswer P) : Prop :=
…
```
Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.FirstInput, OAI.MaxCutGames.Soundness.ZeroInformation.SecondInput, OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.FirstAnswer, OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.SecondAnswer
def OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.predicateGame line 516

theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.actual_partnerProjection_accepts line 525

Source documentation

Points satisfying (6.17) satisfy this named verifier: validity comes from the actual first-question equation subspace and agreement from the actual partnerProjection map.

theorem actual_partnerProjection_accepts
    {P R O N : Type} (g : Incidence O N) (positions : List P)
    (single : P → Bool) (zeta0 : ZeroInformation.Bits R)
    (zeta1 zeta2 omega : P → ZeroInformation.Bits R)
    (occurrences : P → O) (indices : P → Fin 3)
    (point : ZeroInformation.FirstPoint g.rhs occurrences)
    (hone : point.val.1 = true) :
    accepts g single
      (ZeroInformation.firstInput positions single zeta0 zeta1 zeta2 omega
        occurrences indices)
      (ZeroInformation.secondInput positions single zeta0 zeta1 zeta2 omega
        occurrences (fun j => g.name (occurrences j) (indices j)))
…

Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.Bits, OAI.MaxCutGames.Soundness.ZeroInformation.FirstPoint, OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.accepts, OAI.MaxCutGames.Soundness.ZeroInformation.firstInput, OAI.MaxCutGames.Soundness.ZeroInformation.secondInput

theorem OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.accepts_implies_named_incidence line 544
Source documentation
At a single coordinate, actual projection acceptance supplies an accepted named-incidence answer with no access to the retained index.
```
theorem accepts_implies_named_incidence
    {P R O N : Type} (g : Incidence O N) (single : P → Bool)
    (qa : ZeroInformation.FirstInput P R O)
    (qb : ZeroInformation.SecondInput P R O N)
    (answerA : FirstAnswer P) (answerB : SecondAnswer P)
    (h : accepts g single qa qb answerA answerB)
    (j : P) (hj : single j = true) (name : N)
    (hname : qb.question j = Sum.inr name) :
    g.namedAccepts (qa.question j) name (answerA.2 j) (answerB.2.2 j) := by
…
```
Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.FirstInput, OAI.MaxCutGames.Soundness.ZeroInformation.SecondInput, OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.FirstAnswer, OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.SecondAnswer, OAI.MaxCutGames.Soundness.RepeatedGameBounds.ActualProjection.accepts
def OAI.MaxCutGames.Soundness.ActualPointAnswers.sourceTau line 578
def OAI.MaxCutGames.Soundness.ActualPointAnswers.partnerTau line 579
theorem OAI.MaxCutGames.Soundness.ActualPointAnswers.tau_projection line 581
def OAI.MaxCutGames.Soundness.ActualPointAnswers.firstAnswer line 588
def OAI.MaxCutGames.Soundness.ActualPointAnswers.secondAnswer line 593
theorem OAI.MaxCutGames.Soundness.ActualPointAnswers.triple_eq_of_first_second_parity_inline_ActualPointAnswers line 598
theorem OAI.MaxCutGames.Soundness.ActualPointAnswers.secondAnswer_projection line 615
Source documentation
Inactive occurrences determine every full triple. The active right-hand sides never enter the partner answer.
```
theorem secondAnswer_projection (rhs rhs' : Fin k → Bool) (J : Finset (Fin k))
    (slot : Fin k → Slot) (x : ActualHomogeneous.E k)
    (hout : ∀ j, j ∉ J → rhs' j = rhs j) :
    secondAnswer rhs' J (rawProjection rhs J slot x) =
      ActualProjection.project (activeOf J) (fun j => ConcreteExtraction.slotIndex (slot j))
        (firstAnswer rhs x) := by
…
```
Mentions: OAI.MaxCutGames.Soundness.ActualPointAnswers.secondAnswer, OAI.MaxCutGames.Soundness.ConcreteExtraction.slotIndex, OAI.MaxCutGames.Soundness.ActualPointAnswers.firstAnswer
def OAI.MaxCutGames.Soundness.ActualPointAnswers.displayedRhs line 665
theorem OAI.MaxCutGames.Soundness.ActualPointAnswers.displayedRhs_full line 670
theorem OAI.MaxCutGames.Soundness.ActualPointAnswers.actual_accepts line 678
Source documentation
Actual point equality gives acceptance in the named verifier on complete private inputs, with local answer conversions.
```
theorem actual_accepts {Q Id Name : Type} (J : Finset (Fin k))
    (g : IncidenceExtraction.Incidence Id Name)
    (qa : ZeroInformation.FirstInput (Fin k) Q Id)
    (qb : ZeroInformation.SecondInput (Fin k) Q Id Name)
    (slot : Fin k → Slot)
    (hquestion : qb.question = RawPrivateTable.displayed J g.name qa.question slot)
    (x : ActualHomogeneous.E k) (v : RawPoint J)
    (hone : sourceTau x = 1)
    (hprojection : rawProjection (fun j => g.rhs (qa.question j)) J slot x = v) :
    ActualProjection.accepts g (activeOf J) qa qb
      (firstAnswer (fun j => g.rhs (qa.question j)) x)
      (secondAnswer (displayedRhs g.rhs qb.question) J v) := by
…
```
Mentions: OAI.MaxCutGames.Soundness.IncidenceExtraction.Incidence, OAI.MaxCutGames.Soundness.ZeroInformation.FirstInput, OAI.MaxCutGames.Soundness.ZeroInformation.SecondInput, OAI.MaxCutGames.Soundness.RawPrivateTable.displayed, OAI.MaxCutGames.Soundness.ActualPointAnswers.sourceTau, OAI.MaxCutGames.Soundness.ActualPointAnswers.firstAnswer, OAI.MaxCutGames.Soundness.ActualPointAnswers.secondAnswer, OAI.MaxCutGames.Soundness.ActualPointAnswers.displayedRhs