The chip-free three-chain, generic in the core #
This file states one local picture and proves its residual-effectivity statements once, generically in the core.
The picture. A chip-free path v₁ — v₂ — v₃ of three core vertices, with
two chip leaves c₁, c₂ hanging off v₁, one chip leaf c₃ off v₂, and one
chip leaf c₄ off v₃. The six displayed slots are all the slots incident to
v₁, v₂, v₃, and c₁, c₂, c₃, c₄ carry the whole degree-four divisor.
This is not one of Atanasov--Ranganathan's eleven configurations. It is
the natural extension of their configuration 3 -- their "Third" local picture,
a chip-free edge with two chip leaves at each end -- from a chip-free path of
length one to one of length two. Proposition 5.1 of
Atanasov--Ranganathan does not list it, and they never need it: on the row-03
family (Figure 8, scope 3) they avoid it by placing two of the four chips at
interior points of edges, at length-dependent positions
(a = |B5-A5| along B3-A3, and z = min(b, c) along 41-43). A divisor
supported on core vertices cannot follow that route, and on row 03 no
core-supported degree-four divisor is covered by configurations 2, 3 and 5
alone; the chip-free set is always a path of three or four vertices. Hence
this file.
The two profiles. A chip must be delivered to each of v₁ and v₂ (on
row 03 the third chain vertex is the middle vertex of the mirrored picture, so
v₃ is never a centre). Write m = min |c₁v₁| |c₂v₁| for the shorter of the
two leaves at v₁, and put the two lower chips c₃, c₄ at height 0, the
ambient level -- v₃, c₁, c₂ and everything off the picture -- at height
base.
End centre (v₁), endCenter_*:
base = min |v₃c₄| |v₂c₃|
mid = min |v₂v₃| (min (|v₂c₃| - base) m)
top = min |v₁v₂| (m - mid)
height v₃ = base, height v₂ = base + mid, height v₁ = base + mid + top
Middle centre (v₂), midCenter_*:
base = min |v₃c₄| |v₂c₃|
low = min m (min |v₂v₃| (|v₂c₃| - base))
high = min |v₁v₂| (min (|v₂v₃| - low) (|v₂c₃| - base - low))
height v₃ = base, height v₁ = base + low, height v₂ = base + low + high
Both are nested minima of slot lengths, so every height collapses along with
any slot it spans: the same script therefore works verbatim on every nonloopy
forest face, exactly as in ConfigurationFive.
The shift. When |v₂v₃| collapses, v₂ and v₃ become one class, and
the single incoming chip may sit at either end of that class depending on
whether base is attained at |v₃c₄| or at |v₂c₃|. The row's chip
bookkeeping therefore carries one extra conditional transfer, v₃ ⟶ v₂ guarded
by |v₂v₃| = 0 ∧ |v₃c₄| < |v₂c₃|; it appears below as the parameter shift.
With it in place each profile needs a two-branch target owner, not three.
Everything here is stated against an orientation-agnostic ChainLedger, so a
row instantiates each statement in whichever direction its core happens to
orient the two slots whose direction varies (v₁c₁ and v₂v₃ on row 03).
The one-edge arithmetic itself is ConfigurationFive's and is reused
unchanged.
The orientation ledger #
tail L hu hv is the contribution at the end carrying height hu, head
the contribution at the end carrying hv. A row picks forward when the
picture's first end is the core tail of the slot and reverse when it is the
core head.
Contributions at both ends of a chain slot, with the bounds needed to orient each row.
The tail contribution along a chain slot, parameterized by length and endpoint heights.
The head contribution along a chain slot, parameterized by length and endpoint heights.
Instances For
A full slot delivers a chip at its lower end, and a collapsed slot has already delivered the chip by contraction.
A chip leaf gives away at most the one chip it carries.
The slot read from its core tail.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The same slot read from its core head.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The arithmetic of the nested minima #
Everything the four residual statements need about a profile is one bundle of
inequalities and "which argument is attained" disjunctions, proved once. Each
consumer then clears the two nested minimum equations and works with plain
naturals, so no omega below re-derives a three-way minimum. The two single
minima m = min la lb and b = min u s are left in place on purpose: omega
handles one min cheaply, and several branches want to split on it directly.
This is the shape ConfigurationChippedTriangle.bounds,
ConfigurationReservoirChain.bounds and ConfigurationReservoirPair.bounds
already use; this file was the one picture in the family still expanding its
minima at every call, and it was the most expensive module on the library's
critical path because of it (measured 7.7 s, of which the profiler
attributed 9.8 s of CPU to omega across twenty-one calls; 4.2 s after).
Both bundles are private: they are an internal convenience, and every
exported statement in this file is unchanged.
The chip leaves #
All four chip leaves obey the same one-line bound, whichever way the slot is oriented and whatever the ambient height at the far end.
Residual effectivity at a chip leaf of the picture.
The same bound for a leaf whose slot always points away from the chain.
The far chain vertex #
v₃ is shared by both profiles: it always sits at base, gives away at most
one chip along the middle slot v₂v₃, and is refilled by its own leaf c₄
whenever it does.
Residual effectivity at the far chain vertex v₃.
The end-centre profile #
o is the height at v₁, i at v₂, and the three nested minima saturate
outward from v₃.
Residual effectivity at v₁, the centre of the end-centre profile.
Residual effectivity at v₂ in the end-centre profile.
The middle-centre profile #
The same picture read at v₂: v₁ now drains towards v₂, and the nested
minima saturate in the opposite order.
Residual effectivity at v₁ in the middle-centre profile.
Residual effectivity at v₂, the centre of the middle-centre profile.