Audit the separated A2 composition and cleanup split

research/staged544-a2-composition-audit/README.md

@@ -0,0 +1,88 @@
+# Independent acceptance of the separated A2 composition
+
+**Audit of an existing scalar identity. No new κ. Selected κ stays 0.001672660197076918.**
+
+## Scope and evidence
+
+Original card: `independent-moment`, scope **changed**. The card's #2979 group audit is already
+covered by open V45 work (#3543, #3911) and the merged group A–D native-width audits. This package
+takes the still-open handoff on
+[discussion #1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19036786):
+independently accept the composition and projected-cleanup argument in
+[PR #4019](https://github.com/CrocSwap/integer-mult-bounds/pull/4019), head
+`f408e09df300b575235f7f77f81948071397e16d`.
+
+The two rational identities, for distinct registers `x, y, z` and nonzero rationals `a, b`, are
+
+```text
+[S(a), T(b), U(-ab)] = [T(b), S(a)]
+[U(ab), T(b), S(a)]  = [S(a), T(b)]
+```
+
+with `S(a): y += a*z`, `T(b): x += b*y`, and `U(c): x += c*z`. Both sides of the first identity end at
+`(x + b*y, y + a*z, z)`. Both sides of the second end at `(x + b*y + ab*z, y + a*z, z)`, for an
+arbitrary initial triple. The checker proves those endpoints, and the same maps as 3×3 matrices,
+before it looks at a word.
+
+On both vendored provider words the eight published sites each match exactly one identity:
+
+| Section | Indices | Identity | Removed record | New-site cleanup effect |
+|---|---|---|---|---|
+| A | 1858, 1859, 1860 | first, drop `U` | credited PR #3998 site | not counted in the new split |
+| B | 4, 53, 54 | second, drop `U` | target write | helper ADD unchanged |
+| B | 7, 49, 50 | second, drop `U` | target write | helper ADD unchanged |
+| restore | 20, 21, 36 | first, drop `U` | non-target write | one cleanup ADD |
+| restore | 22, 23, 38 | first, drop `U` | non-target write | one cleanup ADD |
+| restore | 26, 27, 51 | first, drop `U` | non-target write | one cleanup ADD |
+| restore | 30, 31, 62 | first, drop `U` | non-target write | one cleanup ADD |
+| restore | 32, 33, 73 | first, drop `U` | non-target write | one cleanup ADD |
+
+Every intervening scalar event misses the site's three registers. The eight supports are pairwise
+disjoint. No new B window contains a native-warp index, and the A site starts at or after the
+prelude. The seven new published replacements equal the identity's right-hand side, including the
+ordered frame list. The credited A1858 replacement has the same ADD edges and the same frame span,
+but the ordered frame is `[42, 82]` rather than the source `[82, 42]`, which PR #4019 already
+discloses. The new record split is **7 forward ADD deletions and 5 projected-cleanup ADD deletions**.
+That is one forward deletion at each new site, and a cleanup deletion only where the deleted ADD
+does not write a target.
+
+This is an acceptance of that composition and record split. It is not a second recursive-histogram
+replay, not a check that PR #4041's later-word transfer is valid, and not a κ claim. The predecessor
+states that the histogram stays `{1:2440, 2:725, 3:224, 4:102, 5:20, 8:8}`. This package does not
+recompute those ranks.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/staged544-a2-composition-audit
+```
+
+Expected marker:
+
+```text
+PASS_A2_COMPOSITION_AUDIT providers=2 sites=8 new_forward_adds=7 new_cleanup_adds=5 known_frame_order_swaps=2 controls=3 no_new_kappa
+```
+
+The three controls reject a flipped B4 coefficient, an intervening read of register 518, and the
+identity-one endpoint under the wrong `U` sign. Inputs are the two compressed provider words and
+`inputs/data.json` taken from PR #4019 at the head above. Their SHA256 pins are checked before use.
+Base commit is `bb4bccbf42844d2801487450727c2f63e10d1d0f`. Priority revision 6.
+
+## Open next questions
+
+- Does one later exact provider word, in particular a PR #3945 word, admit these same contractions?
+  Pin that word and recheck every index, boundary, intervening support, cleanup count and paid
+  profile. This package has only the two PR3734 providers.
+- Can a different scalar graph remove a paid frame transition? Name the changed boundary and a
+  complete favorable bill first. These seven sites do not, by themselves, move a rank count.
+
+## Credit
+
+Chris R / Clear1nsight, PR #3998, for the A2 identity and the consecutive A1858 contraction.
+ToikY, PR #4019, for the seven separated witnesses, the published receipt, and the stated endpoint
+argument accepted here. Dataisfire for the PR3734 words retained by that package. The ordered-frame
+swap on the credited site is their disclosure, not a new defect. New audit by unpaidmoon with
+substantial Cursor Grok assistance. Apache-2.0. No independent human or formal-kernel review is
+claimed.

research/staged544-a2-composition-audit/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}

research/staged544-a2-composition-audit/TASK.json

@@ -0,0 +1,72 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 6,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/rank7-joint-endframes/README.md",
+      "docs/research/research-family-status.md"
+    ],
+    "methods": [
+      "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.",
+      "Implement certified moment inequalities through a different exact enclosure method."
+    ],
+    "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": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.",
+    "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.",
+      "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Independently accept or refute the two rational A2 identities and the projected-cleanup record split on the eight frozen PR3734 sites published by PR #4019, for both providers.",
+  "scope_change_reason": "The catalogue card's stated first audit is one #2979 rank-7 group and its single-change control. That group work is already in open PRs, including #3543 and #3911 for V45 and the merged group A-D native-width audits. This package instead takes the still-open #1166 request to independently accept PR #4019's separated A2 composition and projected-cleanup argument. The scalar-record identity is a different implication from the #2979 joint-frame invoice.",
+  "bottleneck_link": "A scalar ADD deletion changes the multiplication exponent only when the paid profile changes. Accepting this contraction, while its seven new sites remove no rank, blocks treating the ADD count as a moment improvement.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after both frozen providers and all eight published sites are classified, the seven-site record split is checked, and the three negative controls reject. Do not search for further sites or reprice the recursive histogram.",
+  "outcome": "completed",
+  "evidence": "Separate exact-rational endpoint and matrix checks accept both proof identities. On both vendored PR #4019 provider words, all eight sites match exactly one identity, intervening scalar events miss the three-register support, the eight supports are pairwise disjoint, and the seven new published replacements equal the identity right-hand side including ordered frames. The new record split is 7 forward ADD deletions and 5 projected-cleanup ADD deletions. The credited A1858 replacement differs only by the disclosed ordered-frame swap [82, 42] versus [42, 82]. Three semantic controls reject.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance with the audit implementation and write-up.",
+  "open_questions": [
+    {
+      "question": "Does one later exact provider word, in particular a PR #3945 word, admit these same contractions?",
+      "why_it_matters": "PR #4041 reports a transfer onto later words. This audit certifies only the two PR3734 providers vendored from PR #4019, so that transfer is not accepted here.",
+      "first_step": "Pin the later word bytes, recheck every source index, section boundary, intervening support and projected-cleanup count, then compare the full paid profile.",
+      "blocked_by": "The vendored inputs are only BORROW-WORD-base and BORROW-WORD-extra at the PR #4019 head. No later word is in this package."
+    },
+    {
+      "question": "Can a different scalar graph remove a paid frame transition rather than only an ADD record?",
+      "why_it_matters": "These seven sites leave every rank count unchanged, so they do not move the recursive moment.",
+      "first_step": "Name one changed frame boundary and a complete favorable bill before searching another separated motif.",
+      "blocked_by": "This audit does not recompute the recursive histogram; the predecessor states that histogram is unchanged, and that claim is outside this certificate."
+    }
+  ]
+}

research/staged544-a2-composition-audit/VERIFY.json

@@ -0,0 +1,22 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/staged544-a2-composition-audit/inputs/BORROW-WORD-base.json.gz",
+    "research/staged544-a2-composition-audit/inputs/BORROW-WORD-extra.json.gz",
+    "research/staged544-a2-composition-audit/inputs/data.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact endpoint formulas, both provider words, eight site classifications, projected-cleanup record split, and three rejection controls"
+    }
+  ]
+}