TupleRankWitness.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Extract the high-rank witness from failure of the actual forest rank condition.

lemma OAI.TwoPointCorrelations.ColumnWordPattern.finite_departure line 13

theorem OAI.TwoPointCorrelations.tuple_selected_pairs_observed line 26

Source documentation

Selected equal-label pairs are transported to the observed resampling coordinates with their same original left and right departure indices.

theorem tuple_selected_pairs_observed {J R : ℕ} {P : Fin J → Finset ℕ}
    (w : ColumnPrimeAssignment J R P) (hR : 0 < R)
    (forward : Fin R → Bool) (padding : Fin R → ℕ) (j : Fin J) (h : ℕ)
    (perfect : Finset (Fin R)) (cut : Fin R)
    (S : Finset (EqualLabelPairs (fun i : perfect.erase cut =>
      (tupleColumnPattern w hR forward padding j).label i.val.val)))
    (hind : LinearIndependent ℝ (pairFamily (labelPairVectors
      (fun i : perfect.erase cut => (tupleColumnPattern w hR forward padding j).label i.val.val)
      (fun i => formalDeparture
        (columnNatLabel (fun i : Fin R => (tupleColumnPattern w hR forward padding j).label i.val) hR)
        (fun t => ((tupleColumnPattern w hR forward padding j).coefficient h t : ℝ)) i.val.val)) S)) :
    LinearIndependent ℝ (Sum.elim
…

Mentions: OAI.TwoPointCorrelations.ColumnPrimeAssignment, OAI.TwoPointCorrelations.EqualLabelPairs, OAI.TwoPointCorrelations.tupleColumnPattern, OAI.TwoPointCorrelations.pairFamily, OAI.TwoPointCorrelations.labelPairVectors, OAI.TwoPointCorrelations.formalDeparture, OAI.TwoPointCorrelations.columnNatLabel

theorem OAI.TwoPointCorrelations.tuple_selected_pairs_reciprocal_sum line 67

Source documentation

Apply the high-rank estimate using only the original perfect-departure lit conditions. The two divisibility tests per selected pair are derived here, with no additional resampling premise.

theorem tuple_selected_pairs_reciprocal_sum {J R : ℕ} {P : Fin J → Finset ℕ}
    (w : ColumnPrimeAssignment J R P) (hR : 0 < R)
    (forward : Fin R → Bool) (padding : Fin R → ℕ) (j : Fin J)
    (F : Finset (Fin R → P j))
    (hpattern : ∀ v ∈ F, ∀ a b, v a = v b ↔ w j a = w j b)
    (h Q D B H : ℕ) (hP : ∀ p ∈ P j, p.Prime)
    (hV : 0 < primeHarmonicMass (P j)) (hH : 0 < H)
    (hlo : ∀ p ∈ P j, H ≤ p) (hbound : ∀ p ∈ P j, p ≤ B)
    (hq : ∀ i, padding i ≤ Q)
    (hd : ∀ i, (∏ l ∈ univ.erase j, (w l i).val) ≤ D)
    (perfect : Finset (Fin R)) (cut : Fin R)
    (S : Finset (EqualLabelPairs (fun i : perfect.erase cut =>
…

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

theorem OAI.TwoPointCorrelations.tuple_not_low_rank_reciprocal_sum line 114

Source documentation

Failure of the forest's low-rank condition supplies the precise selected-pair witness needed by the reciprocal estimate.

theorem tuple_not_low_rank_reciprocal_sum {J R : ℕ} {P : Fin J → Finset ℕ}
    (w : ColumnPrimeAssignment J R P) (hR : 0 < R)
    (forward : Fin R → Bool) (padding : Fin R → ℕ) (j : Fin J)
    (F : Finset (Fin R → P j))
    (hpattern : ∀ v ∈ F, ∀ a b, v a = v b ↔ w j a = w j b)
    (h Q D B H : ℕ) (hP : ∀ p ∈ P j, p.Prime)
    (hV : 0 < primeHarmonicMass (P j)) (hH : 0 < H)
    (hlo : ∀ p ∈ P j, H ≤ p) (hbound : ∀ p ∈ P j, p ≤ B)
    (hq : ∀ i, padding i ≤ Q)
    (hd : ∀ i, (∏ l ∈ univ.erase j, (w l i).val) ≤ D)
    (perfect : Finset (Fin R)) (cut : Fin R) (r : ℕ)
    (hrank : ¬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