lemmaroutine

Immediate candidates are short and well-formed

Immediate candidates have O(d)O(d)-bit descriptions, correct sums, budgets ≤ M−dM-d
structural facts about candidates for the path lemmas
Lemma·lem:est-paths·§7.5 The additive schedule

Statement (paper)

At a row group of slack dd, immediate candidates have descriptions of O(d)O(d) bits. With exact endpoint grouping their sums equal the specified conditional-walk increments. A product visits its midpoint by a paired correction move before using any factor at that midpoint. Its right-hand task tuple does not depend on the discarded old source. Every child estimator in such a candidate has budget at most M−dM-d.

In plain English

At a row group of slack dd, immediate candidates have O(d)O(d)-bit descriptions, and with exact endpoint grouping their sums equal the specified conditional-walk increments. A product visits its midpoint by a paired correction move before any factor at that midpoint is used, its right-hand task tuple does not depend on the discarded old source, and every child estimator has budget at most M−dM-d.

Why it's here

This lemma collects the structural facts about immediate candidates in the additive schedule that the control-path and recipe lemmas need, namely bounded description length, correct sums, correct midpoint ordering, independence from the discarded source and the budget drop. It builds on the bounded-degree ports and validated walk variants, which keep the candidate rows small and make the grouped sums match the intended increments.
Classified routine:
A bookkeeping lemma that collects structural properties of the paper's own additive-schedule candidates (description length, correct sums, midpoint ordering, budget drop). These follow directly from the earlier walk-variant and atom-port lemmas by a standard verification.

Uses

lemWalk variants avoid storing endpointslemAtom ports: bounded rows with smooth witnesses

Used by

lemUnbalanced estimator paths have ordered restoring formlemEstimator recipes have regenerable records and bounded controllemControl records replay with later-salt independenceclaimImmediate paths and factor values certifiedclaimEstimator edges determine descendant tuples

Sources

PaperOpen
Section
§7.5 The additive schedule
Page
—
Label
lem:est-paths
Line
sections/estimation.tex:482
Leannot aligned

Phase 2 aligns this node to a Lean declaration.