GoodRetainedWordSum.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The good-word bound with the actual, normalized, retained padding weights.

lemma OAI.TwoPointCorrelations.paddingWordWeight_nonneg line 12
def OAI.TwoPointCorrelations.retainedColumnPaddingWeight line 21

theorem OAI.TwoPointCorrelations.good_retained_word_sum line 34

Source documentation

The bound holds uniformly for prime-dependent eligibility, walk shifts, and cutoffs, retaining the exact departure normalization at each step.

theorem good_retained_word_sum {J k S : ℕ} {Code : Type*} [Fintype Code]
    (P : Fin J → Finset ℕ) (Q : Finset ℕ)
    (F : Finset (ColumnPrimeAssignment J (2 * k) P × (Fin (2 * k) → Q)))
    (decode : Code → Fin J → Fin (2 * k) → Fin (2 * k) → Bool)
    (u : ℕ → ℝ) (eligible : ColumnPrimeAssignment J (2 * k) P → ℕ → ℕ → Prop)
    (g : ℤ → ℝ) (L K A : ℝ)
    (extra : ColumnPrimeAssignment J (2 * k) P → ℕ → ℤ → Prop)
    (next : ColumnPrimeAssignment J (2 * k) P → ℕ → ℤ → ℕ → ℤ) (n : ℤ)
    (hL : 0 < L) (hK : 0 ≤ K) (hA : 1 ≤ A) (hu : ∀ q, 0 ≤ u q)
    (hmass : ∀ j, primeHarmonicMass (P j) ≤ A)
    (hsingle : ∀ a ∈ F, columnSingletonCount a.1 ≤ 2 * S)
    (hcover : ∀ a ∈ F, ∃ c, ∀ j i l, decode c j i l = decide (a.1 j i = a.1 j l)) :
…

Mentions: OAI.TwoPointCorrelations.ColumnPrimeAssignment, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.columnSingletonCount

theorem OAI.TwoPointCorrelations.eventually_good_retained_word_sum line 62

Source documentation

The complete good-word prime/padding sum at the manuscript's forest code scale, before signs, designations and external matrix dimensions.

theorem eventually_good_retained_word_sum :
    ∀ᶠ L : ℝ in atTop, ∀ J k S : ℕ, ∀ P : Fin J → Finset ℕ, ∀ Q : Finset ℕ,
      ∀ F : Finset (ColumnPrimeAssignment J (2 * k) P × (Fin (2 * k) → Q)),
      ∀ (u : ℕ → ℝ) (eligible : ColumnPrimeAssignment J (2 * k) P → ℕ → ℕ → Prop)
      (g : ℤ → ℝ) (K W : ℝ)
      (extra : ColumnPrimeAssignment J (2 * k) P → ℕ → ℤ → Prop)
      (next : ColumnPrimeAssignment J (2 * k) P → ℕ → ℤ → ℕ → ℤ) (n : ℤ),
      L / 2 ≤ (k : ℝ) → (k : ℝ) ≤ L → 1 ≤ k → 0 ≤ K → 1 ≤ W →
      (∀ q, 0 ≤ u q) → (∀ j, primeHarmonicMass (P j) ≤ 2 * W) →
      (∀ a ∈ F, columnSingletonCount a.1 ≤ 2 * S) →
      (∀ a ∈ F, ∃ c : BudgetColumnArrayCode J (4 * k) L,
        ∀ j i l, decodeBudgetColumnArray (show 2 * k ≤ 4 * k by omega) c j i l =
…

Mentions: OAI.TwoPointCorrelations.ColumnPrimeAssignment, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.columnSingletonCount, OAI.TwoPointCorrelations.BudgetColumnArrayCode, OAI.TwoPointCorrelations.decodeBudgetColumnArray