Discharging OrdinaryAlong: the longest ordinary run and the next stop #
OrdinaryAlong is false for a general remaining suffix: a later block all
of whose earlier vertices have already been consumed is fed by slot zero.
This module provides the decomposition that the alternating trace needs:
every remaining list splits as the longest ordinary run followed either by
nothing or by a slot-zero-fed head.
The sparse predecessor slot depends only on the processed schedule prefix,
never on the named kernels. The run is therefore a purely combinatorial
takeWhile-style recursion on the remaining list with an evolving
processed accumulator. Its specifications discharge OrdinaryAlong both
for complete certified analytic traces (when the run covers the whole
remaining list) and for certified stop-before-step traces that stop at the
run boundary. The phased one-head transport then iterates exactly up to
the next slot-zero-fed head, at arbitrary Fourier-evaluated endpoints, and
the packaged next-stop data exposes the boundary head with its literal
slot-zero certificate for the exceptional collapse.
The predecessor slot is a function of the processed prefix #
The sparse predecessor slot reads only the active carrier, hence only the processed schedule prefix; the named kernels are irrelevant.
The predecessor slot of a head over a bare processed prefix.
Equations
- Anderson4D.r324WithinHalfListPredecessorSlot processed step = Anderson4D.r324WithinHalfPredecessorSlot { processed := processed, edges := fun (x : Fin (m + 1)) => Anderson4D.greenFn } step
Instances For
Any state computes its predecessor slots through its processed list.
The longest ordinary run #
Length of the longest prefix of the remaining list along which every
head, read at its own evolved processed prefix, has a nonzero predecessor
slot. The recursion consumes one head at a time, appending it to the
processed accumulator exactly as absorb does.
Equations
- One or more equations did not get rendered due to their size.
- Anderson4D.r324WithinHalfOrdinaryRunLength x✝ [] = 0
Instances For
Ordinariness inside the run. Every head whose position lies strictly inside the ordinary run has a nonzero predecessor slot at its own evolved processed prefix.
The head after the run is fed by slot zero. When the run does not exhaust the list, the first head past the run has predecessor slot zero at the processed prefix extended by the whole run.
Processed prefixes are determined by remaining suffixes #
Two residual prefixes of the same schedule with nested remaining lists differ by an explicit consumed middle segment, appended to the processed prefix.
Discharge for complete certified analytic traces #
All-ordinary discharge. If the ordinary run covers the whole remaining list, every certified analytic trace from that residual prefix is ordinary along all of its heads.
Ordinariness along a stop-before-step trace #
Every head genuinely consumed by a stop-before-step trace has a nonzero sparse predecessor slot. The retained stop step itself is not constrained.
Equations
- One or more equations did not get rendered due to their size.
- (Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stop res scale hremaining certificate).OrdinaryAlong = True
Instances For
The retained named suffix is a suffix of every remaining list met by the trace, in particular of the starting one.
Ordinariness along a stop-before-step trace follows from the purely combinatorial statement for every strictly pre-stop head: the retained named suffix must still lie inside the tail.
Run discharge for stop traces. A stop-before-step trace whose consumed prefix lies inside the ordinary run is ordinary along every consumed head.
Phased transport up to the stop #
Integrability transport to the stop. Full integrability of the phased density at the root of an ordinary stop-before-step trace transports to the stopping prefix, at arbitrary endpoints.
Phased recursion to the stop. Along an ordinary stop-before-step trace, the weighted incoming phased residual integral transports exactly to the stopping prefix: the perturbative power drops to twice the retained remaining order and the density becomes the stop phased density with the same coefficient, phase mode, and endpoints.
The exceptional entry at an arbitrary slot-zero-fed head #
The proved exceptional collapse machinery is anchored at the refined
physical root. The two identities below are its endpoint-agnostic core at
an arbitrary residual prefix: the transported outgoing Fourier mode of a
slot-zero-fed head re-anchors the phase at the post-head anchor with one
paper second-order decay, and the phased density splits pointwise into
the head character, the translated erased raw local core, and the
coefficient with the ordinary outer factor. Both hold at every pair of
Fourier-evaluated endpoints, in particular at the endpoint 0 produced
by the first exceptional collapse.
The transported outgoing mode of a slot-zero-fed head at an arbitrary residual prefix: one paper second-order decay times the incoming character read at the post-head phase anchor. Generalizes the root-anchored assembly identity to every stop of the alternating trace.
Consumer form of the re-anchoring identity at an arbitrary slot-zero-fed head: together with the decay extracted by the incoming Fourier evaluation, the collapse leaves a squared second-order decay and the phase re-anchored after the head.
Pointwise exceptional entry for the phased density. At a slot-zero-fed head the incoming phased density splits across the head/post equivalence into the character read at the first head coordinate, the translated erased raw local core, and the coefficient carrying the ordinary head outer factor.
The next exceptional stop of a residual prefix #
The certified decomposition of a remaining list at its next slot-zero-fed head: the longest ordinary run is consumed by a certified stop-before-step trace, ordinary along every consumed head, and the retained named step is the first head past the run.
- pre : List (R322ExtractionStep m)
- terminal : R322ExtractionStep m
- suffix : List (R322ExtractionStep m)
- trace : R324WithinHalfStopBeforeStepTrace self.terminal self.suffix res scale
- ordinary : self.trace.OrdinaryAlong
Instances For
The stopping state has consumed exactly the recorded ordinary run.
The retained head is genuinely exceptional: at the stopping state its sparse predecessor slot is literally zero.
Re-anchoring identity read at the packaged next stop: the transported outgoing mode of the retained head collapses to a squared second-order decay and the phase re-anchored after the head, at arbitrary endpoints.
Pointwise exceptional entry of the phased density at the packaged next stop.
Existence of the next exceptional stop. Whenever the ordinary run does not exhaust the remaining list, the local block provider builds the certified stop-before-step trace to the run boundary, ordinary along every consumed head.
The alternative. Every residual prefix either is ordinary along its whole remaining list, or admits a certified next exceptional stop.
Discharge at the proved exceptional stop assembly #
The OrdinaryAlong hypothesis of the proved phased endgame
theorems holds whenever the ordinary run of the after-head residual
covers the whole retained suffix. When it does not, the after-head
residual instead admits a certified next exceptional stop by
nonempty_r324WithinHalfNextExceptionalStop_of_lt_length.