Verifier: audit_local.py accepts non-centre cut gates; additive guard and regression fixture (no new κ)

research/audit-local-cut-centre-guard/NOTICE.md

@@ -0,0 +1,15 @@
+# Notice
+
+`inputs/BASE-WORD.json.gz` and `inputs/EXTRA-WORD.json.gz` are unmodified copies of PR #1672's
+`research/gmx-t74-k554-signed-001/new/{gauge44,extra}-word-566.json.gz` (Jeremy Kothe / LeverRank, head b8ab040d),
+Apache-2.0, with that package's retained ancestry (PR #1625 mdumitrean; PR #1319, #1297, #1286 Rohan Arun; PR #1274
+Jeremy Kothe; PR #1193 Jeremy Diviney; PR #1148 Thomas DiFiore; PR #1196 chafreaky; PR #1195; the PR564/571/589/645
+lineage). Exact pins: `inputs/PINS.json`.
+
+`inputs/PROBE-CUT-502.json.gz` is derived from the base word in this work (see README) as a semantic counterexample.
+It is not a valid word.
+
+The audited checker, `research/gauge44-frames-x/independent/audit_local.py` (icekylinx, Apache-2.0), is used unchanged
+and pinned in `SOURCES.json`.
+
+New files: Marius-Paul Dumitrean, Apache-2.0, prepared with substantial AI assistance (Anthropic Claude, via Claude Code).

research/audit-local-cut-centre-guard/README.md

@@ -0,0 +1,70 @@
+# audit_local.py accepts non-centre cut gates (guard and regression fixture, no new κ)
+
+**Finding.** The independent local auditor `research/gauge44-frames-x/independent/audit_local.py` climbs frames only in
+sections A and B. In the cut it checks only gates whose source is one of the word's eight centres (the centre-path
+rule). A cut gate with any other source is applied to the scalar map but never frame-checked. A word can therefore move
+priced work into the unpriced cut and still pass, with an understated paid profile.
+
+**Counterexample** (`inputs/PROBE-CUT-502.json.gz`). Start from the genuine base word of the pivot-566+554 T74 supplier
+(`inputs/BASE-WORD.json.gz`, PR #1672). Make width-9 helper 502 entering (start frame of dimension 1 instead of 0), so its
+width drops from 9 to 8. Cancel its initial-value leak with four cut gates `200/203/205/206 += ±½ · 502`, and re-time its
+two A-section writes into B.
+- The unchanged auditor run with `--main` **passes** it: compensation 7,204 gates instead of 7,208, 193 entering helpers instead of 192, local
+  profile `{2: 501, 3: 415}` instead of `{2: 500, 3: 416}`. That is one rank level less, about 2.1M units per call, which
+  would be worth roughly +8e-8 κ through the hosting.
+- The native provider chain **rejects** it at its second step: `hpe_emit_local.py` fails with `emitted column mismatch`
+  at register 153 (`evidence/NATIVE-PROBE.txt`). The base word passes all five native steps.
+
+So the gap does not affect claims whose admission includes the native chain, which every T74 claim does. It does
+affect any acceptance that relies on `audit_local.py` alone.
+
+**Guard** (`guard.py`, standard library). Every cut gate must be an `add` whose source is a centre and whose target is a
+target row (`v <= t < 2v`). This is the structure of every genuine word, and the native emitter relies on it.
+- It accepts all 146 genuine words found at the base commit (every `CANONICAL-WORD`/`FULL-WORD` file with a cut) and both
+  supplier words (`evidence/GUARD-GENUINE-WORDS.json`).
+- It rejects exactly the probe's four gates (`evidence/GUARD-PROBE.json`).
+
+`audit_local.py` is pinned by hash in 421 files at the base commit, so this package does not modify it. The guard is
+additive: run it alongside the auditor, or fold it into a new auditor version.
+
+## Reproduce
+
+```sh
+python3.12 scripts/research_package.py --package research/audit-local-cut-centre-guard
+python3 -B research/audit-local-cut-centre-guard/guard.py WORD.json.gz
+```
+
+`verify.py` checks the input pins and runs the unchanged auditor on the base and probe words; both pass, and the
+receipts equal `evidence/AUDIT-*.json`. The pins cover the three words and two repository files, which are declared in
+both `VERIFY.json` and `SOURCES.json`: the auditor, and the parent `CANONICAL-WORD.json.gz` (PR622 baseline558
+split-centres) that its `--main` interface check reads. The package plus those two files is enough: `verify.py` also
+passes in a Git-free export that contains nothing else. It then runs the guard on all three words and two mutation controls (a
+non-centre cut source, a non-target cut row). It takes a few seconds. The native rejection is recorded evidence, not
+rerun.
+
+## Scope
+
+This audits one condition: frames of cut gates in the local auditor. It is not a new construction and gives no κ. The
+counterexample is built on the pending T74 supplier's base word, which is not in main; the auditor and guard are the
+same for the selected line's words.
+
+## Open next questions
+
+- **Version the guard into the auditor.** The first step is done. ywz65's
+  [handoff](https://github.com/CrocSwap/integer-mult-bounds/pull/2478#issuecomment-6192363481) found seven registered
+  packages that actually call `audit_local.py`; eleven more only hash it, and five use other checkers. Their committed
+  words pass `guard.py` with the same 176-gate cut (re-run here on the six distinct words). Their admitted mutation
+  families do not change the cut, so no existing claim is shown to use the gap. Adoption by those callers is blocked on a
+  maintainer decision about versioning a pinned auditor.
+- **Check the other unpriced sections.** The precondition, the derived compensation and the frame-free cleanup could
+  admit analogous counterexamples. For each one, state the structural rule the native emitter assumes and test it with
+  a constructed word, as here.
+
+## Credit
+
+The auditor is icekylinx's gauge44-frames-x package. The words are PR #1672's (Jeremy Kothe / LeverRank) pivot-554 kernel on
+PR #1625's pivot-566 words (mdumitrean), in the PR #1319/#1297 lineage (Rohan Arun) and its retained ancestry. The native
+chain is PR635's vendored scripts, run through PR #1186's toolkit. The registered-consumer screen is ywz65's (see the
+open questions). See `NOTICE.md`.
+
+Prepared by Marius-Paul Dumitrean with substantial AI assistance (Anthropic Claude, via Claude Code). Apache-2.0.

research/audit-local-cut-centre-guard/SOURCES.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "research/gauge44-frames-x/independent/audit_local.py",
+      "usage": "input",
+      "git_blob": "4744d8783c25bf7bf5076886169077ca3808309a",
+      "sha256": "03afcfc9da428b3f6edac81c1fee7f277ab81b64998efae78380b63498dec6cd"
+    },
+    {
+      "path": "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/CANONICAL-WORD.json.gz",
+      "usage": "input",
+      "git_blob": "a2e5a1ffd454a353bd2d2100bc26259ff5b57af7",
+      "sha256": "66d3c3c70983224650643a0a05a21ac6c6959f84d0f4528650601016f5a76844",
+      "source_commit": "5c5567d15bd019186519a4db267914257b5f1ac0",
+      "note": "Read by audit_local.py --main (check_parent_interface: the transported centre/port interface). Same bytes at base_commit; last changed by source_commit."
+    }
+  ]
+}

research/audit-local-cut-centre-guard/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "supplier-boundary-audit",
+  "priority_revision": 4,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "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": "refined",
+  "actual_scope": "Does the local-word frame obligation checked by research/gauge44-frames-x/independent/audit_local.py follow from its source-bound checks for every section of the word? Audited condition: frames of cut gates.",
+  "scope_change_reason": "The card asks for one selected supplier obligation; the audited checker is the local-word auditor used by the selected and the pending T74 supplier lines, and the semantic counterexample is built on the pending T74 supplier base word because that is where the gap appeared.",
+  "bottleneck_link": "An acceptance gap in the local auditor can admit a word whose paid profile is understated; closing it strengthens every package that relies on this auditor without the native chain. No kappa changes.",
+  "budget_minutes": 90,
+  "stop_rule": "Stop after one semantic counterexample, one guard that accepts every genuine word checked and rejects the counterexample, and two mutation controls.",
+  "outcome": "completed",
+  "evidence": "evidence/AUDIT-BASE.json and AUDIT-PROBE.json (the unchanged auditor passes both); evidence/GUARD-PROBE.json (the four non-centre cut gates); evidence/GUARD-GENUINE-WORDS.json (146 genuine words at the base commit plus the supplier words: no violation); evidence/NATIVE-PROBE.txt (the native chain rejects the probe at hpe_emit_local.py).",
+  "author": "Marius-Paul Dumitrean",
+  "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code): search, construction of the counterexample, code, runs, analysis and text.",
+  "open_questions": [
+    {
+      "question": "Should the guard become part of a new version of the local auditor (or of the registered replays that call it)?",
+      "why_it_matters": "audit_local.py is pinned by hash in 421 files at the base commit, so it is not changed here; packages that rely on it without the native chain inherit the gap.",
+      "first_step": "Done for the registered packages by ywz65 (https://github.com/CrocSwap/integer-mult-bounds/pull/2478#issuecomment-6192363481): seven actual callers of the auditor at the base commit; their committed words pass guard.py with the same 176-gate cut. Next: choose how a versioned auditor (or a guard step before it) is adopted by those callers.",
+      "blocked_by": "A maintainer decision on how to version a pinned auditor."
+    },
+    {
+      "question": "Do the other unpriced sections (precondition, derived compensation, frame-free cleanup) admit analogous counterexamples?",
+      "why_it_matters": "The cut gap shows the auditor trusts structure it does not check; the precondition and cleanup are also frame-free.",
+      "first_step": "For each section, write the structural rule the native emitter assumes and test it against a constructed word as here.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/audit-local-cut-centre-guard/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/gauge44-frames-x/independent/audit_local.py",
+    "research/community-k492-audit/pr622/replay/baseline558/complex-global/base/split-centres/CANONICAL-WORD.json.gz"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "SHA-256/Git-blob pins of the package inputs and of both declared repository inputs (the auditor and the parent CANONICAL-WORD that its --main interface check reads); the unchanged audit_local.py --main PASSES both the genuine base word and the probe word with four non-centre cut gates (receipts equal evidence/AUDIT-*.json); guard.py passes the genuine base and extra words and rejects exactly the probe's four cut gates; two mutation controls (non-centre cut source, non-target cut row) are rejected. The native chain's rejection of the probe is recorded evidence, not rerun."
+    }
+  ]
+}

research/audit-local-cut-centre-guard/evidence/AUDIT-BASE.json

@@ -0,0 +1,13 @@
+{
+ "compensation_gates": 7208,
+ "entering": 192,
+ "local_profile": {
+  "1": 2348,
+  "2": 500,
+  "3": 416,
+  "4": 130,
+  "5": 82,
+  "8": 8
+ },
+ "status": "PASS_INDEPENDENT_EXACT_FORWARD_AND_DUAL_ENDPOINT_FRAMES_ENTRANCES_CONES"
+}

research/audit-local-cut-centre-guard/evidence/AUDIT-PROBE.json

@@ -0,0 +1,13 @@
+{
+ "compensation_gates": 7204,
+ "entering": 193,
+ "local_profile": {
+  "1": 2348,
+  "2": 501,
+  "3": 415,
+  "4": 130,
+  "5": 82,
+  "8": 8
+ },
+ "status": "PASS_INDEPENDENT_EXACT_FORWARD_AND_DUAL_ENDPOINT_FRAMES_ENTRANCES_CONES"
+}