Measured while implementing wave 10a of #4984 (PR #5009).
What the freeze says vs what the ratchet charges
The wave 10a freeze comment
(#4984 (comment)) reports, for
its 74-file set:
| metric |
freeze |
measured on the same commit |
| files |
74 |
74 |
| declarations |
168 |
168 |
| charges |
132 |
90 |
The 168 matches exactly. The 132 does not: on main 7ea1cbdd the ratchet's
--findings output for those 74 files has 132 rows, but only 90 of them sit in the
authoritative ledger (32 NARROW_CHILD + 58 RELOCATION). The other 42 are rows printed
under the report's own banner
# TELEMETRY (NON-AUTHORITATIVE): ... These rows are NOT part of the population, are never
# pinned, and no verdict is computed from them.
i.e. purpose-only Narrow child module for <no placeable quantity> headers. Reproduce with
python3 scripts/header_inventory_claim_ratchet.py --findings > f.tsv
TEL=$(grep -n '^# TELEMETRY' f.tsv | cut -d: -f1)
head -n $((TEL-1)) f.tsv | grep -F -f <frozen file list> | wc -l # 90
tail -n +$TEL f.tsv | grep -F -f <frozen file list> | wc -l # 42
The pin movement confirms the 90: the baseline went 453 charges / 362 keys ->
363 / 277 across wave 10a, i.e. -90 charges and -85 keys, with 0 rows of either kind
left on the 74 files.
Why it matters
The two numbers answer different questions and the freeze uses the larger one to size a
wave and to state its result. A wave whose files are mostly purpose-only headers will
report a charge figure well above what the ratchet can actually charge, and the PR body
that quotes it then states a number the --check output contradicts. Wave 9's PR body has
the mirror-image slip in the other direction: it says "68 rows cleared" where 68 is the
key delta (430 -> 362) and the charge delta was 70 (523 -> 453).
None of this affects any merged Lean content or any gate: --check,
--check-baseline-drift and the pin itself are all computed from the ledger alone and are
correct. What is wrong is the freeze/PR-body accounting layer.
Suggested resolution
State three separate figures per wave -- charged rows, telemetry rows, declarations -- and
derive the charged figure the way the ratchet does (rows above the # TELEMETRY banner),
rather than from a whole-file grep of --findings. Waves 10b-16 are not yet frozen with
new numbers, so the correction can be applied going forward; waves 1-9 are merged and their
bodies would need re-derivation from each freeze commit if the record is to be made exact.
Measured while implementing wave 10a of #4984 (PR #5009).
What the freeze says vs what the ratchet charges
The wave 10a freeze comment
(#4984 (comment)) reports, for
its 74-file set:
The 168 matches exactly. The 132 does not: on
main7ea1cbddthe ratchet's--findingsoutput for those 74 files has 132 rows, but only 90 of them sit in theauthoritative ledger (32
NARROW_CHILD+ 58RELOCATION). The other 42 are rows printedunder the report's own banner
i.e. purpose-only
Narrow child module for <no placeable quantity>headers. Reproduce withThe pin movement confirms the 90: the baseline went 453 charges / 362 keys ->
363 / 277 across wave 10a, i.e. -90 charges and -85 keys, with 0 rows of either kind
left on the 74 files.
Why it matters
The two numbers answer different questions and the freeze uses the larger one to size a
wave and to state its result. A wave whose files are mostly purpose-only headers will
report a charge figure well above what the ratchet can actually charge, and the PR body
that quotes it then states a number the
--checkoutput contradicts. Wave 9's PR body hasthe mirror-image slip in the other direction: it says "68 rows cleared" where 68 is the
key delta (430 -> 362) and the charge delta was 70 (523 -> 453).
None of this affects any merged Lean content or any gate:
--check,--check-baseline-driftand the pin itself are all computed from the ledger alone and arecorrect. What is wrong is the freeze/PR-body accounting layer.
Suggested resolution
State three separate figures per wave -- charged rows, telemetry rows, declarations -- and
derive the charged figure the way the ratchet does (rows above the
# TELEMETRYbanner),rather than from a whole-file
grepof--findings. Waves 10b-16 are not yet frozen withnew numbers, so the correction can be applied going forward; waves 1-9 are merged and their
bodies would need re-derivation from each freeze commit if the record is to be made exact.