The two B < C Dhar profiles for Core 095

This is the middle and right chamber of the first Atanasov--Ranganathan genus-four family. The common a/b profile is in GenusFourCore095; this file records the two remaining pairs of signed windows and packages their endpoint computations as reachability statements.

Case 2: the middle comparison range B < C and min(X, Delta) ≤ C - B.

@[reducible, inline]

abbrev LowGenus.GenusFourRow095.CaseTwo.Y (length : Fin 9 → ℕ) : ℕ

Excess of arm length C over B, used to locate the moving chip in Case 2.

Equations

• LowGenus.GenusFourRow095.CaseTwo.Y length = LowGenus.GenusFourRow095.C length - LowGenus.GenusFourRow095.B length

@[reducible, inline]

abbrev LowGenus.GenusFourRow095.CaseTwo.m (length : Fin 9 → ℕ) : ℕ

The smaller of the two central lengths X and Delta, compared with the arm excess in Case 2.

Equations

• LowGenus.GenusFourRow095.CaseTwo.m length = min (LowGenus.GenusFourRow095.X length) (LowGenus.GenusFourRow095.Delta length)

def LowGenus.GenusFourRow095.CaseTwo.r (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : B length < C length) (hmy : m length ≤ Y length) : (Spec length hLength).Vertex

The moving third chip in Case 2.

Equations

• One or more equations did not get rendered due to their size.

def LowGenus.GenusFourRow095.CaseTwo.dProfile (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : B length < C length) (hmy : m length ≤ Y length) : Utilities.Certificate.WindowProfile.Data (Spec length hLength)

Case-2 window profile which reaches core vertex d=1.

Equations

• One or more equations did not get rendered due to their size.

def LowGenus.GenusFourRow095.CaseTwo.efProfile (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : B length < C length) (hmy : m length ≤ Y length) : Utilities.Certificate.WindowProfile.Data (Spec length hLength)

Case-2 window profile which reaches the two zero-valued core vertices e=2 and f=3.

Equations

• One or more equations did not get rendered due to their size.

theorem LowGenus.GenusFourRow095.CaseTwo.dProfile_endpointDivisors (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : B length < C length) (hmy : m length ≤ Y length) : (dProfile length hLength hBC hmy).endpointDivisors = oneChip ((Spec length hLength).pathVertex 4 ((dProfile length hLength hBC hmy).startPosition 4)) - oneChip ((Spec length hLength).pathVertex 4 ((dProfile length hLength hBC hmy).stopPosition 4)) + (oneChip ((Spec length hLength).pathVertex 5 ((dProfile length hLength hBC hmy).startPosition 5)) - oneChip ((Spec length hLength).pathVertex 5 ((dProfile length hLength hBC hmy).stopPosition 5))) + (oneChip ((Spec length hLength).pathVertex 8 ((dProfile length hLength hBC hmy).startPosition 8)) - oneChip ((Spec length hLength).pathVertex 8 ((dProfile length hLength hBC hmy).stopPosition 8)))

The sparse signed-endpoint expansion of the Case-2 d profile.

theorem LowGenus.GenusFourRow095.CaseTwo.reaches_one (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) (hBC : B length < C length) (hmy : m length ≤ Y length) : Utilities.Certificate.StrongSeparator.Reaches (Spec length hLength).graph (AtanasovRanganathan.Configurations.threeChipDivisor ((Spec length hLength).coreVertex 4) (q length hLength hNorm) (r length hLength hBC hmy)) ((Spec length hLength).coreVertex 1)

In the middle Case-2 chamber the displayed divisor reaches d=1.

@[simp]

theorem LowGenus.GenusFourRow095.CaseTwo.efProfile_slope (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : B length < C length) (hmy : m length ≤ Y length) (edge : Fin 9) : (efProfile length hLength hBC hmy).slope edge = if edge = 3 then -1 else if edge = 4 ∨ edge = 5 ∨ edge = 8 then 1 else 0

theorem LowGenus.GenusFourRow095.CaseTwo.efProfile_endpointDivisors (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) (hBC : B length < C length) (hmy : m length ≤ Y length) : (efProfile length hLength hBC hmy).endpointDivisors = -oneChip ((Spec length hLength).coreVertex 1) + oneChip ((Spec length hLength).coreVertex 3) + (oneChip ((Spec length hLength).pathVertex 4 ((dProfile length hLength hBC hmy).startPosition 4)) - oneChip ((Spec length hLength).coreVertex 4)) + (oneChip ((Spec length hLength).pathVertex 5 ((dProfile length hLength hBC hmy).startPosition 5)) - oneChip (q length hLength hNorm)) + (oneChip ((Spec length hLength).coreVertex 2) - oneChip (r length hLength hBC hmy))

theorem LowGenus.GenusFourRow095.CaseTwo.reaches_two (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) (hBC : B length < C length) (hmy : m length ≤ Y length) : Utilities.Certificate.StrongSeparator.Reaches (Spec length hLength).graph (AtanasovRanganathan.Configurations.threeChipDivisor ((Spec length hLength).coreVertex 4) (q length hLength hNorm) (r length hLength hBC hmy)) ((Spec length hLength).coreVertex 2)

theorem LowGenus.GenusFourRow095.CaseTwo.reaches_three (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) (hBC : B length < C length) (hmy : m length ≤ Y length) : Utilities.Certificate.StrongSeparator.Reaches (Spec length hLength).graph (AtanasovRanganathan.Configurations.threeChipDivisor ((Spec length hLength).coreVertex 4) (q length hLength hNorm) (r length hLength hBC hmy)) ((Spec length hLength).coreVertex 3)

theorem LowGenus.GenusFourRow095.CaseTwo.bnExists_one_three (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) (hBC : B length < C length) (hmy : m length ≤ Y length) : Utilities.BNExists (Spec length hLength).graph 1 3

Case 3: the strict short comparison range 0 < C-B < min(X,Delta).

@[reducible, inline]

abbrev LowGenus.GenusFourRow095.CaseThree.Y (length : Fin 9 → ℕ) : ℕ

Excess of arm length C over B, used in the Case-3 window construction.

Equations

• LowGenus.GenusFourRow095.CaseThree.Y length = LowGenus.GenusFourRow095.C length - LowGenus.GenusFourRow095.B length

def LowGenus.GenusFourRow095.CaseThree.s (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hYsmall : Y length < min (X length) (Delta length)) : (Spec length hLength).Vertex

The moving third chip in Case 3.

Equations

• LowGenus.GenusFourRow095.CaseThree.s length hLength hYsmall = (LowGenus.GenusFourRow095.Spec length hLength).pathVertex 4 ⟨LowGenus.GenusFourRow095.CaseThree.Y length, ⋯⟩

def LowGenus.GenusFourRow095.CaseThree.dProfile (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : B length < C length) (hYsmall : Y length < min (X length) (Delta length)) : Utilities.Certificate.WindowProfile.Data (Spec length hLength)

Case-3 window profile which reaches d=1.

Equations

• One or more equations did not get rendered due to their size.

def LowGenus.GenusFourRow095.CaseThree.efProfile (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : B length < C length) (hYsmall : Y length < min (X length) (Delta length)) : Utilities.Certificate.WindowProfile.Data (Spec length hLength)

Case-3 window profile which reaches e=2 and f=3.

Equations

• One or more equations did not get rendered due to their size.