Soundness check of #4585's coarsened partitions against exact geometry: all 235 realisable profiles covered (no new κ)

research/pr4585-geometry-soundness-check/.gitattributes

@@ -0,0 +1 @@
+PR4585-CERTIFICATE.json -text

research/pr4585-geometry-soundness-check/README.md

@@ -0,0 +1,50 @@
+# Soundness check of #4585's coarsened partitions against exact geometry
+
+**Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.**
+
+mihir-s-05's #4585 (head `025f37fe`) proves that no finite shear word improves any of the 128 #4470 receiver windows. It uses two necessary conditions: mandatory source contacts and admissible-contact-graph bridges. It coarsens each field's path at those contacts into a finite list of `relaxed_partitions`, and proves a capped-rank (majorization) floor over them. For the floor to cover every word, each **actually realisable** word profile must be listed or must **refine** (split into) a listed partition. Concavity then gives `cost(word) ≥ cost(listed partition) ≥ cost(incumbent)`.
+
+#4585's lists are coarser than, and in 33 windows differ from, the identical profile sets of #4567, #4581, #4582 and #4587:
+- smaller in 21 windows;
+- larger in 11;
+- incomparable in 1.
+
+So this package checks the needed property directly against **exact geometry**. #4585's `CERTIFICATE.json` is vendored (blob `74424627`, SHA256-pinned).
+
+## Method
+
+- **Windows.** The 128 windows come from main's #4470 constructor, via `windows_lib.py`, which is my #4567 extraction and census code.
+- **Exact profiles.** Every unit-shear word of length ≤ 5 with the window's endpoint is enumerated. For each word, an exact search over actual nested subspaces of `F₂⁹`, with joint incidence enforced across all gates, yields every exactly realisable profile.
+- **Refinement.** Each realisable profile must be listed by #4585 or refine a listed partition (exact multiset bin-packing).
+- **Incumbent.** The incumbent must be listed and must dominate every listed partition in capped rank sums (equal mass, `Σ min(r,k)` for `k ≤ 9`).
+
+## Results
+
+**All checks pass in all 128 windows.**
+- **Profiles.** There are 235 exactly realisable profiles at length ≤ 5. **151 are listed and 84 refine a listed partition, with 0 violations.**
+- **Incumbent.** It is realisable, listed and capped-rank dominant in every window.
+
+**Length 6 (recorded run, about 20 min, not in the registered verifier because of runtime).** There are 239 realisable profiles, 151 listed and 88 refining, with 0 violations.
+
+**A tightness observation.** For each window, the realisable set is contained in the relaxed set of #4567/#4581/#4582/#4587, because the relaxation contains every actual path. At length 6 the total, 239, equals those certificates' 239 window/profile pairs. So **every relaxed profile is realised exactly by some actual word of length ≤ 6**: the relaxation is tight for these 128 windows.
+
+So #4585's coarsened lists are consistent with exact geometry where they differ from the relaxed sets of the other certificates. Its smaller lists still cover every realised profile by refinement.
+
+## Verify
+
+```text
+python3 -B research/pr4585-geometry-soundness-check/verify.py
+```
+
+This runs in about 75 s with the standard library only.
+
+## Limitations
+
+- **Lengths.** Lengths above 5 are not enumerated. The all-length statement is #4585's written proof; this corroborates its key soundness property on every realisable short word.
+- **Coefficients.** Unit coefficients only, as in #4585's windows. Nonunit words are covered by #4567's ceilings, not here.
+
+## Open next questions
+
+- None new. #4567's nonadjacent and retiming extensions lie outside #4585's scope.
+
+Credit: mihir-s-05 (#4585), Cinna Davis (#4470); the exact-geometry search is from my #4567. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.

research/pr4585-geometry-soundness-check/SOURCES.json

@@ -0,0 +1,60 @@
+{
+  "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/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz",
+      "usage": "input",
+      "git_blob": "4a8c4ed26e53a72362d571c972e65aff546be784",
+      "sha256": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61"
+    },
+    {
+      "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz",
+      "usage": "input",
+      "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c",
+      "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39"
+    },
+    {
+      "path": "research/fresh-helper-boundary/native.py",
+      "usage": "input",
+      "git_blob": "1b36f6cb5f205c33bf48811e0b1b3621c55e8154",
+      "sha256": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29"
+    },
+    {
+      "path": "research/fresh-helper-boundary/CHANGES.json",
+      "usage": "input",
+      "git_blob": "45744fedd0e28967aa72586048b8bc0c72f419a9",
+      "sha256": "cde73b8ff5b3c0d06e69e2293b991b24fd14a16dd4ccab7ff6b3439074a94624"
+    },
+    {
+      "path": "research/missing-join-frame/PATCH.json",
+      "usage": "input",
+      "git_blob": "f96d295d40014d4dd503f58eb3cdabcbb4b8e101",
+      "sha256": "9ab5328245ff02c9d0be21d39bcc375f50bc5d7909e9f7b9a3a9a6f812f5bd6e"
+    },
+    {
+      "path": "research/joint-helper-lattice/PATCH.json",
+      "usage": "input",
+      "git_blob": "51304a6601061ed4e698f910b09135ef109555e3",
+      "sha256": "296d0e8c58cc70febe042c681ef30d6bb469818c0835fbcaac8aa8d330f5b727"
+    },
+    {
+      "path": "research/joint-helper-lattice/native_joint.py",
+      "usage": "input",
+      "git_blob": "0315f80e2fdef5e0eef13e3e9b8f72066238164d",
+      "sha256": "50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46"
+    }
+  ]
+}

research/pr4585-geometry-soundness-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 soundness check of the fourth all-length receiver-window floor certificate, against exact geometry.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop at word length 5.",
+  "outcome": "completed",
+  "evidence": "All 128 windows: 235 exactly realisable profiles (length <= 5, exact nested-subspace search), 151 listed and 84 refining a #4585 partition, 0 violations; incumbent listed and capped-rank dominant everywhere.",
+  "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.",
+      "why_it_matters": "#4567's extensions are outside #4585's scope.",
+      "first_step": "n/a",
+      "blocked_by": "None."
+    }
+  ]
+}

research/pr4585-geometry-soundness-check/VERIFY.json

@@ -0,0 +1,28 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "docs/research/agent-task-catalog.json",
+    "research/fresh-helper-boundary/CHANGES.json",
+    "research/fresh-helper-boundary/native.py",
+    "research/joint-helper-lattice/PATCH.json",
+    "research/joint-helper-lattice/native_joint.py",
+    "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz",
+    "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz",
+    "research/missing-join-frame/PATCH.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Exact-geometry profiles of all words of length <= 5 in 128 #4470 windows are listed in or refine #4585's partitions; incumbent listed and dominant; binding to vendored certificate (sha256)."
+    }
+  ]
+}

research/pr4585-geometry-soundness-check/verify.py

@@ -0,0 +1,135 @@
+#!/usr/bin/env python3
+"""Independent soundness check of PR #4585 (mihir-s-05): receiver-window floors via mandatory contacts and bridges.
+
+#4585 (head 025f37fe; CERTIFICATE.json vendored, blob 74424627, sha256-pinned) lists per window a set of coarsened
+"relaxed_partitions" and proves that every finite scalar-shear word costs at least the incumbent. Its argument needs
+every actually realisable word profile to be listed or to refine (split into) a listed partition; concavity then
+carries the floor. #4585's sets differ from the identical sets of #4567/#4581/#4582/#4587 in 33 windows, so this is
+checked directly against exact geometry:
+
+  * the 128 windows are extracted from main's #4470 constructor by windows_lib.py (my #4567 code);
+  * every word of length <= 5 with the window endpoint is enumerated (unit shears), and an exact search over actual
+    nested subspaces of F_2^9 (joint incidence enforced across all gates) yields every exactly realisable profile;
+  * each realisable profile must be listed or refine a listed partition (exact multiset bin-packing);
+  * the incumbent must be listed and dominate every listed partition in capped rank sums (equal mass,
+    sum min(r, k) for k <= 9), the certificate #4585 uses for every concave price.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from functools import lru_cache
+import hashlib
+import json
+from pathlib import Path
+import sys
+
+HERE = Path(__file__).resolve().parent
+CERT = HERE / "PR4585-CERTIFICATE.json"
+CERT_SHA256 = "bb5c60a41074ea26d09f263755426b7db4a80b369de5daa64fa63be2d3fd66f7"
+MAX_LEN = 5
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def part(h):
+    return tuple(sorted((r for r, n in enumerate(h) for _ in range(n)), reverse=True))
+
+
+def refines(R, C):
+    R, C = tuple(sorted(R, reverse=True)), tuple(sorted(C, reverse=True))
+    if sum(R) != sum(C):
+        return False
+
+    @lru_cache(None)
+    def go(rest, caps):
+        if not rest:
+            return all(c == 0 for c in caps)
+        x, tail, seen = rest[0], rest[1:], set()
+        for i, cap in enumerate(caps):
+            if cap >= x and cap not in seen:
+                seen.add(cap)
+                nc = list(caps)
+                nc[i] -= x
+                if go(tail, tuple(sorted(nc, reverse=True))):
+                    return True
+        return False
+
+    return go(R, C)
+
+
+def main():
+    ns = {"__name__": "windows_lib", "__file__": str(HERE / "windows_lib.py")}
+    exec(compile((HERE / "windows_lib.py").read_bytes(), str(HERE / "windows_lib.py"), "exec"), ns)
+    raw = CERT.read_bytes()
+    need(hashlib.sha256(raw).hexdigest() == CERT_SHA256, "vendored #4585 CERTIFICATE.json")
+    listed = {w["index"]: set(tuple(sorted(p, reverse=True)) for p in w["relaxed_partitions"])
+              for w in json.loads(raw)["windows"]}
+    c, program = ns["construct"]()
+    wins = ns["extract_windows"](c, program)
+    need(len(wins) == 128 and set(listed) == {w["index"] for w in wins}, "same 128 windows")
+
+    def geo_profiles(starts, ends, word):
+        cur, upper = list(ends), [None] * len(word)
+        for k in range(len(word) - 1, -1, -1):
+            i, j, _ = word[k]
+            f = cur[i] & cur[j]
+            upper[k] = f
+            cur[i] = cur[j] = f
+        out = set()
+
+        def rec(k, state, hist):
+            if k == len(word):
+                h = list(hist)
+                for r in range(3):
+                    if not state[r] <= ends[r]:
+                        return
+                    g = ns["dim"](ends[r]) - ns["dim"](state[r])
+                    if g:
+                        h[g] += 1
+                out.add(part(tuple(h)))
+                return
+            i, j, _ = word[k]
+            L, U = ns["ssum"](state[i], state[j]), upper[k]
+            for dd in range(ns["dim"](L), ns["dim"](U) + 1):
+                for F in ns["subspaces_between"](L, U, dd):
+                    h, st = list(hist), list(state)
+                    for r in (i, j):
+                        g = ns["dim"](F) - ns["dim"](st[r])
+                        if g:
+                            h[g] += 1
+                        st[r] = F
+                    rec(k + 1, tuple(st), tuple(h))
+
+        rec(0, tuple(starts), (0,) * 10)
+        return out
+
+    def capped(p, k):
+        return sum(min(r, k) for r in p)
+
+    stats = {"windows": 0, "realisable_profiles": 0, "listed": 0, "refining_a_listed_partition": 0}
+    for w in wins:
+        lst = listed[w["index"]]
+        old = part(ns["actual_profile"](w["starts"], w["ends"], w["frames"]))
+        need(old in lst, f"incumbent listed, window {w['index']}")
+        need(all(sum(old) == sum(p) and all(capped(old, k) <= capped(p, k) for k in range(1, 10)) for p in lst),
+             f"incumbent dominates, window {w['index']}")
+        ms, _ = ns["matches"](*w["coefficients"], MAX_LEN)
+        realisable = set()
+        for word in ms:
+            realisable |= geo_profiles(w["starts"], w["ends"], word)
+        need(old in realisable, "incumbent realisable")
+        for R in realisable:
+            stats["realisable_profiles"] += 1
+            if R in lst:
+                stats["listed"] += 1
+            else:
+                need(any(refines(R, C) for C in lst), f"profile {R} refines a listed partition, window {w['index']}")
+                stats["refining_a_listed_partition"] += 1
+        stats["windows"] += 1
+    print(json.dumps({"status": "PASS_PR4585_GEOMETRY_SOUNDNESS", "max_word_length": MAX_LEN, **stats,
+                      "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())