Ramp (cut-march) scripts on the CLOSED length orthant #
This is the DegSpec counterpart of the Ramp section of
MarkedGraphs/GenusFourCore100.lean, which is stated over
SubdivisionGraph.Spec and is therefore available only on the interior of the
length orthant. Nothing in GenusFourCore100 is touched; these are separate
statements about DegSpec.graph, so the strictly positive path keeps working
verbatim.
What a ramp is #
A ramp moves a chip across a cut of the core. It is the firing script whose
value at path position k of slot e is
pot (tail e) + sgn e * min (k - lo e) t ,
i.e. the script is flat until path position lo e, then rises with slope
sgn e ∈ {-1, 0, 1} for t unit steps, then is flat again. RampData
records the two consistency conditions: the core potential must actually
change by sgn e * t across each slot, and the rising window must fit inside
the slot (unless the slot is flat).
The one new field: repInv #
On the open orthant a ramp needs only potential and window. On the closed
orthant the script is a function on the contracted graph, where a vanishing
slot has already identified its two endpoints, so the core potential must be
constant on each rep-class. That is the third field repInv.
It is not an extra assumption in practice. potential and window together
already force pot (head e) = pot (tail e) on every vanishing slot: a
vanishing slot has lo e + t ≤ 0 or sgn e = 0, and either way sgn e * t = 0
(RampData.pot_head_eq_tail_of_zero). So as soon as rep is generated by
the vanishing slots — which is exactly DegenerateCoreVertexCut.DegSpec .RepIsContraction, and is true by construction for RowProof.censusSpec,
whose rep is a compFold — repInv follows; see RampData.of_reachIn.
Why this is stated generically #
Both catalog row 100 and catalog row 097 march across cuts of a six-vertex,
nine-slot core, and row 097's open proof imports row 100's solely to reuse the
open RampData. Stating the closed analogue here, on an arbitrary
DegSpec n p, means the two closed ports share it rather than each growing a
copy.
The data #
Consistency of the ramp data with the core potential, on the closed
orthant. The first two fields are the open-orthant conditions verbatim; see
the module docstring for repInv.
The core potential is constant on each contracted class.
Instances For
The ramp firing script.
Equations
- d.rampScript pot sgn lo t = d.slotValueScript pot (d.rampValue pot sgn lo t)
Instances For
A vanishing slot carries no potential difference: its window has collapsed
(lo + t ≤ 0) or its slope is zero, and either way sgn e * t = 0.
The potential is constant along any chain of vanishing slots.
repInv for free. If rep-equality is witnessed by a chain of
vanishing slots — DegenerateCoreVertexCut.DegSpec.RepIsContraction, which
holds definitionally whenever rep is a compFold of the vanishing set, as
it is for RowProof.censusSpec — then the two open-orthant conditions already
build a closed-orthant RampData.
Compatibility and the step slopes #
The Laplacian of a ramp #
At a contracted core class the Laplacian of a ramp is the endpoint sum over
all slots of the uncontracted core, vanishing slots included; this is
DegSpec.prin_coreVertex_eq_endpointSum specialised to a ramp.
The form a row proof reads. The Laplacian of a ramp at a contracted
class is the sum, over the members of the class, of the uncontracted
per-core-vertex endpoint formula — the same expression the open-orthant
prin_ramp_coreVertex produces on a SubdivisionGraph.Spec. A row therefore
proves its per-core-vertex value lemmas once and reads every face off by
summing.
Endpoint slopes #
The two lemmas that read the slope at the two ends of a slot. Unlike the open
orthant these must survive length e = 0, where length e - 1 is 0 rather
than the last step; both statements are still true there, and the proofs no
longer need length_pos.
Agreement with the open orthant #
At a strictly positive length vector rep is the identity, so repInv is
vacuous and RampData is exactly the open-orthant structure of
GenusFourCore100.RampData read on DegSpec.toSpec.
On the interior the class sum of prin_ramp_coreVertex_classSum collapses
to a single term, giving literally the open-orthant formula.
Pointwise bookkeeping on the degenerate subdivision #
Everything below is the closed-orthant replacement for the "divisor_ext plus
oneChip at a path position" bookkeeping of GenusFourCore100.lean. The one
structural change is that a value at a core class is the class sum of the
uncontracted per-core-vertex value; that is stated once here, and a row then
never has to mention classes again.
One chip, read at a class and at an interior vertex #
The per-core-vertex indicator of a chip at path position k of slot e.
The uncontracted formula: the value at a contracted class is its class sum,
by one_chip_pathVertex_coreVertex. Written as a nested if rather than a
sum of two indicators because on the closed orthant k = 0 and
k = length e can coincide.
Equations
Instances For
The divisor of a ramp #
prin_ramp_eq is the closed-orthant replacement for the per-march
prin_*_eq divisor identities a row proves on the open orthant. It is stated
once, generically, and in the slot-indexed form: a ramp lifts one chip from
path position lo e + t back to lo e on every slot, weighted by sgn e. A
row instantiates it and expands the nine-term sum, rather than reproving the
identity per march.
The divisor of a ramp, on the closed orthant. Every slot contributes
sgn e chips moved from path position lo e + t back to lo e; slots with
sgn e = 0 contribute nothing, which is why the clamped positions are
harmless.