Prove optimal sparse-union headers: 44 to 19 bits (no κ)

research/union-state-header/PROOF.md

@@ -0,0 +1,113 @@
+# Exact minimum header width
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract
+
+Fix integers L>=2 and g>=1 and shared sorted sets E_i contained in
+{0,...,L-1}, with a_i=|E_i|. A coordinate vector x has g entries in that
+range. The legal tag is either the sentinel g or an axis i with x_i in E_i.
+The flags, canonical boundary ordinals and flag count are determined by x
+and the shared sets. An unflagged ordinal is zero. This is the full legal
+header domain of Mihir Srivastava's PR4583, including sentinel records
+outside the sparse union. There is no restriction on the payload.
+
+A record has a fixed two-bit marker 01 followed by a fixed number of data
+bits. The decoder knows L, g and every E_i, but receives no record-dependent
+side information or previous record state. Records must decode individually
+and exactly. We optimize width within this contract, without a locality,
+time or fixed-tape requirement. Context storage is outside that width.
+
+## Theorem
+
+The number of legal headers is exactly
+
+    N = L^(g-1) (L + sum_i a_i).
+
+Their minimum fixed width, including the marker, is
+
+    H* = 2 + ceil(log2 N).
+
+Writing h=ceil(log2 L) and b=ceil(log2(g+1)), it satisfies
+
+    H* <= 2 + gh + b.
+
+Compared with PR4583's separate-field width
+
+    H_old = 2 + 2gh + g + 2b,
+
+this saves at least gh+g+b bits at every allowed context. All flags,
+ordinals, count, tag, active-round choice, prefix keys and keep decisions
+remain exactly recoverable. This is a representation theorem, with no
+claim about physical time, tape travel or the full multiplication theorem.
+
+## Counting and lower bound
+
+Partition legal headers by tag. The sentinel block has all L^g coordinate
+vectors. The block tagged i has a_i choices for coordinate i and L choices
+for every other coordinate, hence a_i L^(g-1) states. Blocks are disjoint
+because their tags differ, even when the same coordinate occurs in several
+blocks. Summing proves the formula. Flags, ordinals and count add no states,
+since they are determined by the coordinate and shared context.
+
+A width-H record with marker 01 has at most 2^(H-2) distinct bit strings.
+Exact decoding requires distinct legal headers to have distinct strings,
+including headers sharing coordinates but having different legal tags.
+Therefore 2^(H-2)>=N, giving the stated lower bound for every encoder,
+including nonlinear encoders. The conclusion does not apply to variable
+lengths, joint compression across records or an additional side channel.
+
+## Attaining construction
+
+Order the blocks as sentinel, axis 0, ..., axis g-1. The sentinel block
+starts at zero. Axis i starts at
+
+    L^g + L^(g-1) sum_{j<i} a_j.
+
+Inside the sentinel block use the ordinary lexicographic base-L coordinate
+index. Inside axis i's block replace x_i by its zero-based ordinal in E_i
+and use radices L at the other coordinates and a_i at coordinate i.
+For digits d_j and radices r_j, the mixed-radix index is computed by starting
+v=0 and replacing v with v*r_j+d_j in coordinate order. Induction gives a
+bijection to the integers from zero through product(r_j)-1. An empty axis
+block is skipped and never requires division by zero.
+
+Add the block offset to obtain an index k in [0,N). Store k in exactly
+ceil(log2 N) binary bits after 01. Decode by selecting its block, subtracting
+the offset and repeatedly taking quotient and remainder by the radices in
+reverse order. For an active block, select x_i from E_i at the recovered
+ordinal. The mixed-radix bijection and disjoint block intervals prove both
+inverse identities. Unused binary indices k>=N are rejected.
+
+Given the recovered coordinate, sorted-set membership and rank recover every
+flag and ordinal, hence the count. The round-r active axis is the r-th set
+flag, for zero-based r<count. The line key is the preceding coordinate
+prefix together with the active ordinal. A keep decision is count>r+1.
+Retagging re-encodes the same coordinate with that active axis. These are
+semantic operations; they make no assertion about in-place reversibility
+or preservation of an arbitrary previous tag.
+
+Finally a_i<=L implies N<=(g+1)L^g<=2^(b+gh). Thus ceil(log2 N)<=b+gh.
+Subtracting this upper bound from H_old gives the uniform saving. For
+L=16, g=4 and each E_i={0,15}, N=98,304, so H*=19 while H_old=44.
+
+## Scope and implementation
+
+Enumerative coding, mixed-radix conversion and the pigeonhole principle are
+classical. The contribution is their exact application to this full legal
+union-header domain and the new bounded reference codec. The prior field
+codec and its scientific checks are not replayed or audited here.
+
+The written construction holds for arbitrary finite contexts. codec.py
+implements it within explicit capacities of 32 axes, L<=2^4096 and 128
+entries per boundary set. It never enumerates the coordinate box. Boundary
+queries use the supplied sorted lists. The bit-width theorem does not charge
+those lists, arithmetic temporaries, rank/select access or decoding travel.
+In particular, the old tag-only update is replaced by a possible whole-index
+rewrite. Identical contexts may share code words; context boundaries remain
+required. Some bit changes produce another legal state, so this format is
+not an error-detecting code.
+
+The universal claim rests on this written proof. Finite execution corroborates
+only its declared domains. No physical caller, selected-frontier change,
+new kappa or discharge of the five inherited assumptions follows.

research/union-state-header/README.md

@@ -0,0 +1,126 @@
+# Minimum exact state headers for sparse-union records
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written construction and sharp information bound, with
+exact finite corroboration. No new kappa is claimed.
+
+For a shared context of g axes, side L>=2 and boundary sets E_i of sizes a_i,
+the full legal coordinate/tag header domain of Mihir Srivastava's
+[PR4583](https://github.com/CrocSwap/integer-mult-bounds/pull/4583) has exactly
+
+    N = L^(g-1) (L + sum_i a_i)
+
+states. The new mixed-radix codec uses the minimum possible fixed width
+
+    H* = 2 + ceil(log2 N)
+
+including the retained two-bit marker. It recovers every coordinate, flag,
+canonical ordinal, count and tag. The minimum covers arbitrary encoders with
+individual exact decoding under the same fixed shared context.
+
+For h=ceil(log2 L), b=ceil(log2(g+1)), this saves at least gh+g+b bits against
+the predecessor's separate-field format. At L=16, g=4 and E_i={0,15}, all
+98,304 legal states fit in 19 bits including framing; that format uses 44.
+[PROOF.md](PROOF.md) gives the disjoint-tag count, matching lower bound and
+attaining rank/unrank construction. [codec.py](codec.py) implements it.
+
+The source metadata contract is a cited premise. Its codec, schedule and
+scientific results are not replayed or audited. The new finite enumeration
+checks the new representation directly against the legal-state definition.
+
+## Evidence and reproduction
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/union-state-header/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/union-state-header/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/union-state-header
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/union-state-header --check-source-history --check-modes
+```
+
+Substitute another CPython 3.12 executable on other machines. Direct replay
+prints PASS_UNION_STATE_HEADER and a generated JSON receipt bound to every
+package file and both declared source inputs. It writes nothing.
+
+The finite domain includes every boundary subset and every legal state for
+L=2 with g=1..4, L=3 with g=1..3 and L=4 with g=1..2. It enumerates 1,196
+contexts and 57,744 legal states, checks 105,120 retags and their line keys,
+and rejects all 22,022 unused codes within those record widths. Sixty larger
+rank/serialization round trips reach L=2^4096 and g=32. Twenty-seven explicit
+controls reject malformed contexts, coordinates, tags, indices, framing,
+rounds and mismatched line keys. A collision control retains the distinction
+between active and sentinel tags on the same coordinates. A legal substitution
+control makes explicit that this is not an error-detecting code.
+
+Normal and optimized commands execute the same always-enabled contracts.
+Registered replays are bounded individually by 120 seconds. The universal
+conclusion rests on the written proof, not on a finite census.
+
+## Scope, credit and overlap
+
+The shared boundary sets are decoder context. Rank/select access, arbitrary
+precision arithmetic, context storage and temporary space are not free in a
+physical implementation. Retagging may rewrite the entire index. The old
+format's tag-local update and direct metadata fields are not preserved as
+locality guarantees. No faster reader, fixed-tape saving or complete emitter
+is supplied. Context boundaries remain necessary, and payloads are untouched.
+The result does not implement an arbitrary-dirty reversible retagging map.
+
+Credit Mihir Srivastava / mihir-s-05, PR4583, for the precise metadata contract
+and separate-field header. Retain Cinna Davis / PR4100, Jeremy Kothe / PR1731,
+Vlado Vojdanovski / PR1673, Ryanson Jonathan / PR4327 and PR4590, unpaidmoon /
+PR4376, rtyu193-rgb and LeverRank's schedule, layout and review lineage.
+Enumerative coding, mixed-radix indexing and the pigeonhole principle are
+classical. This contribution applies them to that interface and supplies the
+smaller exact codec; no general literature-priority claim is made.
+
+Canonical base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8,
+selected PR6030. SOURCES.json binds the unmodified contract and field-codec
+bytes. The card changes from a selected-assumption audit to this representation
+side result for precision_tape. The source-binding orientation passed.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375380)
+records the target and stop rule. The cached overlap snapshot covers 572 open
+PRs and 6,641 Discussion records with complete reported remote pagination.
+Only 141 of 8,917 local note paths were materialized. Separate main-wide
+README searches and live merged/general-form searches supplement that sparse
+coverage. Historical diffs and unpublished work remain limits.
+
+No selected cold replay, Lean or Docker run is needed for this side result.
+All five selected framework assumptions remain. Independent human and formal
+proof-kernel review are unclaimed. This is not a physical supplier, selected
+frontier change or complete multiplication theorem.
+
+## Open next questions
+
+Can an actual union invocation use this representation with a favorable full
+reader, emitter and retagging bill? Start with one carving description, bind
+rank/select access, and charge every header rewrite and temporary through one
+round. Missing bit-level decoding, context delivery and complete caller costs
+block an operational saving. TASK.json records this handoff explicitly.
+
+## Code bounds and diagnostics
+
+The codec has at most 32 axes, 128 entries per boundary and L<=2^4096, giving
+at most 131,078 index bits and 131,080 serialized bits. No coordinate box is
+materialized by rank/unrank. Each codec loop has at most 32 iterations, and
+boundary validation operates on at most 128 entries. The exhaustive verifier
+retains at most 108 ranks per context. Its context and fixture domains are
+fixed as listed above. Source reads are capped at one MiB and the manifest
+at sixteen rows; the package receipt covers seven fixed filenames. Functions
+stay below sixty physical lines. Warning-strict normal and optimized replay
+provide the available runtime diagnostics; no unavailable static analyzer is
+claimed as run.
+
+Power-of-Ten rule 3 has a managed-runtime deviation in codec.py and verify.py.
+Python allocates integers, strings, tuples, sets and JSON values during the
+run. The enforced dimensions, integer and header lengths, bounded live rank
+set, capped input reads and streamed contexts bound their sizes. This is not
+a static-pool or byte-exact heap bound. Reassess these bounds before enlarging
+the capacities; a fixed-pool backend would be a separate implementation.
+Rule 9's verifier callback deviation is confined to explicit negative-test
+calls to Layout and its encode, decode, unrank, retag and line_key methods.
+No dynamic code or unbounded dispatch is accepted. Normal and optimized
+negative controls exercise every listed target. Production codec calls are
+direct, and decoded Header values and boundary tuples are immutable.

research/union-state-header/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/union-header-encoding/README.md",
+      "usage": "input",
+      "git_blob": "790660a0a0f0c8cbb7945ce766ce8600d8c1dde1",
+      "sha256": "320345a6ed2b7ca82057c4b2a9551c664cd96b5c387e43e6c3a98b422bd77d9a"
+    },
+    {
+      "path": "research/union-header-encoding/header.py",
+      "usage": "input",
+      "git_blob": "424699d49c57e762ca5f04091bfab8f8d145d14c",
+      "sha256": "9e24704bf2b73e5c812827ed03aa9f2fcb8a1999c079ba1d260f7658020e69aa"
+    }
+  ]
+}

research/union-state-header/TASK.json

@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "An information-optimal fixed-width encoding of the full legal PR4583 coordinate/tag header domain, with an attaining mixed-radix codec.",
+  "scope_change_reason": "Replace a supplier-assumption audit by a new smaller representation at the existing per-microbox metadata contract. This is a side result for precision_tape; physical reader and emitter costs are not discharged.",
+  "bottleneck_link": "The sparse-union tape invoice depends on record width. The new representation removes redundant metadata at the information level; physical adoption needs a separately charged decoder and retagging implementation.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first strict width improvement, exact fixed-width lower bound and bounded corroboration. Do not expand into a physical caller or replay predecessor mathematics.",
+  "outcome": "completed",
+  "evidence": "PROOF.md establishes the all-size count, optimality and rank/unrank construction. verify.py independently enumerates the declared small legal state domains and checks metadata queries, unused code rejection, large indices and invalid inputs.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual union invocation use this representation with a favorable complete reader, emitter and retagging bill?",
+      "why_it_matters": "Smaller records do not by themselves reduce tape cost; retagging here may rewrite every index bit.",
+      "first_step": "Bind one carving description to rank/select access and measure all header reads, rewrites and temporary storage through one round.",
+      "blocked_by": "No bit-level fixed-tape decoder, carving producer, context delivery or complete caller budget is supplied."
+    }
+  ],
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375380",
+    "source_pr": 4583,
+    "source_author": "mihir-s-05",
+    "freshness_utc": "2026-11-03T13:57:00Z",
+    "overlap_limits": "Capped live PR searches, sparse historical notes, arbitrary diffs and unpublished work do not establish novelty."
+  }
+}