Task
Round 8 of the ratio_bound_bundle cluster deletion campaign under the user's standing authorization (#4639).
Context
Deletion methodology
Implementation constraints
- Process discipline (MANDATORY):
- ≤3 concurrent Lean procs (serialized builds with warm cache reuse)
- NO
busy-wait / tight polling for build completion
- Self-spawned worker cleanup after each phase
- NO foreign process interference
- Build-system verification:
lake build warning-free
scripts/audit_gate.py V1-V4 + --self-test pass
dead_candidate_scan.py --self-test pass
lake exe GKSTest pass
- CI green before merge
Linked PR
Status
OPEN
Task
Round 8 of the
ratio_bound_bundlecluster deletion campaign under the user's standing authorization (#4639).Context
ratio_bound_bundlecontains 28 total declarations (identified in.self-local/reports/remaining-safe-clusters-2026-07-22.md)log_partitionFunction/partitionFunctionstems (~5-12 declarations, single Lee-Yang-sized batch)Deletion methodology
scripts/dead_candidate_scan.py(textual +--leancross-check) per Fix dead-sweep candidate extraction to require internal-dependency + docs/tex citation checks (10/22 false positives found in Profile.lean audit) #4639 patternsafe-to-deleteby scanner⟨a,b⟩(survive after deletion)Implementation constraints
busy-wait/ tight polling for build completionlake buildwarning-freescripts/audit_gate.pyV1-V4 +--self-testpassdead_candidate_scan.py --self-testpasslake exe GKSTestpassLinked PR
Status
OPEN