claimroutineinferred_dep

Many heavy entries close all gates

With ≥ KK heavy true entries, all gates close in both calculations
heavy-entry case of relative stability
Claim·§8.3 Deterministic comparison arguments·inside lemRelative stability at first overflow

Statement (paper)

Let GG be larger than every gate close threshold and L0L_0 much larger than GG, all sensitivity thresholds, and 11. If at least KK true first entries exceed L0L_0, then all gates are closed, both in the reference calculation and in the perturbed calculation.

In plain English

Take GG larger than every gate close threshold and L0L_0 much larger than GG, all sensitivity thresholds, and 11. If at least KK true first entries exceed L0L_0, then every gate is closed in both the reference calculation and the perturbed calculation.

Why it's here

This handles the heavy-entry case in the proof of the relative stability lemma. With many large true first entries, the gates are shut in both calculations, so the two computations agree in gate state and need no finer comparison. The small relative prefix errors from the reduction claim keep the perturbed entries comparable to the true ones, so the perturbed calculation also sees them as heavy, and the bound does not depend on how large the largest true first entry is.
Classified routine:
A direct threshold comparison inside the relative stability proof. Once the earlier reduction claim makes the relative prefix errors small, the perturbed entries stay comparable to the true ones, and the gate close thresholds then force every gate shut in both calculations.

Uses

claimReduction to small relative prefix errors

Used by

Nothing in the paper

Sources

PaperOpen
Section
§8.3 Deterministic comparison arguments
Page
—
Label
—
Line
sections/compression.tex:328
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Many heavy true entries close all gates" rests on claim-lem-buf-relative-stability-1