VisibleTransfer.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

The complete-data conditional law of the actual projected experiment. The residual private matrix is uniform even when the occurrence law is weighted and the public row map has deficient rank.

def OAI.MaxCutGames.Decoder.VisibleTransfer.fiberEvent line 16
Source documentation
The part of an event in one actual visible-data fiber.
```
def fiberEvent (observe : Ω → D) (d : D) (event : Ω → Bool) : Ω → Bool := by
…
```
def OAI.MaxCutGames.Decoder.VisibleTransfer.fiberMass line 20
theorem OAI.MaxCutGames.Decoder.VisibleTransfer.fiberMass_nonnegative line 25
theorem OAI.MaxCutGames.Decoder.VisibleTransfer.fiberMass_mono line 30
theorem OAI.MaxCutGames.Decoder.VisibleTransfer.sum_fiberMass line 39
theorem OAI.MaxCutGames.Decoder.VisibleTransfer.observation_weight line 49
def OAI.MaxCutGames.Decoder.VisibleTransfer.visibleWitness line 57
Source documentation
Positive projected column-slice mass and sufficient conditional target agreement. Both quantities are computed after fixing actual visible data.
```
def visibleWitness (μ : FiniteDistribution Ω) (observe : Ω → D)
    (slice targetHit : Ω → Bool) (threshold : ℝ) (d : D) : Bool := by
…
```

theorem OAI.MaxCutGames.Decoder.VisibleTransfer.witness_margin_le_visible_probability line 66

Source documentation

The positive part of the witness margin is paid for by the probability of the actual observed data, rather than by the larger hidden sample space.

theorem witness_margin_le_visible_probability
    (μ : FiniteDistribution Ω) (observe : Ω → D)
    (slice targetHit : Ω → Bool) (threshold : ℝ) (hthreshold : 0 ≤ threshold) :
    μ.probability (fun x => slice x && targetHit x) - threshold * μ.probability slice ≤
      (μ.pushforward observe).probability (visibleWitness μ observe slice targetHit threshold) := by
…

Mentions: OAI.MaxCutGames.Decoder.VisibleTransfer.visibleWitness

theorem OAI.MaxCutGames.Decoder.VisibleTransfer.visibleWitness_conditional line 109

Source documentation

On every selected datum the conditional distribution is defined on an actual nonempty positive-mass slice and has the promised target agreement.

theorem visibleWitness_conditional
    (μ : FiniteDistribution Ω) (observe : Ω → D)
    (slice targetHit : Ω → Bool) (threshold : ℝ) (d : D)
    (h : visibleWitness μ observe slice targetHit threshold d = true) :
    ∃ hpositive : 0 < μ.probability (fiberEvent observe d slice),
      threshold ≤ (μ.condition (fiberEvent observe d slice) hpositive).probability targetHit := by
…

Mentions: OAI.MaxCutGames.Decoder.VisibleTransfer.visibleWitness, OAI.MaxCutGames.Decoder.VisibleTransfer.fiberEvent

theorem OAI.MaxCutGames.Decoder.VisibleTransfer.visibleWitness_good line 133

Source documentation

Goodness is inherited from any event whose membership requires good visible advice. Positivity supplies an actual supporting hidden sample.

theorem visibleWitness_good
    (μ : FiniteDistribution Ω) (observe : Ω → D)
    (slice targetHit : Ω → Bool) (threshold : ℝ)
    (good : D → Prop) (hslice : ∀ x, slice x = true → good (observe x))
    (d : D) (h : visibleWitness μ observe slice targetHit threshold d = true) :
    good d := by
…

Mentions: OAI.MaxCutGames.Decoder.VisibleTransfer.visibleWitness

theorem OAI.MaxCutGames.Decoder.VisibleTransfer.margin_transfer line 157

Source documentation

A pair of full-table event probabilities transfers with error (1 + threshold) * TV. This estimate precedes all conditioning.

theorem margin_transfer (μ ν : FiniteDistribution Ω)
    (slice targetHit : Ω → Bool) (threshold : ℝ) (hthreshold : 0 ≤ threshold) :
    μ.probability (fun x => slice x && targetHit x) - threshold * μ.probability slice -
        (1 + threshold) * μ.totalVariation ν ≤
      ν.probability (fun x => slice x && targetHit x) - threshold * ν.probability slice := by
…

theorem OAI.MaxCutGames.Decoder.VisibleTransfer.wholeTable_transfer_to_visibleWitness line 170

Source documentation

The whole-table comparison and the exact finite disintegration combine without any assumption on conditional projection laws.

theorem wholeTable_transfer_to_visibleWitness
    {Γ : Type*} [Fintype Γ]
    (unrestricted : FiniteDistribution Ω) (actual : FiniteDistribution Γ)
    (pad : Γ → Ω) (observe : Γ → D) (slice targetHit : Ω → Bool)
    (threshold γ : ℝ) (hthreshold : 0 ≤ threshold)
    (hmargin : γ ≤
      unrestricted.probability (fun x => slice x && targetHit x) -
        threshold * unrestricted.probability slice -
        (1 + threshold) * unrestricted.totalVariation (actual.pushforward pad)) :
    γ ≤ (actual.pushforward observe).probability
      (visibleWitness actual observe (fun x => slice (pad x))
        (fun x => targetHit (pad x)) threshold) := by
…

Mentions: OAI.MaxCutGames.Decoder.VisibleTransfer.visibleWitness

theorem OAI.MaxCutGames.Decoder.VisibleTransfer.projected_witness_mass line 189
def OAI.MaxCutGames.Decoder.UniformFibers.selectedFiberEquiv line 219
theorem OAI.MaxCutGames.Decoder.UniformFibers.selectedFiberEquiv_point line 239

theorem OAI.MaxCutGames.Decoder.UniformFibers.conditional_probability line 247

Source documentation

Conditioning after fixing the complete datum and the selected column event leaves precisely the uniform restricted private fiber.

theorem conditional_probability [Fintype Ω] [Fintype Y]
    (μ : FiniteDistribution Ω) (observe : Ω → D) (d : D)
    (slice event : Ω → Bool)
    (positive : 0 < μ.probability (VisibleTransfer.fiberEvent observe d slice))
    (c : ℝ) (hconstant : ∀ x, observe x = d → μ.weight x = c)
    (e : Y ≃ {x : Ω // observe x = d}) :
    (μ.condition (VisibleTransfer.fiberEvent observe d slice) positive).probability event =
      𝔼 y : {y : Y // slice (e y).val = true},
        if event (e y.val).val then (1 : ℝ) else 0 := by
…

Mentions: OAI.MaxCutGames.Decoder.VisibleTransfer.fiberEvent

theorem OAI.MaxCutGames.Decoder.ActualConditionalLaw.probability_condition_complete line 294
theorem OAI.MaxCutGames.Decoder.ActualConditionalLaw.observedAgreement_completeDraw line 319
Source documentation
Both provers' answers, and their equality predicate, are fixed on the complete observation fiber. Only the hidden matrix varies within that fiber.
```
theorem observedAgreement_completeDraw (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector r) → VisiblePolicies.ResponseWitness k → Prop)
    (data : AdviceLaw.CompleteData k (Fin S.occurrences) (Alphabet s) (Vector d) (Vector r))
    (N N' : AdviceLaw.PrivateMap data) :
    VisiblePolicies.observedAgreement S labeling good (AdviceLaw.completeDraw data N) =
      VisiblePolicies.observedAgreement S labeling good (AdviceLaw.completeDraw data N') := by
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness, OAI.MaxCutGames.Decoder.AdviceLaw.CompleteData, OAI.MaxCutGames.Decoder.AdviceLaw.PrivateMap, OAI.MaxCutGames.Decoder.VisiblePolicies.observedAgreement, OAI.MaxCutGames.Decoder.AdviceLaw.completeDraw
def OAI.MaxCutGames.Decoder.ActualConditionalLaw.datumAgreement line 331
theorem OAI.MaxCutGames.Decoder.ActualConditionalLaw.datumAgreement_nonneg line 337
theorem OAI.MaxCutGames.Decoder.ActualConditionalLaw.observedAgreement_seed line 346
Source documentation
The actual success observable factors through the complete visible datum; this justifies integrating a lower bound over visible-witness probability.
```
theorem observedAgreement_seed (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector r) → VisiblePolicies.ResponseWitness k → Prop)
    (x : AdviceLaw.FullSeed k (Fin S.occurrences) (Alphabet s) (Vector d) (Vector r)) :
    VisiblePolicies.observedAgreement S labeling good
      (AdviceLaw.seedToActualDraw x.1.1 x.1.2 x.2) =
        datumAgreement S labeling good (AdviceLaw.completeObserve x) := by
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness, OAI.MaxCutGames.Decoder.AdviceLaw.FullSeed, OAI.MaxCutGames.Decoder.VisiblePolicies.observedAgreement, OAI.MaxCutGames.Decoder.AdviceLaw.seedToActualDraw, OAI.MaxCutGames.Decoder.ActualConditionalLaw.datumAgreement, OAI.MaxCutGames.Decoder.AdviceLaw.completeObserve
theorem OAI.MaxCutGames.Decoder.SelectedFiberLaw.univ_congr_inline_SelectedFiberLaw line 393
Source documentation
The universe finset is independent of the chosen finite enumeration. The instances are explicit so elaboration need not unfold either enumeration.
```
private theorem univ_congr_inline_SelectedFiberLaw {X : Type*} (i j : Fintype X) :
    @Finset.univ X i = @Finset.univ X j := by
…
```
theorem OAI.MaxCutGames.Decoder.SelectedFiberLaw.condition_prob_enumeration line 398
def OAI.MaxCutGames.Decoder.SelectedFiberLaw.datumLeft line 413
def OAI.MaxCutGames.Decoder.SelectedFiberLaw.datumMatrix line 416
def OAI.MaxCutGames.Decoder.SelectedFiberLaw.datumProjection line 419
theorem OAI.MaxCutGames.Decoder.SelectedFiberLaw.datumLeft_eq line 422
theorem OAI.MaxCutGames.Decoder.SelectedFiberLaw.datumMatrix_rows line 428
theorem OAI.MaxCutGames.Decoder.SelectedFiberLaw.datumMatrix_rowAdvice line 432

theorem OAI.MaxCutGames.Decoder.SelectedFiberLaw.slice_assemble_iff line 444

Source documentation

Every event membership uses the same selected normalized witness on the entire complete-data fiber.

theorem slice_assemble_iff (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (data : Datum S k s d r) (hgood : GoodAdvice S labeling α (datumLeft S data))
    (N : AdviceLaw.PrivateMap data) :
    slice S k s d r labeling α (AdviceLaw.completeAssemble data N) = true ↔
      mapEquiv k s ((datumMatrix S data N).comp (datumProjection S data)) ∈
        (normalizedDescription S labeling α hα hsmall (datumLeft S data) hgood).toSlice.points := by
…

theorem OAI.MaxCutGames.Decoder.SelectedFiberLaw.target_assemble_iff line 463

Source documentation

On the selected event, the actual full-table target-hit predicate equals projected affine equality with the very same normalized coefficient/intercept.

theorem target_assemble_iff (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (data : Datum S k s d r) (hgood : GoodAdvice S labeling α (datumLeft S data))
    (N : AdviceLaw.PrivateMap data)
    (hN : slice S k s d r labeling α (AdviceLaw.completeAssemble data N) = true) :
    targetHit S k s d r labeling α (AdviceLaw.completeAssemble data N) = true ↔
      TableKeysRestoration.projectedAnswer S k s d labeling (PaddedLaw.choiceMask data.2.1)
        (RawPrivateTable.supported (PaddedLaw.choiceMask data.2.1) (ActualGame.names S)
          data.1.1 (PaddedLaw.choiceSlots data.2.1)) ((datumMatrix S data N).prod data.2.2.1) =
        datumMatrix S data N (datumProjection S data
          (normalizedResponse S labeling α hα hsmall (datumLeft S data) hgood).coefficient) +
…

Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.SelectedFiberLaw.datumLeft, OAI.MaxCutGames.Decoder.AdviceLaw.PrivateMap, OAI.MaxCutGames.Decoder.AdviceLaw.completeAssemble, OAI.MaxCutGames.Decoder.TableKeysRestoration.projectedAnswer, OAI.MaxCutGames.Decoder.PaddedLaw.choiceMask, OAI.MaxCutGames.Decoder.PaddedLaw.choiceSlots, OAI.MaxCutGames.Decoder.SelectedFiberLaw.datumMatrix, OAI.MaxCutGames.Decoder.SelectedFiberLaw.datumProjection

theorem OAI.MaxCutGames.Decoder.SelectedFiberLaw.exists_selected_private line 498
Source documentation
Positive mass supplies a supporting private coordinate in the selected fiber; neither a hidden matrix nor good advice is an additional premise.
```
theorem exists_selected_private (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) (data : Datum S k s d r)
    (positive : 0 < (law S k s d r β hβ hβ').probability
      (VisibleTransfer.fiberEvent AdviceLaw.completeObserve data (slice S k s d r labeling α))) :
    ∃ N : AdviceLaw.PrivateMap data,
      slice S k s d r labeling α (AdviceLaw.completeAssemble data N) = true := by
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisibleTransfer.fiberEvent, OAI.MaxCutGames.Decoder.AdviceLaw.completeObserve, OAI.MaxCutGames.Decoder.AdviceLaw.PrivateMap, OAI.MaxCutGames.Decoder.AdviceLaw.completeAssemble
theorem OAI.MaxCutGames.Decoder.SelectedFiberLaw.good_of_selected_private line 524

def OAI.MaxCutGames.Decoder.SelectedFiberLaw.selectedPrivateEquiv line 538

Source documentation

The actual selected private coordinates are in bijection with the complete projected affine slice. The supporting point is used only to state its column equations; the canonical visible base still defines the private coordinates.

def selectedPrivateEquiv (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (data : Datum S k s d r) (hgood : GoodAdvice S labeling α (datumLeft S data))
    (Nstar : AdviceLaw.PrivateMap data)
    (hstar : slice S k s d r labeling α (AdviceLaw.completeAssemble data Nstar) = true) :
    {N : AdviceLaw.PrivateMap data //
      slice S k s d r labeling α (AdviceLaw.completeAssemble data N) = true} ≃
      RowErasureSliceQuotient.AffineSlice data.1.2
        ((normalizedResponse S labeling α hα hsmall (datumLeft S data) hgood).columns.map
          (datumProjection S data)) (datumMatrix S data Nstar) := by
…

theorem OAI.MaxCutGames.Decoder.SelectedFiberLaw.selectedPrivateEquiv_val line 586

theorem OAI.MaxCutGames.Decoder.SelectedFiberLaw.conditional_eq_transferred line 598

Source documentation

Exact conditional target probability, with no assumed uniformity premise.

theorem conditional_eq_transferred (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1)
    (data : Datum S k s d r) (hgood : GoodAdvice S labeling α (datumLeft S data))
    (Nstar : AdviceLaw.PrivateMap data)
    (hstar : slice S k s d r labeling α (AdviceLaw.completeAssemble data Nstar) = true)
    (positive : 0 < (law S k s d r β hβ hβ').probability
      (VisibleTransfer.fiberEvent AdviceLaw.completeObserve data (slice S k s d r labeling α))) :
    ((law S k s d r β hβ hβ').condition
      (VisibleTransfer.fiberEvent AdviceLaw.completeObserve data (slice S k s d r labeling α))
        positive).probability (targetHit S k s d r labeling α) =
…

theorem OAI.MaxCutGames.Decoder.SelectedFiberLaw.visibleWitness_decoding line 682

Source documentation

Every complete visible datum selected by the actual witness event pays the private-decoding success constant. Good advice and a nonempty transferred slice follow from positivity and are not additional hypotheses.

theorem visibleWitness_decoding (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α : ℝ) (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) (data : Datum S k s d r)
    (hvisible : VisibleTransfer.visibleWitness (law S k s d r β hβ hβ')
      AdviceLaw.completeObserve (slice S k s d r labeling α)
      (targetHit S k s d r labeling α) (α / 4) data = true) :
    (α / 8) ^ 2 / (2 : ℝ) ^ (s * r) / (2 : ℝ) ^ r ≤
      ActualConditionalLaw.datumAgreement S labeling (goodPredicate S labeling α hα hsmall) data := by
…

Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisibleTransfer.visibleWitness, OAI.MaxCutGames.Decoder.AdviceLaw.completeObserve, OAI.MaxCutGames.Decoder.ActualConditionalLaw.datumAgreement

def OAI.MaxCutGames.Decoder.ActualProjectedTransfer.slopeVariation line 724

theorem OAI.MaxCutGames.Decoder.ActualProjectedTransfer.visible_mass line 732

Source documentation

The actual complete-data event has positive mass depending only on the fixed inverse and alphabet parameters.

theorem visible_mass (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α g₀ β : ℝ) (hα : 0 < α) (hβ : 0 ≤ β) (hβ' : β ≤ 1)
    (hgood : g₀ ≤ ActualGoodRows.adviceMass S k s d r labeling α)
    (hvariation : slopeVariation k s d β ≤ ConstantSelection.variationBudget α g₀ s r) :
    ConstantSelection.visibleMass α g₀ s r ≤
      ((ActualSeedEvents.law S k s d r β hβ hβ').pushforward AdviceLaw.completeObserve).probability
        (VisibleTransfer.visibleWitness (ActualSeedEvents.law S k s d r β hβ hβ')
          AdviceLaw.completeObserve (ActualSeedEvents.slice S k s d r labeling α)
          (ActualSeedEvents.targetHit S k s d r labeling α) (α / 4)) := by
…

theorem OAI.MaxCutGames.Decoder.ActualProjectedTransfer.event_expectation_lower line 759

Source documentation

Integrating a pointwise lower bound over a genuine probability event.

theorem event_expectation_lower {Ω : Type*} [Fintype Ω]
    (μ : FiniteDistribution Ω) (event : Ω → Bool) (f : Ω → ℝ)
    (γ₁ γ₂ : ℝ) (hγ₂ : 0 ≤ γ₂) (hf : ∀ x, 0 ≤ f x)
    (hmass : γ₁ ≤ μ.probability event)
    (hpoint : ∀ x, event x = true → γ₂ ≤ f x) :
    γ₁ * γ₂ ≤ μ.expectation f := by
…

theorem OAI.MaxCutGames.Decoder.ActualProjectedTransfer.actual_success_lower line 779
Source documentation
End-to-end lower bound for actual local stochastic responses. No hidden matrix, selected witness, or opposing observation is passed to a prover.
```
theorem actual_success_lower (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α g₀ β : ℝ) (hα : 0 < α)
    (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (hβ : 0 ≤ β) (hβ' : β ≤ 1)
    (hgood : g₀ ≤ ActualGoodRows.adviceMass S k s d r labeling α)
    (hvariation : slopeVariation k s d β ≤ ConstantSelection.variationBudget α g₀ s r) :
    ConstantSelection.decodingMass α g₀ s r ≤
      (ActualSeedEvents.law S k s d r β hβ hβ').expectation
        (fun seed => VisiblePolicies.observedAgreement S labeling
          (SelectedPolicies.goodPredicate S labeling α hα hsmall)
          (AdviceLaw.seedToActualDraw seed.1.1 seed.1.2 seed.2)) := by
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.ActualGoodRows.adviceMass, OAI.MaxCutGames.Decoder.ActualProjectedTransfer.slopeVariation, OAI.MaxCutGames.Decoder.ConstantSelection.variationBudget, OAI.MaxCutGames.Decoder.ConstantSelection.decodingMass, OAI.MaxCutGames.Decoder.ActualSeedEvents.law, OAI.MaxCutGames.Decoder.VisiblePolicies.observedAgreement, OAI.MaxCutGames.Decoder.SelectedPolicies.goodPredicate, OAI.MaxCutGames.Decoder.AdviceLaw.seedToActualDraw