claimroutine

Raw certificates independent of physical constants

Raw record certificates use the same a0,b0a_0,b_0 at every budget
prevents growth of constants in the induction
Claim·§11.5 The uniform space theorem·inside thmController interfaces have restoring O(B)-space implementations

Statement (paper)

The raw caller words of Lemma  are certified with the same coefficients a0,b0a_0,b_0 at every budget, where a lower opaque operation contributes its call recipe but none of its internal working states. Lemma  converts a copied raw portion to its physical bound with one fixed pair A,DA,D. Hence the raw certificate does not depend recursively on the already enlarged physical constants, since a lower operation's physical portion is appended but never substituted into an upper raw graph state.

In plain English

The raw caller words from the recipe lemma are certified with the same coefficients a0,b0a_0,b_0 at every budget, because a lower operation adds only its call recipe and not its internal working states. A copied raw portion is converted to its physical bound using one fixed pair A,DA,D, so the raw certificate never depends on the enlarged physical constants.

Why it's here

This claim blocks a circularity in the induction on allowance: if raw bounds absorbed the lower levels' enlarged physical constants, the constants would grow at each level. Combining the recipe bounds of lem-ctrl-recipes with the fixed conversion A,DA,D from lem-ctrl-local-graph, the physical portion of a lower operation is only appended and never substituted into an upper raw graph state, so the constants stay uniform and the O(B)O(B) space bound goes through.
Classified routine:
A bookkeeping step in the induction on allowance that combines the recipe bounds of lem-ctrl-recipes with the fixed conversion constants A, D of lem-ctrl-local-graph. It checks that the constants do not compound across levels, a standard uniformity check for recursive space-bounded simulations.

Uses

lemEstimator recipes have regenerable records and bounded controllemGuarded local graph for terminal recipes

Used by

Nothing in the paper

Sources

PaperOpen
Section
§11.5 The uniform space theorem
Page
—
Label
—
Line
sections/implementation.tex:1228
Leannot aligned

Phase 2 aligns this node to a Lean declaration.