Independently recount #4518's Levi-adaptive gauges: allowance 157,970/158,018, suffix 4,871, interval optimum verified (no new κ)

research/levi-gauge-recount/.gitattributes

@@ -0,0 +1 @@
+NATIVE-4518.json -text

research/levi-gauge-recount/README.md

@@ -0,0 +1,57 @@
+# Independent recount of #4518: Levi-adaptive gauges
+
+**Claim type:** an independent recount by separately written code. **No new κ.** It covers Dugongue's
+[#4518](https://github.com/CrocSwap/integer-mult-bounds/pull/4518) (head `9f0d81c8`). That PR changes the
+target gauge between dyadic coefficient groups in the four native cleanup windows, and reports a scalar
+allowance of 666 → 616 per orientation and a lower suffix error.
+
+The PR is not merged, so its `NATIVE.json` is vendored here as `NATIVE-4518.json`. The bytes are
+SHA256-pinned to the PR head and marked `-text`.
+
+## Results (both orientations)
+
+| | forward | backward |
+| --- | ---: | ---: |
+| scalar allowance: original → #4505 → #4518 | 158,120 → 158,020 → **157,970** | 158,168 → 158,068 → **158,018** |
+| saving over #4505 / original | 50 / 150 | 50 / 150 |
+| worst suffix ADD+SCALE weight (#4510 model) | 1,328 (unchanged) | **4,871** (from 4,879) |
+
+1. **Logical correctness.** Every non-scalar event is unchanged. All changes lie in one scalar segment
+   (4,208 → 4,212 scalars), whose exact rational linear effect on all 411 touched fields equals the
+   original's. Borrowed fields are therefore restored and no field is dirtied. This uses the same code
+   as my #4513.
+2. **The tariff.** It is re-implemented independently and gives exactly the allowances above.
+3. **The suffix bounds.** These use my independent reverse-response code from #4514, with an
+   initial-input factor of 2.
+4. **The interval theorem.** #4518's optimum within its family,
+   `C + min_{L≤0≤H} [4(H−L) + 2 Σ dist(s_i, [L, H])]`, equals an **exhaustive Dijkstra search** over
+   gauge walks (unit SCALE steps cost 2, start and end at gauge 0) and add orders (an ADD at gauge `g`
+   costs `2|s_i − g|` above its odd-part price) on 400 random valuation multisets of size up to 6.
+
+## Not covered
+
+- #4518's physical frames, phases and prefix envelope (its own literal and prefix loops).
+- The Levi dualization proof itself.
+- Optimality beyond the stated family.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/levi-gauge-recount --check-only
+python3.12 -B scripts/research_package.py --package research/levi-gauge-recount
+```
+
+The verifier prints `PASS_LEVI_GAUGE_RECOUNT` in a few seconds, using only the standard library.
+
+## Open next questions
+
+1. **Does letting the source gauge move too (not only the target) lower the 616 further?**
+   - *First step:* extend the Dijkstra state to two gauges, and price source restoration.
+
+## Credit
+
+- The construction, the interval theorem and the Levi connection are Dugongue's (#4518), building on #4502,
+  #4505 and MathProof's TI_SP proof.
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/levi-gauge-recount/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc",
+  "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/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz",
+      "usage": "input",
+      "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c",
+      "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39"
+    },
+    {
+      "path": "research/native-splice-replay/NATIVE.json",
+      "usage": "input",
+      "git_blob": "8e8fcbc0c6b5d40322ed71e9de48a2687ef66e0b",
+      "sha256": "e71e6fdf04f73a7c3ac77afcf037e0a88bb204765aeec24f72dda7b5e527af47"
+    }
+  ]
+}

research/levi-gauge-recount/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc",
+  "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": "refined",
+  "actual_scope": "Independent recount of #4518's Levi-adaptive gauges.",
+  "scope_change_reason": "Independent coverage of a fresh native-word change.",
+  "bottleneck_link": "Side result: native scalar allowance and precision accounting.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop at the logical recount and interval formula.",
+  "outcome": "completed",
+  "evidence": "Allowance 157,970 forward / 158,018 backward (50 below #4505), logically identical segment, suffix 1,328 / 4,871, interval formula equals exhaustive search on 400 cases.",
+  "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": "Does moving the source gauge too lower 616 further?",
+      "why_it_matters": "Further scalar savings.",
+      "first_step": "Two-gauge Dijkstra with source restoration priced.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/levi-gauge-recount/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz",
+    "research/native-splice-replay/NATIVE.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "#4518 recount: non-scalar events unchanged, one logically identical changed segment, allowance 157,970/158,018, suffix worst 1,328/4,871 under #4510's model, interval-optimum formula vs exhaustive Dijkstra on 400 instances."
+    }
+  ]
+}

research/levi-gauge-recount/verify.py

@@ -0,0 +1,181 @@
+#!/usr/bin/env python3
+"""Independent recount of #4518: Levi-adaptive gauges in the complete THREE-base native word.
+
+Inputs: the pinned original word, #4505's word on main, and #4518's NATIVE.json vendored as NATIVE-4518.json (sha256
+pinned to #4518 head 9f0d81c8). Separately written code checks, in both orientations:
+  * every non-scalar event is unchanged; all changes lie in one scalar segment whose exact linear effect on every
+    touched field equals the original's;
+  * the scalar allowance (re-implemented tariff) is 158,120 -> 158,020 (#4505) -> 157,970 forward and
+    158,168 -> 158,068 -> 158,018 backward: 50 below #4505 and 150 below the original per orientation;
+  * #4510's logical defect model (exact reverse free-word responses): worst ADD+SCALE weight 1,328 forward and
+    4,871 backward (down from 4,879), initial-input factor 2;
+  * #4518's interval optimum C + min_(L<=0<=H) [4(H-L) + 2 sum dist(s_i,[L,H])] equals an exhaustive Dijkstra search
+    over gauge walks (unit SCALE steps cost 2) and add orders (ADD at gauge g costs 2|s_i - g| above the odd part), on
+    400 random valuation multisets of size <= 6.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from collections import defaultdict
+from fractions import Fraction as F
+from fractions import Fraction as Q
+import gzip
+import hashlib
+import heapq
+import json
+from pathlib import Path
+import random
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+OLD = "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz"
+MID = "research/native-splice-replay/NATIVE.json"
+NEW_SHA = "d705f0ea8200e527f94dc6311e1303de497a843cc6bf407321b78cbb8a0874d7"
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def allowance(op):
+    if op[0] in ("clear", "copy"):
+        return 2
+    q = Q(op[3], op[4]) if op[0] == "add" else Q(op[2], op[3])
+    n, d = abs(q.numerator), q.denominator
+    need(n and d & (d - 1) == 0, "nonzero dyadic scalar")
+    if op[0] == "scale":
+        need(n & (n - 1) == 0, "dyadic unit scale")
+        return 2 * (abs(n.bit_length() - d.bit_length()) + (q < 0))
+    need(op[0] == "add", "known scalar op")
+    return 2 * (3 + n.bit_length() - 1 + bin(n).count("1") + d.bit_length() - 1)
+
+
+def segments(word):
+    out = [[]]
+    for e in word:
+        if e[0] == "scalar":
+            out[-1].append(e)
+        else:
+            out.append([])
+    return out
+
+
+def linear_effect(seg):
+    st = {}
+    get = lambda f: st.setdefault(f, {f: Q(1)})
+    for e in seg:
+        op = e[1]
+        if op[0] == "add":
+            dst, src, q = tuple(op[1]), tuple(op[2]), Q(op[3], op[4])
+            v = dict(get(dst))
+            for k, c in get(src).items():
+                v[k] = v.get(k, 0) + q * c
+            st[dst] = {k: c for k, c in v.items() if c}
+        elif op[0] == "scale":
+            f, q = tuple(op[1]), Q(op[2], op[3])
+            st[f] = {k: q * c for k, c in get(f).items()}
+        elif op[0] == "clear":
+            st[tuple(op[1])] = {}
+        elif op[0] == "copy":
+            st[tuple(op[1])] = dict(get(tuple(op[2])))
+        else:
+            raise AssertionError(f"unknown scalar op {op[0]}")
+    return st
+
+
+def response(word):
+    # adjoint[role] = {(output_index, warp_word): coeff}; reverse sweep
+    roles=[('L',i) for i in range(632)]+[('C',0)]
+    idx={r:i for i,r in enumerate(roles)}
+    adj={r:{(idx[r],()):F(1)} for r in roles}
+    w=defaultdict(lambda: defaultdict(F))   # class -> output -> weight
+    def acc(dst,src,q):
+        for k,c in src.items():
+            v=dst.get(k,0)+q*c
+            if v: dst[k]=v
+            else: dst.pop(k,None)
+    for e in reversed(word):
+        t=e[0]
+        if t=='scalar':
+            op=e[1]; tgt=tuple(op[1]); cls=op[0]
+        elif t=='warp': tgt=tuple(e[1]); cls='warp'
+        elif t=='climb': tgt=('L',e[2]); cls='rank-%d'%e[5]
+        elif t=='center': tgt=('C',e[1]); cls='rank-%d'%e[4]
+        else: continue
+        for (o,_),c in adj[tgt].items(): w[cls][o]+=abs(c)
+        if t=='scalar':
+            if op[0]=='add': acc(adj[tuple(op[2])],adj[tgt],F(op[3],op[4]))
+            elif op[0]=='scale':
+                q=F(op[2],op[3]); adj[tgt]={k:q*c for k,c in adj[tgt].items()}
+            elif op[0]=='clear': adj[tgt]={}
+            elif op[0]=='copy': acc(adj[tuple(op[2])],adj[tgt],F(1)); adj[tgt]={}
+        elif t=='warp':
+            s=e[2]; new={}
+            for (o,wd),c in adj[tgt].items():
+                nw=wd[:-1] if wd and wd[-1]==-s else wd+(s,)
+                new[(o,nw)]=new.get((o,nw),0)+c
+            adj[tgt]={k:c for k,c in new.items() if c}
+    E0=max(sum(abs(c) for r in roles for (o2,_),c in adj[r].items() if o2==o) for o in range(632))
+    return w,E0
+
+
+
+
+def formula(s):
+    lo, hi = min(min(s), 0), max(max(s), 0)
+    return min(4 * (H - L) + 2 * sum(max(L - x, 0) + max(x - H, 0) for x in s)
+               for L in range(lo, 1) for H in range(0, hi + 1))
+
+
+def brute(s):
+    n, lo, hi = len(s), min(min(s), 0) - 2, max(max(s), 0) + 2
+    dist, pq = {(0, 0): 0}, [(0, 0, 0)]
+    while pq:
+        d, g, mask = heapq.heappop(pq)
+        if d > dist.get((g, mask), 1 << 60):
+            continue
+        if mask == (1 << n) - 1 and g == 0:
+            return d
+        moves = [(d + 2, g + dg, mask) for dg in (-1, 1) if lo <= g + dg <= hi]
+        moves += [(d + 2 * abs(s[i] - g), g, mask | 1 << i) for i in range(n) if not mask >> i & 1]
+        for nd, ng, nm in moves:
+            if nd < dist.get((ng, nm), 1 << 60):
+                dist[(ng, nm)] = nd
+                heapq.heappush(pq, (nd, ng, nm))
+
+
+def main():
+    for row in json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"]:
+        need(hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], row["path"])
+    raw = (HERE / "NATIVE-4518.json").read_bytes()
+    need(hashlib.sha256(raw).hexdigest() == NEW_SHA, "#4518 NATIVE.json bytes")
+    old = json.loads(gzip.decompress((ROOT / OLD).read_bytes()))
+    mid = json.loads((ROOT / MID).read_bytes())
+    new = json.loads(raw)
+    expect = {"forward": (158120, 158020, 157970, 1328), "backward": (158168, 158068, 158018, 4871)}
+    out = {}
+    for o in ("forward", "backward"):
+        need([e for e in old[o] if e[0] != "scalar"] == [e for e in new[o] if e[0] != "scalar"], f"{o}: non-scalar events")
+        A, B = segments(old[o]), segments(new[o])
+        ch = [i for i in range(len(A)) if A[i] != B[i]]
+        need(len(ch) == 1, f"{o}: one changed segment")
+        ea, eb = linear_effect(A[ch[0]]), linear_effect(B[ch[0]])
+        for f in set(ea) | set(eb):
+            need(ea.get(f, {f: Q(1)}) == eb.get(f, {f: Q(1)}), f"{o}: field {f} same linear effect")
+        cost = tuple(sum(allowance(e[1]) for e in w[o] if e[0] == "scalar") for w in (old, mid, new))
+        need(cost == expect[o][:3], f"{o}: allowance {cost}")
+        w, E0 = response(new[o])
+        worst = max(w["add"][i] + w["scale"][i] for i in range(632))
+        need(worst == expect[o][3] and E0 == 2, f"{o}: suffix worst {worst}")
+        out[o] = {"allowance_orig_4505_4518": list(cost), "suffix_worst_add_scale": str(worst),
+                  "segment_scalars": [len(A[ch[0]]), len(B[ch[0]])]}
+    rng = random.Random(4518)
+    for _ in range(400):
+        s = [rng.randint(-5, 5) for _ in range(rng.randint(1, 6))]
+        need(formula(s) == brute(s), f"interval optimum {s}")
+    print(json.dumps({"status": "PASS_LEVI_GAUGE_RECOUNT", **out, "interval_formula_cases": 400,
+                      "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())