Core 095, first Atanasov--Ranganathan chamber

This is the B ≥ C chamber of the first-family picture. The moving chip is on slot 3, at distance P = B - C from the vertex 1. The two window profiles below are exactly the two Dhar moves recorded in the reassessment note: the first reaches vertex 1, and the second simultaneously reaches vertices 2 and 3.

The proof deliberately uses only signed-window endpoint identities. Thus the rather complicated firing scripts on arbitrary subdivisions are never expanded vertex-by-vertex.

@[reducible, inline]

abbrev LowGenus.GenusFourRow095.CaseOne.P (length : Fin 9 → ℕ) : ℕ

The excess of the d--f slot over the e--c slot.

Equations

• LowGenus.GenusFourRow095.CaseOne.P length = LowGenus.GenusFourRow095.B length - LowGenus.GenusFourRow095.C length

@[reducible, inline]

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

The common depth of the three positive windows in the first Dhar move.

Equations

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

def LowGenus.GenusFourRow095.CaseOne.p (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (_hBC : C length ≤ B length) : (Spec length hLength).Vertex

The third chip in the chamber B ≥ C.

Equations

• LowGenus.GenusFourRow095.CaseOne.p length hLength _hBC = (LowGenus.GenusFourRow095.Spec length hLength).pathVertex 3 ⟨LowGenus.GenusFourRow095.CaseOne.P length, ⋯⟩

def LowGenus.GenusFourRow095.CaseOne.pStart (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) : (Spec length hLength).Vertex

The first profile's three positive-window starts.

Equations

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

def LowGenus.GenusFourRow095.CaseOne.deltaStart (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) : (Spec length hLength).Vertex

Starting vertex of the window on slot 4, at path coordinate Delta - m measured from its tail.

Equations

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

def LowGenus.GenusFourRow095.CaseOne.xStart (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) : (Spec length hLength).Vertex

Starting vertex of the window on slot 5, at path coordinate X - m measured from its tail.

Equations

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

def LowGenus.GenusFourRow095.CaseOne.dProfile (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (_hBC : C length ≤ B length) : Utilities.Certificate.WindowProfile.Data (Spec length hLength)

The signed-window profile reaching the vertex d=1.

Equations

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

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

The profile used for both e=2 and f=3.

Equations

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

@[simp]

theorem LowGenus.GenusFourRow095.CaseOne.dProfile_slope (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : C length ≤ B length) (edge : Fin 9) : (dProfile length hLength hBC).slope edge = if edge = 3 ∨ edge = 4 ∨ edge = 5 then 1 else 0

@[simp]

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

@[simp]

theorem LowGenus.GenusFourRow095.CaseOne.dProfile_start_three (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : C length ≤ B length) : (Spec length hLength).pathVertex 3 ((dProfile length hLength hBC).startPosition 3) = pStart length hLength

@[simp]

theorem LowGenus.GenusFourRow095.CaseOne.dProfile_stop_three (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : C length ≤ B length) : (Spec length hLength).pathVertex 3 ((dProfile length hLength hBC).stopPosition 3) = p length hLength hBC

@[simp]

theorem LowGenus.GenusFourRow095.CaseOne.dProfile_start_four (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : C length ≤ B length) : (Spec length hLength).pathVertex 4 ((dProfile length hLength hBC).startPosition 4) = deltaStart length hLength

@[simp]

theorem LowGenus.GenusFourRow095.CaseOne.dProfile_stop_four (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : C length ≤ B length) : (Spec length hLength).pathVertex 4 ((dProfile length hLength hBC).stopPosition 4) = (Spec length hLength).coreVertex 4

@[simp]

theorem LowGenus.GenusFourRow095.CaseOne.dProfile_start_five (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : C length ≤ B length) : (Spec length hLength).pathVertex 5 ((dProfile length hLength hBC).startPosition 5) = xStart length hLength

@[simp]

theorem LowGenus.GenusFourRow095.CaseOne.dProfile_stop_five (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) (hBC : C length ≤ B length) : (Spec length hLength).pathVertex 5 ((dProfile length hLength hBC).stopPosition 5) = q length hLength hNorm

@[simp]

theorem LowGenus.GenusFourRow095.CaseOne.efProfile_start_three (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : C length ≤ B length) : (Spec length hLength).pathVertex 3 ((efProfile length hLength hBC).startPosition 3) = p length hLength hBC

@[simp]

theorem LowGenus.GenusFourRow095.CaseOne.efProfile_stop_three (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : C length ≤ B length) : (Spec length hLength).pathVertex 3 ((efProfile length hLength hBC).stopPosition 3) = (Spec length hLength).coreVertex 3

@[simp]

theorem LowGenus.GenusFourRow095.CaseOne.efProfile_start_eight (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : C length ≤ B length) : (Spec length hLength).pathVertex 8 ((efProfile length hLength hBC).startPosition 8) = (Spec length hLength).coreVertex 2

@[simp]

theorem LowGenus.GenusFourRow095.CaseOne.efProfile_stop_eight (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : C length ≤ B length) : (Spec length hLength).pathVertex 8 ((efProfile length hLength hBC).stopPosition 8) = (Spec length hLength).coreVertex 4

theorem LowGenus.GenusFourRow095.CaseOne.dProfile_endpointDivisors (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) (hBC : C length ≤ B length) : (dProfile length hLength hBC).endpointDivisors = oneChip (pStart length hLength) - oneChip (p length hLength hBC) + oneChip (deltaStart length hLength) - oneChip ((Spec length hLength).coreVertex 4) + oneChip (xStart length hLength) - oneChip (q length hLength hNorm)

Exact sparse endpoint divisor of the d profile.

theorem LowGenus.GenusFourRow095.CaseOne.efProfile_endpointDivisors (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hBC : C length ≤ B length) : (efProfile length hLength hBC).endpointDivisors = -oneChip (p length hLength hBC) + oneChip ((Spec length hLength).coreVertex 3) + oneChip ((Spec length hLength).coreVertex 2) - oneChip ((Spec length hLength).coreVertex 4)

Exact sparse endpoint divisor of the common e/f profile.

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

The first Dhar profile reaches d=1.

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

The second Dhar profile reaches e=2.

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

The same second profile reaches f=3.

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

The first Core-095 chamber proves the genus-four degree-three pencil.