HighRankFixedPadding.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The full numerical column sum for fixed signs, padding and perfect positions.

lemma OAI.TwoPointCorrelations.outside_column_mass_bound line 13

theorem OAI.TwoPointCorrelations.high_rank_fixed_padding_sum line 40

Source documentation

Every column pattern is encoded internally. No rank probability, numerical assignment count, or pattern-cover hypothesis is assumed.

theorem high_rank_fixed_padding_sum {J R : ℕ} (P : Fin J → Finset ℕ)
    (F : Finset (ColumnPrimeAssignment J R P))
    (hR : 0 < R) (forward : Fin R → Bool) (padding : Fin R → ℕ) (j : Fin J)
    (h Q D B H r : ℕ) (U : ℝ) (hU : 1 ≤ U)
    (hP : ∀ p ∈ P j, p.Prime) (hV : 0 < primeHarmonicMass (P j))
    (hmass : ∀ l, primeHarmonicMass (P l) ≤ U) (hH : 0 < H)
    (hlo : ∀ p ∈ P j, H ≤ p) (hbound : ∀ p ∈ P j, p ≤ B)
    (hq : ∀ i, padding i ≤ Q)
    (hd : ∀ w ∈ F, ∀ i, (∏ l ∈ univ.erase j, (w l i).val) ≤ D)
    (perfect : Finset (Fin R)) (cut : Fin R)
    (hrank : ∀ w ∈ F,
      ¬ColumnLowRank (tupleColumnPattern w hR forward padding j) hR h perfect cut r)
…

Mentions: OAI.TwoPointCorrelations.ColumnPrimeAssignment, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.ColumnLowRank, OAI.TwoPointCorrelations.tupleColumnPattern