Research audit: tighten the packed-bit repair envelope (no new kappa)

[AryanSudhirDev]

The original packed selected-bit proof bounds the correction fraction by min(1, 80(f-1)2^-K). This research audit derives an invariant carry/borrow guard envelope with exact density

1 - (1 - 2^(1-K) + 2^(1-2K))^(f-1) <= min(1, 2(f-1)2^-K).

The note proves agreement off that envelope, its invariance under both the ideal and actual permutations, and maximality within a precisely defined local no-escape guard class. It retains the eight rotations and existing correction argument. The factor of 40 applies to the conservative union-bound coefficient; this is not a runtime benchmark or a new kappa. The envelope is not the exact failure set, and the note distinguishes complete-rectangle density from fixed-source-fiber density.

The contribution is confined to research/packed-guard-envelope-audit/. It includes a written proof, source pins, exact receipt, and an independent standard-library verifier. Upstream sources and the selected construction are unchanged. This audits the original primitive, not the different compact-control primitive or the current supplier surcharge.

Validation:

• 581,888 exhaustive packed states and 37,760 boundary/seeded states passed.
• Four removed guard conditions, two broken rotation programs, and reversed correction order have concrete failure witnesses, all at K=6.
• All 14 relevant existing tests and make selected-record-check passed; 2,240 comparisons with the pre-existing simulator agreed.
• Full make verify and the separate selected-supplier cold replay were not run.

Reproduce from the repository root:

python3 -B research/packed-guard-envelope-audit/verify.py

Expected: PASS_PACKED_GUARD_ENVELOPE_AUDIT, with all evidence matching RESULT.json.

Base commit: 66849e1475c930fd7732b1a0067ffee7e1e95f60. Track: adversarial mathematical audit; OS-random assignment seed 62. No pinned sprint issue was present; the claim and overlap review are recorded locally in the package.

Attribution: Aryan Sudhir (AryanSudhirDev), with substantial OpenAI Codex assistance. The note credits the retained OpenAI #109 manuscript and the repository's preceding finite, packed-movement, and short-guard audits. New material is Apache-2.0. This is a written address-map proof with finite corroboration, not a Lean formalization or a full multiplication theorem.

[Mister-Meeseeks]

100-PR batch review at 8d36139e49add1e55795e283b3bfa45e1cfe1bf0.

Merged to main, preserving the original contributor commits and package attribution.

Reviewed scope: Sharper invariant no-escape envelope for the eight-rotation map; envelope density is not the actual failure probability, and original streaming assumptions remain.

The pinned scoped command passed; the batch ledger contains its command, input hashes, environment and log. This incorporates the research/tooling contribution and does not change the selected κ or discharge the inherited multiplication-theorem assumptions.

Batch review, attribution and evidence. Thank you for the contribution.