Audit (no κ): PR3259's P104 fixed-cover support cut is valid but loose; under PR3427's one-helper criterion 2,682 of 4,992 required entries are unsupported and rank(U−I) ≥ 23

research/p104-fixed-cover-cut-review/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "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"
+    },
+    {
+      "path": "research/p104-joint-unit-flags/CERTIFICATE.json",
+      "usage": "input",
+      "git_blob": "0fa7d2d40566e92f3ea1539723abf438ba65adb8",
+      "sha256": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128"
+    },
+    {
+      "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json",
+      "usage": "input",
+      "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706",
+      "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e"
+    },
+    {
+      "path": "research/p104-native-channel/inputs/P104-FIXTURE.json",
+      "usage": "input",
+      "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9",
+      "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4"
+    }
+  ]
+}

research/p104-fixed-cover-cut-review/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "p104-side-correction",
+  "priority_revision": 6,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "original_card": {
+    "id": "p104-side-correction",
+    "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/p104-native-channel/README.md",
+      "research/p104-native-channel/PROOF.md",
+      "docs/research/community-efficient1000-review.md",
+      "research/p104-joint-unit-flags/README.md"
+    ],
+    "methods": [
+      "Construct one side-correction word at an explicit chronological cut with the needed frames still available.",
+      "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget."
+    ],
+    "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.",
+      "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission."
+    },
+    "first_experiment": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.",
+    "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.",
+    "allowed_variations": [
+      "One correction factorization, one chronological cut, or one explicit hosting obstruction.",
+      "A changed correction schedule with an updated full bill and native frame contract."
+    ],
+    "scope_change_triggers": [
+      "Recompiling the already certified low-rank channel without closing a new obligation.",
+      "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.",
+      "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.",
+      "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful."
+    ],
+    "overlap_terms": [
+      "P104",
+      "I-G/2",
+      "side correction",
+      "native channel",
+      "1972",
+      "1991",
+      "2586",
+      "endpoint transport",
+      "physical dual",
+      "relay composition",
+      "2981",
+      "joint unit flags",
+      "acquisition delivery",
+      "static nesting"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #2981 reports static joint endpoint flags and a matching of 208 departure and arrival flags; archival intake is not independent verification.",
+        "evidence": "research/p104-joint-unit-flags/README.md",
+        "remaining": "Independent flag check and a chronological coefficient program with dirty restoration and a complete cost.",
+        "status": "author-checked",
+        "source_commit": "3d24b92d8ba057b57cb2d480170ec407520e6882",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Independent hypothesis-by-hypothesis review of the PR3259 fixed-cover support-cut embedding argument (and PR3252's memory-relaxation proof, and what PR3427 consumes). PR3427's one-recombined-helper criterion (which PR3427 already calls exact for the pooled untimed relaxation) is re-proved and evaluated on all 104 columns, with its closed form, vertex cover and rank consequences, single-relaxation support rows and a small-domain exhaustive check. Audit only; author-checked and AI-assisted.",
+  "scope_change_reason": "The card asks for a chronological correction program. The revision-6 decisions table (row 1) instead asks first for a review of the submitted #3259 support cut and its contract, which decides whether the fixed-cover route is closed and what any reopening must cover. No construction is attempted.",
+  "bottleneck_link": "Decides whether the pooled fixed-cover, frozen-path, immutable-X, unread-Y, independent-dirt, monotone equal-frame P104 contract is closed and how large its obstruction is (2,682 unsupported required entries, not one), which bounds what a contract change or source preconditioner must reopen before any construction round.",
+  "budget_minutes": 150,
+  "stop_rule": "Stop at a proof-review verdict per step; on an engine disagreement, a proof gap or an oracle escape, stop and minimize. No matching search, no correction construction, no pricing beyond counting witness operations, at most three new relaxation rows, no Lean. Deviation: five rows were delivered, relaxing three hypotheses (K5 as R1, R1c and R1u, the last added at a round-1 review's request; K1 as R2; K6 as R3).",
+  "outcome": "completed",
+  "evidence": "PROOF-REVIEW.md (step table a-h, lemma proof, PR3252 review, PR3427 consumption, rank consequence, load-bearing rows); verify.py (exact channel run of 4,058 events: Y increment = G/2; layered control reproducing PR3259 numbers; sharp support by one criterion in two loop orders and by an independent PR3252 full-memory recurrence over all 104 columns (PR3427 ran the same operations on its four columns), all equal, shape = 2,309 own port pairs + (73,83), with routes asserted (31 own pairs also admitted by another type; (73,83) only by type (17,147), X83's dim-4 frame to Y73's cap); PR3427 four-column masks, which exclude 92 required entries that PR3259's test grants; perfect matching of the 2,682 missing entries (vertex cover 104); rank(U-I)>=23 from a maximum independent 23x23 principal block, size checked by two exact searches, rank by Fraction elimination, det(2C[S,S])=2^30 by Bareiss; rank(G/2)=8, so any unsupported rectangle has rank at most 31; rows R1/R1u/R1c/R2/R3; 9,000 seeded small instances with exhaustive untimed reachability, 13,242 realized checked programs and 18,000 random legal programs (9,000 directed, run in the checked interpreter; 9,000 uniform, legal by construction), exact Fractions; six in-verifier contract-violation controls); test_verify.py (seven tests: four defect controls with their own FAIL messages and three fact checks, including a containment-free variant that grants an unreachable pair).",
+  "author": "Sagar Thakrar (thakrarsagar)",
+  "ai_assistance": "Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for analysis, code and writing. No independent human or formal-kernel review is claimed.",
+  "open_questions": [
+    {
+      "question": "What rank does the full unsupported pattern force on a P104 source preconditioner (U-I)?",
+      "why_it_matters": "A maximum unsupported principal block already gives rank(U-I)>=23 versus PR3427's 4, and no principal block does better; a non-principal rectangle or a min-rank completion of -C on all 8,506 unsupported pairs may force more and would further constrain joint native source preparation. Any unsupported rectangle C[R,S] has rank at most |R & S| + 8 <= 31, since the common ports R & S are independent and rank(G/2) = 8 (asserted).",
+      "first_step": "Search non-principal rectangles up to the cap of 31, or bound the min-rank completion exactly, with the pinned sharp support; no matching search.",
+      "blocked_by": "Nothing beyond the sharp support certificate here; pricing a joint preparation remains separate."
+    },
+    {
+      "question": "Which changed contract supports all 4,992 required entries, in particular the 2,682 sharp-missing ones, at least cost, and what is its full bill?",
+      "why_it_matters": "Under the present cover the supported entries are exactly those whose own slot pair is compatible, plus (73,83); relaxing the cover (R2) reopens every entry at support level, but its cost is unknown. The missing entries need a vertex cover of 104, so path changes alone must touch at least 104 registers. Pending #3618's T48 (one target lift, +2 rank mass, a whole row) changes the target path instead and is the first priced data point; additivity across rows is not established.",
+      "first_step": "Name the changed hypothesis among K1-K7 (or added storage), support all 4,992 required entries at support level (a changed cover or path can lose some of the 2,310 pairs supported now), and list each added operation.",
+      "blocked_by": "Coefficients, dirty restoration, chronology, native/hosting/precision/consumer costs are unknown."
+    },
+    {
+      "question": "Is there a coefficient-level correction that reads channel state (R1c/R3) and restores it?",
+      "why_it_matters": "Channel state already carries the support of G/2, so support tests reopen everything; only a coefficient-level construction can decide this route.",
+      "first_step": "Specify one target row, the channel registers read, the restoration of each, and the changed channel obligations.",
+      "blocked_by": "Changed original channel; restoration and pricing unknown."
+    }
+  ]
+}

research/p104-fixed-cover-cut-review/VERIFY.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p104-joint-unit-flags/CERTIFICATE.json",
+    "research/p104-native-channel/inputs/LOWRANK-WITNESS.json",
+    "research/p104-native-channel/inputs/P104-FIXTURE.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-Werror",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Exact channel run (Y increment = G/2); PR3259 layered control; sharp support by one criterion in two loop orders and PR3252 full-memory recurrence (all equal; 2,309 own port pairs + (73,83); routes: 31 own pairs also via another type, (73,83) only via type (17,147)); PR3427 masks; vertex cover 104 of the 2,682 missing entries; rank(U-I)>=23 from a maximum independent 23x23 block; rank(G/2)=8 (rectangle cap 31); rows R1/R1u/R1c/R2/R3; 9,000-instance small-domain oracle (exhaustive reachability, realized programs, 18,000 random legal programs, the 9,000 directed ones run in the checked interpreter); six contract-violation controls"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-Werror",
+        "-B",
+        "{package}/test_verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Seven tests: tampered hash, unsound and too-tight oracle tests, wrong rank block (each with its own FAIL message); shared-type drop, containment drop (the containment-free variant over-grants), Y-relay escape (fact checks)"
+    }
+  ]
+}

research/p104-fixed-cover-cut-review/test_verify.py

@@ -0,0 +1,109 @@
+#!/usr/bin/env python3
+"""Negative controls: each deliberate defect must make verify.py fail."""
+
+import unittest
+from pathlib import Path
+from unittest import mock
+
+import runpy
+
+V = runpy.run_path(str(Path(__file__).resolve().parent / "verify.py"))
+
+
+_CACHE = []
+
+
+def result():
+    if not _CACHE:
+        _CACHE.append(V["p104"]())
+    return _CACHE[0]
+
+
+def fails(why, fn, *args):
+    """True when fn stops with the FAIL message that names `why`."""
+    try:
+        fn(*args)
+    except SystemExit as exc:
+        return str(exc).startswith("FAIL: " + why)
+    return False
+
+
+class Controls(unittest.TestCase):
+    def test_tampered_input_hash(self):
+        bad = {k: "0" * 64 for k in V["INPUTS"]}
+        with mock.patch.dict(V["load"].__globals__["INPUTS"], bad):
+            self.assertTrue(fails("input hash", V["load"]))
+
+    def test_oracle_rejects_an_unsound_test(self):
+        # A test that grants only shared snapshots misses helper paths.
+        g = V["oracle"].__globals__
+        with mock.patch.dict(g, {"small_sharp": lambda inst: {
+                (t, s) for s, xc in enumerate(inst[1])
+                for t, yc in enumerate(inst[2]) if set(xc) & set(yc)}}):
+            self.assertTrue(fails("oracle: exhaustive untimed support differs",
+                                  V["oracle"], 7, ((3, 400),), 120))
+
+    def test_oracle_rejects_a_too_tight_exhaustive_search(self):
+        # An exhaustive search that never switches helper type misses the
+        # legal two-type relay of the unpooled F_2^4 example.
+        g = V["unpooled_relay_example"].__globals__
+        with mock.patch.dict(g, {"small_exact": lambda inst: (
+                V["small_sharp"](inst), {})}):
+            self.assertTrue(fails("pooling is needed",
+                                  V["unpooled_relay_example"]))
+
+    def test_dropping_shared_type_breaks_pr3427_masks(self):
+        # Pairing a source snapshot and a target snapshot that are each
+        # admitted by some helper type, not necessarily the same one.
+        g = V["sharp_by_frames"].__globals__
+        r = result()
+        loose = [0] * 104
+        geo, paths = r["geo"], r["paths"]
+        masks = V["endpoint_masks"](geo)
+        frames = {f for k in "XY" for i in range(104)
+                  for f in paths[k + str(i)]}
+        adm = {f: V["admit_mask"](geo, masks, f) for f in frames}
+        for t in range(104):
+            for s in range(104):
+                if any(adm[v] and adm[w] for v in paths["X%d" % s]
+                       for w in paths["Y%d" % t]):
+                    loose[t] |= 1 << s
+        got = [sum(1 << t for t in range(104) if loose[t] >> s & 1)
+               for s in range(4)]
+        self.assertNotEqual(tuple(got), g["PR3427_SOURCE_MASKS"])
+
+    def test_dropping_containment_loses_exactness_in_principle(self):
+        # Containment V <= W is not decisive at P104 (verify.py checks this),
+        # but without it the test over-grants: it stays sound, not exact.
+        # F_2^4, one pooled type with line <e1> and hyperplane <e1,e2,e3>:
+        # X0 passes the admitted plane <e1,e2>, Y0 the admitted plane
+        # <e1,e3>, and no path joins them.
+        key = V["key"]
+        full = key([1, 2, 4, 8])
+        ty = {0: (), 1: key([1]), 3: key([1, 2, 4]), 4: full}
+        inst = (4, [[key([2]), key([1, 2]), full]],
+                [[(), key([1, 4]), key([1, 4, 8])]], [ty])
+        v, w = key([1, 2]), key([1, 4])
+        self.assertTrue(V["small_admit"](ty, v) and V["small_admit"](ty, w))
+        self.assertNotIn((0, 0), V["small_exact"](inst)[0])
+        self.assertNotIn((0, 0), V["small_sharp"](inst))
+        # The containment-free variant grants the unreachable pair (0,0).
+        self.assertFalse(V["le"](v, w))
+        self.assertIn((0, 0), V["small_sharp"](inst, nested=False))
+
+    def test_wrong_rank_block_is_rejected(self):
+        # The block is a maximum independent set, so any added port meets a
+        # supported pair; a shrunk block fails the size-23 check.
+        g = V["rank_consequence"].__globals__
+        r = result()
+        for bad, why in ((g["MIS_BLOCK"] + (45,), "principal block"),
+                         (g["MIS_BLOCK"][1:], "maximum independent set")):
+            with mock.patch.dict(g, {"MIS_BLOCK": bad}):
+                self.assertTrue(fails(why, V["rank_consequence"], r))
+
+    def test_y_relay_counterexample_is_a_real_escape(self):
+        self.assertEqual(V["y_relay_counterexample"](), (1, True))
+
+
+if __name__ == "__main__":
+    unittest.main()