Independent verification: #2802's seven-stage increment over #2751 (retired5 + retired7 stages) passes 28/28 rules and 20/20 controls; covers #2818's identical construction (no κ)

research/t74-retired7-increment-audit/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "544a7e82810e30cab61c297cb2e2ea86127fe944",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "889b95d936746df124872133ae1e7cc339adcb92",
+      "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6"
+    }
+  ]
+}

research/t74-retired7-increment-audit/TASK.json

@@ -0,0 +1,72 @@
+{
+  "schema_version": 1,
+  "task_id": "supplier-boundary-audit",
+  "priority_revision": 5,
+  "base_commit": "544a7e82810e30cab61c297cb2e2ea86127fe944",
+  "original_card": {
+    "id": "supplier-boundary-audit",
+    "question": "Does one selected supplier obligation follow from its actual source-bound checks?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/owner-boundary-audit/README.md"
+    ],
+    "methods": [
+      "Trace one hypothesis through the source, checker and complete caller.",
+      "Construct one semantically invalid but superficially well-formed fixture and test rejection."
+    ],
+    "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/owner-boundary-audit/verify.py"
+      ],
+      "expected": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT",
+      "inspect": "Identify why the timing-only omission passes but the full production controller still rejects it.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Choose one current supplier obligation and trace whether its acceptance depends on an independent check.",
+    "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.",
+    "allowed_variations": [
+      "Audit one named current condition using a new semantic counterexample."
+    ],
+    "scope_change_triggers": [
+      "Reporting the historical timing-only diagnostic as a new current acceptance bug."
+    ],
+    "overlap_terms": [
+      "owner boundary",
+      "bridge omission",
+      "hosting"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Adversarial audit of PR #2802's seven-stage increment (head 17b2ee6e) over its parent PR #2751 (head 4cfbb0cc): the retired5 stages refit5/alias5/refit5c and the retired7 stages refit7/hostmove2/alias7/refit7c (seven retired-lender aliases, two hostee moves, refits) and the FILL2751->FILL transform, checked with fresh exact code on both words: event diff, per-register occupancy timeline, forward/dual free-algebra replay plus a matrix realisation, GF(2) warp frames, refit exactness and above-floor neutrality, profile/inventory recount by two subspace representations, the 271,728-role fill with word-derived R, complete profile/mass/root, and attribution against PR #2766's pinned word and #2802's recorded retired5 evidence. The verdict extends to PR #2818 (head 175822ae), whose words/fill/order/providers are byte-identical, and covers the shared word-level base of #2824, #2827, #2833, #2839 and #2843 (their own later stages are not checked).",
+  "scope_change_reason": "The card asks whether one selected-supplier obligation follows from its source-bound checks. The selected supplier is unchanged. The audited object is instead the pending T74 construction of #2802 (repackaged by #2818, and the base of #2824/#2827/#2833/#2839/#2843 as of 2026-10-16 02:10 UTC): it changed two acceptance checks (R read from the providers; the A-retired-lender alias control), and its new construction had no independent check. The maintainer's T74 reviews (community-efficient1000, #1992 row) ask to separate the actual new construction from inherited ancestors.",
+  "bottleneck_link": "A defect would remove the +5.38e-7 kappa margin of #2802/#2818 over #2766/#2767 and the shared base of #2824/#2827/#2833/#2839/#2843; a pass is necessary but not sufficient (T74/#1319 admission, native lowering and the PR1673 outer proof remain). It also settles the two changed acceptance checks: R is bound to the words, and alias occupancy holds for the shipped words but is a conformance property, not a kappa-soundness condition, in the finite model: no check on the pricing path reads it, and a lender's dead last write (after its last read) moved past its alias warp to the end of restore at frame FULL (C4d/C4e) still replays correctly and is identically priced, while a moved read (C4f) or a moved write the lender still reads (C4g) is rejected by both replays.",
+  "budget_minutes": 180,
+  "stop_rule": "Publish an independent verification if S1, S2 and S5 pass, S3/S4/S6 agree and every negative control is rejected by its named rule; on any mismatch minimise a witness, post a FINDING in #2612 and ship a negative result without repair. No search; #2751's twelve-source recovery treated as a pinned parent.",
+  "outcome": "completed",
+  "evidence": "verify.py --fetch: PASS_T74_RETIRED7_INCREMENT_AUDIT rules=28/28 controls=20/20 (about 2 minutes). Both words: 63 relabelled B gates = 63 declared edit pairs (alias5 35, hostmove2 14, alias7 14); 62 frame changes = 62 declared refit frames; nothing else changed; 704 register segments (632 + 72 = 639 + 65) each exactly one parent role (lenders 401/403 last act at A3175/A3174 before warps at B259/B262; 550-553/562 at B901-B910; 564/565 at B911/B912 before B941/B944); forward+dual replay over Q<free group> on 632 live inputs with 72 zero buffers and the re-derived 4547-item cleanup; 4x4 matrix realisation mod 2^61-1; 72 B warps + 24 prelude warp items with G(U)=E and U the propagated frame; refit floors 26/26, 25/32, 2/2, 2/2, the 7 above-floor refit5c frames cost-neutral; profile {1:2382,2:648,3:268,4:128,5:26,8:8}, inventory {4:26,5:2,7:62,8:78,9:240}; fill R=408 from the words, 271728 roles, idle {1:17316,3:6594,5:9878,32:1,48:26558}, FILL = FILL2751 minus 4662 roles; complete profile and mass 4816512; f(C) < 66304 < f(C+1e-24) with a written error budget. Attribution: PR #2766's own word differs from W2751 only at B1151; the other 19 frames #2802 lists with it are cost-neutral; the reconstructed retired5 state reproduces #2802's recorded retired5 endpoint 0.001717409316335491643448, local profile and fill sha256 3501f6bd...; the retired7 stages add 385667783143020379/10^24 over retired5 (the split #2802 states). Occupancy controls: a lender's last (dead) write moved past its alias warp is accepted by both scalar replays (C4a-C4e); at frame FULL (C4d/C4e) also by the frame chain, recount, refits, stage records, fill and price, and rejected only by OCC-TIMELINE plus the undeclared-edit checks; a moved lender read (C4f) and a moved write that precedes the lender's last read (C4g, A3158) are rejected by both replays and accepted by the frame chain, fill and price. #2818 identical.",
+  "author": "thakrarsagar",
+  "ai_assistance": "Substantial AI assistance: Claude (Anthropic, Claude Opus 5.5) wrote and ran increment_audit.py, increment_controls.py and verify.py from the written model (PR2226 PROOF.md, PR README text and the JSON layouts); PR code was read as pinned data only and never imported or executed. AI review passes in the same loop (reproducibility, mathematics, provenance, referee) reviewed the package in two rounds and two revisions addressed their findings. No human has hand-checked the findings.",
+  "open_questions": [
+    {
+      "question": "Does any layer outside the finite BORROW-WORD model rely on alias occupancy (no lender event at or after its alias warp)?",
+      "why_it_matters": "In the finite model no pricing check reads occupancy, and a lender's dead last write moved past its alias warp to the end of restore at frame FULL (C4d/C4e) is a correct, identically priced word, so occupancy matters only if the native lowering, physical hosting or routing treats a warp as a register hand-over point.",
+      "first_step": "Inspect whether #2802's native lowering assigns roles per register segment; if so, add a C4d-type mutant against #2802's stage-structure check and an occupancy predicate to #2818's retired7 patch check (optional regression controls otherwise).",
+      "blocked_by": "Not blocked by access: #2802's full_replay.py downloads and authenticates the 491 pinned PR2679 files and rebuilds the native providers (needs #2802's requirements.txt; author-recorded cold run 411 s); an independent check should read its outputs as data."
+    },
+    {
+      "question": "Is the whole refit frame assignment (refit5c/refit7c, 'certified optimal') optimal under the moment cost?",
+      "why_it_matters": "A better assignment could only raise kappa; it cannot invalidate the checked value, and the seven above-floor refit5c frames are cost-neutral.",
+      "first_step": "Run an independent exact optimiser over all gates' frames with the same COPY pricing.",
+      "blocked_by": "A written objective for the #1186 optimal_frames certificate."
+    },
+    {
+      "question": "Do the new warps 30, 31 and 66-72 have exact native Clifford/Gaussian lifts in both orientations?",
+      "why_it_matters": "#2802's release records native warp-recipe checks, but this audit checks K_G only through its binary-symplectic image.",
+      "first_step": "Instantiate the exact Gaussian products of each new K_G and check every column, as PR2226 did for its 80 pairs.",
+      "blocked_by": "Not blocked by access: the native inputs are rebuilt by #2802's full_replay.py from the pinned PR2679 sources (as for question 1)."
+    }
+  ]
+}

research/t74-retired7-increment-audit/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py",
+        "--fetch"
+      ],
+      "timeout_seconds": 600,
+      "checks": "fetches PR #2802/#2751/#2818/#2766 heads only if absent (inputs pinned by sha256); 28 named rules on both words: event diff, occupancy timeline, free-algebra and matrix replays, GF(2) warps/refits and above-floor neutrality, profile, fill with word-derived R, complete profile/mass/root, #2818 identity, #2751 positive control, stage-chain rebuild, attribution against PR #2766's word and #2802's recorded retired5 evidence; 20 negative controls, each rejected by its named rule, seven also accepted by named rules"
+    }
+  ]
+}