diff --git a/research/pr5427-hold-head-receipt/README.md b/research/pr5427-hold-head-receipt/README.md new file mode 100644 index 0000000000..b18632c9b1 --- /dev/null +++ b/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. diff --git a/research/pr5427-hold-head-receipt/SOURCES.json b/research/pr5427-hold-head-receipt/SOURCES.json new file mode 100644 index 0000000000..8c1bee9912 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/pr5427-hold-head-receipt/TASK.json b/research/pr5427-hold-head-receipt/TASK.json new file mode 100644 index 0000000000..19696b8c88 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/pr5427-hold-head-receipt/VERIFY.json b/research/pr5427-hold-head-receipt/VERIFY.json new file mode 100644 index 0000000000..c8bca83ab8 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/pr5427-hold-head-receipt/verify.py b/research/pr5427-hold-head-receipt/verify.py new file mode 100644 index 0000000000..e5821fc4b8 --- /dev/null +++ b/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()