ShortcodeInterfaceLemmas.lean`

77 declarations, 0 contain sorry, 0 declared as axioms

The shortcode inverse principle uses an arbitrary table function, full uniform factor sampling, and an affine intercept.

abbrev OAI.UniqueGamesTheorem.Inverse.Shortcode.F2 line 30
abbrev OAI.UniqueGamesTheorem.Inverse.Shortcode.Vector line 31
abbrev OAI.UniqueGamesTheorem.Inverse.Shortcode.Mat line 32
def OAI.UniqueGamesTheorem.Inverse.Shortcode.rankOne line 34
def OAI.UniqueGamesTheorem.Inverse.Shortcode.evaluate line 37
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.evaluate_zero line 40
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.rankOne_zero_left line 44
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.rankOne_zero_right line 49
def OAI.UniqueGamesTheorem.Inverse.Shortcode.equalityAcceptance line 56
Source documentation
Both perturbation factors are independent uniform vectors, including zero. The matrix is sampled independently as well.
```
def equalityAcceptance {ell m : ℕ} (f : Mat ell m → Vector ell) : ℝ :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Mat, OAI.UniqueGamesTheorem.Inverse.Shortcode.Vector
structure OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice line 61
Source documentation
A description includes possibly dependent equations; the row and column counts need not equal their ranks.
```
structure Slice (ell m : ℕ) where
…
```
def OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.Contains line 69
def OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.points line 73
def OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.affineAgreement line 76
def OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.constantAgreement line 80
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.constantAgreement_eq_affine line 86
Source documentation
The fiber/Grassmann route produces the constant affine target 0,u. Keeping u is essential: this result does not claim a homogeneous target.
```
theorem Slice.constantAgreement_eq_affine {ell m : ℕ} (S : Slice ell m)
    (f : Mat ell m → Vector ell) (u : Vector ell) :
    S.constantAgreement f u = S.affineAgreement f 0 u := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice, OAI.UniqueGamesTheorem.Inverse.Shortcode.Mat, OAI.UniqueGamesTheorem.Inverse.Shortcode.Vector
def OAI.UniqueGamesTheorem.Inverse.Shortcode.HasAffineSlice line 91
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.hasAffineSlice_of_constant line 95
def OAI.UniqueGamesTheorem.Inverse.Shortcode.InversePrinciple line 105
Source documentation
Dimension-uniform inverse statement. The constants α,r depend only on η; only the final input dimension threshold may depend on ell. There is no folding assumption, and no inverse-theorem certificate is hidden in f.
```
def InversePrinciple : Prop :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.dotFunctional_zero_binary line 133
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.dotFunctional_ne_zero line 140
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.vecMulLinear_rankOne line 146
Source documentation
The shortcode outer product is precisely the rank-one chart map.
```
theorem vecMulLinear_rankOne (a : Vector ell) (l : Vector m) :
    (rankOne a l).vecMulLinear = (dotFunctional a).smulRight l := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.dotFunctional
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.vecMulLinear_add_rankOne line 154
Source documentation
This is the exact perturbation, including its functional/vector order.
```
theorem vecMulLinear_add_rankOne (M : Mat ell m) (a : Vector ell) (l : Vector m) :
    (M + rankOne a l).vecMulLinear = M.vecMulLinear + (dotFunctional a).smulRight l := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.dotFunctional
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.adjacent_matrixVertex_add_rankOne line 164
abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.NonzeroVectorFactors line 173
abbrev OAI.UniqueGamesTheorem.Inverse.MatrixChart.MatrixVertexChartNeighbors line 178
Source documentation
Actual Grassmann vertices adjacent to matrixVertex M and remaining inside the finite matrix chart.
```
abbrev MatrixVertexChartNeighbors (M : Mat ell m) :=
…
```
def OAI.UniqueGamesTheorem.Inverse.MatrixChart.vectorFactorMatrixNeighbor line 182
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.vectorFactorMatrixNeighbor_injective line 188
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.vectorFactorMatrixNeighbor_surjective line 199
def OAI.UniqueGamesTheorem.Inverse.MatrixChart.vectorFactorsEquivMatrixVertexChartNeighbors line 228
Source documentation
Uniform independent nonzero vector factors induce exactly uniform neighbors of the actual Grassmann vertex within the matrix chart.
```
noncomputable def vectorFactorsEquivMatrixVertexChartNeighbors (M : Mat ell m) :
    NonzeroVectorFactors ell m ≃ MatrixVertexChartNeighbors M :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.NonzeroVectorFactors, OAI.UniqueGamesTheorem.Inverse.MatrixChart.MatrixVertexChartNeighbors
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.vectorFactorsEquivMatrixVertexChartNeighbors_apply line 233
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.card_matrixVertexChartNeighbors line 239
Source documentation
The chart degree in the actual KMS vertex type.
```
theorem card_matrixVertexChartNeighbors (M : Mat ell m) :
    Nat.card (MatrixVertexChartNeighbors M) = (2 ^ ell - 1) * (2 ^ m - 1) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.MatrixChart.MatrixVertexChartNeighbors
theorem OAI.UniqueGamesTheorem.Inverse.MatrixChart.exists_shortcode_slice line 261
def OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.rowMap line 331
Source documentation
The simultaneous row functionals, allowing dependent and zero rows.
```
def rowMap (S : Slice ell m) : Vector ell →ₗ[F2] Vector S.rows :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice, OAI.UniqueGamesTheorem.Inverse.Shortcode.Vector, OAI.UniqueGamesTheorem.Inverse.Shortcode.F2
def OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.columnSpan line 335
Source documentation
Column specifications fix the matrix on this entire subspace.
```
def columnSpan (S : Slice ell m) : Submodule F2 (Vector m) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice, OAI.UniqueGamesTheorem.Inverse.Shortcode.F2, OAI.UniqueGamesTheorem.Inverse.Shortcode.Vector
abbrev OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.Directions line 339
Source documentation
Free directions of a row/column slice, intrinsically as quotient maps.
```
abbrev Directions (S : Slice ell m) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice
def OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.directionMap line 342
def OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.directionMatrix line 346
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.directionMatrix_injective line 349
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.directionMatrix_row line 360
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.directionMatrix_column line 369
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.contains_add_direction line 379
def OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.directionEmbedding line 396
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.columnSpan_finrank_le line 406
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.quotient_finrank_ge line 414
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.rowKernel_finrank_ge line 422
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.card_directions line 431
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.card_directions_le line 439
Source documentation
A nonempty affine slice is at least as large as its free-direction space.
```
theorem card_directions_le (S : Slice ell m) (hne : S.points.Nonempty) :
    Nat.card S.Directions ≤ S.points.card := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.pow_dimension_le_card line 450
Source documentation
The size bound, with truncation making it valid also in small dimensions. There is no independence hypothesis on the listed equations.
```
theorem pow_dimension_le_card (S : Slice ell m) (r : ℕ)
    (hrows : S.rows ≤ r) (hcolumns : S.columns ≤ r)
    (hne : S.points.Nonempty) :
    2 ^ ((ell - r) * (m - r)) ≤ S.points.card := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.evaluate_eq_toLin line 484
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.row_equations_iff line 487
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.contains_iff_inSlice line 510
Source documentation
This is an equivalence of the actual equations, not merely a cardinality comparison or a homogeneous approximation of the affine slice.
```
theorem contains_iff_inSlice (S : Slice ell m) (M₀ : Mat ell m)
    (hM₀ : S.Contains M₀) (M : Mat ell m) :
    S.Contains M ↔
      AffineWitness.InSlice S.rowMap S.columnSpan
        (Matrix.toLin' M₀) (Matrix.toLin' M) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice, OAI.UniqueGamesTheorem.Inverse.Shortcode.Mat, OAI.UniqueGamesTheorem.Inverse.AffineWitness.InSlice
def OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.linearSliceEquiv line 530
Source documentation
Exact finite sample-space equivalence between the matrix representation and the linear-map representation of a nonempty affine slice.
```
def linearSliceEquiv (S : Slice ell m) (M₀ : Mat ell m)
    (hM₀ : S.Contains M₀) :
    S.points ≃ AffineWitness.Slice S.rowMap S.columnSpan (Matrix.toLin' M₀) where
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice, OAI.UniqueGamesTheorem.Inverse.Shortcode.Mat, OAI.UniqueGamesTheorem.Inverse.AffineWitness.Slice
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.affineAgreement_eq_of_target_eq line 549
Source documentation
Pointwise preservation on the genuine slice preserves its exact uniform affine agreement, including the empty-slice convention.
```
theorem affineAgreement_eq_of_target_eq (S : Slice ell m)
    (f : Mat ell m → Vector ell) (z z' : Vector m) (u u' : Vector ell)
    (htarget : ∀ M, S.Contains M → evaluate M z' + u' = evaluate M z + u) :
    S.affineAgreement f z' u' = S.affineAgreement f z u := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice, OAI.UniqueGamesTheorem.Inverse.Shortcode.Mat, OAI.UniqueGamesTheorem.Inverse.Shortcode.Vector, OAI.UniqueGamesTheorem.Inverse.Shortcode.evaluate
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.affineAgreement_eq_of_linear_target_eq line 560
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.affineAgreement_translate line 572
Source documentation
Changing the representative inside the column span and correcting the intercept leaves the shortcode agreement exactly unchanged.
```
theorem affineAgreement_translate (S : Slice ell m)
    (M₀ : Mat ell m) (hM₀ : S.Contains M₀)
    (f : Mat ell m → Vector ell) (z w : Vector m) (hw : w ∈ S.columnSpan)
    (u : Vector ell) :
    S.affineAgreement f (z + w) (u + evaluate M₀ w) =
      S.affineAgreement f z u := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice, OAI.UniqueGamesTheorem.Inverse.Shortcode.Mat, OAI.UniqueGamesTheorem.Inverse.Shortcode.Vector, OAI.UniqueGamesTheorem.Inverse.Shortcode.evaluate
def OAI.UniqueGamesTheorem.Inverse.Shortcode.functionalRow line 603
Source documentation
The coordinate row of a binary linear functional.
```
def functionalRow (e : Vector m →ₗ[F2] F2) : Vector m :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Vector, OAI.UniqueGamesTheorem.Inverse.Shortcode.F2
theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.toMatrix_shift line 606

theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.affineAgreement_eq_linear_ratio line 620

Source documentation

Exact density identity on the complete nonempty affine slice, with no lost conditioning factor in the change from matrices to linear maps.

theorem affineAgreement_eq_linear_ratio (S : Slice ell m)
    (M₀ : Mat ell m) (hM₀ : S.Contains M₀)
    (f : Mat ell m → Vector ell) (z : Vector m) (u : Vector ell) :
    S.affineAgreement f z u =
      (Nat.card {N : AffineWitness.Slice S.rowMap S.columnSpan (Matrix.toLin' M₀) //
        f (LinearMap.toMatrix' N.val) = N.val z + u} : ℝ) /
      (Nat.card (AffineWitness.Slice S.rowMap S.columnSpan (Matrix.toLin' M₀)) : ℝ) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice.first_bit_normalization line 639

Source documentation

First-bit normalization for the exact selected shortcode slice. The original affine agreement is preserved, not merely bounded below.

theorem first_bit_normalization (S : Slice ell m)
    (M₀ : Mat ell m) (hM₀ : S.Contains M₀)
    (e : Vector m →ₗ[F2] F2)
    (f : Mat ell m → Vector ell) (z : Vector m) (u : Vector ell)
    (hfold : ∀ (h : S.rowMap.ker) M,
      f (M + rankOne h (functionalRow e)) = f M + h)
    (α : ℝ) (hα : 0 < α) (hgood : α / 2 ≤ S.affineAgreement f z u)
    (hsmall : 1 / (2 : ℝ) ^ (ell - S.rows) < α / 8) :
    ∃ z' : Vector m, ∃ u' : Vector ell, e z' = 1 ∧
      S.affineAgreement f z' u' = S.affineAgreement f z u ∧
      ∀ M, S.Contains M → evaluate M z' + u' = evaluate M z + u := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.Shortcode.Slice, OAI.UniqueGamesTheorem.Inverse.Shortcode.Mat, OAI.UniqueGamesTheorem.Inverse.Shortcode.Vector, OAI.UniqueGamesTheorem.Inverse.Shortcode.F2, OAI.UniqueGamesTheorem.Inverse.Shortcode.rankOne, OAI.UniqueGamesTheorem.Inverse.Shortcode.functionalRow, OAI.UniqueGamesTheorem.Inverse.Shortcode.evaluate

abbrev OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.RowMap line 690
Source documentation
A row map is represented by all its binary matrix coefficients.
```
abbrev RowMap (ell r : ℕ) := Fin r → Vector ell
```
abbrev OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.Description line 695
Source documentation
Ordered padded row coefficients, row values, column coefficients, column values, affine coefficient, and affine intercept. Redundant descriptions are intentional: counting descriptions provides an upper bound on distinct slices.
```
abbrev Description (ell m r : ℕ) :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.card_vector line 699
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.card_rowMap line 702
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.card_description line 705
def OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.Description.toSlice line 712
def OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.Description.coefficient line 720
def OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.Description.intercept line 723
def OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.padZero line 727
Source documentation
Add vacuous equations after the original finite list.
```
def padZero {n r : ℕ} {V : Type*} [Zero V] (f : Fin n → V) : Fin r → V :=
…
```
def OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.padSlice line 730
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.padSlice_contains_iff line 738
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.padSlice_points line 762
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.padSlice_affineAgreement line 769
def OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.describe line 775
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.describe_toSlice line 780
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.describe_coefficient line 784
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.describe_intercept line 787
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.exists_description line 792
Source documentation
Every slice/target returned by the bounded inverse theorem has a fixed-size description with the same solution set and exactly the same agreement.
```
theorem exists_description {ell m r : ℕ} (S : Slice ell m)
    (hrows : S.rows ≤ r) (hcols : S.columns ≤ r)
    (z : Vector m) (u : Vector ell) :
    ∃ d : Description ell m r, d.toSlice.points = S.points ∧
      d.coefficient = z ∧ d.intercept = u := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptions.Description