DONE: source-bound header encoding for the PR4100 sparse-union schedule (#4583)

[mihir-s-05]

DONE / 2026-10-22T08:12:18Z / priority revision 7 / claim released

PR #4583, commit 8d259a89fcff2a347de640a2f91cbe629c2e7a5c, supplies a sufficient per-microbox header contract for #4100 and the field-capacity part of #4327's handoff. The exact format has 2gh+g+2ceil(log2(g+1))+2 bits. At the actual beta/core side it is o(p); an exact symbolic cutoff gives H<p/16 even with upward group rounding. Registered normal/optimized replays, committed-byte checks and both Git-free export modes pass. Source/receipt/tag-code mutations reject. This is author-checked evidence with substantial OpenAI Codex assistance, not independent human or formal acceptance. No new kappa.

Public proof, codec and receipt: package at the exact commit. The next useful tasks are an actual tape-level carving/rank emitter and the coarse-context caller boundary; those remain open.

Evidence: 2,040 finite width cases, 746 codec round trips, 688 active headers, 14 semantic rejections, and six serialized runs of #4327's retained simulator with 28,976 header decodes. Its operator and movement checks pass with the serialized width. The simulator is reused evidence, not independently reimplemented. A two-context collision makes the local/global boundary explicit. The cutoff concerns header width only, not the complete algorithm. Source pins, licenses and attribution are retained; the central ledger labels the predecessors partially reviewed.

Final main refresh stayed at f626db5c3a3d781d8f7695038776c621651f75e1. Final overlap covered 358 open PR bodies and 3,493 Discussion records, with complete reported pagination and explicitly incomplete sparse local coverage. The optional history preflight was not run in the shallow checkout. The baseline stopped on omitted selected packages. Hosted CI was in progress when this update was posted.

Original claim and source history (now completed)

CLAIM / 2026-10-22 UTC / priority revision 7

Taking the record-header obligation left by #4327, its handoff, and #4376. Base: canonical main f626db5c3a3d781d8f7695038776c621651f75e1; #4100 source head 337d04939571a637aeab54a0f58f54fde811663a is retained there.

Question: can a concrete fixed-width header supply the flags, local coordinate comparisons, active tag and boundary ordinal used by the per-microbox sparse-union schedule, with o(p) bits at #4100's actual core side and beta? I will specify a codec, prove its all-size width bound, certify an explicit sufficient cutoff without constructing enormous arrays, and check the actual finite schedule's metadata on serialized headers. Controls will cover lost coordinates, bad flags/ordinals/tags, truncated records and the boundary between local and global context.

This is a refined uniform-transfer-audit task. #4327 already checks tape travel and #4376 checks row-field padding; neither binds the header layout. The caller's retained core size is 2^ceil(400 log2 p) and the composition ledger's beta is 1 - 3/10^30; historical numerical examples in vendor notes are not the current parameters. No complete tape compiler, coefficient producer, new kappa or selected-frontier update is intended.

Expected artifact: research/union-header-encoding/ with proof, source pins, executable codec and bounded positive/failure controls, followed by a focused PR if the implication holds. Stop at an unsupported field/context cost or counterexample. Local-only until publication. Claim expires 2026-10-22T10:00:00Z.

Overlap: 355 open PR bodies and 3,470 Discussion records with complete reported pagination at 07:47-07:49 UTC; targeted live searches for record/header width and #4327/#4376 found their existing handoffs. Sparse local notes are incomplete and not novelty evidence. The baseline orientation command was attempted but stopped on an omitted selected package; no selected cold replay is claimed.

Credit Cinna Davis (#4100), Jeremy Kothe's PR1731 schedule lineage, Vlado Vojdanovski's PR1673 layout, Ryanson Jonathan (#4327), unpaidmoon (#4376), rtyu193-rgb and LeverRank. Prepared for Mihir Srivastava / mihir-s-05 with substantial OpenAI Codex assistance. Apache-2.0.

{"schema":"integer-mult-coordination/v1","kind":"DONE","task":"uniform-transfer-audit","scope":"Sufficient per-microbox header contract and sublinear width for PR4100; actual field emission and coarse-context caller remain open","base":"f626db5c3a3d781d8f7695038776c621651f75e1","expiry":null,"artifact":"https://github.com/CrocSwap/integer-mult-bounds/pull/4583"}