The row-authoring layer over a marked script #
GenusFiveRow05 proved AR's sixth family by hand: it named the two marked
slots, built the potential, checked MarksAdmissible, read each slot as one or
two ordinary arms, and closed the residual. All of that except the tables is
independent of the row and of which slots carry a mark, and AR's seventh family
(row 08) needs it three times over -- once per chamber, with a different pair
of marked slots each time. This file is that layer, stated once.
The whole interface is driven by a single function mark : Fin 12 → ℕ. There
is no separate "is this slot marked" flag, because
the mark value can be defined uniformly,
markValue e = if 0 < mark e then 0 else potential (tail e)-- a marked slot whose mark has slid back to the tail carries height zero there anyway; andthe two endpoint readings can be too,
tail e = if 0 < mark e then tailContribution (mark e) hu 0 else tailContribution (length e) hu hv head e = if 0 < mark e then (if mark e < length e then headContribution (length e - mark e) 0 hv else headContribution (length e) hu hv) else headContribution (length e) hu hvwhich specialize to
ConfigurationCommon's single-ramp ledger on every slot withmark e = 0. So a chamber marks the one or two slots it needs and says nothing at all about the other ten.
What a chamber supplies is a Profile: the mark is inside its slot, the height
at each end of a marked slot is bounded by that end's half, one of those two
heights vanishes (the chip sits where a flat stretch meets a full ramp), and
the height is constant across collapsed slots. Those five facts give
MarksAdmissible, the ledger reading of every slot, and the hypotheses of
prin_splitScript_interiorVertex_ge_neg_one at the mark -- so the interior chip
costs a chamber nothing beyond declaring its profile.
The script of a height profile #
The potential of a height profile, read at the canonical class representative so that class invariance is definitional.
Equations
- AtanasovRanganathan.ConfigurationMarkedRow.heightPotential d h v = -↑(h (d.rep v))
Instances For
The script's value at each mark. Zero on a genuinely marked slot -- the chip sits at the ambient level -- and the tail's own value on an unmarked one, which is what makes the unmarked slot literally the old single ramp.
Equations
- AtanasovRanganathan.ConfigurationMarkedRow.markValue d mark h e = if 0 < mark e then 0 else AtanasovRanganathan.ConfigurationMarkedRow.heightPotential d h (d.core.tail e)
Instances For
The marked firing script of a height profile.
Equations
- One or more equations did not get rendered due to their size.
Instances For
What a chamber has to say about its height profile. Everything else in this file follows from these five facts.
Each mark lies inside its slot.
The near half of a marked slot is long enough for its rise.
The far half of a marked slot is long enough for its rise.
The chip sits where a flat stretch meets a full ramp.
The profile is constant across a collapsed slot, hence on every contracted class.
Instances For
Class constancy #
Admissibility #
Each slot as one or two ordinary arms #
The tail contribution of a slot, splitting at an interior mark when one is present.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The head contribution of a slot, using the arm beyond an interior mark when it exists.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Specializations a chamber actually uses #
At a marked slot one of the two end heights vanishes. Which one it is decides
which of the two halves the chamber reads as an arm, and these four lemmas name
the four readings so that a chamber never unfolds slotTailForm by hand.
The tail end of a slot whose tail height vanishes.
The head end of a slot whose head height vanishes. The extra hypothesis is free at a marked slot: a mark sitting at the tail carries the tail's height, which is then zero as well.
The near half of a marked slot, read as an arm from the tail.
The far half of a marked slot, read as an arm from the head.
The endpoint ledger of a chamber. Every slot, marked or not, reads as one or two ordinary arms; a chamber expands this sum against its own core.
From per-vertex coefficients to the residual #
The hypotheses of the kink lemma, at a mark strictly inside its slot.
The local Dhar move of a chamber. The divisor is abstract; a chamber supplies its value on core classes, its nonnegativity at interior vertices, and the one chip it keeps at each mark.
Divisors with one or two chips inside a slot #
A chamber's divisor is a core-class weight plus one chip at each marked slot's
mark. These wrappers supply the four facts residual_effective asks for.
A core-class weight plus chips at the marks of two slots.
Equations
- AtanasovRanganathan.ConfigurationMarkedRow.markedDivisorTwo d W mark e f = d.coreClassDivisor W + oneChip (d.pathAt e (mark e)) + oneChip (d.pathAt f (mark f))
Instances For
A core-class weight plus a chip at the mark of one slot.
Equations
- AtanasovRanganathan.ConfigurationMarkedRow.markedDivisorOne d W mark e = d.coreClassDivisor W + oneChip (d.pathAt e (mark e))
Instances For
The core-class weight of a two-mark divisor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The core-class weight of a one-mark divisor.
Equations
- AtanasovRanganathan.ConfigurationMarkedRow.baseOne d W mark e v = W v + AtanasovRanganathan.ConfigurationMarkedThree.markChipWeight d mark e v
Instances For
The chip a two-mark divisor keeps at each mark. hsupp says the mark
function is supported on the two named slots, which is how a chamber declares
which slots it marks.