TransferredDecoding.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Decoding an actual transferred column slice

The point Mstar used to parametrize a transferred slice is distinct from the canonical visible row base observedBase A rows. The right strategy uses only the latter. Their kernel-valued difference appears solely in the analysis. The exact quotient equivalence transports uniform slice agreement, including the affine offset, to the conditional private-decoder theorem.

theorem OAI.MaxCutGames.Decoder.TransferredDecoding.indicator_congr line 40
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.MaxCutGames.Decoder.TransferredDecoding.privateOrigin line 52
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.MaxCutGames.Decoder.AdviceFibers.ObservedRow
theorem OAI.MaxCutGames.Decoder.TransferredDecoding.assemble_privateOrigin line 58
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.MaxCutGames.Decoder.AdviceFibers.ObservedRow
def OAI.MaxCutGames.Decoder.TransferredDecoding.visibleFallback line 79
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.MaxCutGames.Decoder.TableKeys.visibleTau
theorem OAI.MaxCutGames.Decoder.TransferredDecoding.actual_slice_agreement_eq_private line 84
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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.AdviceFibers.ObservedRow
theorem OAI.MaxCutGames.Decoder.TransferredDecoding.actual_transferred_decoding line 121
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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.AdviceFibers.ObservedRow
structure OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness line 198
Source documentation
The part of a normalized affine witness needed by the left sampler.
```
structure ResponseWitness (k : ℕ) where
…
```
def OAI.MaxCutGames.Decoder.VisiblePolicies.defaultWitness line 203
abbrev OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput line 208
abbrev OAI.MaxCutGames.Decoder.VisiblePolicies.RightInput line 212
def OAI.MaxCutGames.Decoder.VisiblePolicies.chosenWitness line 218
Source documentation
The witness choice has only the left observation as its variable input.
```
def chosenWitness {S : Source}
    (good : LeftInput S k s d R → ResponseWitness k → Prop)
    (q : LeftInput S k s d R) : ResponseWitness k :=
…
```
Mentions: OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness
theorem OAI.MaxCutGames.Decoder.VisiblePolicies.chosenWitness_spec line 223
def OAI.MaxCutGames.Decoder.VisiblePolicies.leftPolicy line 230
def OAI.MaxCutGames.Decoder.VisiblePolicies.pointLaw line 237
Source documentation
A fixed valid fallback gives a total policy even on impossible row inputs.
```
def pointLaw {X : Type*} [Fintype X] (x : X) : FiniteDistribution X where
…
```
def OAI.MaxCutGames.Decoder.VisiblePolicies.rightPolicy line 243
Source documentation
The right kernel consumes its own complete visible observation only.
```
def rightPolicy (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (J : Finset (Fin k)) (q : RightInput S J s d R) :
    FiniteDistribution (ActualAnswer (TableKeys.visibleTau J)) :=
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.RightInput, OAI.MaxCutGames.Decoder.TableKeys.visibleTau
theorem OAI.MaxCutGames.Decoder.VisiblePolicies.rightPolicy_on_attainable line 254
theorem OAI.MaxCutGames.Decoder.VisiblePolicies.leftPolicy_changeHidden line 265
theorem OAI.MaxCutGames.Decoder.VisiblePolicies.rightPolicy_on_draw line 274
def OAI.MaxCutGames.Decoder.VisiblePolicies.observedAgreement line 292
Source documentation
The literal product of the two observation-local stochastic responses.
```
def observedAgreement (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : LeftInput S k s d R → ResponseWitness k → Prop)
    (draw : AdviceExperiment.Draw k (Fin S.occurrences) (Alphabet s) (Vector d) R) : ℝ :=
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness, OAI.MaxCutGames.Decoder.AdviceExperiment.Draw
theorem OAI.MaxCutGames.Decoder.VisiblePolicies.observedAgreement_eq_private line 304
Source documentation
The private-decoding expression is exactly the actual local-kernel product probability. In particular there is no shared decoder random tape.
```
theorem observedAgreement_eq_private (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : LeftInput S k s d R → ResponseWitness k → Prop)
    (draw : AdviceExperiment.Draw k (Fin S.occurrences) (Alphabet s) (Vector d) R) :
    observedAgreement S labeling good draw =
      let w := chosenWitness good (AdviceExperiment.leftObservation (ActualGame.rhs S) draw)
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness, OAI.MaxCutGames.Decoder.AdviceExperiment.Draw, OAI.MaxCutGames.Decoder.VisiblePolicies.observedAgreement, OAI.MaxCutGames.Decoder.VisiblePolicies.chosenWitness, OAI.MaxCutGames.Decoder.AdviceExperiment.leftObservation