Independently check #4544's sharp cancellation audit: exact identities, necessity of #4483's (10), controls, source binding (no new κ)

research/pr4544-cancellation-check/README.md

@@ -0,0 +1,36 @@
+# Independent check of #4544: the sharp cancellation threshold
+
+**Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.**
+
+Clear1nsight's #4544 (head `0898b3a8`) audits the implication (10) ⇒ (11) in zxv's #4483, `research/rank-convergence/PROOF.md` Section 4, and states that its threshold is sharp. This package checks each of #4544's claims with a separately written exact verifier. Nothing is imported from #4544's checker.
+
+## Results
+
+All of #4544's claims are confirmed.
+
+1. **Slack identity.** With `I = B+F+A`, `(1−β)(ηI−B−F) = (η−β)A − (1−η)F + (1−η)(βI−B)` holds as a polynomial identity in ℚ[β, η, B, F, A]. A rejection control that drops the mirror term fails.
+2. **Extremiser.** At `B* = β(A+F)/(1−β)` the exit fraction equals `(βA+F)/(A+F)`. This is checked as a polynomial identity after clearing `1−β`. The fraction is linear-fractional in `B` with derivative numerator `A ≥ 0`, so the maximum over `0 ≤ B ≤ B*` is at `B*`. An exact grid of 11,968 cases confirms that the uniform guarantee holds iff `(η−β)A ≥ (1−η)F`.
+3. **Necessity of #4483's own (10).** If only (3) `F ≤ X` and (9) `A ≥ D·X` are known, with `X = P^(G+1)`, the adversary takes `A = D·X`, `F = X` and a saturated mirror. Its exit fraction is `(βD+1)/(D+1)`, and `(D+1)(η − (βD+1)/(D+1)) = (η−β)D − (1−η)` identically. So (10) is exactly the uniform condition, which supports #4544's statement that no better threshold follows from these scalar premises.
+4. **Failure controls.** For the root-debit control, with `β = 1/4`, `η = 1/2`, `F = 1`, gross production 2 and `R = 1/2`, the exit fraction is `11/20 > η`. The gross test passes with equality and the net test rejects. The leaf-omission control gives an exit fraction of 1.
+5. **Binding.** The pinned source (sha256 `3c971c56…`, blob `75f45183`) states equations (2), (3), `A_t = (T−P)H_t − R_t`, (9), (10), (11) and the premises `B_t ≤ βI_t` and `β < η < 1` verbatim, as #4544 uses them.
+
+I also replayed #4544's registered package at its head: `PASS_REGISTERED_RESEARCH_PACKAGE research/adaptive-cancellation-audit` in 1.3 s.
+
+## Verify
+
+```text
+python3 -B research/pr4544-cancellation-check/verify.py
+```
+
+This runs in under 1 s with the standard library only.
+
+## Limitations
+
+- This checks #4544's scalar lemma and its binding only. The Chernoff bounds behind `D`, the mirror certificate, funding and realisation are out of scope, as #4544 also says.
+- #4544's upstream diff also carries shared CI and navigation repairs from its preparation base. Those are not reviewed here.
+
+## Open next questions
+
+- Whether actual-flow correlations between `F` and `A` give a strictly better uniform threshold than (10). First step: bound the joint occupation of leaf exits and net production on one certified witness and compare it with the adversary in item 3.
+
+Credit: zxv (#4483) and Clear1nsight (#4544). Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.

research/pr4544-cancellation-check/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/rank-convergence/PROOF.md",
+      "usage": "input",
+      "git_blob": "75f451837204bd141f357e7f5e5d6c6f42e1423e",
+      "sha256": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376"
+    }
+  ]
+}

research/pr4544-cancellation-check/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "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": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "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.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "unchanged",
+  "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+  "scope_change_reason": null,
+  "bottleneck_link": "Independent coverage of the cancellation lemma that every #4483-compiler κ claim (including #4535) depends on.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop at #4544's stated claims.",
+  "outcome": "completed",
+  "evidence": "Slack identity, extremiser and necessity of (10) verified as exact polynomial identities; 11,968-case threshold grid; both failure controls; source statements bound to pinned PROOF.md; #4544's own package replays.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Do actual-flow correlations between F and A beat threshold (10)?",
+      "why_it_matters": "(10) is sharp for the scalar premises only.",
+      "first_step": "Bound joint occupation of leaf exits and net production on one certified witness.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/pr4544-cancellation-check/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/rank-convergence/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact polynomial identities (slack, extremiser, necessity of (10)) with rejection control, 11,968-case threshold grid, two failure controls, and binding to pinned rank-convergence/PROOF.md."
+    }
+  ]
+}

research/pr4544-cancellation-check/verify.py

@@ -0,0 +1,164 @@
+#!/usr/bin/env python3
+"""Independent check of PR #4544 (Clear1nsight): the sharp cancellation audit of PR #4483 Section 4.
+
+Written separately from #4544's checker; nothing is imported from it. Checks, in exact rational arithmetic:
+  1. the slack identity (1-b)(eI-B-F) = (e-b)A-(1-e)F+(1-e)(bI-B) as a polynomial identity in Q[b,e,B,F,A], I=B+F+A;
+  2. the extremiser: at B*=b(A+F)/(1-b) the exit fraction equals (bA+F)/(A+F), as a polynomial identity, and the
+     fraction is linear-fractional in B, hence monotone, so the maximum over 0<=B<=B* sits at an endpoint (grid check);
+  3. necessity of #4483's own threshold (10): with only F<=X and A>=D*X known, the adversary A=D*X, F=X with a
+     saturated mirror has exit fraction (bD+1)/(D+1), and (D+1)(e-(bD+1)/(D+1)) = (e-b)D-(1-e) identically;
+  4. #4544's two failure controls (root debit dropped; leaf mass dropped);
+  5. the binding: the pinned source PROOF.md (sha256) states equations (2), (3), (9), (10), (11) as #4544 uses them.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from fractions import Fraction as Fr
+import hashlib
+import json
+from pathlib import Path
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+SOURCE = ROOT / "research/rank-convergence/PROOF.md"
+SOURCE_SHA256 = "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376"
+VARS = ("b", "e", "B", "F", "A", "D")
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+class P:
+    """Sparse multivariate polynomial over Q in VARS."""
+
+    def __init__(self, terms=None):
+        self.t = {k: v for k, v in (terms or {}).items() if v}
+
+    @staticmethod
+    def var(name):
+        k = [0] * len(VARS)
+        k[VARS.index(name)] = 1
+        return P({tuple(k): Fr(1)})
+
+    @staticmethod
+    def const(c):
+        return P({(0,) * len(VARS): Fr(c)})
+
+    def __add__(self, o):
+        o = o if isinstance(o, P) else P.const(o)
+        t = dict(self.t)
+        for k, v in o.t.items():
+            t[k] = t.get(k, 0) + v
+        return P(t)
+
+    __radd__ = __add__
+
+    def __neg__(self):
+        return P({k: -v for k, v in self.t.items()})
+
+    def __sub__(self, o):
+        return self + (-(o if isinstance(o, P) else P.const(o)))
+
+    def __rsub__(self, o):
+        return P.const(o) - self
+
+    def __mul__(self, o):
+        o = o if isinstance(o, P) else P.const(o)
+        t = {}
+        for k1, v1 in self.t.items():
+            for k2, v2 in o.t.items():
+                k = tuple(x + y for x, y in zip(k1, k2))
+                t[k] = t.get(k, 0) + v1 * v2
+        return P(t)
+
+    __rmul__ = __mul__
+
+    def is_zero(self):
+        return not self.t
+
+
+def symbolic():
+    b, e, B, F, A, D = (P.var(v) for v in VARS)
+    I = B + F + A
+    slack = (1 - b) * (e * I - B - F) - ((e - b) * A - (1 - e) * F + (1 - e) * (b * I - B))
+    need(slack.is_zero(), "slack identity")
+    # Rejection control: dropping the mirror slack term breaks the identity.
+    need(not ((1 - b) * (e * I - B - F) - ((e - b) * A - (1 - e) * F)).is_zero(), "rejection control")
+    # Extremiser, cleared of the denominator (1-b): Bs = b(A+F)/(1-b), so (1-b)Bs = b(A+F).
+    # (Bs+F)/(Bs+A+F) = (bA+F)/(A+F)  <=>  ((1-b)Bs+(1-b)F)(A+F) = (bA+F)((1-b)Bs+(1-b)(A+F)).
+    sB = b * (A + F)
+    ext = (sB + (1 - b) * F) * (A + F) - (b * A + F) * (sB + (1 - b) * (A + F))
+    need(ext.is_zero(), "extremiser value")
+    # Derivative numerator of (B+F)/(B+A+F) in B: (B+A+F) - (B+F) = A >= 0 (monotone nondecreasing).
+    need(((B + A + F) - (B + F) - A).is_zero(), "monotonicity numerator")
+    # Necessity of (10): (D+1)*e - (bD+1) = (e-b)D - (1-e).
+    nec = (D + 1) * e - (b * D + 1) - ((e - b) * D - (1 - e))
+    need(nec.is_zero(), "necessity of (10)")
+    return 4
+
+
+def frac(B, F, A):
+    return (B + F) / (B + A + F)
+
+
+def grid():
+    vals = [Fr(n, d) for d in (1, 2, 3, 5, 7) for n in range(0, 2 * d + 1)]
+    betas = [Fr(n, 8) for n in range(0, 8)]
+    cases = 0
+    for b in betas:
+        for A in vals[::3]:
+            for F in vals[::3]:
+                if A + F == 0:
+                    continue
+                Bs = b * (A + F) / (1 - b)
+                top = (b * A + F) / (A + F)
+                need(frac(Bs, F, A) == top, "attained")
+                need(frac(Fr(0), F, A) <= top, "endpoint order")
+                for j in range(9):
+                    need(frac(Bs * j / 8, F, A) <= top, "interior below the maximum")
+                # The guarantee B+F <= eI for all admissible B holds iff top <= e iff (e-b)A >= (1-e)F.
+                for e in [Fr(n, 16) for n in range(1, 16)]:
+                    if e <= b:
+                        continue
+                    need((top <= e) == ((e - b) * A >= (1 - e) * F), "threshold equivalence")
+                    cases += 1
+    return cases
+
+
+def controls():
+    b, e = Fr(1, 4), Fr(1, 2)
+    F, gross, R = Fr(1), Fr(2), Fr(1, 2)
+    A = gross - R
+    I = (A + F) / (1 - b)
+    B = b * I
+    need(I + R == B + F + gross, "exact cancellation (2)")
+    need((B + F) / I == Fr(11, 20) and Fr(11, 20) > e, "root-debit control exits above eta")
+    need((e - b) * gross == (1 - e) * F, "gross test passes with equality")
+    need(not ((e - b) * A >= (1 - e) * F), "net test rejects")
+    # Leaf omission: A=0, F=1 gives exit fraction 1 > eta although A >= 0.
+    need(frac(Fr(0), Fr(1), Fr(0)) == 1, "leaf-omission control")
+    # Zero mass: A=F=0 and B<=bI with I=B force I=B=0.
+    return 2
+
+
+def binding():
+    raw = SOURCE.read_bytes()
+    need(hashlib.sha256(raw).hexdigest() == SOURCE_SHA256, "pinned source bytes")
+    text = raw.decode("utf-8")
+    for s in ("I_t+R_t = B_t+F_t+(T_t-P_t)H_t.", "F_t <= P_t^(G+1).", "Set A_t=(T-P)H_t-R_t.",
+              "A_t >=D_ell(t)P^(G+1),", "(eta-beta)D_ell(t) >=1-eta,", "B_t+F_t <=eta I_t.",
+              "B_t<=beta I_t", "beta<eta<1"):
+        need(s in text, f"source states: {s}")
+    return 8
+
+
+def main():
+    report = {"status": "PASS_PR4544_CANCELLATION_CHECK", "symbolic_identities": symbolic(),
+              "grid_threshold_cases": grid(), "failure_controls": controls(), "source_statements_bound": binding(),
+              "new_kappa_claimed": False}
+    print(json.dumps(report, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())