lemmaroutine

Endpoint comparisons are restoring with O(d) control

Endpoint comparison is a restoring test with O(d)O(d) suspended control
address-free endpoint comparison primitive
Lemma·lem:ctrl-equality·§11.4 Certificates for the estimator recipes

Statement (paper)

At slack dd, comparisons of two valid candidate or old-list endpoints are restoring, catalyst-independent tests with O(d)O(d) suspended structural control, in addition to the costs of their lower endpoint visits. They use no saved endpoint address. Their choice between an exact comparison and the designated fingerprint comparison is independent of a surrounding numerical clock.

In plain English

At slack dd, comparing two valid candidate or old-list endpoints is a restoring, catalyst-independent test needing only O(d)O(d) suspended structural control, beyond the cost of the lower endpoint visits. It saves no endpoint address, and whether it uses an exact or the designated fingerprint comparison does not depend on any surrounding numerical clock.

Why it's here

This packages the catalytic fingerprint equality test with the ordered-path bookkeeping into one comparison primitive whose control cost and behavior are fixed at each slack level. The later realization theorem and its inductive construction of total restoring procedures can then call endpoint comparisons as black boxes, without tracking addresses, catalyst contents, or clock-dependent choices.
Classified routine:
Packages the earlier catalytic fingerprint equality test (lem-fp-catalytic) with the ordered restoring path bookkeeping (lem-ctrl-paths) into one comparison primitive. The control-cost accounting is a direct consequence of those two lemmas.

Uses

lemUnbalanced estimator paths have ordered restoring formlemCatalytic equality test for endpoint keys

Used by

thmController interfaces have restoring O(B)-space implementationsclaimInductive construction of total restoring procedures

Sources

PaperOpen
Section
§11.4 Certificates for the estimator recipes
Page
—
Label
lem:ctrl-equality
Line
sections/implementation.tex:711
Leannot aligned

Phase 2 aligns this node to a Lean declaration.