RowErasureSelectionNormalization.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Normalize the affine target chosen from visible row advice. The selected row and column equations are unchanged. Only the target coefficient and intercept are replaced, with exact target equality on the entire selected slice.

def OAI.MaxCutGames.Inverse.RowErasureDescriptions.Description.withTarget line 18
Source documentation
Replace the affine target while retaining all row and column data.
```
def Description.withTarget {ell m r : ℕ} (d : Description ell m r)
    (z : Vector m) (u : Vector ell) : Description ell m r :=
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasureDescriptions.Description
theorem OAI.MaxCutGames.Inverse.RowErasureDescriptions.Description.withTarget_toSlice line 22
theorem OAI.MaxCutGames.Inverse.RowErasureDescriptions.Description.withTarget_coefficient line 26
theorem OAI.MaxCutGames.Inverse.RowErasureDescriptions.Description.withTarget_intercept line 30

theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.exists_normalizedChosenDescription line 49

Source documentation

Normalization of the already chosen description. The sampled matrix is absent from the selector's inputs; pointwise target equality holds afterward for every matrix in the selected slice.

theorem exists_normalizedChosenDescription
    (f : Mat ell m → Vector ell) (α : ℝ) (A : RowMap ell r) (S : Mat r m)
    (hgood : (family ell m r).GoodAdvice f α A S)
    (e : Vector m →ₗ[F2] F2)
    (hfold : ∀ (h : Vector ell) M,
      f (M + rankOne h (functionalRow e)) = f M + h)
    (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (ell - r) < α / 8) :
    let d₀ := (family ell m r).chosenDescription f α A S hgood
…

Mentions: OAI.MaxCutGames.Inverse.RowErasureMatrix.family

def OAI.MaxCutGames.Inverse.RowErasureMatrix.normalizedChosenDescription line 90

Source documentation

A fixed normalized witness determined by the visible table and row advice. All remaining inputs are the fixed normalization functional and proofs.

def normalizedChosenDescription
    (f : Mat ell m → Vector ell) (α : ℝ) (A : RowMap ell r) (S : Mat r m)
    (hgood : (family ell m r).GoodAdvice f α A S)
    (e : Vector m →ₗ[F2] F2)
    (hfold : ∀ (h : Vector ell) M,
      f (M + rankOne h (functionalRow e)) = f M + h)
    (hα : 0 < α) (hsmall : 1 / (2 : ℝ) ^ (ell - r) < α / 8) :
    Description ell m r :=
…

Mentions: OAI.MaxCutGames.Inverse.RowErasureMatrix.family

theorem OAI.MaxCutGames.Inverse.RowErasureMatrix.normalizedChosenDescription_spec line 100