A symbolic pencil for genus-four Core 096 (skeleton) #
Row 096 of the genus-four pseudocore catalog is the necklace of three
bananas: bananas β₀ = {v0,v5} (arcs e1,e2), β₁ = {v1,v4} (arcs
e4,e5), β₂ = {v2,v3} (arcs e6,e7), joined in a cycle by the three
single slots e0 : v0–v4 (length a₀), e3 : v1–v3 (a₁), and
e8 : v2–v5 (a₂).
The row is already closed (RowProof.Row096Replacement.rowSolved_row096) by a
17,705-node replayed Farkas cover in 274 kernel jobs. This file is the
skeleton of a symbolic replacement in the style of
GenusFourCore099/100/097, from the divisor rule discovered and empirically
verified on 2026-08-13 (400/400 random positive length vectors, plus a
member-by-member verification of the complete regime-1 pencil on 45/45
vectors; see the accompanying analysis §6 and
auxiliary calculations):
Rotate by the order-three necklace rotation so that a₀ = max(a₀,a₁,a₂),
and write x = a₀ − a₁ − a₂.
- Regime 1 (
x ≤ 0):D = v0 + v5 + (point on e3 at distance a₀ − a₂ from v1). The pencil is the level set of the conserved quantityτ = j + k + m = a₀: one chip on each single slot at distancesj, k, mfromv0, v1, v2respectively, every such configuration withj ≤ a₀, k ≤ a₁, m ≤ a₂being equivalent, together with the six full-arc reflection families hanging off the three configurations where the two chips flanking a banana reach its endpoints. Coverage is immediate interval arithmetic; the window[max aᵢ, min (aᵢ+aⱼ)]forτis nonempty exactly by the triangle inequality. - Regime 2 (
x > 0):D = v0 + v5 + (point on the longer arc of β₂ at distance min(x, shorter arc length) from v3)(after the arc swap ofe6/e7, "longer arc = e6").
Every equivalence needed is an instance of the public RampData machinery in
Utilities.Subdivision.RampScript, through the single generic primitive prin_cutRamp
below: the Laplacian of a ramp supported on the slots crossing a cut moves one
chip by t along each of them. Both regimes are cut marches only — no capped
reflections are needed, because the anchor-only route (the embedded core
vertices are a strong separator, so
Certificate.CoreVertexReachability.bnExists_of_reaches_coreVertices upgrades
reachability at the six core vertices to rank ≥ 1) removes the nine-slot
interior sweep from the obligation. The "banana relay" of regime 2 is the
three-slot instance of prin_cutRamp at the cut {e0,e6,e7}.
This file is complete: no sorry remains.
The rotation and arc-swap automorphisms of the necklace #
The order-three rotation of the necklace on core vertices:
v0 → v1 → v2 → v0, v4 → v3 → v5 → v4.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The order-three rotation on edge slots: singles e0 → e3 → e8 → e0,
arcs e1 → e4 → e6 → e1 and e2 → e5 → e7 → e2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The rotation preserves every slot's reading direction.
Equations
Instances For
Swapping the two arcs of β₂ (slots e6, e7), fixing everything
else.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The arc swap fixes every core vertex and reverses no slot.
Equations
Instances For
The necklace core, as a predicate on an arbitrary spec #
Stating the incidence data as a predicate lets the pencil and its sweep be
developed for an arbitrary Spec 6 9, with the public row-096 core
instantiating it at the end.
The incidence structure of the necklace of three bananas: bananas
β₀ = {v0,v5} on arcs e1,e2, β₁ = {v1,v4} on e4,e5, β₂ = {v2,v3} on
e6,e7, joined by the singles e0 : v0–v4, e3 : v1–v3, e8 : v2–v5.
Instances For
The catalog's split core is a necklace.
The regime-1 pencil divisor #
D = v0 + v5 + (point on e3 at distance a₀ − a₂ from v1). In regime 1 the
offset a₀ − a₂ lies in [0, a₁]: nonnegative because a₀ is maximal, and at
most a₁ by the triangle inequality, so it names a genuine path position.
The interior offset of the third chip on slot e3: a₀ − a₂.
Equations
- LowGenus.GenusFourRow096Pencil.kPos spec = spec.length 0 - spec.length 8
Instances For
The regime-1 divisor.
Equations
- LowGenus.GenusFourRow096Pencil.pencil1 spec htri = oneChip (spec.coreVertex 0) + oneChip (spec.coreVertex 5) + oneChip (spec.pathVertex 3 ⟨LowGenus.GenusFourRow096Pencil.kPos spec, ⋯⟩)
Instances For
The regime-2 relay depth s = min(x, a₇), where x = a₀ − a₁ − a₂. It is
both the distance of the third chip from v3 along the long arc e6 and the
length of the three-slot relay march across β₂.
Equations
Instances For
The regime-2 divisor D = v0 + v5 + (point on e6 at distance s from v3).
No hypothesis is needed to state it: the offset length e6 - s is a path
position of e6 whatever the lengths are.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Chip bookkeeping and the two-slot march #
All the regime-1 marches are instances of a single generic move: a ramp whose
sign vector is supported on two slots, -1 on one and +1 on the other. Its
Laplacian carries one chip forward by t along the first slot and one chip
back by t along the second, so it preserves the total depth τ. Proving
that once, for an arbitrary spec, is what keeps the rest of this file short.
The two oneChip readings below are stated with nested conditionals rather
than conjunctive ones on purpose: split_ifs treats a conjunction as a single
atom, so the conjunctive form makes the case split in prin_twoSlotRamp
exponentially larger than it needs to be.
A one-chip divisor at a path position, read at a core vertex: it registers only at the two ends of its own slot.
The same reading at an interior vertex: the chip registers exactly when the slot matches and the depth matches.
A path position at depth 0 is the tail of its slot.
A path position at full depth is the head of its slot.
The cut march, in full generality.
Let the sign vector of a ramp be supported on a finite set A of slots, each
of which has room for the whole window. Then the Laplacian of the ramp is,
slot by slot, sgn e times the move of one chip from path position lo e + t
back to lo e. (So sgn e = +1 pulls a chip backwards and sgn e = -1
pushes it forwards; that is the convention forced by rampSlope.)
A is typically the set of slots crossing a cut of the core, and then the
signs are the coboundary of the side indicator — see cutSgn/rampData_cut.
The regime-1 marches use two-slot cuts (prin_twoSlotRamp below); the
regime-2 banana relay uses the three-slot cut {e0, e6, e7}.
The path positions are taken as arguments constrained by their .val rather
than built from lo and t inside the statement, so that no omega proof
terms get buried in the Fin literals.
The two-slot march.
A ramp whose sign vector is -1 on α, +1 on β and zero elsewhere has a
Laplacian that carries one chip forward by t along α and one chip back by
t along β. The two displacements cancel, so any total depth summed over
the active slots is conserved — which is the whole content of the regime-1
pencil.
This is prin_cutRamp at the two-element set {α, β}.
The four path positions are taken as arguments rather than built from lo and
t inside the statement, so that no proof terms are buried in the Fin
literals and callers can supply whatever positions they already have.
The three-slot march, in the all--1 case.
A ramp whose sign vector is -1 on each of three slots α, β, γ and zero
elsewhere advances one chip by t along each of them. This is the banana
relay of regime 2 (cut {e0,e6,e7}, side {v0,v2,v5}) and the arrival at
v4 (cut {e0,e4,e5}, the star of v4).
This is prin_cutRamp at the three-element set {α, β, γ}.
Three-chip configurations #
Regime 2 moves its chips through five different slot triples, so it is stated
against a divisor of three chips at arbitrary vertices rather than against a
family indexed by a fixed triple of slots (as tauDiv is for regime 1).
Three chips, at arbitrary vertices of a subdivision.
Instances For
Swapping the last two chips of a configuration.
The τ-family and the three regime-1 marches #
Write a₀ = length 0, a₁ = length 3, a₂ = length 8 for the three single
lengths. The τ-family carries one chip on each single slot, at depths
j, k, m measured from v0, v1, v2; the two-slot marches below all preserve
τ = j + k + m, so the whole level set τ = a₀ is one equivalence class.
Every march is a cut march: its potential is t on one side of a two-slot
cut of the necklace and 0 on the other, which makes RampData.potential
automatic.
The sign vector a cut potential forces: ±1 on the slots crossing the
cut, zero on the rest.
Equations
Instances For
A cut potential is always consistent with its own sign vector, so the only thing a cut march has to check is its window.
The τ-family: one chip on each single slot.
Equations
- LowGenus.GenusFourRow096Pencil.tauDiv spec j k m = oneChip (spec.pathVertex 0 j) + oneChip (spec.pathVertex 3 k) + oneChip (spec.pathVertex 8 m)
Instances For
A τ-family member carries a chip at u as soon as one of its three
positions names u.
The regime-1 pencil is the τ-family member T(0, a₀ − a₂, a₂): its two
core chips are the tail of e0 and the head of e8.
All eighteen incidence equalities, as a simp bundle.
March A, across the cut {e0,e8}: the chip on e8 returns to v2
while the chip on e0 advances by a₂.
March B, across the cut {e0,e3}: the chip on e3 returns to v1
while the chip on e0 advances from a₂ to a₀.
Needs a₂ < a₀; when a₂ = a₀ the march is vacuous and march A alone already
lands on the configuration this produces.
March C, across the cut {e3,e8}: the chip on e3 advances to the far
end v3 while the chip on e8 retreats, conserving τ.
Needs a₀ < a₁ + a₂; at the triangle boundary the march is vacuous, and there
the pencil's own middle chip already sits on v3.
The single regime-1 obligation #
bnExists_regime1 is reduced to one statement: that the pencil reaches the
six core vertices. Nothing about interior vertices is needed.
That is the anchor-only route back-ported into
the accompanying analysis from the row-proof-format branch:
the embedded core vertices are a strong separator of any positive
subdivision, so Certificate.CoreVertexReachability.bnExists_of_reaches_coreVertices
upgrades reachability at the core to rank ≥ 1 outright. The capped
reflections that sweep the nine slots are needed only to exhibit the pencil,
not to prove the rank statement — which is what makes this proposal much
smaller than the row-100 file it is modelled on.
Stated against IsNecklace rather than the catalog row so the marches can be
developed for an arbitrary spec.
Every core vertex is reached by the regime-1 pencil.
Route, worked out and checked by hand 2026-08-13. Introduce the
τ-family T(j,k,m) = one chip on each single slot, at distances j, k, m
from v0, v1, v2 (i.e. pathVertex 0 j + pathVertex 3 k + pathVertex 8 m).
Then:
pencil1 = T(0, a₀ − a₂, a₂), becausepathVertex 0 0 = v0(pathVertex_zeroandhn.t0) andpathVertex 8 a₂ = v5(pathVertex_lengthandhn.h8);- the six core vertices are covered by just three members of the level set
j + k + m = a₀:v0,v5:T(0, a₀ − a₂, a₂), the pencil itself;v1,v2,v4:T(a₀, 0, 0)— chips at the head ofe0(= v4, byhn.h0), the tail ofe3(= v1,hn.t3) and the tail ofe8(= v2,hn.t8);v3:T(a₀ − a₁ − m, a₁, m)withm = min a₂ (a₀ − a₁), whose middle chip is at the head ofe3(= v3,hn.h3). The bounds needa₁ ≤ a₀(hmax₁) andm ≤ a₀ − a₁(from themin).
The marches themselves are now proved: march_A, march_B and march_C
above realize exactly the three equivalences this needs. What is left is
purely the coverage bookkeeping — instantiate the marches at the six vertices
and identify the endpoints via pathVertex_zero/pathVertex_length and the
IsNecklace fields — together with the two degenerate cases that the marches
carry as hypotheses:
a₂ = a₀: march B is vacuous, and march A alone already lands onT(a₀, 0, 0), sov1, v2, v4are still covered.a₀ = a₁ + a₂(the triangle boundary): march C is vacuous, but therea₀ − a₂ = a₁, so the pencil's own middle chip already sits onpathVertex 3 a₁ = v3.
Chaining A and B uses prin additivity: the script is scriptA + scriptB and
map_add splits its Laplacian.
Note the interior slots need no attention at all: by the strong-separator route this lemma is the whole obligation.
Regime 2: the banana relay #
Regime 2 is x = a₀ − a₁ − a₂ > 0 in the chart where a₀ is a longest single
and e6 is the longer arc of β₂. Write s = min(x, a₇); the divisor is
D = v0 + v5 + (point on e6 at distance s from v3).
The pencil is a single chain of marches, all of them cut marches with the chip
on e0 advancing, and the sides forming an increasing chain
{v0,v5} ⊂ {v0,v2,v5} ⊂ {v0,v2,v3,v5} ⊂ {v0,v1,v2,v3,v5}
as the two trailing chips walk backwards around the necklace v5 → v2 → v3 → v1 → v4. Crossing the banana β₂ is the "relay": the parked chip on e6
and the arriving chip (now on e7) advance together, which is the
three-slot cut {e0,e6,e7}; crossing β₁ at the end is the three-slot cut
{e0,e4,e5}, i.e. the star of v4. The chain, with the e0 depth in
brackets:
[0] v0 + (e6 at a₆−s) + v5
[a₂] · + (e6 at a₆−s) + v2 (cut {e0,e8})
[a₂+s] · + v3 + (e7 at s) (cut {e0,e6,e7}, the relay)
[a₂+s+a₁] · + (e7 at s) + v1 (cut {e0,e3})
which already covers v0, v1, v2, v3, v5. For v4, put r = x − s. If
r = 0 the last configuration already has its e0 chip at v4. Otherwise
s = a₇, so the chip on e7 is a second chip at v3; one more {e0,e3}
march of length min(a₁, r) either lands the e0 chip on v4 or leaves two
chips at v1, and then the star march at v4 delivers a chip to v4
whichever of its three slots runs out first.
Coverage bookkeeping for configurations, once.
The {e0,e8} march: a chip retreats by t along e8 while a chip
advances by t along e0. A third chip, anywhere, is untouched.
The {e0,e3} march: a chip retreats by t along e3 while a chip
advances by t along e0. A third chip, anywhere, is untouched.
The relay: the three-slot {e0,e6,e7} march. The chip parked on the
long arc e6 and the chip arriving on the short arc e7 advance together
with the chip on e0.
The star march at v4: the three-slot {e0,e4,e5} march, i.e. firing
the complement of v4. Two chips at v1 enter the banana β₁ while the
chip on e0 advances.
Arrival at v4. Whenever the pencil reaches a configuration with two
chips at v1 and one on e0, it reaches v4: either the e0 chip is already
at the head of e0, or the star march at v4 runs for
t = min(a₄, a₅, a₀ − j) steps and whichever of the three slots attains the
minimum delivers its chip to v4.
Every core vertex is reached by the regime-2 pencil.
The chain of marches is the one described in the section docstring; only the six core vertices are needed, by the strong-separator route.
The two regime lemmas #
Both are stated in the rotated chart a₀ = max: hypotheses
length 3 ≤ length 0 and length 8 ≤ length 0.
Regime 1: the three single lengths satisfy the triangle inequality.
D = v0 + v5 + (point on e3 at distance a₀ − a₂ from v1), and the pencil is
the τ = a₀ level family described in the module docstring.
The proof uses RampData marches for the T(j,k,m) equivalences and capScript
reflections at the three banana stations, exactly as in
the public ramp-script infrastructure.
Regime 2: x = a₀ − a₁ − a₂ > 0, and (after the e6/e7 arc swap) the
arc e6 of β₂ is at least as long as e7.
D = v0 + v5 + (point on e6 at distance min(x, length e7) from v3).
Verified empirically on 153/153 regime-2 random vectors
(auxiliary calculations); proved by regime2_reaches_core,
whose chain of cut marches is described in the section docstring above. Only
the six core vertices are needed, by the strong-separator route.
Assembly: rotation and arc-swap case split #
In the chart where slot 0 is a longest single, close the row by the
regime split, swapping the two β₂ arcs first if e6 is the shorter.
Every positive integral subdivision of the necklace core carries a degree-three rank-one divisor.
The proof rotates the maximal single slot into position e0 with the
core-symmetry transport applied
to rotVertex/rotSlot/rotReversed, then
split on the triangle inequality, applying the arc swap swapSlot in
regime 2 if length e6 < length e7.