RowErasureSelection.lean`

72 declarations, 0 contain sorry, 0 declared as axioms

Visible selection of a row-erasure witness. The selected description depends only on the fixed table function, the row map, and the observed row value. The full sampled matrix enters only the later event testing its membership in the already selected slice. Classical choice fixes one witness once and for all; proof irrelevance makes the choice independent of the goodness proof.

def OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.chosenDescription line 21
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.chosenDescription_spec line 26
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.chosenDescription_congr line 35
def OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedDescription line 46
Source documentation
A total visible selector. Bad advice has no selected witness.
```
def SliceFamily.selectedDescription (F : SliceFamily X Y A S D)
    (f : X → Y) (α : ℝ) (a : A) (s : S) : Option D := by
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasure.SliceFamily
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedDescription_of_good line 52
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.good_of_selectedDescription line 58
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedDescription_spec line 67
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedDescription_congr line 78
def OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedEvent line 88
Source documentation
Good visible advice and the selected column restrictions on the hidden matrix. The selector receives only its observed row value.
```
def SliceFamily.selectedEvent (F : SliceFamily X Y A S D)
    (f : X → Y) (α : ℝ) (a : A) (x : X) : Prop :=
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasure.SliceFamily
def OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedMatch line 92
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedEvent_iff_of_advice line 97
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedMatch_iff_of_advice line 110
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedEvent_good line 125
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedMatch_event line 131
def OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.fiber line 151
def OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.event line 154
def OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.matchEvent line 158
theorem OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.expect_le_expect_of_fiber_sum_le line 164
Source documentation
Arbitrary real summands can be compared fiber by fiber. No uniformity of the induced observation distribution is asserted or required.
```
theorem expect_le_expect_of_fiber_sum_le (observe : X → S) (f g : X → ℝ)
    (hle : ∀ s, (∑ x ∈ fiber observe s, f x) ≤ ∑ x ∈ fiber observe s, g x) :
    Finset.univ.expect f ≤ Finset.univ.expect g := by
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.fiber
theorem OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.sum_event_mul_fiber line 176
Source documentation
On good visible data, the selected event sums exactly over the selected points, including for arbitrary real weights on the hidden sample.
```
theorem sum_event_mul_fiber (observe : X → S) (good : S → Prop)
    (chosen : S → Finset X)
    (support : ∀ s x, x ∈ chosen s → observe x = s)
    (s : S) (hgood : good s) (w : X → ℝ) :
    (∑ x ∈ fiber observe s, indicator (event observe good chosen x) * w x) =
      ∑ x ∈ chosen s, w x := by
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.fiber, OAI.MaxCutGames.Inverse.RowErasure.indicator, OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.event
theorem OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.sum_event_fiber line 199
theorem OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.sum_match_fiber line 208
theorem OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.mass_event_ge line 228
Source documentation
A lower fraction inside every good fiber gives the same lower fraction of the actual good-advice mass. Empty fibers and empty sample spaces are valid.
```
theorem mass_event_ge (observe : X → S) (good : S → Prop)
    (chosen : S → Finset X)
    (support : ∀ s x, x ∈ chosen s → observe x = s)
    (c : ℝ)
    (hsize : ∀ s, good s →
      c * ((fiber observe s).card : ℝ) ≤ ((chosen s).card : ℝ)) :
    c * uniformMass (fun x => good (observe x)) ≤
      uniformMass (event observe good chosen) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.fiber, OAI.MaxCutGames.Inverse.RowErasure.uniformMass, OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.event
theorem OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.mass_match_ge line 267
Source documentation
A matching fraction in every selected good fiber survives averaging over the hidden sample space, without any equiprobability assumption on fibers.
```
theorem mass_match_ge (observe : X → S) (good : S → Prop)
    (chosen : S → Finset X)
    (support : ∀ s x, x ∈ chosen s → observe x = s)
    (hit : S → X → Prop) (β : ℝ)
    (hmatch : ∀ s, good s →
      β * ((chosen s).card : ℝ) ≤ ∑ x ∈ chosen s, indicator (hit s x)) :
    β * uniformMass (event observe good chosen) ≤
      uniformMass (matchEvent observe good chosen hit) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasure.indicator, OAI.MaxCutGames.Inverse.RowErasure.uniformMass, OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.event, OAI.MaxCutGames.Inverse.RowErasure.SelectionPartition.matchEvent
theorem OAI.MaxCutGames.Inverse.RowErasureColumnMass.card_affineSlice line 315
theorem OAI.MaxCutGames.Inverse.RowErasureColumnMass.card_rowFiber line 323
theorem OAI.MaxCutGames.Inverse.RowErasureColumnMass.card_rowFiber_eq_mul line 332
Source documentation
The exact number of row-fiber points for each compatible specification on the column span. Dependent column equations cost only their actual rank.
```
theorem card_rowFiber_eq_mul (A : K →ₗ[F2] R) (Q : Submodule F2 E)
    (M₀ : E →ₗ[F2] K) :
    Nat.card (RowFiber A (A.comp M₀)) = Nat.card (AffineSlice A Q M₀) *
      2 ^ (Module.finrank F2 Q * Module.finrank F2 A.ker) := by
…
```

theorem OAI.MaxCutGames.Inverse.RowErasureColumnMass.card_rowFiber_le_mul line 341

Source documentation

A denominator-free bound by the listed column count and ambient output dimension, with no independence or full-rank hypothesis.

theorem card_rowFiber_le_mul (A : K →ₗ[F2] R) (Q : Submodule F2 E)
    (M₀ : E →ₗ[F2] K) (ell r : ℕ)
    (hQ : Module.finrank F2 Q ≤ r) (hK : Module.finrank F2 K ≤ ell) :
    Nat.card (RowFiber A (A.comp M₀)) ≤
      Nat.card (AffineSlice A Q M₀) * 2 ^ (ell * r) := by
…

theorem OAI.MaxCutGames.Inverse.RowErasureColumnMass.column_fraction_eq line 354

Source documentation

The exact uniform fraction of the row fiber occupied by its compatible affine column slice.

theorem column_fraction_eq (A : K →ₗ[F2] R) (Q : Submodule F2 E)
    (M₀ : E →ₗ[F2] K) :
    (Nat.card (AffineSlice A Q M₀) : ℝ) /
        (Nat.card (RowFiber A (A.comp M₀)) : ℝ) =
      1 / (2 : ℝ) ^ (Module.finrank F2 Q * Module.finrank F2 A.ker) := by
…

theorem OAI.MaxCutGames.Inverse.RowErasureColumnMass.column_fraction_ge line 368

Source documentation

At most r independent column constraints retain at least the fraction 2^(-ell*r) of any nonempty row-advice fiber.

theorem column_fraction_ge (A : K →ₗ[F2] R) (Q : Submodule F2 E)
    (M₀ : E →ₗ[F2] K) (ell r : ℕ)
    (hQ : Module.finrank F2 Q ≤ r) (hK : Module.finrank F2 K ≤ ell) :
    1 / (2 : ℝ) ^ (ell * r) ≤
      (Nat.card (AffineSlice A Q M₀) : ℝ) /
        (Nat.card (RowFiber A (A.comp M₀)) : ℝ) := by
…

theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.difference_row_zero line 395
theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.difference_range_le line 408
theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.difference_vanishes_columns line 415
theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.directionEmbedding_surjective line 428
Source documentation
Every actual slice point differs from the base by a unique quotient map.
```
theorem directionEmbedding_surjective (S : Slice ell m)
    (M₀ : Mat ell m) (h₀ : S.Contains M₀) :
    Function.Surjective (S.directionEmbedding M₀ h₀) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.Shortcode.Slice, OAI.MaxCutGames.Inverse.Shortcode.Mat
def OAI.MaxCutGames.Inverse.Shortcode.Slice.directionEquiv line 450
Source documentation
The concrete simultaneous slice is exactly an affine copy of Hom(domain / columnSpan, commonRowKernel).
```
def directionEquiv (S : Slice ell m) (M₀ : Mat ell m) (h₀ : S.Contains M₀) :
    S.Directions ≃ S.points :=
…
```
Mentions: OAI.MaxCutGames.Inverse.Shortcode.Slice, OAI.MaxCutGames.Inverse.Shortcode.Mat
theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.directionEquiv_val line 455
instance OAI.MaxCutGames.Inverse.Shortcode.Slice.directionsFintype line 459
theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.card_points_eq_directions line 467
theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.points_expect_eq_directions line 473
Source documentation
Uniform quotient parameters give precisely the uniform measure on the actual finite slice, including all its inhomogeneous row/column equations.
```
theorem points_expect_eq_directions (S : Slice ell m) (M₀ : Mat ell m)
    (h₀ : S.Contains M₀) (f : Mat ell m → ℝ) :
    S.points.expect f = 𝔼 N : S.Directions, f (M₀ + S.directionMatrix N) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.Shortcode.Slice, OAI.MaxCutGames.Inverse.Shortcode.Mat
theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.directionMatrix_evaluate line 481
theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.direction_affine_target line 489
Source documentation
The decoder's affine offset is the original intercept plus the base matrix evaluated at the target; it is not silently replaced by zero.
```
theorem direction_affine_target (S : Slice ell m) (M₀ : Mat ell m)
    (N : S.Directions) (z : Vector m) (u : Vector ell) :
    evaluate (M₀ + S.directionMatrix N) z + u =
      (N (S.columnSpan.mkQ z) : Vector ell) + (evaluate M₀ z + u) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.Shortcode.Slice, OAI.MaxCutGames.Inverse.Shortcode.Mat, OAI.MaxCutGames.Inverse.Shortcode.Vector, OAI.MaxCutGames.Inverse.Shortcode.evaluate
theorem OAI.MaxCutGames.Inverse.Shortcode.Slice.affineAgreement_eq_directions line 500
def OAI.MaxCutGames.Inverse.RowErasureDescriptionColumnMass.rowFiber line 526
theorem OAI.MaxCutGames.Inverse.RowErasureDescriptionColumnMass.mem_rowFiber line 530
def OAI.MaxCutGames.Inverse.RowErasureDescriptionColumnMass.rowOnly line 535
Source documentation
Forget only the column equations of a slice.
```
def rowOnly {ell m : ℕ} (S : Slice ell m) : Slice ell m where
…
```
theorem OAI.MaxCutGames.Inverse.RowErasureDescriptionColumnMass.rowOnly_contains_iff line 543
theorem OAI.MaxCutGames.Inverse.RowErasureDescriptionColumnMass.rowOnly_points line 556
theorem OAI.MaxCutGames.Inverse.RowErasureDescriptionColumnMass.contains_rowOnly line 562
theorem OAI.MaxCutGames.Inverse.RowErasureDescriptionColumnMass.rowOnly_columnSpan line 566
theorem OAI.MaxCutGames.Inverse.RowErasureDescriptionColumnMass.rowOnly_quotient_finrank line 572
theorem OAI.MaxCutGames.Inverse.RowErasureDescriptionColumnMass.rowFiber_card line 584
Source documentation
The size of an actual nonempty row fiber, in the same coordinates used by the selector's uniform matrix sample.
```
theorem rowFiber_card {ell m : ℕ} (S : Slice ell m) (M₀ : Mat ell m)
    (h₀ : S.Contains M₀) :
    (rowFiber S.rowCoefficient S.rowValue).card =
      2 ^ (m * Module.finrank F2 S.rowMap.ker) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasureDescriptionColumnMass.rowFiber
theorem OAI.MaxCutGames.Inverse.RowErasureDescriptionColumnMass.rowFiber_nonempty line 593
theorem OAI.MaxCutGames.Inverse.RowErasureDescriptionColumnMass.column_fraction_ge line 603
Source documentation
The chosen nonempty column event has the required mass inside its actual row-advice fiber. The target coefficient and intercept do not affect its size.
```
theorem column_fraction_ge {ell m r : ℕ} (d : Description ell m r)
    (hne : d.toSlice.points.Nonempty) :
    1 / (2 : ℝ) ^ (ell * r) ≤
      (d.toSlice.points.card : ℝ) / ((rowFiber d.1 d.2.1).card : ℝ) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasureDescriptionColumnMass.rowFiber
def OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedPoints line 640
def OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedHit line 646
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedPoints_of_good line 650
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedHit_of_good line 657
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedPoints_support line 670
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedEvent_iff_points line 684
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedMatch_iff_points line 700
theorem OAI.MaxCutGames.Inverse.RowErasure.SliceFamily.selectedPoints_match_sum line 718
theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.selectedPoints_column_mass line 745
theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.selected_event_mass_ge line 762
theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.selected_match_mass_ge line 789
def OAI.MaxCutGames.Inverse.RowErasureMatrix.selectedEventMass line 813
def OAI.MaxCutGames.Inverse.RowErasureMatrix.selectedMatchMass line 816
theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.selectedEventMass_ge line 819
theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.selectedMatchMass_ge line 832
theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.selectedEventMass_weighted_ge line 841
Source documentation
Context weights may be the pushforward of verifier seeds and need not be uniform on distinct questions. Normalization is not needed for this inequality.
```
theorem selectedEventMass_weighted_ge {Q : Type*} [Fintype Q]
    (w : Q → ℝ) (hw : ∀ q, 0 ≤ w q) (f : Q → Mat ell m → Vector ell)
    (α g₀ : ℝ)
    (hgood : g₀ ≤ ∑ q, w q * adviceMass ((family ell m r).goodAt (f q) α)) :
    (1 / (2 : ℝ) ^ (ell * r)) * g₀ ≤ ∑ q, w q * selectedEventMass r (f q) α := by
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasureMatrix.family, OAI.MaxCutGames.Inverse.RowErasureMatrix.selectedEventMass
theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.selectedMatchMass_weighted_ge line 859
theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.selectedMatchMass_conditional_ge line 873
theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.selectedEventMass_contextual_ge line 881
Source documentation
The same bound for a uniform finite seed space, allowing repeated contexts.
```
theorem selectedEventMass_contextual_ge {Q : Type*} [Fintype Q]
    (f : Q → Mat ell m → Vector ell) (α g₀ : ℝ)
    (hgood : g₀ ≤ 𝔼 q, adviceMass ((family ell m r).goodAt (f q) α)) :
    (1 / (2 : ℝ) ^ (ell * r)) * g₀ ≤ 𝔼 q, selectedEventMass r (f q) α := by
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasureMatrix.family, OAI.MaxCutGames.Inverse.RowErasureMatrix.selectedEventMass
theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.selectedMatchMass_contextual_ge line 890