theorem cond_15_6_ofRank (k : ℕ) {ε : GeneType} (hε : ε ≠ GeneType.NonPolarized) : Chromosome.signature (Chromosome.prime (Gene.ofRank k ε)) - Chromosome.signature (Chromosome.prime (Chromosome.prime (Gene.ofRank k ε))) ≤ (Chromosome.signature (Gene.ofRank k ε) - Chromosome.signature (Chromosome.prime (Gene.ofRank k ε))).swap

theorem cond_15_6_Pi {Y : Chromosome} (hY : Y ∈ Variety.Pi) : Chromosome.signature (Chromosome.prime Y) - Chromosome.signature (Chromosome.prime (Chromosome.prime Y)) ≤ (Chromosome.signature Y - Chromosome.signature (Chromosome.prime Y)).swap

noncomputable def Sigma.sigma (X : Chromosome) : ℕ → ℚ × ℚ

For X ∈ Π, σ(X) is the 2×∞ nonneg integral matrix whose k-th column is (aₖ, bₖ) = sig X^(k), as defined in [Djoković 1982, (15.1)].

Represented as a function ℕ → ℚ × ℚ, where the first component is aₖ and the second is bₖ.

Equations

• Sigma.sigma X k = Chromosome.signature ((⇑Chromosome.prime)^[k] X)

theorem Sigma.antitone (X : Chromosome) : Antitone (sigma X)

theorem Sigma.eventually_zero (X : Chromosome) : ∃ (K : ℕ), ∀ k ≥ K, sigma X k = 0

theorem Sigma.cond_15_2 (X : Chromosome) : (∀ (k : ℕ), (sigma X (k + 1)).1 ≤ (sigma X k).1) ∧ ∃ (K : ℕ), ∀ k ≥ K, (sigma X k).1 = 0

theorem Sigma.cond_15_3 (X : Chromosome) : (∀ (k : ℕ), (sigma X (k + 1)).2 ≤ (sigma X k).2) ∧ ∃ (K : ℕ), ∀ k ≥ K, (sigma X k).2 = 0

theorem Sigma.cond_15_4 (X : Chromosome) (k : ℕ) : if Even k then (sigma X (k + 1)).2 ≤ (sigma X k).1 else (sigma X (k + 1)).1 ≤ (sigma X k).2

(15.4) a₀ ≥ b₁ ≥ a₂ ≥ b₃ ≥ …

theorem Sigma.cond_15_5 (X : Chromosome) (k : ℕ) : if Even k then (sigma X (k + 1)).1 ≤ (sigma X k).2 else (sigma X (k + 1)).2 ≤ (sigma X k).1

(15.5) b₀ ≥ a₁ ≥ b₂ ≥ a₃ ≥ …

theorem Sigma.cond_15_6 (X : Chromosome) (k : ℕ) (hX : X ∈ Variety.Pi) : if Even k then (sigma X (k + 1)).2 - (sigma X (k + 2)).2 ≤ (sigma X k).1 - (sigma X (k + 1)).1 else (sigma X (k + 1)).1 - (sigma X (k + 2)).1 ≤ (sigma X k).2 - (sigma X (k + 1)).2

(15.6) a₀ − a₁ ≥ b₁ − b₂ ≥ a₂ − a₃ ≥ b₃ − b₄ ≥ …

theorem Sigma.cond_15_7 (X : Chromosome) (k : ℕ) (hX : X ∈ Variety.Pi) : if Even k then (sigma X (k + 1)).1 - (sigma X (k + 2)).1 ≤ (sigma X k).2 - (sigma X (k + 1)).2 else (sigma X (k + 1)).2 - (sigma X (k + 2)).2 ≤ (sigma X k).1 - (sigma X (k + 1)).1

(15.7) b₀ − b₁ ≥ a₁ − a₂ ≥ b₂ − b₃ ≥ a₃ − a₄ ≥ …

theorem Sigma.cond_15_8 {X Y : ↥Variety.Pi} (h : X < Y) (k : ℕ) : (sigma (↑X) k).1 ≤ (sigma (↑Y) k).1 ∧ (sigma (↑X) k).2 ≤ (sigma (↑Y) k).2

(15.8) If X < Y in Π then aₖ ≤ cₖ and bₖ ≤ dₖ for all k, where (aₖ, bₖ) = σ(X)ₖ and (cₖ, dₖ) = σ(Y)ₖ.