The W5 endpoint chip bridge #
RichChipDecoder.rawChipMassAt is the physical signed chip mass sitting at
one literal coordinate of a displayed slot: it selects the raw chips of that
slot whose form evaluates to the coordinate. The checker, by contrast,
accounts for chips syntactically: chipPrefix sums the chips whose first
syntactic match among the named points of the anchor is one of the first s
named points.
This module proves that the two agree exactly, at the tail coordinate 0 and
at the head coordinate eval (coordForm e) x. Exactness — rather than a
one-sided bound — is forced: ordinary leaves permit negative chip
coefficients, so a chip landing on an endpoint can make the actual endpoint
contribution smaller, and an inequality in the wrong direction would be
useless to W5.
The reason no geometry is needed is that chipMatches compares forms with
formEq, i.e. syntactically. Arith.eval_eq_of_formEq therefore identifies
a matched chip with its named point at every parameter point, so the two
indicators agree chipwise:
- existence of a first match is W3;
- uniqueness of a first match (among nonzero indices) is the
range (i - 1)clause ofchipMatches; - a matched chip evaluates to
0exactly when its match index lies in the collapsed prefix.
Finally, W1's slack discipline bounds the realized collapse count by the
declared slack, which is what the minOver in tailContribution /
headContribution needs.
Elementary sum plumbing #
The head-side chip sum used by headCandidate, named so that the bridge
can be stated without repeating the fold.
Equations
Instances For
chipPrefix as a single list sum of per-chip first-match indicators.
headChipSum as a single list sum of per-chip first-match indicators.
The chipwise first match #
First-match existence and uniqueness. On an accepted rich leaf every
raw chip has exactly one nonzero named index at which chipMatches fires, and
that index is a genuine interior index of the anchor's block list.
Index 0 is deliberately excluded from the uniqueness clause: point a e 0
is the empty form, so a chip whose form is identically zero also matches
there. The checker never reads index 0 (chipAt returns 0), so this is
exactly the uniqueness statement the accounting needs.
The tail bridge #
The W5 tail chip bridge. The physical signed chip mass at the tail
coordinate of slot e is exactly the checker's first-match prefix sum through
the last collapsed named point.
The two hypotheses say precisely that the named points 1, …, s are the ones
which have fallen into the tail; no other geometric input is used, because
chipMatches identifies a chip with its named point syntactically.
The head bridge #
The W5 head chip bridge, the mirror of rawChipMassAt_zero_eq_chipPrefix
at the far endpoint of the slot. Here s counts the named points which have
fallen into the head, and L is the evaluated slot length.
The interior bridge #
W4's residual is stated against w4ChipSum, the first-match chip total over a
run of named indices. At a forward selector change the run is a maximal
block of named indices sharing one strictly interior coordinate, so the same
chipwise argument as at the endpoints identifies it with the physical chip
mass there. Unlike the endpoint bridges no index 0 case arises, because a
W4 run starts at 1.
w4ChipSum as a single list sum of per-chip first-match indicators.
The W4 interior chip bridge. The physical signed chip mass at a
coordinate carried by exactly the named points i, …, j of the anchor is the
checker's first-match run total.
The three hypotheses say that i … j is the maximal run of named interior
indices at the coordinate; that is what a forward selector change supplies.
Realizing the collapse counts, with W1's slack discipline #
The bridges above take the realized collapse count as a parameter. W1
supplies it: the named points are weakly monotone, so the collapsed ones form
a prefix (resp. a suffix), and the positiveCheck receipts on
point a e (α + 1) and on coordForm e − point a e (k − 1 − ω) bound that
prefix (resp. suffix) by the declared slack. That bound is exactly what
tailContribution_le_candidate / headContribution_le_candidate need.
The realized tail collapse count of an accepted rich leaf, with the tail
bridge and the W1 slack bound. This is the hypothesis-shaped form consumed by
RichW5Aggregation.w5ActualResidual_class_nonneg.
The head-side mirror of exists_tail_collapse.
A zero-length displayed slot carries no raw chips on that slot in an
accepted rich leaf. This is the zero-slot half of the W5 endpoint accounting:
its two physical endpoints are the same quotient-core vertex, so the tail and
head mass must not be added. W1 makes the two maximal collapsed runs exhaust
the named points; its α + ω + 1 ≤ k discipline then forces k = 1, and W3
has no interior named index at which a chip could occur.
Consequently each physical endpoint mass of a zero-length displayed slot is zero. This is the form used when one endpoint contribution is retained and the other is omitted in the quotient-core W5 sum.
The W5 endpoint comparisons #
Composing the bridge with minOver_le_candidate gives the two inequalities
in the shape RichW5Aggregation.w5ActualResidual_class_nonneg consumes, with
the actual endpoint contribution still written as the physical chip mass
plus (resp. minus) the declared slope bound of the first surviving (resp. last
surviving) block. Only the slope comparison — W2's lo ≤ actual ≤ hi on that
block — remains between these and the closed-face endpoint contributions.
W5's conservative tail contribution is dominated by the physical chip mass
at the tail plus the declared lower slope bound of the first block which
survives the collapse. The returned index s is the last named point that
has fallen into the tail.
The head-side mirror of exists_tailContribution_le. Here
(w.blockList a e).length - s is the first named point that has reached the
head, and (w.blockList a e).length - 1 - s indexes the last surviving
block.