claimroutine
Structural leaves and buffered tests use fixed precision
Structural leaves and buffered tests use fixed precision, independent of output clock
handles discrete decisions in the recipe class
Statement (paper)
Structural validity branches are finite branches of the circuit organization, with length at most the full intrinsic bound, and they request the structural operand at clock zero. Buffered tests are separate recipes with structural starting clock zero and precision fixed by Lemma , and this precision is not altered when a surrounding value is requested more accurately. Hence no discontinuous comparison of exact reals at unbounded precision is part of the interface.
In plain English
Structural validity branches are finite branches of the circuit organization, of length at most the full intrinsic bound, and they request the structural operand at clock zero. Buffered tests are separate recipes that start at structural clock zero, with precision fixed by the buffered-test lemma and unchanged when a surrounding value is requested more accurately, so the interface never needs a discontinuous comparison of exact reals at unbounded precision.
Why it's here
This claim covers the discrete decisions in the theorem's recipe class, showing they obey the digit and record-length bounds without depending on the output clock . It relies on the buffered comparison test, which decides at fixed precision, so the clock-dependent bounds apply only to the continuous arithmetic parts.
Classified routine:
Direct bookkeeping consequence of the buffered comparison test (lem-arith-buffered-test) and the circuit organization's structural bounds. It checks that the discrete branches use fixed precision independent of the output clock.
Uses
Used by
Nothing in the paper
Sources
PaperOpen
- Section
- §10.6 The numerical interface
- Page
- —
- Label
—- Line
sections/arithmetic.tex:821
Leannot aligned
Phase 2 aligns this node to a Lean declaration.