Independently check #4583's union header: separate codec, exact width chain, cutoff and β binding (no new κ)

research/pr4583-header-check/README.md

@@ -0,0 +1,45 @@
+# Independent check of #4583: a serialized header for the PR4100 sparse-union schedule
+
+**Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.**
+
+mihir-s-05's #4583 (head `8d259a89`) gives a fixed-width per-microbox header for #4100's sparse-union schedule:
+
+`H = 2gh + g + 2⌈log₂(g+1)⌉ + 2` bits, with `h = ⌈log₂ L⌉`.
+
+At #4100's core side `L = 2^⌈400 log₂ p⌉` and `β = 1 − 3/10^30`, it shows `H ≤ 810 p^β log₂ p = o(p)` for `g ≤ p^β`, with an explicit cutoff `p ≥ 2^(40·10^30)` beyond which `H < p/32` (or `< p/16` with doubled `g`). This package checks it with a separately written codec and exact integer arithmetic. Nothing is imported from #4583's `header.py` or `verify.py`.
+
+## Results
+
+All checked claims are confirmed.
+
+1. **Codec.** I built it from #4583's field table: marker `01`, coordinates, membership flags, boundary ordinals, flag count and tag, all big-endian.
+   - **Round trips.** 2,888 of them, over random contexts for `g ≤ 5` and `L ≤ 16`, plus every boundary subset of a small domain. Every encoded width equals `H`.
+   - **Active headers.** 2,094 checks: the `(r+1)`st set flag gives the active axis, a record is kept iff its count exceeds `r+1`, and the active ordinal recovers the boundary point.
+   - **Corruptions.** All 3,600 corrupted headers (bad markers, inconsistent counts) are rejected.
+2. **Width chain.** 6,448 cases, for integer `p` (2–69, powers of two up to `2^40`, and two non-powers) and `g ≤ 2000`.
+   - `h = ⌈400 log₂ p⌉` is computed exactly as `(p^400 − 1).bit_length()`.
+   - `H ≤ 2gh + 5g` holds (`b ≤ g`).
+   - `H ≤ 810·g·t_lo` holds, where `t_lo = (h−1)/400 < log₂ p`, so `H < 810 g log₂ p`.
+3. **Cutoff and binding.**
+   - `δ = 1 − β = 3/10^30` matches both `β` and the `group_headers` slack in the pinned #4100 ledger (`composition-controls.json`), and `L = 2^⌈400 log₂ p⌉` matches `GAUSSIAN.md`.
+   - `δ·t0 = 120` at `t0 = 40·10^30`, and `810·t0 < 2^115` and `1620·t0 < 2^116`, so `H/p < 1/32` and `< 1/16` there.
+   - The tail is monotone, since `δ·t·ln 2 > 1` for `t ≥ t0` (using `ln 2 > 1/2`).
+
+## Verify
+
+```text
+python3 -B research/pr4583-header-check/verify.py
+```
+
+This runs in under 1 s with the standard library only.
+
+## Limitations
+
+- **Not covered.** #4583's adaptation of #4327's tape simulator, and the reader-cost accounting (`O(H polylog p)`), which is an asymptotic argument in #4583.
+- **Codec.** The codec checked here is the reference format. Whether #4100 serialises headers this way is outside both PRs.
+
+## Open next questions
+
+- None new from these checks. The producer and global-context tape obligations that #4583 names remain open.
+
+Credit: mihir-s-05 (#4583); the #4100, #4327 and #4376 union-schedule lineage. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.

research/pr4583-header-check/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/unconditional-batched-crt/GAUSSIAN.md",
+      "usage": "input",
+      "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b",
+      "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242"
+    },
+    {
+      "path": "research/unconditional-batched-crt/evidence/composition-controls.json",
+      "usage": "input",
+      "git_blob": "fd4ef818b4a31038871ee85213d2b9694b5fd0d3",
+      "sha256": "f235c5eb28bf0e0dfec32f062dd61cae879010b6ac8f237ee122af6cb87df400"
+    }
+  ]
+}

research/pr4583-header-check/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+    "allowed_variations": [
+      "Reconstruct either a source ledger or a numeric enclosure with a different method."
+    ],
+    "scope_change_triggers": [
+      "Importing the primary function and calling its output independent verification.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "unchanged",
+  "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+  "scope_change_reason": null,
+  "bottleneck_link": "Independent coverage of a metadata-width obligation in the unconditional batched-CRT (PR4100) route.",
+  "budget_minutes": 25,
+  "stop_rule": "Stop at #4583's codec width and cutoff.",
+  "outcome": "completed",
+  "evidence": "Separate codec: 2,888 round trips, 2,094 active-header checks, 3,600 rejected corruptions; width chain on 6,448 exact cases; cutoff integers and beta/L binding to pinned #4100 sources.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "None new; #4583's producer/global-context tape obligations remain.",
+      "why_it_matters": "Needed for the full union schedule.",
+      "first_step": "See #4583.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/pr4583-header-check/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/unconditional-batched-crt/GAUSSIAN.md",
+    "research/unconditional-batched-crt/evidence/composition-controls.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Separate header codec round trips, active-header decisions and corruption rejection; exact width chain; cutoff integers; beta/core-side binding to pinned #4100 sources."
+    }
+  ]
+}

research/pr4583-header-check/verify.py

@@ -0,0 +1,156 @@
+#!/usr/bin/env python3
+"""Independent check of PR #4583 (mihir-s-05): a serialized header for the PR4100 sparse-union schedule.
+
+Written from #4583's README field table; nothing is imported from #4583's header.py or verify.py.
+  1. A separate big-endian codec: marker 01 (2 bits), local coordinates x_0..x_(g-1) (h bits each), membership flags
+     (g bits), boundary ordinals (h bits each; rank in E_i when flagged, 0 otherwise), flag count and current tag
+     (b = ceil(log2(g+1)) bits each, tag = g as the untagged sentinel). Round trips over random contexts and every
+     boundary subset in a small domain; the encoded width equals H = 2gh + g + 2b + 2; in round r the (r+1)st set
+     flag gives the active axis, a record is kept iff count > r + 1, and the active ordinal is read back; a bad marker
+     and an inconsistent flag count are rejected.
+  2. The width bound H < 810 g log2 p with h = ceil(400 log2 p) computed exactly as (p^400 - 1).bit_length(), for
+     integer p (powers of two and others) and g <= 2000, via the chain H <= 2gh + 5g <= 800 g t + 7g <= 807 g t.
+  3. The cutoff: delta = 1 - beta = 3/10^30 bound to the pinned #4100 ledger (beta and the group_headers slack), the
+     core side L = 2^ceil(400 log2 p) bound to GAUSSIAN.md, delta*t0 = 120 at t0 = 40*10^30, 810 t0 < 2^115 and
+     1620 t0 < 2^116 (so H/p < 1/32 and < 1/16 at t0), and the derivative sign 1 - delta t ln 2 < 0 for t >= t0.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from fractions import Fraction as Fr
+import json
+from pathlib import Path
+import random
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+LEDGER = ROOT / "research/unconditional-batched-crt/evidence/composition-controls.json"
+GAUSSIAN = ROOT / "research/unconditional-batched-crt/GAUSSIAN.md"
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def bits_for(g):
+    return g.bit_length()  # ceil(log2(g+1))
+
+
+def encode(x, sets, tag, h):
+    g = len(x)
+    b = bits_for(g)
+    flags = [1 if x[i] in sets[i] else 0 for i in range(g)]
+    ords = [sorted(sets[i]).index(x[i]) if flags[i] else 0 for i in range(g)]
+    bits = "01" + "".join(format(v, f"0{h}b") for v in x) + "".join(map(str, flags))
+    bits += "".join(format(v, f"0{h}b") for v in ords) + format(sum(flags), f"0{b}b") + format(tag, f"0{b}b")
+    return bits
+
+
+def decode(bits, g, h):
+    b = bits_for(g)
+    need(bits[:2] == "01", "record marker")
+    pos = 2
+    x = [int(bits[pos + i * h: pos + (i + 1) * h], 2) for i in range(g)]
+    pos += g * h
+    flags = [int(c) for c in bits[pos: pos + g]]
+    pos += g
+    ords = [int(bits[pos + i * h: pos + (i + 1) * h], 2) for i in range(g)]
+    pos += g * h
+    count = int(bits[pos: pos + b], 2)
+    tag = int(bits[pos + b: pos + 2 * b], 2)
+    need(pos + 2 * b == len(bits), "exact length")
+    need(count == sum(flags) and tag <= g, "consistent count and tag")
+    return x, flags, ords, count, tag
+
+
+def check_codec(rng):
+    trips = active = rejects = 0
+    for g in range(1, 6):
+        for L in (2, 3, 4, 7, 8, 16):
+            h = (L - 1).bit_length()
+            for _ in range(60):
+                sets = [set(v for v in range(L) if rng.random() < 0.4) for _ in range(g)]
+                x = [rng.randrange(L) for _ in range(g)]
+                bits = encode(x, sets, g, h)
+                need(len(bits) == 2 * g * h + g + 2 * bits_for(g) + 2, "width formula")
+                xd, flags, ords, count, tag = decode(bits, g, h)
+                need(xd == x and tag == g, "round trip")
+                for i in range(g):
+                    if flags[i]:
+                        need(sorted(sets[i])[ords[i]] == x[i], "ordinal recovers the boundary point")
+                trips += 1
+                set_axes = [i for i in range(g) if flags[i]]
+                for r in range(g):
+                    need((count > r + 1) == (len(set_axes) > r + 1), "keep decision")
+                    if r < len(set_axes):
+                        f = set_axes[r]
+                        _, _, o2, _, t2 = decode(encode(x, sets, f, h), g, h)
+                        need(t2 == f and o2[f] == sorted(sets[f]).index(x[f]), "active axis and ordinal")
+                        active += 1
+                try:
+                    decode("10" + bits[2:], g, h)
+                except AssertionError:
+                    rejects += 1
+                b = bits_for(g)
+                cpos = 2 + 2 * g * h + g
+                wrong = (sum(flags) + 1) % (1 << b)
+                if wrong != sum(flags):
+                    try:
+                        decode(bits[:cpos] + format(wrong, f"0{b}b") + bits[cpos + b:], g, h)
+                    except AssertionError:
+                        rejects += 1
+    for g in (1, 2):
+        L, h = 4, 2
+        for mask in range(1 << (L * g)):
+            sets = [set(v for v in range(L) if mask >> (i * L + v) & 1) for i in range(g)]
+            for x0 in range(L):
+                x = [x0] * g
+                xd, flags, _, _, _ = decode(encode(x, sets, g, h), g, h)
+                need(xd == x and flags == [1 if x0 in s else 0 for s in sets], "exhaustive subsets")
+                trips += 1
+    return trips, active, rejects
+
+
+def check_width():
+    cases = 0
+    for p in list(range(2, 70)) + [2 ** k for k in range(7, 41)] + [10 ** 6 + 3, 3 ** 20]:
+        h = (p ** 400 - 1).bit_length()
+        need(1 << (h - 1) < p ** 400 <= 1 << h, "h = ceil(400 log2 p)")
+        # t = log2 p satisfies 400 t > h - 1, i.e. t > (h - 1)/400 =: t_lo, and t >= 1 since p >= 2.
+        t_lo = max(Fr(h - 1, 400), Fr(1))
+        for g in list(range(1, 60)) + [100, 500, 2000]:
+            b = bits_for(g)
+            H = 2 * g * h + g + 2 * b + 2
+            need(b <= g and H <= 2 * g * h + 5 * g, "first link: b <= g")
+            # 2gh = 2g((h - 1) + 1) < 2g(400 t) + 2g, so H < 800 g t + 7 g <= 807 g t (t >= 1) < 810 g t.
+            need(H <= 800 * g * Fr(h, 400) + 5 * g, "second link: 2gh = 800 g (h/400)")
+            need(H <= 810 * g * t_lo, "H < 810 g t, since t > t_lo")
+            cases += 1
+    return cases
+
+
+def check_cutoff():
+    ledger = json.loads(LEDGER.read_bytes())
+    beta = Fr(ledger["parameters"]["beta"])
+    delta = 1 - beta
+    need(delta == Fr(3, 10 ** 30) and Fr(ledger["side_slacks"]["group_headers"]) == delta, "beta and header slack")
+    need("L=2^ceil(400log2 p)" in GAUSSIAN.read_text(encoding="utf-8"), "core side L = 2^ceil(400 log2 p)")
+    t0 = 40 * 10 ** 30
+    need(delta * t0 == 120, "delta t0 = 120")
+    need(810 * t0 < 2 ** 115 and 1620 * t0 < 2 ** 116, "cutoff integers")
+    need(Fr(810 * t0, 2 ** 120) < Fr(1, 32) and Fr(1620 * t0, 2 ** 120) < Fr(1, 16), "ratios at t0")
+    need(delta * t0 * Fr(1, 2) > 1, "monotone tail (ln 2 > 1/2)")
+    return str(delta)
+
+
+def main():
+    rng = random.Random(4583)
+    trips, active, rejects = check_codec(rng)
+    report = {"status": "PASS_PR4583_HEADER_CHECK", "codec_round_trips": trips, "active_header_checks": active,
+              "rejected_corruptions": rejects, "width_cases": check_width(), "delta": check_cutoff(),
+              "new_kappa_claimed": False}
+    print(json.dumps(report, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())