claimroutineinferred_dep

Order of constant choices is consistent

Constants are chosen in a fixed non-circular order
checks that the constant choices are consistent
Claim·§9.5 Closing the coupled induction·inside propActual runs stay close to clean runs

Statement (paper)

The fixed constants can be chosen in the following order: first the analytical hierarchy, table thresholds and trivial-case bound; then the precision and cutoff constants for the mean comparisons; then the compression floors, capacities and walk lengths; then the clamping ranges and the crude exponents in the fixed-variant comparisons. These choices determine CC, and only afterwards are D2,D1,ϵD_2,D_1,\epsilon chosen, so that reducing ϵ\epsilon to obtain the direct collision gain does not alter any earlier clean-coefficient requirement. Later choices of the common stage-size bound, top-budget coefficient, environment-field exponent and fixed identifier-length coefficient do not change CC, and can be absorbed after D2,D1,ϵD_2,D_1,\epsilon have been fixed.

In plain English

The fixed constants can be selected in a definite order, with the analytical hierarchy and thresholds first and D2,D1,ϵD_2, D_1, \epsilon last, and later parameter choices do not change CC, so no choice circularly depends on a later one.

Why it's here

This closes the coupled induction for the proposition by showing the constants are not circular. CC is fixed by the earlier clean-coefficient requirements, and then D2,D1,ϵD_2, D_1, \epsilon are chosen to close the recurrence, so shrinking ϵ\epsilon to get the direct collision gain leaves earlier requirements intact. The later choices of stage-size bound, top-budget coefficient, environment-field exponent and identifier-length coefficient leave CC unchanged and can be absorbed afterwards, which keeps the hash collision bound valid.
Classified routine:
Bookkeeping that checks the dependency order of the constants so the earlier choices are not circular. It follows directly from the constant choices in claim-prop-fp-coupling-3 and the hash lemma lem-fp-hash.

Uses

lemPairwise-collision hash from few random bitsclaimConstants chosen to close coupling recurrence

Used by

Nothing in the paper

Sources

PaperOpen
Section
§9.5 Closing the coupled induction
Page
—
Label
—
Line
sections/fingerprints.tex:703
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Order of constant choices is consistent" rests on claim-prop-fp-coupling-3