Multi-code divisors and multi-break slope scripts #
AffinePosition names a single point of a subdivided slot by an affine
offset and decodes it to a typed vertex once the local cone is checked. Two
row-independent constructions are built on top of it here.
A multi-code divisor. A finite family of position codes, each with its own cone-certified bounds, assembles into the sum of the one-chip divisors at the decoded vertices. Its degree is the number of codes (repetitions are allowed and produce multiplicities), it is effective, and its value at a vertex is the number of codes decoding to that vertex. This is the divisor format needed by rows whose pencil is not supported on the core.
A multi-break slope script.
Certificate.SlopeScriptcomputes the Laplacian of a firing script from its unit-step slopes. The scripts used by the genus-four all-length rows have exactly one slope window per slot (rampScript) or one plateau (capScript). Rows without a cut need potentials that bend several times inside one slot. A break list is a list of pairs(start, slope): the slope of the script at unit stepkis the value of the last entry whosestartis at mostk, and0before every entry. The resulting Laplacian is exact:- at a core vertex it is the endpoint-slope sum, as always;
- at an interior vertex it is the jump of the break list there, and in particular it vanishes at every interior vertex which is not a break position.
Finally the breaks themselves are named by affine position codes, so one passive
SlopeScriptdatum describes a whole cone of length vectors.
Nothing here is row specific and nothing here is decidable-by-decide: the
only Boolean checks are the fail-closed bound checks already introduced by
AffinePosition.
Interior decoding #
A strictly interior path position names an interior vertex. This is the
positional form of pathVertex's middle branch.
An affine position code whose normalized coordinate is strictly interior decodes to the interior vertex one step below that coordinate.
Geometry-only certificate carriers #
ExplicitPotential.CertificateData.Valid bundles two unrelated things: the
geometry of the length cone (a loopless core and a cone which forces every
segment to be positive) and the interpolated-script rank-one data
(alpha, beta, potential, and the endpoint inequalities). Only the
geometry is needed to form subdivisionSpec, and hence to decode affine
positions or to run a multi-break script.
A row whose pencil is not an interpolated script therefore should not have to
invent interpolated-script witnesses. carrier packages a core, its segment
forms and a cone with trivial witness data and the all-ones core divisor, and
carrier_valid discharges Valid from the two geometric hypotheses alone.
A certificate carrying only length geometry. Its divisor and witness
fields are placeholders: the real pencil is a MultiCode and the real firing
scripts are multi-break scripts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A geometry-only carrier is valid as soon as its core is loopless and its cone literally contains the positivity row of every segment. No interpolated-script data is required.
Multi-code divisors #
A finite family of affine position codes. Repetitions are allowed and
become chip multiplicities in divisorOf.
The indexed family of affine positions; repeated positions contribute repeated chips to its divisor.
Instances For
Every code of the family has its two bound rows in the local cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Fail-closed executable bounds check for a whole family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The decoded subdivision vertex of one member of the family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The divisor named by a family of affine position codes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The degree of a multi-code divisor is the number of codes.
A multi-code divisor is effective.
A multi-code divisor vanishes at every vertex named by no code.
A multi-code divisor carries exactly one chip at a vertex named by a single code.
A multi-code divisor which reaches every embedded core vertex has rank at
least one. This is the unmarked end-to-end entry point for affine-positioned
pencils: MultiBreakScript supplies the individual Reaches witnesses, and
the public core-vertex strong-separator theorem supplies all remaining
subdivision vertices. No stability hypothesis on the core is needed.
Break lists and their piecewise-constant slopes #
Scan a break list left to right, keeping the value of the last entry
whose start index is at most k. initial is the slope in force before the
list begins.
Equations
- One or more equations did not get rendered due to their size.
- Utilities.Certificate.SubdivisionGraph.Spec.breakSlopeFrom initial [] x✝ = initial
Instances For
The slope named by a break list at unit step k: the value of the last
entry whose start is at most k, and 0 before every entry.
Equations
Instances For
Path values of a multi-break script: the core potential at the tail plus the accumulated break slopes.
Equations
- spec.breakValue potential breaks edge k = potential (spec.core.tail edge) + ∑ j ∈ Finset.range k, Utilities.Certificate.SubdivisionGraph.Spec.breakSlope (breaks edge) j
Instances For
The multi-break firing script.
Equations
- spec.breakScript potential breaks = spec.slotValueScript potential (spec.breakValue potential breaks)
Instances For
The single closing condition on multi-break data: on every slot the total accumulated rise is the core potential difference.
- balance (edge : Fin p) : potential (spec.core.head edge) = potential (spec.core.tail edge) + ∑ j ∈ Finset.range (spec.length edge), breakSlope (breaks edge) j
Instances For
The unit-step slopes of a multi-break script are exactly its break list slopes.
At a core vertex the Laplacian of a multi-break script is the sum of the outgoing break slopes at each incident endpoint.
At an interior vertex the Laplacian of a multi-break script is the jump of its break list at that coordinate.
A multi-break script has trivial Laplacian at every interior vertex which is not a break position. This is the reason for the format: the principal divisor of a multi-break script is supported on the core together with the finitely many named break points.
Affine-positioned multi-break scripts #
A passive multi-break script: an ordered family of affine-positioned breaks. Order matters, exactly as in a break list: a later entry on the same slot overrides an earlier one from its start index onwards.
- entry : Fin b → BreakPoint m p
The ordered break entries; a later entry on the same slot overrides an earlier one from its starting position onward.
Instances For
Every break position of the script has its bound rows in the local cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Fail-closed executable bounds check for a multi-break script.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The concrete per-slot break list obtained by evaluating every affine break position at a length point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every entry of a decoded break list comes from a named break of the script, on the named slot and at its decoded coordinate.
If no break of the script sits on edge at coordinate coordinate, then
the decoded break list has no entry starting there.
The multi-break firing script on the concrete subdivision named by a length point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The closing condition for a multi-break script at one length point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Laplacian of an affine-positioned multi-break script at an interior vertex is the jump of the decoded break list there.
The principal divisor of an affine-positioned multi-break script vanishes
at every interior vertex which no break of the script names. Together with
MultiCode.divisorOf_apply_eq_zero this is the row-independent statement that
lets a residual be checked at the finitely many named positions only.
The Laplacian of an affine-positioned multi-break script at a core vertex is the usual endpoint-slope sum.