docs(mirror): record #4746 Item A batch 4 (#4754) and correct the stale Concrete directory size - #4755
Merged
Merged
Conversation
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…le Concrete directory size Adds the batch-4 record to the local mirror of issue #4746: 9 modules / 31 declarations / 712 lines deleted, the same-commit docs/index.md and tex/proof-guide.tex retraction, the two-sweep condition (v) result (7 verdict moves, all protective, 0 violations), and every gate re-measured on the merged main ee98192. Also corrects one figure the mirror carried in its F1 note: the largest library directory is Concrete 851, not 869. 869 predated PR #4751's ten-module deletion (859 at fd7a2a7). The same stale figure was fixed in scripts/test_audit_gate.py inside PR #4754. Adds an F1 update for batch 4: the floors were not lowered, so the measured slack is 27 / 27 / 37 and the F1 decision stays due before batch 5. Remaining scope re-derived on the merged main: 23 modules left on the tier-2 tracked list; freshly measured population 199 fully dead raw / 194 excluding Lemma_17_5_2 / 146 lane-eligible. .self-local/ only; no library, docs, tex or script change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of #4746.
Syncs
.self-local/issues/4746.mdwith the merged state of Item A batch 4 (PR #4754,main
ee981926) and repairs one stale figure the mirror carried.same-commit
docs/index.md+tex/proof-guide.texretraction (four re-measuredwrapper counts, the nested-brace label split, the one family label that lost all its
members, 12 in-library doc comments), the two-sweep condition (v) result (7 verdict
moves, all protective, 0 violations), and every gate re-measured on the merged
main.
to the measured slack 27 / 27 / 37, and the F1 note's
Concrete, 869figure iscorrected to 851 — 869 predated PR refactor: delete 10 zero-consumer Mayer/vd-polymer wrapper modules (safe-to-delete batch 3) #4751's ten-module deletion (859 at
fd7a2a71). The same stale figure was fixed inscripts/test_audit_gate.pyinsiderefactor: delete 9 zero-consumer partition/free-energy, magnetization/Mayer and J = 0 pseudo-mass wrapper modules (safe-to-delete batch 4) #4754.
list; freshly measured population 199 fully dead raw / 194 excluding
Lemma_17_5_2/146 lane-eligible (157 before: 9 deleted here plus 2 that left the set because
this PR's documentation retraction protected their declarations).
of Item A.
.self-local/only; no library, docs, tex or script change.🤖 Generated with Claude Code