Unconditional CLOSED-ORTHANT existence on genus-four Core 097

The pencil is expressed over Utilities.Certificate.DegenerateSpec.DegSpec, whose lengths may vanish, so the conclusion covers the whole closed orthant: every subdivision of the row-097 core and every equal-genus contraction of one.

The positive-length statement follows from the result here.

The face ℓ₈ = 0 also supplies the corresponding row-068 case.

The mathematics is the same; the bookkeeping is different

Writing the split core as

e0 0-4   e1 0-5   e2 0-5   e3 1-2   e4 1-3
e5 1-5   e6 2-3   e7 2-4   e8 3-4

the vertices 2 and 3 are the hubs of a theta graph with arcs e6, e3 + e4 (through 1) and e7 + e8 (through 4); the interior vertices 1 and 4 of the last two arcs are joined by a handle 1 —e5— 5 =banana(e1,e2)= 0 —e0— 4. Writing Δ = length 0 - length 5 and d = min Δ (length 4), the pencil is

D = 3 + 4 + (the point at distance d from 1 along e3),

moved onto the core by marches across the three-edge cuts star 2, {e0,e3,e4}, star 0 and across the two-edge cut {e0,e5} (used twice). The Klein four-group σ = (0 5)(1 4), τ = (2 3) puts an arbitrary length vector in the chamber length 5 ≤ length 0, length 4 ≤ length 3.

Three things change on the closed orthant, and all three are handled once, in Certificate/DegenerateRamp.lean, rather than per march:

• Vertices are classes. DegSpec.Vertex = Class ⊕ Interior, and coreVertex is not injective at a face. Every value at a class is the class sum of the uncontracted per-core-vertex value (DegSpec.prin_coreVertex_eq_classSum), so the per-vertex arithmetic of the open proof transfers by addition.
• Path positions have three cases, k = 0, 0 < k < length, k = length, and the last is reachable. DegSpec.pathAt is the unbounded path vertex: it clamps k to the slot, so no statement below carries a position bound at all.
• A ramp must be constant on classes. That is RampData.repInv, and it is free whenever rep is generated by the vanishing slots (RampData.of_reachIn), which is how RowProof.censusSpec is built.

The four per-march divisor identities of the retired open proof — four set_option maxHeartbeats 1000000 declarations there — are replaced by a single generic one, DegSpec.prin_ramp_eq, instantiated nine-slot-wise. This file needs no heartbeat override.

Finite-index bookkeeping

theorem LowGenus.GenusFourRow097Closed.sum_univ_nine {M : Type u_1} [AddCommMonoid M] (f : Fin 9 → M) : ∑ i : Fin 9, f i = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7 + f 8

theorem LowGenus.GenusFourRow097Closed.forall_fin_nine {P : Fin 9 → Prop} (h0 : P 0) (h1 : P 1) (h2 : P 2) (h3 : P 3) (h4 : P 4) (h5 : P 5) (h6 : P 6) (h7 : P 7) (h8 : P 8) (e : Fin 9) : P e

theorem LowGenus.GenusFourRow097Closed.forall_fin_six {P : Fin 6 → Prop} (h0 : P 0) (h1 : P 1) (h2 : P 2) (h3 : P 3) (h4 : P 4) (h5 : P 5) (v : Fin 6) : P v

Rank one from reaching the core classes

The closed-orthant analogue of Utilities.Certificate.CoreVertexReachability.bnExists_of_reaches_coreVertices. Both hypotheses it needs about the ambient graph are already hypothesis-free on a DegSpec: the class vertices are a strong separator (DegSpec.strongSeparatorCertificate) and connectivity comes from the finite cut certificate on the uncontracted core (DegSpec.graph_connected_of_coreConnected).

theorem LowGenus.GenusFourRow097Closed.bnExists_of_reaches_coreVertices {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core.Connected) (D : CFDiv d.graph) (degree : ℤ) (hDegree : CFDiv.degree D = degree) (hReaches : ∀ (v : Fin n), Utilities.Certificate.StrongSeparator.Reaches d.graph D (d.coreVertex v)) : Utilities.BNExists d.graph 1 degree

The oriented row-097 core

structure LowGenus.GenusFourRow097Closed.IsCore097 (core : Utilities.Certificate.ExplicitPotential.Core 6 9) : Prop

The orientation data of the row-097 split core, read on the core rather than on a positive subdivision: on the closed orthant the slot lengths are not part of this datum.

• t0 : core.tail 0 = 0
• t1 : core.tail 1 = 0
• t2 : core.tail 2 = 0
• t3 : core.tail 3 = 1
• t4 : core.tail 4 = 1
• t5 : core.tail 5 = 1
• t6 : core.tail 6 = 2
• t7 : core.tail 7 = 2
• t8 : core.tail 8 = 3
• h0 : core.head 0 = 4
• h1 : core.head 1 = 5
• h2 : core.head 2 = 5
• h3 : core.head 3 = 2
• h4 : core.head 4 = 3
• h5 : core.head 5 = 5
• h6 : core.head 6 = 3
• h7 : core.head 7 = 4
• h8 : core.head 8 = 4

theorem LowGenus.GenusFourRow097Closed.IsCore097.core_connected {core : Utilities.Certificate.ExplicitPotential.Core 6 9} (hp : IsCore097 core) : core.Connected

The row-097 core is connected: any nonempty proper cut of the six vertices is crossed by some slot. Assuming no slot crosses the cut, the nine slots link all six vertices into a single chain 0 - 4, 0 - 5 - 1, 1 - 2, 1 - 3, so every vertex agrees with 0.

The pencil parameters

Every parameter is a function of the length vector alone; no positivity and no spec is involved.

def LowGenus.GenusFourRow097Closed.dpos (L : Fin 9 → ℕ) : ℕ

Depth of the moving chip on slot e3.

Equations

• LowGenus.GenusFourRow097Closed.dpos L = min (L 0 - L 5) (L 4)

def LowGenus.GenusFourRow097Closed.cRest (L : Fin 9 → ℕ) : ℕ

Residual handle imbalance.

Equations

• LowGenus.GenusFourRow097Closed.cRest L = L 0 - L 5 - LowGenus.GenusFourRow097Closed.dpos L

def LowGenus.GenusFourRow097Closed.uMax (L : Fin 9 → ℕ) : ℕ

Length of the star 2 march.

Equations

• LowGenus.GenusFourRow097Closed.uMax L = min (L 3 - LowGenus.GenusFourRow097Closed.dpos L) (min (L 6) (L 7))

def LowGenus.GenusFourRow097Closed.m2Max (L : Fin 9 → ℕ) : ℕ

Length of the second pass of the {e0,e5} march.

Equations

• LowGenus.GenusFourRow097Closed.m2Max L = min (LowGenus.GenusFourRow097Closed.cRest L) (L 5)

def LowGenus.GenusFourRow097Closed.wMax (L : Fin 9 → ℕ) : ℕ

Length of the star 0 march.

Equations

• LowGenus.GenusFourRow097Closed.wMax L = min (LowGenus.GenusFourRow097Closed.cRest L - LowGenus.GenusFourRow097Closed.m2Max L) (min (L 1) (L 2))

The four marches

def LowGenus.GenusFourRow097Closed.vPot (u : ℕ) : Fin 6 → ℤ

Core potential of the star 2 march.

Equations

• LowGenus.GenusFourRow097Closed.vPot u v = if v = 2 then -↑u else 0

def LowGenus.GenusFourRow097Closed.vSgn : Fin 9 → ℤ

Slot signs of the star 2 march.

Equations

• LowGenus.GenusFourRow097Closed.vSgn e = if e = 3 then -1 else if e = 6 then 1 else if e = 7 then 1 else 0

def LowGenus.GenusFourRow097Closed.vLo (L : Fin 9 → ℕ) (u : ℕ) : Fin 9 → ℕ

Window starts of the star 2 march.

Equations

• LowGenus.GenusFourRow097Closed.vLo L u e = if e = 3 then LowGenus.GenusFourRow097Closed.dpos L else if e = 6 then L 6 - u else if e = 7 then L 7 - u else 0

def LowGenus.GenusFourRow097Closed.pPot (s : ℕ) : Fin 6 → ℤ

Core potential of the {e0,e3,e4} march.

Equations

• LowGenus.GenusFourRow097Closed.pPot s v = if v = 0 then -↑s else if v = 1 then -↑s else if v = 5 then -↑s else 0

def LowGenus.GenusFourRow097Closed.pSgn : Fin 9 → ℤ

Slot signs of the {e0,e3,e4} march.

Equations

• LowGenus.GenusFourRow097Closed.pSgn e = if e = 0 then 1 else if e = 3 then 1 else if e = 4 then 1 else 0

def LowGenus.GenusFourRow097Closed.pLo (L : Fin 9 → ℕ) (s : ℕ) : Fin 9 → ℕ

Window starts of the {e0,e3,e4} march.

Equations

• LowGenus.GenusFourRow097Closed.pLo L s e = if e = 0 then L 0 - s else if e = 3 then LowGenus.GenusFourRow097Closed.dpos L - s else if e = 4 then L 4 - s else 0

def LowGenus.GenusFourRow097Closed.mPot (r : ℕ) : Fin 6 → ℤ

Core potential of the {e0,e5} march.

Equations

• LowGenus.GenusFourRow097Closed.mPot r v = if v = 0 then -↑r else if v = 5 then -↑r else 0

def LowGenus.GenusFourRow097Closed.mSgn : Fin 9 → ℤ

Slot signs of the {e0,e5} march.

Equations

• LowGenus.GenusFourRow097Closed.mSgn e = if e = 0 then 1 else if e = 5 then -1 else 0

def LowGenus.GenusFourRow097Closed.mLo (a r : ℕ) : Fin 9 → ℕ

Window starts of the {e0,e5} march starting from depth a on e0.

Equations

• LowGenus.GenusFourRow097Closed.mLo a r e = if e = 0 then a - r else 0

def LowGenus.GenusFourRow097Closed.wPot (w : ℕ) : Fin 6 → ℤ

Core potential of the star 0 march.

Equations

• LowGenus.GenusFourRow097Closed.wPot w v = if v = 0 then -↑w else 0

def LowGenus.GenusFourRow097Closed.wSgn : Fin 9 → ℤ

Slot signs of the star 0 march.

Equations

• LowGenus.GenusFourRow097Closed.wSgn e = if e = 0 then 1 else if e = 1 then 1 else if e = 2 then 1 else 0

def LowGenus.GenusFourRow097Closed.wLo (L : Fin 9 → ℕ) (w : ℕ) : Fin 9 → ℕ

Window starts of the star 0 march.

Equations

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

@[simp]

theorem LowGenus.GenusFourRow097Closed.vPot_0 {u : ℕ} : vPot u 0 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vPot_1 {u : ℕ} : vPot u 1 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vPot_2 {u : ℕ} : vPot u 2 = -↑u

@[simp]

theorem LowGenus.GenusFourRow097Closed.vPot_3 {u : ℕ} : vPot u 3 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vPot_4 {u : ℕ} : vPot u 4 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vPot_5 {u : ℕ} : vPot u 5 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vSgn_0 : vSgn 0 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vSgn_1 : vSgn 1 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vSgn_2 : vSgn 2 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vSgn_3 : vSgn 3 = -1

@[simp]

theorem LowGenus.GenusFourRow097Closed.vSgn_4 : vSgn 4 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vSgn_5 : vSgn 5 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vSgn_6 : vSgn 6 = 1

@[simp]

theorem LowGenus.GenusFourRow097Closed.vSgn_7 : vSgn 7 = 1

@[simp]

theorem LowGenus.GenusFourRow097Closed.vSgn_8 : vSgn 8 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vLo_0 {L : Fin 9 → ℕ} {u : ℕ} : vLo L u 0 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vLo_1 {L : Fin 9 → ℕ} {u : ℕ} : vLo L u 1 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vLo_2 {L : Fin 9 → ℕ} {u : ℕ} : vLo L u 2 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vLo_3 {L : Fin 9 → ℕ} {u : ℕ} : vLo L u 3 = dpos L

@[simp]

theorem LowGenus.GenusFourRow097Closed.vLo_4 {L : Fin 9 → ℕ} {u : ℕ} : vLo L u 4 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vLo_5 {L : Fin 9 → ℕ} {u : ℕ} : vLo L u 5 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.vLo_6 {L : Fin 9 → ℕ} {u : ℕ} : vLo L u 6 = L 6 - u

@[simp]

theorem LowGenus.GenusFourRow097Closed.vLo_7 {L : Fin 9 → ℕ} {u : ℕ} : vLo L u 7 = L 7 - u

@[simp]

theorem LowGenus.GenusFourRow097Closed.vLo_8 {L : Fin 9 → ℕ} {u : ℕ} : vLo L u 8 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pPot_0 {s : ℕ} : pPot s 0 = -↑s

@[simp]

theorem LowGenus.GenusFourRow097Closed.pPot_1 {s : ℕ} : pPot s 1 = -↑s

@[simp]

theorem LowGenus.GenusFourRow097Closed.pPot_2 {s : ℕ} : pPot s 2 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pPot_3 {s : ℕ} : pPot s 3 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pPot_4 {s : ℕ} : pPot s 4 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pPot_5 {s : ℕ} : pPot s 5 = -↑s

@[simp]

theorem LowGenus.GenusFourRow097Closed.pSgn_0 : pSgn 0 = 1

@[simp]

theorem LowGenus.GenusFourRow097Closed.pSgn_1 : pSgn 1 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pSgn_2 : pSgn 2 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pSgn_3 : pSgn 3 = 1

@[simp]

theorem LowGenus.GenusFourRow097Closed.pSgn_4 : pSgn 4 = 1

@[simp]

theorem LowGenus.GenusFourRow097Closed.pSgn_5 : pSgn 5 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pSgn_6 : pSgn 6 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pSgn_7 : pSgn 7 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pSgn_8 : pSgn 8 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pLo_0 {L : Fin 9 → ℕ} {s : ℕ} : pLo L s 0 = L 0 - s

@[simp]

theorem LowGenus.GenusFourRow097Closed.pLo_1 {L : Fin 9 → ℕ} {s : ℕ} : pLo L s 1 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pLo_2 {L : Fin 9 → ℕ} {s : ℕ} : pLo L s 2 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pLo_3 {L : Fin 9 → ℕ} {s : ℕ} : pLo L s 3 = dpos L - s

@[simp]

theorem LowGenus.GenusFourRow097Closed.pLo_4 {L : Fin 9 → ℕ} {s : ℕ} : pLo L s 4 = L 4 - s

@[simp]

theorem LowGenus.GenusFourRow097Closed.pLo_5 {L : Fin 9 → ℕ} {s : ℕ} : pLo L s 5 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pLo_6 {L : Fin 9 → ℕ} {s : ℕ} : pLo L s 6 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pLo_7 {L : Fin 9 → ℕ} {s : ℕ} : pLo L s 7 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.pLo_8 {L : Fin 9 → ℕ} {s : ℕ} : pLo L s 8 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mPot_0 {r : ℕ} : mPot r 0 = -↑r

@[simp]

theorem LowGenus.GenusFourRow097Closed.mPot_1 {r : ℕ} : mPot r 1 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mPot_2 {r : ℕ} : mPot r 2 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mPot_3 {r : ℕ} : mPot r 3 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mPot_4 {r : ℕ} : mPot r 4 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mPot_5 {r : ℕ} : mPot r 5 = -↑r

@[simp]

theorem LowGenus.GenusFourRow097Closed.mSgn_0 : mSgn 0 = 1

@[simp]

theorem LowGenus.GenusFourRow097Closed.mSgn_1 : mSgn 1 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mSgn_2 : mSgn 2 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mSgn_3 : mSgn 3 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mSgn_4 : mSgn 4 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mSgn_5 : mSgn 5 = -1

@[simp]

theorem LowGenus.GenusFourRow097Closed.mSgn_6 : mSgn 6 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mSgn_7 : mSgn 7 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mSgn_8 : mSgn 8 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mLo_0 {r a : ℕ} : mLo a r 0 = a - r

@[simp]

theorem LowGenus.GenusFourRow097Closed.mLo_1 {r a : ℕ} : mLo a r 1 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mLo_2 {r a : ℕ} : mLo a r 2 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mLo_3 {r a : ℕ} : mLo a r 3 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mLo_4 {r a : ℕ} : mLo a r 4 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mLo_5 {r a : ℕ} : mLo a r 5 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mLo_6 {r a : ℕ} : mLo a r 6 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mLo_7 {r a : ℕ} : mLo a r 7 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.mLo_8 {r a : ℕ} : mLo a r 8 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wPot_0 {w : ℕ} : wPot w 0 = -↑w

@[simp]

theorem LowGenus.GenusFourRow097Closed.wPot_1 {w : ℕ} : wPot w 1 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wPot_2 {w : ℕ} : wPot w 2 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wPot_3 {w : ℕ} : wPot w 3 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wPot_4 {w : ℕ} : wPot w 4 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wPot_5 {w : ℕ} : wPot w 5 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wSgn_0 : wSgn 0 = 1

@[simp]

theorem LowGenus.GenusFourRow097Closed.wSgn_1 : wSgn 1 = 1

@[simp]

theorem LowGenus.GenusFourRow097Closed.wSgn_2 : wSgn 2 = 1

@[simp]

theorem LowGenus.GenusFourRow097Closed.wSgn_3 : wSgn 3 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wSgn_4 : wSgn 4 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wSgn_5 : wSgn 5 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wSgn_6 : wSgn 6 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wSgn_7 : wSgn 7 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wSgn_8 : wSgn 8 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wLo_0 {L : Fin 9 → ℕ} {w : ℕ} : wLo L w 0 = cRest L - m2Max L - w

@[simp]

theorem LowGenus.GenusFourRow097Closed.wLo_1 {L : Fin 9 → ℕ} {w : ℕ} : wLo L w 1 = L 1 - w

@[simp]

theorem LowGenus.GenusFourRow097Closed.wLo_2 {L : Fin 9 → ℕ} {w : ℕ} : wLo L w 2 = L 2 - w

@[simp]

theorem LowGenus.GenusFourRow097Closed.wLo_3 {L : Fin 9 → ℕ} {w : ℕ} : wLo L w 3 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wLo_4 {L : Fin 9 → ℕ} {w : ℕ} : wLo L w 4 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wLo_5 {L : Fin 9 → ℕ} {w : ℕ} : wLo L w 5 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wLo_6 {L : Fin 9 → ℕ} {w : ℕ} : wLo L w 6 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wLo_7 {L : Fin 9 → ℕ} {w : ℕ} : wLo L w 7 = 0

@[simp]

theorem LowGenus.GenusFourRow097Closed.wLo_8 {L : Fin 9 → ℕ} {w : ℕ} : wLo L w 8 = 0

The ramps

RampData.repInv — the one field the open orthant does not need — is supplied uniformly by RampData.of_reachIn from RepGen, so each march below proves exactly the two conditions its open counterpart proves.

def LowGenus.GenusFourRow097Closed.RepGen (d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9) : Prop

The census hypothesis every closed-orthant march needs: rep-equality is witnessed by a chain of vanishing slots. Free for RowProof.censusSpec, whose rep is compFold of the vanishing set (compFold_iff).

Equations

• LowGenus.GenusFourRow097Closed.RepGen d = ∀ (u v : Fin 6), d.rep u = d.rep v → Utilities.Certificate.ContractionForestCensusGeneral.ReachIn d.core {e : Fin 9 | d.length e = 0} u v

theorem LowGenus.GenusFourRow097Closed.vRamp {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hrep : RepGen d) {u : ℕ} (hu3 : dpos d.length + u ≤ d.length 3) (hu6 : u ≤ d.length 6) (hu7 : u ≤ d.length 7) : d.RampData (vPot u) vSgn (vLo d.length u) u

theorem LowGenus.GenusFourRow097Closed.pRamp {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hrep : RepGen d) {s : ℕ} (hs0 : s ≤ d.length 0) (hsd : s ≤ dpos d.length) (hd3 : dpos d.length ≤ d.length 3) (hs4 : s ≤ d.length 4) : d.RampData (pPot s) pSgn (pLo d.length s) s

theorem LowGenus.GenusFourRow097Closed.mRamp {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hrep : RepGen d) {a r : ℕ} (ha : a ≤ d.length 0) (hr1 : r ≤ a) (hr2 : r ≤ d.length 5) : d.RampData (mPot r) mSgn (mLo a r) r

theorem LowGenus.GenusFourRow097Closed.wRamp {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hrep : RepGen d) {w : ℕ} (hx : cRest d.length - m2Max d.length ≤ d.length 0) (hww : w ≤ cRest d.length - m2Max d.length) (hw1 : w ≤ d.length 1) (hw2 : w ≤ d.length 2) : d.RampData (wPot w) wSgn (wLo d.length w) w

def LowGenus.GenusFourRow097Closed.vScript (d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9) (u : ℕ) : firingScript d.graph

The star 2 march.

Equations

• LowGenus.GenusFourRow097Closed.vScript d u = d.rampScript (LowGenus.GenusFourRow097Closed.vPot u) LowGenus.GenusFourRow097Closed.vSgn (LowGenus.GenusFourRow097Closed.vLo d.length u) u

def LowGenus.GenusFourRow097Closed.pScript (d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9) (s : ℕ) : firingScript d.graph

The {e0,e3,e4} march.

Equations

• LowGenus.GenusFourRow097Closed.pScript d s = d.rampScript (LowGenus.GenusFourRow097Closed.pPot s) LowGenus.GenusFourRow097Closed.pSgn (LowGenus.GenusFourRow097Closed.pLo d.length s) s

def LowGenus.GenusFourRow097Closed.mScript (d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9) (a r : ℕ) : firingScript d.graph

The {e0,e5} march.

Equations

• LowGenus.GenusFourRow097Closed.mScript d a r = d.rampScript (LowGenus.GenusFourRow097Closed.mPot r) LowGenus.GenusFourRow097Closed.mSgn (LowGenus.GenusFourRow097Closed.mLo a r) r

def LowGenus.GenusFourRow097Closed.wScript (d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9) (w : ℕ) : firingScript d.graph

The star 0 march.

Equations

• LowGenus.GenusFourRow097Closed.wScript d w = d.rampScript (LowGenus.GenusFourRow097Closed.wPot w) LowGenus.GenusFourRow097Closed.wSgn (LowGenus.GenusFourRow097Closed.wLo d.length w) w

Divisor identities for the four marches

Each is one instantiation of the generic DegSpec.prin_ramp_eq, expanded over the nine slots. No case analysis and no heartbeat override occurs.

theorem LowGenus.GenusFourRow097Closed.prin_v_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} {u : ℕ} (h : d.RampData (vPot u) vSgn (vLo d.length u) u) (hu6 : u ≤ d.length 6) (hu7 : u ≤ d.length 7) : (prin d.graph) (vScript d u) = oneChip (d.pathAt 3 (dpos d.length + u)) - oneChip (d.pathAt 3 (dpos d.length)) + (oneChip (d.pathAt 6 (d.length 6 - u)) - oneChip (d.pathAt 6 (d.length 6))) + (oneChip (d.pathAt 7 (d.length 7 - u)) - oneChip (d.pathAt 7 (d.length 7)))

theorem LowGenus.GenusFourRow097Closed.prin_p_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} {s : ℕ} (h : d.RampData (pPot s) pSgn (pLo d.length s) s) (hs0 : s ≤ d.length 0) (hsd : s ≤ dpos d.length) (hs4 : s ≤ d.length 4) : (prin d.graph) (pScript d s) = oneChip (d.pathAt 0 (d.length 0 - s)) - oneChip (d.pathAt 0 (d.length 0)) + (oneChip (d.pathAt 3 (dpos d.length - s)) - oneChip (d.pathAt 3 (dpos d.length))) + (oneChip (d.pathAt 4 (d.length 4 - s)) - oneChip (d.pathAt 4 (d.length 4)))

theorem LowGenus.GenusFourRow097Closed.prin_m_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} {a r : ℕ} (h : d.RampData (mPot r) mSgn (mLo a r) r) (hr1 : r ≤ a) : (prin d.graph) (mScript d a r) = oneChip (d.pathAt 0 (a - r)) - oneChip (d.pathAt 0 a) - (oneChip (d.pathAt 5 0) - oneChip (d.pathAt 5 r))

theorem LowGenus.GenusFourRow097Closed.prin_w_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} {w : ℕ} (h : d.RampData (wPot w) wSgn (wLo d.length w) w) (hww : w ≤ cRest d.length - m2Max d.length) (hw1 : w ≤ d.length 1) (hw2 : w ≤ d.length 2) : (prin d.graph) (wScript d w) = oneChip (d.pathAt 0 (cRest d.length - m2Max d.length - w)) - oneChip (d.pathAt 0 (cRest d.length - m2Max d.length)) + (oneChip (d.pathAt 1 (d.length 1 - w)) - oneChip (d.pathAt 1 (d.length 1))) + (oneChip (d.pathAt 2 (d.length 2 - w)) - oneChip (d.pathAt 2 (d.length 2)))

Bridging core classes and path positions

On the closed orthant these are the only places where a slot's two endpoints can coincide, and pathAt already knows: pathAt e k = coreVertex (head e) for every k ≥ length e, including k = 0 on a vanishing slot.

theorem LowGenus.GenusFourRow097Closed.cvT0 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 0 0 = d.coreVertex 0

theorem LowGenus.GenusFourRow097Closed.cvT1 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 1 0 = d.coreVertex 0

theorem LowGenus.GenusFourRow097Closed.cvT2 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 2 0 = d.coreVertex 0

theorem LowGenus.GenusFourRow097Closed.cvT3 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 3 0 = d.coreVertex 1

theorem LowGenus.GenusFourRow097Closed.cvT4 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 4 0 = d.coreVertex 1

theorem LowGenus.GenusFourRow097Closed.cvT5 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 5 0 = d.coreVertex 1

theorem LowGenus.GenusFourRow097Closed.cvT6 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 6 0 = d.coreVertex 2

theorem LowGenus.GenusFourRow097Closed.cvT7 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 7 0 = d.coreVertex 2

theorem LowGenus.GenusFourRow097Closed.cvH0 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 0 (d.length 0) = d.coreVertex 4

theorem LowGenus.GenusFourRow097Closed.cvH1 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 1 (d.length 1) = d.coreVertex 5

theorem LowGenus.GenusFourRow097Closed.cvH2 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 2 (d.length 2) = d.coreVertex 5

theorem LowGenus.GenusFourRow097Closed.cvH3 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 3 (d.length 3) = d.coreVertex 2

theorem LowGenus.GenusFourRow097Closed.cvH4 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 4 (d.length 4) = d.coreVertex 3

theorem LowGenus.GenusFourRow097Closed.cvH5 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 5 (d.length 5) = d.coreVertex 5

theorem LowGenus.GenusFourRow097Closed.cvH6 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 6 (d.length 6) = d.coreVertex 3

theorem LowGenus.GenusFourRow097Closed.cvH7 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) : d.pathAt 7 (d.length 7) = d.coreVertex 4

The pencil and the states it passes through

def LowGenus.GenusFourRow097Closed.pen (d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9) : CFDiv d.graph

The degree-three pencil of row 097.

Equations

• LowGenus.GenusFourRow097Closed.pen d = oneChip (d.pathAt 3 (LowGenus.GenusFourRow097Closed.dpos d.length)) + oneChip (d.coreVertex 3) + oneChip (d.coreVertex 4)

theorem LowGenus.GenusFourRow097Closed.deg_pen {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} : CFDiv.degree (pen d) = 3

theorem LowGenus.GenusFourRow097Closed.state_v {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hrep : RepGen d) {u : ℕ} (hu3 : dpos d.length + u ≤ d.length 3) (hu6 : u ≤ d.length 6) (hu7 : u ≤ d.length 7) : pen d + (prin d.graph) (vScript d u) = oneChip (d.pathAt 3 (dpos d.length + u)) + oneChip (d.pathAt 6 (d.length 6 - u)) + oneChip (d.pathAt 7 (d.length 7 - u))

theorem LowGenus.GenusFourRow097Closed.state_p {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hrep : RepGen d) {s : ℕ} (hs0 : s ≤ d.length 0) (hsd : s ≤ dpos d.length) (hd3 : dpos d.length ≤ d.length 3) (hs4 : s ≤ d.length 4) : pen d + (prin d.graph) (pScript d s) = oneChip (d.pathAt 0 (d.length 0 - s)) + oneChip (d.pathAt 3 (dpos d.length - s)) + oneChip (d.pathAt 4 (d.length 4 - s))

theorem LowGenus.GenusFourRow097Closed.state_m1 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hrep : RepGen d) (hd0 : dpos d.length ≤ d.length 0) (hd3 : dpos d.length ≤ d.length 3) (hd4 : dpos d.length ≤ d.length 4) {r : ℕ} (hr : r ≤ d.length 5) (hrle : r ≤ d.length 0 - dpos d.length) : pen d + (prin d.graph) (pScript d (dpos d.length) + mScript d (d.length 0 - dpos d.length) r) = oneChip (d.pathAt 0 (d.length 0 - dpos d.length - r)) + oneChip (d.pathAt 5 r) + oneChip (d.pathAt 4 (d.length 4 - dpos d.length))

theorem LowGenus.GenusFourRow097Closed.state_m2 {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hrep : RepGen d) (hd0 : dpos d.length ≤ d.length 0) (hd3 : dpos d.length ≤ d.length 3) (hd4 : dpos d.length ≤ d.length 4) (hcase : d.length 4 = dpos d.length) (h5 : d.length 5 ≤ d.length 0 - dpos d.length) {r : ℕ} (hr : r ≤ d.length 5) (hrc : r ≤ cRest d.length) : pen d + (prin d.graph) (pScript d (dpos d.length) + mScript d (d.length 0 - dpos d.length) (d.length 5) + mScript d (cRest d.length) r) = oneChip (d.pathAt 0 (cRest d.length - r)) + oneChip (d.pathAt 5 r) + oneChip (d.coreVertex 5)

theorem LowGenus.GenusFourRow097Closed.state_w {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hrep : RepGen d) (hd0 : dpos d.length ≤ d.length 0) (hd3 : dpos d.length ≤ d.length 3) (hd4 : dpos d.length ≤ d.length 4) (hcase : d.length 4 = dpos d.length) (h5 : d.length 5 ≤ d.length 0 - dpos d.length) (hm2 : m2Max d.length = d.length 5) {w : ℕ} (hww : w ≤ cRest d.length - m2Max d.length) (hw1 : w ≤ d.length 1) (hw2 : w ≤ d.length 2) : pen d + (prin d.graph) (pScript d (dpos d.length) + mScript d (d.length 0 - dpos d.length) (d.length 5) + mScript d (cRest d.length) (d.length 5) + wScript d w) = oneChip (d.pathAt 0 (cRest d.length - m2Max d.length - w)) + oneChip (d.pathAt 1 (d.length 1 - w)) + oneChip (d.pathAt 2 (d.length 2 - w))

Reaching every core class

theorem LowGenus.GenusFourRow097Closed.chip_three {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (A B C q : d.graph.V) (hq : q = A ∨ q = B ∨ q = C) : 1 ≤ (oneChip A + oneChip B + oneChip C) q

theorem LowGenus.GenusFourRow097Closed.reaches_three {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (script : firingScript d.graph) (A B C : d.graph.V) (hst : pen d + (prin d.graph) script = oneChip A + oneChip B + oneChip C) (q : d.graph.V) (hq : q = A ∨ q = B ∨ q = C) : Utilities.Certificate.StrongSeparator.Reaches d.graph (pen d) q

The covering argument

theorem LowGenus.GenusFourRow097Closed.bounds {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hba : d.length 5 ≤ d.length 0) (hbc : d.length 4 ≤ d.length 3) : dpos d.length ≤ d.length 4 ∧ dpos d.length ≤ d.length 3 ∧ dpos d.length ≤ d.length 0 ∧ d.length 5 ≤ d.length 0 - dpos d.length

theorem LowGenus.GenusFourRow097Closed.uBounds {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hbc : d.length 4 ≤ d.length 3) : dpos d.length + uMax d.length ≤ d.length 3 ∧ uMax d.length ≤ d.length 6 ∧ uMax d.length ≤ d.length 7

theorem LowGenus.GenusFourRow097Closed.wLen {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hba : d.length 5 ≤ d.length 0) : cRest d.length - m2Max d.length ≤ d.length 0

theorem LowGenus.GenusFourRow097Closed.wBounds {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} : wMax d.length ≤ cRest d.length - m2Max d.length ∧ wMax d.length ≤ d.length 1 ∧ wMax d.length ≤ d.length 2

theorem LowGenus.GenusFourRow097Closed.mBounds {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} : m2Max d.length ≤ cRest d.length ∧ m2Max d.length ≤ d.length 5

theorem LowGenus.GenusFourRow097Closed.cRest_le {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hba : d.length 5 ≤ d.length 0) : cRest d.length ≤ d.length 0

theorem LowGenus.GenusFourRow097Closed.dpos_eq_of_cRest_pos {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (h : 0 < cRest d.length) : d.length 4 = dpos d.length

A nonzero residual imbalance forces the moving chip to sit at the far end of slot e4.

theorem LowGenus.GenusFourRow097Closed.m2Max_eq_of_pos {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (h : 0 < cRest d.length - m2Max d.length) : m2Max d.length = d.length 5

If the star 0 march is nontrivial then the second {e0,e5} pass ran to the end of slot e5.

theorem LowGenus.GenusFourRow097Closed.cRest_pos_of {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (h : 0 < cRest d.length - m2Max d.length) : 0 < cRest d.length

theorem LowGenus.GenusFourRow097Closed.banana_pair {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hrep : RepGen d) (hba : d.length 5 ≤ d.length 0) (hbc : d.length 4 ≤ d.length 3) (hx0 : cRest d.length - m2Max d.length = 0) : ∃ (script : firingScript d.graph) (Z : d.graph.V), pen d + (prin d.graph) script = oneChip (d.coreVertex 0) + oneChip (d.coreVertex 5) + oneChip Z

A state with chips at both banana endpoints, available whenever the star 0 march is trivial.

theorem LowGenus.GenusFourRow097Closed.hub_two {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hbc : d.length 4 ≤ d.length 3) : d.coreVertex 2 = d.pathAt 3 (dpos d.length + uMax d.length) ∨ d.coreVertex 2 = d.pathAt 6 (d.length 6 - uMax d.length) ∨ d.coreVertex 2 = d.pathAt 7 (d.length 7 - uMax d.length)

At the end of the star 2 march there is a chip at the hub 2.

theorem LowGenus.GenusFourRow097Closed.hub_zero {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hba : d.length 5 ≤ d.length 0) : d.coreVertex 0 = d.pathAt 0 (cRest d.length - m2Max d.length - wMax d.length) ∨ d.coreVertex 0 = d.pathAt 1 (d.length 1 - wMax d.length) ∨ d.coreVertex 0 = d.pathAt 2 (d.length 2 - wMax d.length)

At the end of the star 0 march there is a chip at the vertex 0.

theorem LowGenus.GenusFourRow097Closed.reaches_core {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hrep : RepGen d) (hba : d.length 5 ≤ d.length 0) (hbc : d.length 4 ≤ d.length 3) (v : Fin 6) : Utilities.Certificate.StrongSeparator.Reaches d.graph (pen d) (d.coreVertex v)

Every core class is reached.

theorem LowGenus.GenusFourRow097Closed.bnExists_one_three {d : Utilities.Certificate.DegenerateSpec.DegSpec 6 9} (hp : IsCore097 d.core) (hrep : RepGen d) (hba : d.length 5 ≤ d.length 0) (hbc : d.length 4 ≤ d.length 3) : Utilities.BNExists d.graph 1 3

Row 097 on the closed orthant, in the chamber length 5 ≤ length 0, length 4 ≤ length 3.

The catalog row, on the closed orthant

An arbitrary length vector is moved into the chamber length 5 ≤ length 0 ∧ length 4 ≤ length 3 by the Klein four-group of automorphisms of the row-097 core, transported with ClosedCoreSymmetry.bnExists_iff — the closed-orthant counterpart of Certificate/SubdivisionIso.lean's bnExists_of_coreAuto. The transport is along the contracted graphs, so the chamber reduction costs nothing extra at a face.

@[reducible, inline]

abbrev LowGenus.GenusFourRow097Closed.core : Utilities.Certificate.ExplicitPotential.Core 6 9

The row-097 split core is the public cubic-atlas presentation.

Equations

• LowGenus.GenusFourRow097Closed.core = AtanasovRanganathan.GenusFourCubicAtlas.row097Core

theorem LowGenus.GenusFourRow097Closed.isCore097_core : IsCore097 core

def LowGenus.GenusFourRow097Closed.sigVertex : Equiv.Perm (Fin 6)

σ = (0 5)(1 4) on core vertices.

Equations

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

def LowGenus.GenusFourRow097Closed.sigSlot : Equiv.Perm (Fin 9)

σ on edge slots: e0 ↔ e5, e3 ↔ e7, e4 ↔ e8.

Equations

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

def LowGenus.GenusFourRow097Closed.sigReversed : Fin 9 → Bool

Reading directions of the σ-image slots.

Equations

• LowGenus.GenusFourRow097Closed.sigReversed = ![true, true, true, true, true, true, false, true, true]

def LowGenus.GenusFourRow097Closed.tauVertex : Equiv.Perm (Fin 6)

τ = (2 3) on core vertices.

Equations

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

def LowGenus.GenusFourRow097Closed.tauSlot : Equiv.Perm (Fin 9)

τ on edge slots: e3 ↔ e4, e7 ↔ e8.

Equations

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

def LowGenus.GenusFourRow097Closed.tauReversed : Fin 9 → Bool

Reading directions of the τ-image slots.

Equations

• LowGenus.GenusFourRow097Closed.tauReversed = ![false, false, false, false, false, false, true, false, false]

def LowGenus.GenusFourRow097Closed.sigma : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry core

σ, as a core symmetry.

Equations

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

def LowGenus.GenusFourRow097Closed.tau : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry core

τ, as a core symmetry.

Equations

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

theorem LowGenus.GenusFourRow097Closed.repGen_censusSpec (ℓ : Fin 9 → ℕ) (hForest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest core (Utilities.Certificate.ClosedFaceCensus.zeroSet ℓ)) (hNotLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy core (Utilities.Certificate.ClosedFaceCensus.zeroSet ℓ)) : RepGen (Utilities.Certificate.ClosedFaceCensus.censusSpec core repGen_censusSpec._proof_1 ℓ hForest hNotLoopy)

censusSpec's representative map is a compFold of the vanishing set, so RepGen — the one hypothesis a closed-orthant ramp needs beyond the open-orthant ones — is free.

theorem LowGenus.GenusFourRow097Closed.bnExists_closed (ℓ : Fin 9 → ℕ) (hForest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest core (Utilities.Certificate.ClosedFaceCensus.zeroSet ℓ)) (hNotLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy core (Utilities.Certificate.ClosedFaceCensus.zeroSet ℓ)) : Utilities.BNExists (Utilities.Certificate.ClosedFaceCensus.censusSpec core repGen_censusSpec._proof_1 ℓ hForest hNotLoopy).graph 1 3

BNExists … 1 3 for catalog row 097, on the whole closed length orthant. Quantified over every length vector whose vanishing set is a non-loopy forest — every subdivision of the row-097 core and every equal-genus contraction of one.

No Boolean check, no generated data, and no length chamber decomposition occurs anywhere below: the four cases are the orbit of one under the core's Klein four-group.

theorem LowGenus.GenusFourRow097Closed.genus_eq (ℓ : Fin 9 → ℕ) (hForest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest core (Utilities.Certificate.ClosedFaceCensus.zeroSet ℓ)) (hNotLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy core (Utilities.Certificate.ClosedFaceCensus.zeroSet ℓ)) : (Utilities.Certificate.ClosedFaceCensus.censusSpec core repGen_censusSpec._proof_1 ℓ hForest hNotLoopy).graph.genus = 4

The object the conclusion speaks about has the row's genus at every face.