Cursor/pr5427 hold head receipt b562

research/pr5427-hold-head-receipt/README.md

@@ -0,0 +1,94 @@
+# Receipt for the four queue-oct24a holds, and the changed head of #5427
+
+**Task:** `overlap-receipt`, refined to one existing intake receipt.
+**Base:** canonical main `32890bc5de034ab8fc93ac88ead7279a6a416d04`.
+**No new κ. No closure, merge, or ledger edit.**
+
+The 2026-10-24 queue snapshot
+`docs/research/pr-intake-evidence/queue-oct24a-20261024.json` records 20
+decisions, of which four are `waiting_revision`: #4580, #4612, #5427 and
+#5432. The central ledger on this base still has those four open,
+partially reviewed, and not installed. Three of those recorded heads were
+still the GitHub heads when this note was written. **#5427 was not.**
+
+## What the retained receipt says
+
+| PR | Author on the receipt | Recorded head | Retained on this base |
+|---|---|---|---|
+| [#4580](https://github.com/CrocSwap/integer-mult-bounds/pull/4580) | Matarener | `55de56abdfd9cd7fb83758241793c18b9ae9ce71` | nothing |
+| [#4612](https://github.com/CrocSwap/integer-mult-bounds/pull/4612) | Matarener | `0e0df631da41a1f9ed3489e8df532189c2643cbf` | nothing |
+| [#5427](https://github.com/CrocSwap/integer-mult-bounds/pull/5427) | Matarener | `389578f2d3ef075495ce76f08100ac50e18f7d40` | nothing |
+| [#5432](https://github.com/CrocSwap/integer-mult-bounds/pull/5432) | hevlyo | `6532b45ce9f3259d7408594ec480a140ec81e0e2` | nothing |
+
+#5427's unresolved question is still Clear1nsight's Part 1 qualification:
+the head claims rational-span consequences from one modular calculation, the
+counterexample is `A=[p]`, `b=1`, and Part 2 is not independently accepted.
+Credit for that comment stays with Chris R / Clear1nsight. Credit for the
+ZQY census stays with Mark / Matarener.
+
+## What changed after the receipt
+
+GitHub on 2026-10-25 showed #5427 at
+`e0192de5d97e5ac09f42d26d9ceedee6377c77e2`
+(updated 2026-10-24T17:50:50Z). That commit's parents are exactly
+
+- `dacc35b1f35c2b4bc2e3910520ba5cf46a020bed` — "Compute every ZQY span exactly over Q instead of modulo 2^61-1", whose parent is the recorded head `389578f2`;
+- `32890bc5de034ab8fc93ac88ead7279a6a416d04` — this receipt's base.
+
+`dacc35b1f` is not contained in the base. The recorded hold therefore
+describes `389578f2` and does not describe the head that was live during
+this check. The intake rule that a different head wakes an entry applies
+to #5427 only. It does not, on these pins, apply to #4580, #4612 or #5432:
+those three GitHub heads matched the receipt on the same observation.
+
+On `dacc35b1f` the false sentence "non-membership modulo p therefore
+implies non-membership over the rationals" is gone from `PROOF.md`. The
+proof states the `A=[p]`, `b=1` counterexample. `verify.py` no longer
+assigns `P = (1 << 61) - 1` or takes a modular inverse. Its `Span.add`
+reports that `1` lies in the rational span of `p = 2^61-1`. An independent
+one-line check agrees: `p ≡ 0` modulo `p`, while `(1/p)·p = 1` over `Q`.
+
+## Author-checker replay, not acceptance
+
+At `e0192de5`, in `/tmp` on CPython 3.12.3:
+
+```sh
+python3 -I -W error -B research/zqy-observation-not-retained/verify.py
+```
+
+exited 0 and printed `PASS_ZQY_OBSERVATION_NOT_RETAINED`. The script
+compares its recomputation with the committed `RESULT.json`, so the
+recorded ranks matched that run. This is one replay of Matarener's
+checker. It is not an independent census, not a review of Part 2's
+EARLY/LATE or caller-output reading, and not a reason to merge. The
+`--left-depth 2` run and the optimised command were not run. The package
+was absent from base `32890bc5`.
+
+## Reproduce this receipt
+
+```sh
+python3 -B research/pr5427-hold-head-receipt/verify.py
+python3 -B scripts/research_package.py --package research/pr5427-hold-head-receipt --check-only
+```
+
+Expected marker: `PASS_PR5427_HOLD_HEAD_RECEIPT`.
+
+The checker reads the two receipt files, checks the commit parents above,
+and runs the one-column rational dependence on the repaired `Span` class.
+It does not contact GitHub. A later push of #5427 can move the live head
+without changing this historical observation.
+
+## Open next questions
+
+Re-read #5427 at `e0192de5` before any closure. The arithmetic sentence that
+blocked `389578f2` is not the text of `dacc35b1f`, but Part 2 was never
+accepted, and a passing author checker is not that acceptance. The blocker
+is a maintainer review of the new head; this receipt does not perform it.
+
+## Credit
+
+The queue-oct24a snapshot and the ledger rows are the maintained intake
+record on `32890bc5`. Clear1nsight wrote the Part 1 qualification at
+`389578f2`. Mark / Matarener wrote the ZQY package and the exact-Q repair.
+The package scaffold is Douglas Colkitt's. Prepared by unpaidmoon with
+substantial Cursor Grok assistance. Apache-2.0. No selected-frontier change.

research/pr5427-hold-head-receipt/SOURCES.json

@@ -0,0 +1,58 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "docs/research/pr-intake-evidence/queue-oct24a-20261024.json",
+      "usage": "input",
+      "git_blob": "f5f1ed6ba8330714a11f499c9849503101d80639",
+      "sha256": "65f6edd08052d7160a5318badea7c982e91252891a2cb02f7d8d24a8efc660e5"
+    },
+    {
+      "path": "docs/research/pr-ledger.json",
+      "usage": "input",
+      "git_blob": "0ef27eee22300a0a512af129a0d8778ae4af46ab",
+      "sha256": "30af48f6f9bb64c698feeeafcf5c68e5ff76f6175f8757ee6ff45566152d1529"
+    },
+    {
+      "path": "research/zqy-observation-not-retained/verify.py",
+      "usage": "provenance",
+      "pin": "head:389578f2d3ef075495ce76f08100ac50e18f7d40:research/zqy-observation-not-retained/verify.py",
+      "git_blob": "791a136c2711854e53a021a0040a976c4ded233b",
+      "sha256": "40fd198b79490c5897feb45cd8b6fbe9cf3f8f5c9e0215efb2b9973c8e92106a"
+    },
+    {
+      "path": "research/zqy-observation-not-retained/PROOF.md",
+      "usage": "provenance",
+      "pin": "head:389578f2d3ef075495ce76f08100ac50e18f7d40:research/zqy-observation-not-retained/PROOF.md",
+      "git_blob": "df5c291257f1957427ec1be4a5b2549464e0473d",
+      "sha256": "2aa0021037d3b3fa7419322d00fa0191cd064076eaf031175275ea0bfd902eab"
+    },
+    {
+      "path": "research/zqy-observation-not-retained/verify.py",
+      "usage": "provenance",
+      "pin": "head:dacc35b1f35c2b4bc2e3910520ba5cf46a020bed:research/zqy-observation-not-retained/verify.py",
+      "git_blob": "714261b7b91a58cff6bffcd2c9dbd7f88f3cf345",
+      "sha256": "ae307d2474a9cb6e5ea1ae3f723f2c28e22c04678672b757eaa675fa7b59363a"
+    },
+    {
+      "path": "research/zqy-observation-not-retained/PROOF.md",
+      "usage": "provenance",
+      "pin": "head:dacc35b1f35c2b4bc2e3910520ba5cf46a020bed:research/zqy-observation-not-retained/PROOF.md",
+      "git_blob": "87145494a75de26c10991d890341977ea3a193dc",
+      "sha256": "8eda309451f20ac25aff3746752060b95151799f65a6537dc59cb0aff758f25c"
+    }
+  ]
+}

research/pr5427-hold-head-receipt/TASK.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "task_id": "overlap-receipt",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "original_card": {
+    "id": "overlap-receipt",
+    "question": "What exact content and credit of a small named PR set has already been retained?",
+    "starting_points": [
+      "docs/research/pr-ledger.md",
+      "CONTRIBUTORS.md"
+    ],
+    "methods": [
+      "Compare exact heads and retained artifacts to write a source-bound disposition receipt.",
+      "Audit an existing receipt for missing content or predecessor attribution."
+    ],
+    "acceptance_gate": "Separate complete integration, partial retention and changed heads; make no autonomous closures.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read one small PR set in the ledger and identify exact reviewed heads and unresolved content.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Compare that set to retained artifacts; produce a complete or explicitly partial disposition receipt.",
+    "bottleneck_link": "Reliable overlap evidence preserves credit and prevents repeated review of already-retained material.",
+    "allowed_variations": [
+      "One small related PR family or one existing integration receipt."
+    ],
+    "scope_change_triggers": [
+      "Treating matching titles or one shared blob as proof of full incorporation."
+    ],
+    "overlap_terms": [
+      "overlap receipt",
+      "partial integration",
+      "attribution"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Audit the four waiting_revision rows of the queue-oct24a receipt and separate #5427's recorded modular head from its exact-Q child.",
+  "scope_change_reason": "The catalogue card allows one existing integration receipt. This audit names that receipt, the four unretained heads, and the one head that moved. It does not survey a new PR family or recommend a closure.",
+  "bottleneck_link": "Side result for review routing. A stale modular obstruction on #5427 mis-states whether the ZQY observation is rationally unavailable; that question is adjacent to a supplied-observation screen, but this receipt does not change kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the four-row receipt. Do not replay the ZQY census inside this package, edit the ledger, or close #5427.",
+  "outcome": "completed",
+  "evidence": "Verifier checks the pinned ledger and queue-oct24a rows, the parent link 389578f2 -> dacc35b1f -> e0192de5, removal of the false modular implication, and the repaired Span on A=[p], b=1. One author-checker replay at e0192de5 printed PASS_ZQY_OBSERVATION_NOT_RETAINED and is not acceptance.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance with the receipt, the checker, and the one author-checker replay.",
+  "open_questions": [
+    {
+      "question": "Does the exact-Q text at e0192de5 discharge only the Part 1 arithmetic hold, leaving Part 2 unaccepted?",
+      "why_it_matters": "Closing #5427 from the old sentence would treat a changed head as reviewed, and accepting Part 2 from a shared Span class would go beyond Clear1nsight's stated boundary.",
+      "first_step": "Re-read PROOF.md Part 2 and the EARLY/LATE caller tests at e0192de5, using the author replay only as a numerical control.",
+      "blocked_by": "This receipt does not review Part 2 and does not recommend a GitHub state change."
+    }
+  ]
+}

research/pr5427-hold-head-receipt/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "docs/research/pr-intake-evidence/queue-oct24a-20261024.json",
+    "docs/research/pr-ledger.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Four waiting_revision heads remain unretained in the pinned ledger and queue-oct24a snapshot; #5427's repair commit is the child of the recorded head and is not in the base; the false modular implication stays on the old proof; the repaired Span accepts 1 in the rational span of 2^61-1 and rejects an off-axis target."
+    }
+  ]
+}

research/pr5427-hold-head-receipt/verify.py

@@ -0,0 +1,155 @@
+#!/usr/bin/env python3
+"""Receipt check for the four waiting-revision rows in queue-oct24a.
+
+The retained ledger and intake snapshot still name PR #5427 head
+389578f2. That head's child, dacc35b1f, replaces the modular span with an
+exact rational span. This checker does not replay the ZQY census and does
+not close the pull request.
+"""
+
+import json
+import os
+import subprocess
+
+OLD = "389578f2d3ef075495ce76f08100ac50e18f7d40"
+REPAIR = "dacc35b1f35c2b4bc2e3910520ba5cf46a020bed"
+LIVE = "e0192de5d97e5ac09f42d26d9ceedee6377c77e2"
+BASE = "32890bc5de034ab8fc93ac88ead7279a6a416d04"
+PKG = "research/zqy-observation-not-retained"
+FALSE_IMPLICATION = (
+    "The computed non-membership modulo p therefore implies\n"
+    "non-membership over the rationals."
+)
+COUNTEREXAMPLE = "for `A = [p]`, `b = 1` the target is outside the modular"
+HOLDS = {
+    4580: "55de56abdfd9cd7fb83758241793c18b9ae9ce71",
+    4612: "0e0df631da41a1f9ed3489e8df532189c2643cbf",
+    5427: OLD,
+    5432: "6532b45ce9f3259d7408594ec480a140ec81e0e2",
+}
+
+ROOT = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
+
+
+def fail(message):
+    raise SystemExit(message)
+
+
+def git(*args):
+    result = subprocess.run(
+        ["git", *args], cwd=ROOT, check=False, capture_output=True, text=True,
+    )
+    if result.returncode != 0:
+        fail(args[0] + " failed: " + (result.stderr or result.stdout).strip())
+    return result.stdout.strip()
+
+
+def show(rev, path):
+    return subprocess.check_output(
+        ["git", "show", rev + ":" + path], cwd=ROOT,
+    ).decode("utf-8")
+
+
+def ancestor(commit, descendant):
+    result = subprocess.run(
+        ["git", "merge-base", "--is-ancestor", commit, descendant],
+        cwd=ROOT, check=False,
+    )
+    return result.returncode == 0
+
+
+def load_span(source):
+    start = source.index("class Span:")
+    end = source.index("\ndef modrow(")
+    namespace = {}
+    exec(
+        "from fractions import Fraction as Fr\nP = (1 << 61) - 1\n" + source[start:end],
+        namespace,
+    )
+    return namespace["Span"], namespace["Fr"]
+
+
+def member(span_cls, rows, target):
+    span = span_cls()
+    for row in rows:
+        span.add(dict(row))
+    return span.reduce(dict(target)) == {}
+
+
+def receipt_rows():
+    ledger = json.loads(
+        open(os.path.join(ROOT, "docs/research/pr-ledger.json"), encoding="utf-8").read()
+    )
+    intake = json.loads(
+        open(
+            os.path.join(ROOT, "docs/research/pr-intake-evidence/queue-oct24a-20261024.json"),
+            encoding="utf-8",
+        ).read()
+    )
+    by_number = {row["number"]: row for row in ledger["pull_requests"]}
+    contributions = {row["number"]: row for row in intake["contributions"]}
+    for number, head in HOLDS.items():
+        if number not in by_number or number not in contributions:
+            fail("missing receipt row " + str(number))
+        recorded = by_number[number]
+        decision = contributions[number]
+        if recorded["current_head"] != head or recorded["reviewed_head"] != head:
+            fail("ledger head moved for " + str(number))
+        if recorded["github_state"] != "OPEN" or recorded["disposition"] != "partially_reviewed":
+            fail("ledger state changed for " + str(number))
+        if recorded["closure"] is not None or recorded["integration_location"]:
+            fail("PR " + str(number) + " is recorded as retained")
+        if decision["head"] != head or decision["lane"] != "waiting_revision":
+            fail("intake row changed for " + str(number))
+    text = by_number[5427]["unresolved_question"]
+    if "A=[p]" not in text or "b=1" not in text or "Q certificate" not in text:
+        fail("ledger no longer states the modular-arithmetic hold")
+    if "Part 2 is not independently accepted" not in text:
+        fail("ledger dropped the Part 2 boundary")
+
+
+def commit_chain():
+    if git("rev-parse", REPAIR + "^") != OLD:
+        fail("repair commit is not the child of the recorded head")
+    parents = git("rev-parse", LIVE + "^@").split()
+    if parents != [REPAIR, BASE]:
+        fail("live head parents are " + " ".join(parents))
+    if ancestor(REPAIR, BASE):
+        fail("repair commit is already contained in the receipt base")
+    if not ancestor(OLD, REPAIR) or not ancestor(BASE, LIVE):
+        fail("expected ancestry does not hold")
+
+
+def arithmetic():
+    old_proof = show(OLD, PKG + "/PROOF.md")
+    new_proof = show(REPAIR, PKG + "/PROOF.md")
+    old_code = show(OLD, PKG + "/verify.py")
+    new_code = show(REPAIR, PKG + "/verify.py")
+    if FALSE_IMPLICATION not in old_proof or FALSE_IMPLICATION in new_proof:
+        fail("false modular implication is not confined to the recorded head")
+    if COUNTEREXAMPLE not in new_proof or COUNTEREXAMPLE in old_proof:
+        fail("reviewer counterexample is not stated on the repair head")
+    if "pow(v[c], P - 2, P)" not in old_code or "pow(v[c], P - 2, P)" in new_code:
+        fail("modular inverse is not confined to the recorded checker")
+    if "P = (1 << 61) - 1" not in old_code or "P = (1 << 61) - 1" in new_code:
+        fail("prime modulus assignment is not confined to the recorded checker")
+    new_span, fraction = load_span(new_code)
+    prime = (1 << 61) - 1
+    if not member(new_span, [{0: fraction(prime)}], {0: fraction(1)}):
+        fail("repaired Span missed the rational dependence 1 = (1/p) p")
+    if member(new_span, [{0: fraction(1)}], {1: fraction(1)}):
+        fail("repaired Span reported a vector outside a one-coordinate span")
+    # Independent of either checker: the Fp image of [p] is 0, while 1 = (1/p)·p over Q.
+    if prime % prime != 0 or fraction(1, prime) * prime != 1:
+        fail("counterexample arithmetic failed")
+
+
+def main():
+    receipt_rows()
+    commit_chain()
+    arithmetic()
+    print("PASS_PR5427_HOLD_HEAD_RECEIPT")
+
+
+if __name__ == "__main__":
+    main()