lemmaroutine

Depth-first circuit evaluation uses path-only storage

Depth-first circuit evaluation stores only O(1)O(1) bits per gate on the path
space accounting for all arithmetic primitives
Lemma·lem:arith-gate-evaluation·§10.1 Streams, records, and uniformity

Statement (paper)

Consider a finite Boolean circuit of bounded fan-in, with a specified output gate. Conditional gates may evaluate their selector first and then only their selected branch. Suppose the type and immediate predecessors of a gate, or its operand label and digit place if it is an input gate, can be computed from the root parameters and a path of child choices from the output gate. Suppose these computations use O(B+t+d)O(B+t+d) scratch bits and make no operand or graph queries. Then depth-first evaluation retains O(1)O(1) bits per gate on its current path, and requires no saved absolute gate address per gate. Its suspended record above an operand input has length at most a constant times the length of that path, plus any explicitly retained root-local record.

In plain English

For a bounded fan-in circuit whose gate types, predecessors and input labels and digit places can be computed in O(B+t+d)O(B+t+d) scratch bits from the root parameters and a path of child choices, depth-first evaluation keeps O(1)O(1) bits per gate on the current path and no saved absolute gate addresses. The suspended record above an operand input is at most a constant times the path length, plus any explicitly retained root-local record.

Why it's here

This is the basic space accounting for evaluating arithmetic circuits in the paper: gates are identified by their path of child choices rather than stored addresses, so the stored data is proportional to path length. The later arithmetic lemmas (elementary operations, multiplication, ranks) and the uniform interface theorem rely on it to bound the storage suspended at an operand input.
Classified routine:
This is the standard depth-first evaluation of a bounded fan-in circuit in space proportional to depth, with gates named by their child-choice path, as in Borodin's 1977 simulation of depth-d circuits in O(d) space. Here it is only adapted to the paper's record bookkeeping.

Uses

Nothing else in the paper

Used by

lemElementary arithmetic operations have linear-space residue procedureslemMultiplication with linear clock-gap storagelemOrder statistics have linear-space residue proceduresthmUniform numerical interface for arithmetic recipesclaimClock gap pays band path lengthclaimAddresses regenerable from saved choices

Sources

PaperOpen
Section
§10.1 Streams, records, and uniformity
Page
—
Label
lem:arith-gate-evaluation
Line
sections/arithmetic.tex:123
Leannot aligned

Phase 2 aligns this node to a Lean declaration.