MatrixChartKMSNeighbors.lean`

44 declarations, 0 contain sorry, 0 declared as axioms

Exact full-neighbor count in the KMS vertex representation.

def OAI.MaxCutGames.Inverse.MatrixChart.grassmannNeighborsMapEquiv line 14

Source documentation

Ambient linear equivalence transports the actual neighbor subspaces.

noncomputable def grassmannNeighborsMapEquiv
    {E F : Type*} [AddCommGroup E] [Module (ZMod 2) E]
    [AddCommGroup F] [Module (ZMod 2) F]
    (e : E ≃ₗ[ZMod 2] F) (L : Submodule (ZMod 2) E) :
    GrassmannNeighbors L ≃ GrassmannNeighbors (L.map e.toLinearMap) := by
…

Mentions: OAI.MaxCutGames.Inverse.MatrixChart.GrassmannNeighbors

def OAI.MaxCutGames.Inverse.MatrixChart.kmsNeighborsEquiv line 31
Source documentation
Extrinsic submodule neighbors and the finite KMS neighbor predicate agree.
```
def kmsNeighborsEquiv {n ell : Nat} (L : KMS.Vertex n ell) :
    GrassmannNeighbors L.val ≃ {W : KMS.Vertex n ell // KMS.Adjacent L W} where
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.MatrixChart.GrassmannNeighbors, OAI.MaxCutGames.Inverse.KMS.Adjacent
theorem OAI.MaxCutGames.Inverse.MatrixChart.card_full_neighbors line 46
theorem OAI.MaxCutGames.Inverse.MatrixChart.card_full_neighbors_twice line 62
Source documentation
Exactly two full Grassmann neighbors for every nonzero factor pair.
```
theorem card_full_neighbors_twice {ell m : Nat} (M : Matrix (Fin ell) (Fin m) (ZMod 2)) :
    (KMS.neighbors (matrixVertex M)).card =
      2 * ((2 ^ ell - 1) * (2 ^ m - 1)) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.neighbors, OAI.MaxCutGames.Inverse.MatrixChart.matrixVertex
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.relativeDensity_eq_expect_subtype_inline_KMSBasisComparisonNeighborsRetention line 81
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.outsideNeighbor_retention line 100
Source documentation
The ordered-basis test conditioned on its good event samples every full Grassmann neighbor uniformly. The target observable is the original lifted indicator, so this identity directly feeds the matrix-test retention bound.
```
theorem outsideNeighbor_retention {n ell : ℕ} (S : Finset (KMS.Vertex n ell))
    (X : BasisMap n ell) (hX : Function.Injective X) :
    (𝔼 p : OutsideNeighborFactors X,
      liftedIndicator S (rankOneUpdate X p.1.val p.2.val)) =
        KMS.relativeDensity S (KMS.neighbors (rangeVertex X hX)) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.OutsideNeighborFactors, OAI.MaxCutGames.Inverse.KMSBasisComparison.liftedIndicator, OAI.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdate, OAI.MaxCutGames.Inverse.KMS.relativeDensity, OAI.MaxCutGames.Inverse.KMS.neighbors, OAI.MaxCutGames.Inverse.KMSBasisComparison.rangeVertex
def OAI.MaxCutGames.Inverse.KMSBasisComparison.fullStepRetention line 153
Source documentation
The complete rank-one update experiment at a specified starting map.
```
def fullStepRetention {n ell : ℕ} (S : Finset (KMS.Vertex n ell))
    (X : BasisMap n ell) : ℝ :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap
def OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRetention line 159
Source documentation
Start uniformly in the lifted set, then run the unconditioned update.
```
def liftRetention {n ell : ℕ} (S : Finset (KMS.Vertex n ell)) : ℝ :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex
def OAI.MaxCutGames.Inverse.KMSBasisComparison.goodParametersEquiv line 163
Source documentation
Equivalence of the two explicit presentations of the good sampling event.
```
def goodParametersEquiv {n ell : ℕ} (X : BasisMap n ell) :
    goodParameters X ≃ OutsideNeighborFactors X where
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.goodParameters, OAI.MaxCutGames.Inverse.KMSBasisComparison.OutsideNeighborFactors
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.goodParameters_expect line 173
Source documentation
Good-event conditioning is the exact full-neighbor Grassmann retention.
```
theorem goodParameters_expect {n ell : ℕ} (S : Finset (KMS.Vertex n ell))
    (X : BasisMap n ell) (hX : Function.Injective X) :
    (goodParameters X).expect
      (fun p => liftedIndicator S (rankOneUpdate X p.1 p.2)) =
        KMS.relativeDensity S (KMS.neighbors (rangeVertex X hX)) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.goodParameters, OAI.MaxCutGames.Inverse.KMSBasisComparison.liftedIndicator, OAI.MaxCutGames.Inverse.KMSBasisComparison.rankOneUpdate, OAI.MaxCutGames.Inverse.KMS.relativeDensity, OAI.MaxCutGames.Inverse.KMS.neighbors, OAI.MaxCutGames.Inverse.KMSBasisComparison.rangeVertex
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.fullStepRetention_compare line 187
Source documentation
Quantitative local comparison, with a slightly smaller exceptional-mass bound than the stated KMS Lemma 2.7.
```
theorem fullStepRetention_compare {n ell : ℕ} (S : Finset (KMS.Vertex n ell))
    (X : BasisMap n ell) (hX : Function.Injective X) :
    |fullStepRetention S X -
      KMS.relativeDensity S (KMS.neighbors (rangeVertex X hX))| ≤
        ((2 : ℝ) ^ ell)⁻¹ + (2 : ℝ) ^ ell / (2 : ℝ) ^ n := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.fullStepRetention, OAI.MaxCutGames.Inverse.KMS.relativeDensity, OAI.MaxCutGames.Inverse.KMS.neighbors, OAI.MaxCutGames.Inverse.KMSBasisComparison.rangeVertex
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRange_retention_expect line 201
Source documentation
Choosing a uniform accepted ordered basis chooses a uniform element of the original Grassmann set.
```
theorem liftRange_retention_expect {n ell : ℕ} (S : Finset (KMS.Vertex n ell)) :
    (𝔼 X : lift S,
      KMS.relativeDensity S (KMS.neighbors (liftRange S X).val)) = KMS.retention S := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.lift, OAI.MaxCutGames.Inverse.KMS.relativeDensity, OAI.MaxCutGames.Inverse.KMS.neighbors, OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRange, OAI.MaxCutGames.Inverse.KMS.retention
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRetention_compare line 215
Source documentation
The actual full sampling-law comparison for the lifted Grassmann set.
```
theorem liftRetention_compare {n ell : ℕ} (S : Finset (KMS.Vertex n ell))
    (hS : S.Nonempty) :
    |liftRetention S - KMS.retention S| ≤
      ((2 : ℝ) ^ ell)⁻¹ + (2 : ℝ) ^ ell / (2 : ℝ) ^ n := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRetention, OAI.MaxCutGames.Inverse.KMS.retention
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRetention_compare_kms line 231
Source documentation
The bound in the primary statement, with ordinary quotient notation instead of an integer exponent ell - n.
```
theorem liftRetention_compare_kms {n ell : ℕ} (S : Finset (KMS.Vertex n ell))
    (hS : S.Nonempty) :
    |liftRetention S - KMS.retention S| ≤
      ((2 : ℝ) ^ ell)⁻¹ + 2 * ((2 : ℝ) ^ ell / (2 : ℝ) ^ n) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRetention, OAI.MaxCutGames.Inverse.KMS.retention
def OAI.MaxCutGames.Inverse.KMSBasisComparison.liftDensity line 239
Source documentation
The indicator's density in the full linear-map space.
```
def liftDensity {n ell : ℕ} (S : Finset (KMS.Vertex n ell)) : ℝ :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.liftDensity_eq_card line 242
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.liftDensity_pos line 247
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.liftDensity_mul_retention line 256
Source documentation
Fourier correlation uses the full ambient space. This identity is the exact conversion to the conditional-start retention and preserves density.
```
theorem liftDensity_mul_retention {n ell : ℕ} (S : Finset (KMS.Vertex n ell)) :
    liftDensity S * liftRetention S =
      𝔼 X : BasisMap n ell, liftedIndicator S X * fullStepRetention S X := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.liftDensity, OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRetention, OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.liftedIndicator, OAI.MaxCutGames.Inverse.KMSBasisComparison.fullStepRetention
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.fullStepRetention_eq_noise line 267
Source documentation
Swapping the independent factors matches the Fourier noise convention of first choosing a direction, then a functional, including both zero cases.
```
theorem fullStepRetention_eq_noise {n ell : ℕ} (S : Finset (KMS.Vertex n ell))
    (X : BasisMap n ell) :
    fullStepRetention S X =
      𝔼 y : KMS.Ambient n, 𝔼 a : Functional ell,
        liftedIndicator S (X + a.smulRight y) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.fullStepRetention, OAI.MaxCutGames.Inverse.KMS.Ambient, OAI.MaxCutGames.Inverse.KMSBasisComparison.Functional, OAI.MaxCutGames.Inverse.KMSBasisComparison.liftedIndicator
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRetention_le_of_correlation_le line 278
Source documentation
A proved ambient correlation bound converts directly to the conditional retention bound; positive density follows from the actual nonempty lift.
```
theorem liftRetention_le_of_correlation_le {n ell : ℕ}
    (S : Finset (KMS.Vertex n ell)) (hS : S.Nonempty) (ζ : ℝ)
    (hc : (𝔼 X : BasisMap n ell,
      liftedIndicator S X * fullStepRetention S X) ≤ ζ * liftDensity S) :
    liftRetention S ≤ ζ := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.liftedIndicator, OAI.MaxCutGames.Inverse.KMSBasisComparison.fullStepRetention, OAI.MaxCutGames.Inverse.KMSBasisComparison.liftDensity, OAI.MaxCutGames.Inverse.KMSBasisComparison.liftRetention
def OAI.MaxCutGames.Inverse.KMSBasisComparison.LiftExpansionPrinciple line 297
Source documentation
The precise analytic obligation at the ordered-basis lift. Its constants are fixed before the tuple length, which is fixed before the ambient size.
```
def LiftExpansionPrinciple : Prop :=
…
```
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.exists_binary_ratio_threshold line 307
Source documentation
Elementary eventual decay, using Archimedean unboundedness of powers. No dimensional rate is hidden in a limit or a filter assumption.
```
theorem exists_binary_ratio_threshold (c ε : ℝ) (hε : 0 < ε) :
    ∃ k : ℕ, ∀ n : ℕ, k ≤ n → c / (2 : ℝ) ^ n ≤ ε := by
…
```
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.nonempty_of_relativeDensity_pos line 320
Source documentation
Positive relative density implies a nonempty intersection, even though relative density itself is defined to be zero on empty intervals.
```
theorem nonempty_of_relativeDensity_pos {Ω : Type*} [DecidableEq Ω]
    (S I : Finset Ω) (h : 0 < KMS.relativeDensity S I) : (S ∩ I).Nonempty := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.relativeDensity
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.expansion_of_liftExpansion line 328
Source documentation
The complete inverse implication from the explicit analytic lift theorem to the dimension-uniform Grassmann theorem required by the v2 inverse.
```
theorem expansion_of_liftExpansion (h : LiftExpansionPrinciple) :
    KMS.ExpansionPrinciple := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparison.LiftExpansionPrinciple, OAI.MaxCutGames.Inverse.KMS.ExpansionPrinciple

theorem OAI.MaxCutGames.Inverse.KMSMomentToExpansion.liftExpansion_of_upperMoments line 371

Source documentation

Any proved dimension-independent upper moment with a finite local budget supplies the exact ordered-basis expansion interface.

theorem liftExpansion_of_upperMoments
    (C : ℕ → ℝ) (hC : ∀ r, 0 ≤ C r) (R ellMin : ℕ → ℕ)
    (hupper : ∀ r : ℕ, ∀ ε : ℝ, 0 ≤ ε → ε ≤ 1 →
      ∀ ell : ℕ, ellMin r ≤ ell → ∀ n : ℕ,
      ∀ S : Finset (Vertex n ell), TuplePseudorandom S (R r) ε →
      ∀ i : ℕ, i ≤ r →
        (𝔼 X : BasisMap n ell, rankComponent i (liftedIndicator S) X ^ 4) ≤
          C r * (𝔼 X : BasisMap n ell, rankComponent i (liftedIndicator S) X ^ 2) * ε) :
    LiftExpansionPrinciple := by
…

theorem OAI.MaxCutGames.Inverse.KMSMomentToExpansion.expansion_of_upperMoments line 412

Source documentation

Checked finite bridges and parameter choices reduce the full KMS expansion principle to the displayed actual upper-moment estimate, and nothing weaker.

theorem expansion_of_upperMoments
    (C : ℕ → ℝ) (hC : ∀ r, 0 ≤ C r) (R ellMin : ℕ → ℕ)
    (hupper : ∀ r : ℕ, ∀ ε : ℝ, 0 ≤ ε → ε ≤ 1 →
      ∀ ell : ℕ, ellMin r ≤ ell → ∀ n : ℕ,
      ∀ S : Finset (Vertex n ell), TuplePseudorandom S (R r) ε →
      ∀ i : ℕ, i ≤ r →
        (𝔼 X : BasisMap n ell, rankComponent i (liftedIndicator S) X ^ 4) ≤
          C r * (𝔼 X : BasisMap n ell, rankComponent i (liftedIndicator S) X ^ 2) * ε) :
    KMS.ExpansionPrinciple :=
…

Mentions: OAI.MaxCutGames.Inverse.KMS.ExpansionPrinciple

theorem OAI.MaxCutGames.Inverse.KMSExpansion.kms_expansion line 436
Source documentation
The KMS expansion theorem with constants independent of both dimensions and with the ambient threshold chosen after the plane dimension.
```
theorem kms_expansion : KMS.ExpansionPrinciple := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.ExpansionPrinciple
def OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.matrixFiber line 453
def OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.liftedFiber line 456
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.liftedFiber_subset_chart line 459
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.matrixVertex_mem_liftedFiber line 466
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.image_slice_points line 480
Source documentation
The slice and the interval intersected with the chart correspond exactly. The hypothesis states equality of the actual membership predicates.
```
theorem image_slice_points {ell m : ℕ} (S : Slice ell m)
    (I : Finset (KMS.Vertex (ell + m) ell))
    (hS : ∀ M, S.Contains M ↔ matrixVertex M ∈ I) :
    S.points.image matrixVertex = I ∩ matrixChart ell m := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.image_slice_fiber line 496
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.constantAgreement_eq_chart_density line 520
Source documentation
Uniform agreement on a slice is the actual Grassmann fiber density in the chart-intersected interval. Empty sets are allowed on both sides of this identity, with the standard zero-denominator convention.
```
theorem constantAgreement_eq_chart_density {ell m : ℕ} (S : Slice ell m)
    (I : Finset (KMS.Vertex (ell + m) ell))
    (hS : ∀ M, S.Contains M ↔ matrixVertex M ∈ I)
    (f : Mat ell m → Vector ell) (y : Vector ell) :
    S.constantAgreement f y =
      KMS.relativeDensity (liftedFiber f y) (I ∩ matrixChart ell m) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMS.relativeDensity, OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.liftedFiber
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.hasAffineSlice_of_dense_interval line 531
theorem OAI.MaxCutGames.Inverse.MatrixChart.span_basis_values line 562
theorem OAI.MaxCutGames.Inverse.MatrixChart.lowerRows_basis line 569

theorem OAI.MaxCutGames.Inverse.MatrixChart.mem_iff_annihilator_basis line 575

Source documentation

Checking an annihilator basis suffices to test membership in a subspace.

theorem mem_iff_annihilator_basis {ι : Type*} (B : Submodule K (X × Y))
    (b : Module.Basis ι K B.dualAnnihilator) (x : X × Y) :
    x ∈ B ↔ ∀ i, (b i).val x = 0 := by
…

theorem OAI.MaxCutGames.Inverse.MatrixChart.functional_coordinate_decomposition line 590
Source documentation
Split a product functional into its two coordinate functionals.
```
theorem functional_coordinate_decomposition (φ : (X × Y) →ₗ[K] K) (x : X) (y : Y) :
    φ (x, y) = φ (x, 0) + φ (0, y) := by
…
```
theorem OAI.MaxCutGames.Inverse.MatrixChart.upperColumns_annihilator_basis line 595

theorem OAI.MaxCutGames.Inverse.MatrixChart.exists_interval_coordinates line 618

Source documentation

Coordinates for an arbitrary interval. There are exactly dim A rows and codim B columns, so an interval order bound gives the required slice bound.

theorem exists_interval_coordinates [FiniteDimensional K X] [FiniteDimensional K Y]
    (A B : Submodule K (X × Y)) :
    ∃ (n_r n_c : Nat) (d : Fin n_r → X) (s : Fin n_r → Y)
      (t : Fin n_c → X →ₗ[K] K) (q : Fin n_c → Y →ₗ[K] K),
      n_r = Module.finrank K A ∧ n_c = Module.finrank K ((X × Y) ⧸ B) ∧
      ∀ T : X →ₗ[K] Y,
        (A ≤ T.graph ∧ T.graph ≤ B) ↔
          ((∀ i, T (d i) = s i) ∧ (∀ j, (q j).comp T = t j)) := by
…

theorem OAI.MaxCutGames.Inverse.MatrixChart.dotFunctional_surjective line 653
theorem OAI.MaxCutGames.Inverse.MatrixChart.exists_matrix_interval_slice line 664

theorem OAI.MaxCutGames.Inverse.MatrixChart.exists_bounded_matrix_interval_slice line 685

Source documentation

An interval order bound yields separate row and column budgets.

theorem exists_bounded_matrix_interval_slice
    (A B : Submodule K ((ι → K) × (κ → K))) (r : Nat)
    (horder : Module.finrank K A +
      Module.finrank K (((ι → K) × (κ → K)) ⧸ B) ≤ r) :
    ∃ (n_r n_c : Nat) (d : Fin n_r → ι → K) (s : Fin n_r → κ → K)
      (t : Fin n_c → ι → K) (q : Fin n_c → κ → K),
      n_r ≤ r ∧ n_c ≤ r ∧
      ∀ M : Matrix ι κ K,
        (A ≤ matrixGraph M ∧ matrixGraph M ≤ B) ↔
          ((∀ i, d i ᵥ* M = s i) ∧ (∀ j, M *ᵥ q j = t j)) := by
…

Mentions: OAI.MaxCutGames.Inverse.MatrixChart.matrixGraph