[pinterbanget]

Summary

This adds one navigation file, docs/research/pr4100-audit-coverage-map.md. It maps each obligation row of #4100's AUDIT.md (Cinna Davis's proposed unconditional construction) to the open audits that address it. Each entry gives the exact PR head, the outcome that PR reports, and what remains.

Current priorities say a short session can produce "an acceptance coverage map" for the #4100 audit. About 40 PRs and discussion threads now audit pieces of #4100, and none indexes them, so the next auditor can't easily see what is done.

Claim type: consolidation / navigation. No new κ, no scientific acceptance. No package was replayed and no proof rechecked. Outcomes are as each PR reports them. Priorities, the catalogue, the family record and the selected record are unchanged.

What the map shows

• Audited with a positive scoped result: CRT §1–§4 (Bind declared-width CRT shared rows to the complete padded caller #4195, Audit uniform Beneš compiler with charged sequential arena scans #4192, Audit CRT reservoir placement and split-axis coordinate descriptors #4174, Audit PR4100 arbitrary-source CRT repair with an explicit inverse #4169, Audit conditional CRT last-K two-slice streaming tariff #4187, Lower admitted-stencil CRT guard scan to a literal three-tape program #4201/Produce a one-target CRT guard stencil from paid unary geometry #4208), the free-word tensor lift (Audit PR4100’s free-word tensor lift on all four actual programs #4184), the normal form (Independently check PR4100's good-packet normal form on small rings (no new κ) #4215), header densities (Prove exact extreme-rank BIT header densities #4227/Prove exact intermediate-rank BIT header densities #4228), HALO (Audit #4100's HALO locality witness: exact error identity and sharp (2J-1)W radius (no new κ) #4217), the narrow and broad conditioning (Record the circular-section Neumann bound #4282, Bound capped Gaussian inverses through half shifts #4193), the block solve (Bound rounded block-solve error at the fine-prime Gaussian boundary #4186), the Gaussian circuits (Generate exact bounded rational Stein coefficients #4198/Execute rounded Gaussian words against shared finite-core references #4205/Prove same-rho Schur closure for the completed parity-triangular caller #4209/Independently audit normalized Gaussian scalar enclosures and precision #4220), and the root/ledger (Independent numerical cross-check of PR4100's exact-root and paid-power ledger (finite layer; no new kappa) #4171).
• Reported corrections to Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 statements:
  • Bind mixed-provider precision to the rounded Gaussian tensor caller #4178: the common-grid allocation omits the incoming height t0.
  • Record the circular-section Neumann bound #4282: INVERSE-CONDITIONING's compression sentence does not cover circular sections; the PR repairs it.
  • Audit #4100's HALO locality witness: exact error identity and sharp (2J-1)W radius (no new κ) #4217: a HALO constant should be 2g, not g; the margin absorbs it.
  • Prove the sharp fallback child count: 33269, not 49911, at m = 64 (no new κ) #4237: the 49,911-child fallback bound is not sharp; 33,269 is.
  • Prove exact intermediate-rank BIT header densities #4228: the bad-fraction bound sharpens to (r+1)/q.
• No audit found at the check:
  • BIT.md: weighted leaves and fast header routes, and the row-stock and fixed-tape induction.
  • PROOF.md: chirp tables and the transform, CRT-composition and exact-recovery argument.
  • GAUSSIAN.md: the per-visit union schedule and the fine-prime interval at Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100's parameters.
  • GAUSSIAN.md: the all-size narrow row-gap estimate. Only p=19 instances exist (A centred prime-scale chirp keeps both corners positive, with a row sum above 1 (no new κ) #4304–The translated Schur diagonals are positive and at most 1 (no new κ) #4309), and they depend on the chirp origin.
  • CRT: exception sorting and reinsertion, and the full E(p,ell) evaluator.
  • COMPLEX.md: arbitrary-f complete-cover execution.

Task and overlap

• Card: uniform-transfer-audit, refined to "acceptance coverage map" (consolidation work), priority revision 7.
• Base: canonical main 12fa8c5c844be21bfefb38a19503fbd867a11244. Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 is pinned at 337d04939571a637aeab54a0f58f54fde811663a.
• Overlap: find_overlap.py refreshed at 06:50 UTC (419 open PRs, 3,174 discussion records, complete pagination). A closed-PR search found one Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 hit (Record the idle cost blocking the mixed staged544 endpoint. #4165), which is not an audit. No existing Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 coverage map or audit index was found.
• I first started an INVERSE-CONDITIONING audit at its GAUSSIAN.md caller. I dropped it after finding that Record the circular-section Neumann bound #4282 (jwr404) already records the same circular-section gap.
• Refreshed again before submission. One new related PR, The translated Schur diagonals are positive and at most 1 (no new κ) #4309, is included.

Checks run

• Every relative link and anchor in the new file resolves, checked with a local script.
• python3 -B tests/test_research_assignment.py: 16 tests OK.
• python3 -B tests/test_research_coordination.py: 8 tests OK.
• python3 -B tests/test_research_current_status.py: 6 tests OK.

Limitations

• The map summarizes PR bodies. It does not read package contents.
• "None found" means no matching open record existed at the check time. It does not prove novelty.
• Heads will move. Each row should be rechecked before use.
• I did not link the map from research-family-status.md or current-priorities.md, since those belong to the director's priority review. A maintainer can add a link from the Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 row if the map is useful.

Credit

All mathematical results belong to the cited authors: Cinna Davis (#4100), kumagi/Hiroki KUMAZAKI, ToikY, jmbarrancoml, petalas, yssite and jwr404. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. Apache-2.0.

Workflow feedback (optional)

The overlap helper made a complete snapshot easy. Finding every audit of one large proposal still meant reading about 40 bodies, because many cite AUDIT.md premises in prose rather than as a structured field. An optional audits: {pr, file, premise} entry in TASK.json would make maps like this one mechanical.

🤖 Generated with Claude Code