ShortcodeFromGrassmannLemmas.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The exact finite sampling conversion in the v2 shortcode proof. Independent nonzero binary vector factors parametrize chart neighbors bijectively; the full Grassmann degree is twice the chart degree. These identities imply the exact factor one half, including its averaging over a nonempty output fiber.

def OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.zeroFactorMass line 19
Source documentation
The exact self-loop mass when independent uniform binary factors include zero. The overlap of the two zero events is subtracted once.
```
def zeroFactorMass (ell m : ℕ) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.exists_zeroFactorMass_threshold line 25
Source documentation
A common lower bound on both dimensions makes the zero-factor probability as small as required. This threshold depends only on the acceptance parameter.
```
theorem exists_zeroFactorMass_threshold {η : ℝ} (hη : 0 < η) :
    ∃ N : ℕ, ∀ ell m : ℕ, N ≤ ell → N ≤ m → zeroFactorMass ell m ≤ η / 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.zeroFactorMass
def OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.ChartFiberRetention line 45
Source documentation
OPEN finite sampling bridge, stated on the actual equality test, actual lifted output fibers, and actual Grassmann retention. The positive dimensions exclude the degenerate empty-neighbor cases. No KMS or inverse principle is part of this proposition.
```
def ChartFiberRetention : Prop :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.inversePrinciple_of_expansion_and_chart line 52

theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.relativeDensity_filter_eq_expect line 107

Source documentation

Relative density is uniform expectation on the predicate subtype.

theorem relativeDensity_filter_eq_expect {Ω : Type*} [Fintype Ω] [DecidableEq Ω]
    (S : Finset Ω) (P : Ω → Prop) [DecidablePred P] :
    KMS.relativeDensity S (Finset.univ.filter P) =
      𝔼 x : {x : Ω // P x}, if x.val ∈ S then (1 : ℝ) else 0 := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity

theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.retention_image line 125
Source documentation
Lifting a finite set along an injection preserves its uniform starting law. No regularity or nonempty-neighbor hypothesis is needed for this step.
```
theorem retention_image {X : Type*} [DecidableEq X] {n ell : ℕ}
    (S : Finset X) (e : X → KMS.Vertex n ell) (he : Function.Injective e) :
    KMS.retention (S.image e) =
      S.expect fun x => KMS.relativeDensity (S.image e) (KMS.neighbors (e x)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMS.retention, OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity, OAI.UniqueGamesTheorem.Inverse.KMS.neighbors
theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.relativeDensity_neighbors_eq_nonzero_average_half line 139
Source documentation
At every starting matrix the full-neighbor retention is half the uniform nonzero-factor retention. This follows from exact finite bijections and degree counts; the zero-factor law is handled separately before this theorem.
```
theorem relativeDensity_neighbors_eq_nonzero_average_half {ell m : ℕ}
    (f : Mat ell m → Vector ell) (y : Vector ell) (M : Mat ell m) :
    KMS.relativeDensity (liftedFiber f y) (KMS.neighbors (matrixVertex M)) =
      (𝔼 p : NonzeroVectorFactors ell m,
        if f (M + rankOne p.1.val p.2.val) = y then (1 : ℝ) else 0) / 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity, OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.liftedFiber, OAI.UniqueGamesTheorem.Inverse.KMS.neighbors
theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.liftedFiber_retention_eq_half line 182
Source documentation
The exact Grassmann retention of an output fiber is half its retention under independent uniform nonzero vector factors. Empty fibers and degenerate dimensions also satisfy this identity with zero-expectation conventions.
```
theorem liftedFiber_retention_eq_half {ell m : ℕ}
    (f : Mat ell m → Vector ell) (y : Vector ell) :
    KMS.retention (liftedFiber f y) =
      (𝔼 M ∈ matrixFiber f y, 𝔼 p : NonzeroVectorFactors ell m,
        if f (M + rankOne p.1.val p.2.val) = y then (1 : ℝ) else 0) / 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.retention, OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.liftedFiber, OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.matrixFiber
theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.chartFiberRetention line 208
Source documentation
The finite sampling bridge has no expansion or inverse premise.
```
theorem chartFiberRetention : ChartFiberRetention := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.ChartFiberRetention
theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.inversePrinciple_of_expansion line 222
Source documentation
Conditional Grassmann-to-matrix implication, preserving all quantifiers and the affine target. KMS expansion is the sole remaining displayed premise.
```
theorem inversePrinciple_of_expansion (hKMS : KMS.ExpansionPrinciple) :
    Shortcode.InversePrinciple :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.ExpansionPrinciple, OAI.UniqueGamesTheorem.Inverse.Shortcode.InversePrinciple