The signed-window proof for genus-four Core 095

Core 095 is the loopless six-vertex, nine-slot core occurring as the first family in Atanasov--Ranganathan. This file translates the short firing profiles recorded in the accompanying analysis into the generic signed-window API.

The catalog orientation is

0: 0--4   1,2: 0--5   3: 1--3   4: 1--4
5: 1--5   6,7: 2--3   8: 2--4.

We first normalize length 0 <= length 5. The opposite chamber is carried to this one by the Core-095 involution and is treated separately below.

def LowGenus.GenusFourRow095.core : Utilities.Certificate.ExplicitPotential.Core 6 9

The ordered nine-slot presentation of the catalog's loopless Core 095. Keeping the concrete cardinalities visible makes subsequent Fin arithmetic small and transparent.

Equations

• LowGenus.GenusFourRow095.core = { tail := ![0, 0, 0, 1, 1, 1, 2, 2, 2], head := ![4, 5, 5, 3, 4, 5, 3, 3, 4] }

theorem LowGenus.GenusFourRow095.core_eq_atlas : core = AtanasovRanganathan.GenusFourCubicAtlas.row095Core

The proof core is definitionally the public cubic-atlas row.

theorem LowGenus.GenusFourRow095.core_loopless (edge : Fin 9) : core.tail edge ≠ core.head edge

theorem LowGenus.GenusFourRow095.core_connected : core.Connected

@[reducible, inline]

abbrev LowGenus.GenusFourRow095.Spec (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) : Utilities.Certificate.SubdivisionGraph.Spec 6 9

Core 095 with arbitrary positive integral edge lengths.

Equations

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

theorem LowGenus.GenusFourRow095.graphConnected (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) : _root_.graphConnected (Spec length hLength).graph

@[reducible, inline]

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

The comparison parameters used in the paper's first-family picture.

Equations

• LowGenus.GenusFourRow095.A length = length 0

@[reducible, inline]

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

Excess length of central slot 5 over slot 0, computed with natural-number subtraction.

Equations

• LowGenus.GenusFourRow095.X length = length 5 - length 0

@[reducible, inline]

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

Length of slot 3, the first arm parameter in the row-095 construction.

Equations

• LowGenus.GenusFourRow095.B length = length 3

@[reducible, inline]

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

Length of slot 8, the second arm parameter in the row-095 construction.

Equations

• LowGenus.GenusFourRow095.C length = length 8

@[reducible, inline]

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

Length of central slot 4 in the row-095 construction.

Equations

• LowGenus.GenusFourRow095.Delta length = length 4

theorem LowGenus.GenusFourRow095.length_five_eq_A_add_X (length : Fin 9 → ℕ) (hNorm : length 0 ≤ length 5) : length 5 = A length + X length

Under the normalized inequality, the long central slot has length A + X.

def LowGenus.GenusFourRow095.q (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (_hNorm : length 0 ≤ length 5) : (Spec length hLength).Vertex

The moving chip q, at distance X from vertex 1 on slot 5.

Equations

• LowGenus.GenusFourRow095.q length hLength _hNorm = (LowGenus.GenusFourRow095.Spec length hLength).pathVertex 5 ⟨LowGenus.GenusFourRow095.X length, ⋯⟩

def LowGenus.GenusFourRow095.abProfile (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) : Utilities.Certificate.WindowProfile.Data (Spec length hLength)

The common profile reaching vertices a=0 and b=5 from every one of the three displayed divisors. Its endpoint divisor is a + b - c - q.

Equations

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

@[simp]

theorem LowGenus.GenusFourRow095.abProfile_slope (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) (edge : Fin 9) : (abProfile length hLength hNorm).slope edge = if edge = 0 then 1 else if edge = 5 then -1 else 0

@[simp]

theorem LowGenus.GenusFourRow095.abProfile_start_zero (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) : (Spec length hLength).pathVertex 0 ((abProfile length hLength hNorm).startPosition 0) = (Spec length hLength).coreVertex 0

@[simp]

theorem LowGenus.GenusFourRow095.abProfile_stop_zero (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) : (Spec length hLength).pathVertex 0 ((abProfile length hLength hNorm).stopPosition 0) = (Spec length hLength).coreVertex 4

@[simp]

theorem LowGenus.GenusFourRow095.abProfile_start_five (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) : (Spec length hLength).pathVertex 5 ((abProfile length hLength hNorm).startPosition 5) = q length hLength hNorm

@[simp]

theorem LowGenus.GenusFourRow095.abProfile_stop_five (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) : (Spec length hLength).pathVertex 5 ((abProfile length hLength hNorm).stopPosition 5) = (Spec length hLength).coreVertex 5

theorem LowGenus.GenusFourRow095.abProfile_endpointDivisors (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) : (abProfile length hLength hNorm).endpointDivisors = oneChip ((Spec length hLength).coreVertex 0) + oneChip ((Spec length hLength).coreVertex 5) - oneChip ((Spec length hLength).coreVertex 4) - oneChip (q length hLength hNorm)

Exact sparse principal divisor of the common a/b profile.

theorem LowGenus.GenusFourRow095.reaches_zero (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) (third : (Spec length hLength).Vertex) : Utilities.Certificate.StrongSeparator.Reaches (Spec length hLength).graph (AtanasovRanganathan.Configurations.threeChipDivisor ((Spec length hLength).coreVertex 4) (q length hLength hNorm) third) ((Spec length hLength).coreVertex 0)

The common profile reaches a=0 for any effective third chip.

theorem LowGenus.GenusFourRow095.reaches_five (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) (third : (Spec length hLength).Vertex) : Utilities.Certificate.StrongSeparator.Reaches (Spec length hLength).graph (AtanasovRanganathan.Configurations.threeChipDivisor ((Spec length hLength).coreVertex 4) (q length hLength hNorm) third) ((Spec length hLength).coreVertex 5)

The same common profile reaches b=5.