MatrixChartShortcode.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

The concrete interface consumed by the shortcode assembly: an arbitrary KMS interval becomes a Shortcode.Slice, with exact equation counts.

theorem OAI.MaxCutGames.Inverse.MatrixChart.exists_shortcode_slice line 15
def OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.zeroFactorMass line 71
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.MaxCutGames.Inverse.ShortcodeFromGrassmann.exists_zeroFactorMass_threshold line 77
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.MaxCutGames.Inverse.ShortcodeFromGrassmann.zeroFactorMass
def OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.ChartFiberRetention line 97
Source documentation
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.MaxCutGames.Inverse.ShortcodeFromGrassmann.inversePrinciple_of_expansion_and_chart line 104
theorem OAI.MaxCutGames.Inverse.MatrixChart.dotFunctional_zero_binary line 154
theorem OAI.MaxCutGames.Inverse.MatrixChart.dotFunctional_ne_zero line 161
theorem OAI.MaxCutGames.Inverse.MatrixChart.vecMulLinear_rankOne line 167
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.MaxCutGames.Inverse.MatrixChart.dotFunctional
theorem OAI.MaxCutGames.Inverse.MatrixChart.vecMulLinear_add_rankOne line 175
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.MaxCutGames.Inverse.MatrixChart.dotFunctional
theorem OAI.MaxCutGames.Inverse.MatrixChart.adjacent_matrixVertex_add_rankOne line 185
abbrev OAI.MaxCutGames.Inverse.MatrixChart.NonzeroVectorFactors line 194
abbrev OAI.MaxCutGames.Inverse.MatrixChart.MatrixVertexChartNeighbors line 199
Source documentation
Actual Grassmann vertices adjacent to matrixVertex M and remaining inside the finite matrix chart.
```
abbrev MatrixVertexChartNeighbors (M : Mat ell m) :=
…
```
def OAI.MaxCutGames.Inverse.MatrixChart.vectorFactorMatrixNeighbor line 203
theorem OAI.MaxCutGames.Inverse.MatrixChart.vectorFactorMatrixNeighbor_injective line 209
theorem OAI.MaxCutGames.Inverse.MatrixChart.vectorFactorMatrixNeighbor_surjective line 220
def OAI.MaxCutGames.Inverse.MatrixChart.vectorFactorsEquivMatrixVertexChartNeighbors line 249
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.MaxCutGames.Inverse.MatrixChart.NonzeroVectorFactors, OAI.MaxCutGames.Inverse.MatrixChart.MatrixVertexChartNeighbors
theorem OAI.MaxCutGames.Inverse.MatrixChart.vectorFactorsEquivMatrixVertexChartNeighbors_apply line 254
theorem OAI.MaxCutGames.Inverse.MatrixChart.card_matrixVertexChartNeighbors line 260
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.MaxCutGames.Inverse.MatrixChart.MatrixVertexChartNeighbors

theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.relativeDensity_filter_eq_expect line 284

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.MaxCutGames.Inverse.KMS.relativeDensity

theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.retention_image line 302
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.MaxCutGames.Inverse.KMS.Vertex, OAI.MaxCutGames.Inverse.KMS.retention, OAI.MaxCutGames.Inverse.KMS.relativeDensity, OAI.MaxCutGames.Inverse.KMS.neighbors
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.relativeDensity_neighbors_eq_nonzero_average_half line 316
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.MaxCutGames.Inverse.KMS.relativeDensity, OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.liftedFiber, OAI.MaxCutGames.Inverse.KMS.neighbors
theorem OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.liftedFiber_retention_eq_half line 359
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.MaxCutGames.Inverse.KMS.retention, OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.liftedFiber, OAI.MaxCutGames.Inverse.ShortcodeFromGrassmann.matrixFiber
def OAI.MaxCutGames.Inverse.EqualityFiber.fiberMass line 392
def OAI.MaxCutGames.Inverse.EqualityFiber.fiberFlow line 396
def OAI.MaxCutGames.Inverse.EqualityFiber.equalityAcceptance line 400
theorem OAI.MaxCutGames.Inverse.EqualityFiber.sum_fiberMass line 404
theorem OAI.MaxCutGames.Inverse.EqualityFiber.fiberMass_nonneg line 412
theorem OAI.MaxCutGames.Inverse.EqualityFiber.fiberFlow_nonneg line 422
theorem OAI.MaxCutGames.Inverse.EqualityFiber.fiberFlow_le_mass line 435
theorem OAI.MaxCutGames.Inverse.EqualityFiber.sum_sameFiber_indicator_inline_EqualityFiber line 453
theorem OAI.MaxCutGames.Inverse.EqualityFiber.sum_fiberFlow line 466

theorem OAI.MaxCutGames.Inverse.EqualityFiber.exists_positive_mass_le_flow line 481

Source documentation

A probability-weighted average at least η contains a positive-weight fiber whose unnormalized flow is at least η times its mass.

theorem exists_positive_mass_le_flow (mass flow : Y → ℝ)
    (hmass : IsProbability mass) (_hflow : ∀ y, 0 ≤ flow y)
    (hzero : ∀ y, mass y = 0 → flow y = 0)
    {η : ℝ} (haccept : η ≤ ∑ y, flow y) :
    ∃ y, 0 < mass y ∧ η * mass y ≤ flow y := by
…

theorem OAI.MaxCutGames.Inverse.EqualityFiber.exists_fiber_retention line 511
Source documentation
Equality acceptance supplies a nonempty output fiber with the claimed retention. The kernel is the actual sampling kernel; no conditioned sampling law is silently substituted.
```
theorem exists_fiber_retention (p : X → ℝ) (k : X → X → ℝ)
    (hp : IsProbability p) (hk : ∀ x, IsProbability (k x))
    (f : X → Y) {η : ℝ} (haccept : η ≤ equalityAcceptance p k f) :
    ∃ y, 0 < fiberMass p f y ∧ η ≤ fiberFlow p k f y / fiberMass p f y := by
…
```
Mentions: OAI.MaxCutGames.Inverse.EqualityFiber.equalityAcceptance, OAI.MaxCutGames.Inverse.EqualityFiber.fiberMass, OAI.MaxCutGames.Inverse.EqualityFiber.fiberFlow
theorem OAI.MaxCutGames.Inverse.EqualityFiber.nonzero_retention_ge_half line 528
Source documentation
Removing a self-loop mass p₀ ≤ η/2 leaves retention at least η/2. This is the precise algebra needed when one or both rank-one factors may be zero in the unconditioned test.
```
theorem nonzero_retention_ge_half {η p₀ R : ℝ}
    (hη : 0 < η) (hη1 : η < 1) (hp₀ : 0 ≤ p₀) (hp₀η : p₀ ≤ η / 2)
    (haccept : η ≤ p₀ + (1 - p₀) * R) : η / 2 ≤ R := by
…
```
theorem OAI.MaxCutGames.Inverse.EqualityFiber.chart_retention_ge_quarter line 536
def OAI.MaxCutGames.Inverse.Shortcode.matrixWeight line 552
theorem OAI.MaxCutGames.Inverse.Shortcode.matrixWeight_probability line 555
def OAI.MaxCutGames.Inverse.Shortcode.matrixKernel line 564
theorem OAI.MaxCutGames.Inverse.Shortcode.matrixKernel_nonneg line 568
theorem OAI.MaxCutGames.Inverse.Shortcode.matrixKernel_probability line 576
theorem OAI.MaxCutGames.Inverse.Shortcode.matrixKernel_equality line 589
theorem OAI.MaxCutGames.Inverse.Shortcode.equalityAcceptance_eq_kernel line 602
theorem OAI.MaxCutGames.Inverse.Shortcode.exists_output_fiber line 623
Source documentation
Positive-mass fibers, with their actual transition flow, are obtained from the full uniform factor law. This is the first step before conditioning both factors to be nonzero and passing to Grassmann neighbors.
```
theorem exists_output_fiber {ell m : ℕ} (f : Mat ell m → Vector ell)
    {η : ℝ} (haccept : η ≤ equalityAcceptance f) :
    ∃ y : Vector ell, 0 < EqualityFiber.fiberMass matrixWeight f y ∧
      η ≤ EqualityFiber.fiberFlow matrixWeight matrixKernel f y /
        EqualityFiber.fiberMass matrixWeight f y := by
…
```
Mentions: OAI.MaxCutGames.Inverse.Shortcode.Mat, OAI.MaxCutGames.Inverse.Shortcode.Vector, OAI.MaxCutGames.Inverse.Shortcode.equalityAcceptance, OAI.MaxCutGames.Inverse.EqualityFiber.fiberMass, OAI.MaxCutGames.Inverse.Shortcode.matrixWeight, OAI.MaxCutGames.Inverse.EqualityFiber.fiberFlow, OAI.MaxCutGames.Inverse.Shortcode.matrixKernel
def OAI.MaxCutGames.Inverse.FactorSampling.fullAverage line 643
def OAI.MaxCutGames.Inverse.FactorSampling.nonzeroFlow line 646
def OAI.MaxCutGames.Inverse.FactorSampling.zeroMass line 649
theorem OAI.MaxCutGames.Inverse.FactorSampling.boundary_indicator_inline_FactorSampling line 653
theorem OAI.MaxCutGames.Inverse.FactorSampling.boundary_mass line 660
Source documentation
The overlap of the two zero-factor events is subtracted exactly once.
```
theorem boundary_mass (p : A → ℝ) (q : B → ℝ)
    (hp : IsProbability p) (hq : IsProbability q) :
    fullAverage p q (fun a b => if a = 0 ∨ b = 0 then 1 else 0) = zeroMass p q := by
…
```
Mentions: OAI.MaxCutGames.Inverse.FactorSampling.fullAverage, OAI.MaxCutGames.Inverse.FactorSampling.zeroMass
theorem OAI.MaxCutGames.Inverse.FactorSampling.fullAverage_eq_zeroMass_add_nonzeroFlow line 682
Source documentation
A self-loop occurs whenever either perturbation factor is zero.
```
theorem fullAverage_eq_zeroMass_add_nonzeroFlow (p : A → ℝ) (q : B → ℝ)
    (hp : IsProbability p) (hq : IsProbability q) (h : A → B → ℝ)
    (hleft : ∀ b, h 0 b = 1) (hright : ∀ a, h a 0 = 1) :
    fullAverage p q h = zeroMass p q + nonzeroFlow p q h := by
…
```
Mentions: OAI.MaxCutGames.Inverse.FactorSampling.fullAverage, OAI.MaxCutGames.Inverse.FactorSampling.zeroMass, OAI.MaxCutGames.Inverse.FactorSampling.nonzeroFlow
def OAI.MaxCutGames.Inverse.FactorSampling.conditionedRetention line 709
theorem OAI.MaxCutGames.Inverse.FactorSampling.fullAverage_eq_mixture line 712

theorem OAI.MaxCutGames.Inverse.FactorSampling.conditionedRetention_ge_half line 725

Source documentation

This is the full sampling-law implication, rather than only the scalar inequality under an assumed mixture identity.

theorem conditionedRetention_ge_half (p : A → ℝ) (q : B → ℝ)
    (hp : IsProbability p) (hq : IsProbability q) (h : A → B → ℝ)
    (hleft : ∀ b, h 0 b = 1) (hright : ∀ a, h a 0 = 1)
    {η : ℝ} (hη : 0 < η) (hη1 : η < 1)
    (hzero : 0 ≤ zeroMass p q) (hzeroη : zeroMass p q ≤ η / 2)
    (haccept : η ≤ fullAverage p q h) : η / 2 ≤ conditionedRetention p q h := by
…

Mentions: OAI.MaxCutGames.Inverse.FactorSampling.zeroMass, OAI.MaxCutGames.Inverse.FactorSampling.fullAverage, OAI.MaxCutGames.Inverse.FactorSampling.conditionedRetention

theorem OAI.MaxCutGames.Inverse.FactorSampling.zeroMass_binary_uniform line 739
Source documentation
Specialization of the excluded zero-factor mass to uniform binary vector spaces. The powers are supplied by the cardinalities, so the formula also keeps track of the overlap when both factors are zero.
```
theorem zeroMass_binary_uniform (p : A → ℝ) (q : B → ℝ) (ell m : ℕ)
    (hp0 : p 0 = ((2 : ℝ) ^ ell)⁻¹) (hq0 : q 0 = ((2 : ℝ) ^ m)⁻¹) :
    zeroMass p q = ((2 : ℝ) ^ ell)⁻¹ + ((2 : ℝ) ^ m)⁻¹ - ((2 : ℝ) ^ (ell + m))⁻¹ := by
…
```
Mentions: OAI.MaxCutGames.Inverse.FactorSampling.zeroMass