claimroutine

Addresses regenerable from saved choices

Gate and digit addresses are recomputed from root parameters and saved choices
verifies the path-only storage hypothesis for recipes
Claim·§10.6 The numerical interface·inside thmUniform numerical interface for arithmetic recipes

Statement (paper)

All gate, digit and descriptor addresses of the recipe can be regenerated from the root parameters and the saved gate choices by integer arithmetic, scanning the choices from the root, without referring to an ancestor cursor address and without requiring any operand value to determine the next gate. The integers involved have O(B+d+t)O(B+d+t) bits and repeated scans reuse one scratch area, so Lemma  applies at every Boolean portion of the recipe.

In plain English

Every gate, digit and descriptor address in the recipe can be recomputed by integer arithmetic from the root parameters and the saved gate choices, scanning the choices from the root. No ancestor cursor address or operand value is needed to find the next gate, and the integers have O(B+d+t)O(B+d+t) bits with one reused scratch area.

Why it's here

This checks the hypothesis of the depth-first evaluation lemma: addresses come from the path of choices alone, within O(B+d+t)O(B+d+t) scratch. So path-only storage applies to every Boolean portion of the recipe, which is what bounds the suspended record length in the interface theorem.
Classified routine:
Bookkeeping check that the recipe's addresses satisfy the hypothesis of the paper's depth-first evaluation lemma (lem-arith-gate-evaluation). It uses a standard path-from-root regeneration argument, as in Borodin-style depth-first evaluation of bounded fan-in circuits in small space.

Uses

lemDepth-first circuit evaluation uses path-only storage

Used by

Nothing in the paper

Sources

PaperOpen
Section
§10.6 The numerical interface
Page
—
Label
—
Line
sections/arithmetic.tex:830
Leannot aligned

Phase 2 aligns this node to a Lean declaration.