Hudson–Kaplan bound on recombination events

AbbreviationFour-gamete condition for two sites#✓fully proved

Sites i and j show all four gametes: for every pair of alleles (a, b) some haplotype carries a at i and b at j. This reuses Cslib.Bioinformatics.Phylogenetics.Splits.FourGametes applied to the site columns (M · i) and (M · j); it is not a second definition of the four-gamete predicate.

abbrev FourGametes (i j : Fin s) : Prop :=
  Cslib.Bioinformatics.Phylogenetics.Splits.FourGametes (M · i) (M · j)

Uses 1 · Used by 10

Statement usesFour-gamete condition for binary characters

Used byValidity of the bound · The sweep yields exactly \(R_m\) distinct breakpoints · Valid set of recombination breakpoints · Sweep cuts form a valid breakpoint set · Disjoint family of four-gamete intervals · Hudson–Kaplan sweep yields disjoint four-gamete intervals · Intervals kept by the Hudson–Kaplan sweep are distinct · Characterization of site pairs failing the four-gamete test · Hudson and Kaplan's bound for tree-like blocks · One step of the Hudson–Kaplan sweep

DefinitionHaplotypes carrying an allele at a site#✓fully proved

The haplotypes carrying allele a at site i; when a is the derived allele this is the clade defined by the mutation at i.

def carriers (i : Fin s) (a : Bool) : Finset (Fin n) :=
  Finset.univ.filter fun r => M r i = a

Used by 2

Used byCharacterization of site pairs failing the four-gamete test · Hudson and Kaplan's bound for tree-like blocks

DefinitionBreakpoint separating two sites#✓fully proved

A breakpoint g (a cut immediately to the left of site g) separates sites i and j when i < g ≤ j.

def Separates (g i j : Fin s) : Prop := i < g ∧ g ≤ j

Used by 7

Used byValidity of the bound · The sweep yields exactly \(R_m\) distinct breakpoints · Valid set of recombination breakpoints · Sweep cuts form a valid breakpoint set · Hudson–Kaplan sweep yields disjoint four-gamete intervals · Intervals kept by the Hudson–Kaplan sweep are distinct · Hudson and Kaplan's bound for tree-like blocks

DefinitionValid set of recombination breakpoints#✓fully proved

A set B of breakpoints is valid for the sample M when it separates every pair of sites i < j showing all four gametes.

def IsBreakpointSet (B : Finset (Fin s)) : Prop :=
  ∀ i j : Fin s, i < j → FourGametes M i j → ∃ g ∈ B, Separates g i j

Uses 2 · Used by 4

Statement usesFour-gamete condition for two sites · Breakpoint separating two sites

Used byValidity of the bound · \(R_m\) is the minimum size of a valid breakpoint set · Sweep cuts form a valid breakpoint set · R_m is a lower bound

DefinitionDisjoint family of four-gamete intervals#✓fully proved

A family F of site pairs (i, j) consists of four-gamete intervals (i < j, all four gametes at i and j) that are pairwise disjoint: of two distinct intervals, one ends at or before the start of the other, so no breakpoint separates both.

def IsDisjointFamily (F : Finset (Fin s × Fin s)) : Prop :=
  (∀ x ∈ F, x.1 < x.2 ∧ FourGametes M x.1 x.2) ∧
    ∀ x ∈ F, ∀ y ∈ F, x ≠ y → x.2 ≤ y.1 ∨ y.2 ≤ x.1

Uses 1 · Used by 4

Statement usesFour-gamete condition for two sites

Used byValidity of the bound · Greedy optimality · \(R_m\) is the maximum number of disjoint four-gamete intervals · Hudson–Kaplan sweep yields disjoint four-gamete intervals

DefinitionOne step of the Hudson–Kaplan sweep#✓fully proved

One step of the sweep at right endpoint j. The list acc holds the intervals kept so far, most recent first; the next interval must start at or after the right end of the most recent one (at or after site 0 if none was kept). Among the admissible four-gamete intervals ending at j, the shortest one is kept.

def sweepStep (acc : List (Fin s × Fin s)) (j : Fin s) : List (Fin s × Fin s) :=
  let last : ℕ := (acc.head?.map fun x => (x.2 : ℕ)).getD 0
  let cands := Finset.univ.filter fun i : Fin s => last ≤ (i : ℕ) ∧ i < j ∧ FourGametes M i j
  if h : cands.Nonempty then (cands.max' h, j) :: acc else acc

Uses 2 · Used by 5

Statement usesFour-gamete condition for binary characters · Four-gamete condition for two sites

Used byThe sweep yields exactly \(R_m\) distinct breakpoints · Sweep cuts form a valid breakpoint set · Hudson–Kaplan sweep yields disjoint four-gamete intervals · Intervals kept by the Hudson–Kaplan sweep are distinct · Hudson–Kaplan left-to-right sweep

DefinitionHudson–Kaplan left-to-right sweep#✓fully proved

The intervals kept by Hudson and Kaplan's left-to-right sweep, most recent first.

def sweep : List (Fin s × Fin s) :=
  (List.finRange s).foldl (sweepStep M) []

Uses 1 · Used by 9

Statement usesOne step of the Hudson–Kaplan sweep

Used byGreedy optimality · The sweep yields exactly \(R_m\) distinct breakpoints · \(R_m\) is the minimum size of a valid breakpoint set · \(R_m\) is the maximum number of disjoint four-gamete intervals · Sweep cuts form a valid breakpoint set · Hudson–Kaplan sweep yields disjoint four-gamete intervals · Intervals kept by the Hudson–Kaplan sweep are distinct · Hudson and Kaplan's R_m · R_m is a lower bound

DefinitionHudson and Kaplan's R_m#✓fully proved

The number of intervals kept by the sweep.

def rm : ℕ := (sweep M).length

Uses 1 · Used by 6

Statement usesHudson–Kaplan left-to-right sweep

Used byGreedy optimality · The sweep yields exactly \(R_m\) distinct breakpoints · \(R_m\) is the minimum size of a valid breakpoint set · \(R_m\) is the maximum number of disjoint four-gamete intervals · R_m is a lower bound · Hudson and Kaplan's bound for tree-like blocks

TheoremIntervals kept by the Hudson–Kaplan sweep are distinct#✓fully proved

The intervals kept by the sweep are distinct.

theorem nodup_sweep : (sweep M).Nodup

Uses 5 · Used by 2

Statement usesHudson–Kaplan left-to-right sweep

Proof usesFour-gamete condition for binary characters · Four-gamete condition for two sites · Breakpoint separating two sites · One step of the Hudson–Kaplan sweep

Used by\(R_m\) is the maximum number of disjoint four-gamete intervals · R_m is a lower bound

TheoremHudson–Kaplan sweep yields disjoint four-gamete intervals#✓fully proved

The intervals kept by the sweep are pairwise disjoint four-gamete intervals.

theorem isDisjointFamily_sweep : IsDisjointFamily M (sweep M).toFinset

Uses 6 · Used by 2

Statement usesDisjoint family of four-gamete intervals · Hudson–Kaplan left-to-right sweep

Proof usesFour-gamete condition for binary characters · Four-gamete condition for two sites · Breakpoint separating two sites · One step of the Hudson–Kaplan sweep

Used by\(R_m\) is the maximum number of disjoint four-gamete intervals · R_m is a lower bound

TheoremSweep cuts form a valid breakpoint set#✓fully proved

Cutting immediately to the left of the right endpoint of every kept interval gives a valid breakpoint set.

theorem isBreakpointSet_sweep : IsBreakpointSet M ((sweep M).map Prod.snd).toFinset

Uses 6 · Used by 2

Statement usesValid set of recombination breakpoints · Hudson–Kaplan left-to-right sweep

Proof usesFour-gamete condition for binary characters · Four-gamete condition for two sites · Breakpoint separating two sites · One step of the Hudson–Kaplan sweep

Used byGreedy optimality · \(R_m\) is the minimum size of a valid breakpoint set

TheoremThe sweep yields exactly \(R_m\) distinct breakpoints#✓fully proved

The right endpoints of the kept intervals are distinct, so there are R_m of them.

theorem card_sweep_snd : ((sweep M).map Prod.snd).toFinset.card = rm M

Uses 6 · Used by 2

Statement usesHudson and Kaplan's R_m · Hudson–Kaplan left-to-right sweep

Proof usesFour-gamete condition for binary characters · Four-gamete condition for two sites · Breakpoint separating two sites · One step of the Hudson–Kaplan sweep

Used byGreedy optimality · \(R_m\) is the minimum size of a valid breakpoint set

TheoremValidity of the bound#✓fully proved

Validity of the bound (Hudson–Kaplan 1985): a valid breakpoint set has at least as many points as any family of pairwise disjoint four-gamete intervals, since each interval needs its own breakpoint.

theorem card_le_card_of_isBreakpointSet {F : Finset (Fin s × Fin s)} {B : Finset (Fin s)}
    (hF : IsDisjointFamily M F) (hB : IsBreakpointSet M B) : F.card ≤ B.card

Uses 4 · Used by 2

Statement usesValid set of recombination breakpoints · Disjoint family of four-gamete intervals

Proof usesFour-gamete condition for two sites · Breakpoint separating two sites

Used byGreedy optimality · R_m is a lower bound

TheoremR_m is a lower bound#✓fully proved

R_m is a lower bound (Hudson–Kaplan 1985): every valid breakpoint set has at least R_m points.

theorem rm_le_card_of_isBreakpointSet {B : Finset (Fin s)} (hB : IsBreakpointSet M B) :
    rm M ≤ B.card

Uses 6 · Used by 1

Statement usesValid set of recombination breakpoints · Hudson and Kaplan's R_m

Proof usesValidity of the bound · Hudson–Kaplan sweep yields disjoint four-gamete intervals · Intervals kept by the Hudson–Kaplan sweep are distinct · Hudson–Kaplan left-to-right sweep

Used byHudson and Kaplan's bound for tree-like blocks

Theorem\(R_m\) is the minimum size of a valid breakpoint set#✓fully proved

The bound is attained: some valid breakpoint set has exactly R_m points, so R_m is the minimum size of a valid breakpoint set.

theorem exists_isBreakpointSet_card_eq_rm :
    ∃ B : Finset (Fin s), IsBreakpointSet M B ∧ B.card = rm M

Uses 5

Statement usesValid set of recombination breakpoints · Hudson and Kaplan's R_m

Proof usesThe sweep yields exactly \(R_m\) distinct breakpoints · Sweep cuts form a valid breakpoint set · Hudson–Kaplan left-to-right sweep

TheoremGreedy optimality#✓fully proved

No family of pairwise disjoint four-gamete intervals has more than R_m members.

theorem card_le_rm {F : Finset (Fin s × Fin s)} (hF : IsDisjointFamily M F) : F.card ≤ rm M

Uses 6

Statement usesDisjoint family of four-gamete intervals · Hudson and Kaplan's R_m

Proof usesValidity of the bound · The sweep yields exactly \(R_m\) distinct breakpoints · Sweep cuts form a valid breakpoint set · Hudson–Kaplan left-to-right sweep

Theorem\(R_m\) is the maximum number of disjoint four-gamete intervals#✓fully proved

The sweep attains the maximum: R_m is the largest size of a family of pairwise disjoint four-gamete intervals.

theorem exists_isDisjointFamily_card_eq_rm :
    ∃ F : Finset (Fin s × Fin s), IsDisjointFamily M F ∧ F.card = rm M

Uses 5

Statement usesDisjoint family of four-gamete intervals · Hudson and Kaplan's R_m

Proof usesHudson–Kaplan sweep yields disjoint four-gamete intervals · Intervals kept by the Hudson–Kaplan sweep are distinct · Hudson–Kaplan left-to-right sweep

TheoremCharacterization of site pairs failing the four-gamete test#✓fully proved

Two sites miss one of the four gametes exactly when, for some choice of the alleles a at i and b at j (the derived alleles), the carrier sets are nested or disjoint, as two clades of one rooted tree are.

theorem not_fourGametes_iff (i j : Fin s) :
    ¬FourGametes M i j ↔ ∃ a b : Bool,
      carriers M i a ⊆ carriers M j b ∨ Disjoint (carriers M i a) (carriers M j b)

Uses 2 · Used by 1

Statement usesFour-gamete condition for two sites · Haplotypes carrying an allele at a site

Used byHudson and Kaplan's bound for tree-like blocks

TheoremHudson and Kaplan's bound for tree-like blocks#✓fully proved

Suppose the breakpoints B cut the sequence into blocks such that, within a block, the derived-allele clades of every two sites are nested or disjoint for some choice of the derived alleles (as for sites whose mutations sit on one tree under the infinite-sites model). Then there are at least R_m breakpoints.

theorem rm_le_card_of_nested_or_disjoint {B : Finset (Fin s)}
    (h : ∀ i j : Fin s, i < j → (∀ g ∈ B, ¬Separates g i j) → ∃ a b : Bool,
      carriers M i a ⊆ carriers M j b ∨ Disjoint (carriers M i a) (carriers M j b)) :
    rm M ≤ B.card

Uses 6

Statement usesBreakpoint separating two sites · Haplotypes carrying an allele at a site · Hudson and Kaplan's R_m

Proof usesFour-gamete condition for two sites · Characterization of site pairs failing the four-gamete test · R_m is a lower bound

19 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.