Endpoint replay for the short Core-095 chamber

GenusFourCore095CasesTwoThree defines the two compatible signed-window profiles in the chamber 0 < C-B < min(X,Delta). This file performs their sparse endpoint replay and closes the three remaining core reachability tests.

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

Sparse endpoint expansion of the Case-3 profile reaching d=1.

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

In the short chamber, the first profile reaches d=1; after endpoint cancellation the residual is exactly two positive chips.

theorem LowGenus.GenusFourRow095.CaseThree.efProfile_endpointDivisors (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) (hBC : B length < C length) (hYsmall : Y length < min (X length) (Delta length)) : (efProfile length hLength hBC hYsmall).endpointDivisors = oneChip ((Spec length hLength).coreVertex 3) - oneChip (s length hLength hYsmall) + oneChip ((Spec length hLength).pathVertex 5 ((efProfile length hLength hBC hYsmall).startPosition 5)) - oneChip (q length hLength hNorm) + oneChip ((Spec length hLength).coreVertex 2) - oneChip ((Spec length hLength).coreVertex 4)

Simplified endpoint divisor of the shared Case-3 e/f profile.

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

The shared short-chamber profile reaches e=2.

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

The same profile reaches f=3.

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

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