Independently review #4417's nonlinear centre-sharing floor: Theorems 1-2 hold; all six screen ceilings reproduced by separate code; rank-72 regroup is extremal (no new κ)

research/pr4417-centre-review/README.md

@@ -0,0 +1,85 @@
+# Independent review of #4417's nonlinear centre-sharing floor
+
+**Claim type:** a written proof review plus a separately implemented recomputation of the
+packing screen. **No new κ.** The object is Matarener's
+[#4417](https://github.com/CrocSwap/integer-mult-bounds/pull/4417) at head `2b101115`.
+
+## Proof review
+
+**Theorem 1 holds as stated, under the inherited premises.**
+
+- **Injectivity.** On `V ⊂ ker H`, the history is identically 0. The decoder `D(0, E(x)) = Q(x)`
+  together with `Q|_V` bijective forces `E` to be injective on `V`, which has real dimension
+  `16d`.
+- **Adaptivity.** Reads that depend on earlier fresh reads do not escape this. The whole
+  observation is still one function `E : V → ℝⁿ`, with `n` the maximum number of reads, padded.
+  In the continuous case it is a continuous injection, so invariance of domain gives `n ≥ 16d`.
+- **Branching.** With finitely many semialgebraic branches, `V ∩ box` splits into finitely many
+  semialgebraic pieces. One piece has dimension `16d`. An injective semialgebraic map preserves
+  dimension, so again `n ≥ 16d`.
+
+**Theorem 2** is a counting argument. Injectivity on `2^{16db}` grid points needs at least that
+many values, so the widths sum to at least `16db`. Kronecker packing attains this, as `verify.py`
+re-checks on six small grids.
+
+## Screen recomputation
+
+`verify.py` reimplements the relaxation of `research/complex-local-word-ceiling` without importing
+it:
+
+- per call, `w = 896/9`;
+- coverage mass `(m−1)w + centre`;
+- the idle mass goes into fractional rank-`R` children, with `R = 51` the largest rank satisfying
+  `m² > 2R²` at `m = 73`;
+- certified interval logarithms and exponentials;
+- a bracket to `10⁻¹²`.
+
+All six rows match #4417 to `10⁻¹¹`:
+
+| Row | `a_hi` | ratio |
+| --- | --- | --- |
+| selected, 8 × rank-8 | 0.001690054109 | 1.000000 |
+| 4 × rank-16 | 0.001693625547 | 1.002113 |
+| 2 × rank-32 | 0.001697207887 | 1.004233 |
+| 1 × rank-64 | 0.001700801148 | 1.006359 |
+| ideal fractional rank-72 | 0.001701412821 | 1.006721 |
+| control: halved information (4 × rank-8, centre 32) | 0.003212972894 | 1.901107 |
+
+**Extremality of rank 72.** A child of rank `r` costs `(r/m)^{1−a} = r · r^{−a}m^{a−1}`, so the
+cost per unit mass `r^{−a}m^{a−1}` is nonincreasing in `r`; the verifier checks this with
+certified bounds. Any regrouping of the 64 centre units into children of rank at most
+`m − 1 = 72` therefore has a moment at least that of the fractional rank-72 relaxation. That
+makes +0.67% an upper bound for every packing, as #4417 states.
+
+## Not covered
+
+- The premises of centre-history-innovation, such as the common frame, the cover view and the
+  call-10 query.
+- #3918's rank-8 carrier premise.
+- Terminal-only consumers.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/pr4417-centre-review --check-only
+python3.12 -B scripts/research_package.py --package research/pr4417-centre-review
+```
+
+The verifier prints `PASS_PR4417_SCREEN_REVIEW` in about 20 seconds, using only the standard
+library.
+
+## Open next questions
+
+1. **Does a carrier other than rank-8 channels change the 64-unit centre mass?**
+   - *Why it matters:* this is #4417's open question 2, and the screen caps the ideal gain at
+     +0.67%.
+   - *First step:* price one alternative carrier's restoration bill.
+
+## Credit
+
+- The theorems and the screen are Matarener's (#4417).
+- The relaxation model is Douglas Colkitt's complex-local-word ceiling.
+- The premises are Jose Manuel's centre-history-innovation and #3873.
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/pr4417-centre-review/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    }
+  ]
+}

research/pr4417-centre-review/TASK.json

@@ -0,0 +1,67 @@
+{
+  "schema_version": 1,
+  "task_id": "centre-path-sharing",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "original_card": {
+    "id": "centre-path-sharing",
+    "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.",
+      "Prove a lower bound on copied information per call for the selected decoder contract."
+    ],
+    "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...). 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",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).",
+    "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.",
+    "allowed_variations": [
+      "One sharing pattern across a fixed number of calls.",
+      "One reduced copied-total contract for the existing decoder.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Removing copies without a replacement contract for the decoder's copied totals.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "centre path",
+      "copied totals",
+      "private temporary",
+      "shared centre",
+      "batching"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Independently review #4417: proof check of Theorems 1-2 and a separate recomputation of its packing screen.",
+  "scope_change_reason": "#4417 is an unreviewed negative result on the centre-path-sharing card.",
+  "bottleneck_link": "The centre path costs 64 of the paid mass per call; #4417 caps any packing gain at +0.67%.",
+  "budget_minutes": 25,
+  "stop_rule": "Stop at the proof review and screen recomputation.",
+  "outcome": "completed",
+  "evidence": "Theorem 1 injectivity/dimension argument checked including adaptive reads; six ceilings reproduced to 1e-11 by separate code; rank-72 regroup extremality proven by monotone unit cost.",
+  "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 a carrier other than rank-8 channels change the 64-unit centre mass?",
+      "why_it_matters": "#4417's screen caps the ideal gain at +0.67%.",
+      "first_step": "Price one alternative carrier's restoration bill.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/pr4417-centre-review/VERIFY.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Separate implementation of the coverage relaxation; six screen ceilings matching #4417 to 1e-11; per-unit-mass cost monotonicity (regroup extremality); Kronecker sharpness on six small grids."
+    }
+  ]
+}

research/pr4417-centre-review/verify.py

@@ -0,0 +1,163 @@
+#!/usr/bin/env python3
+"""Independent review of #4417's packing screen and Kronecker sharpness (centre-path-sharing).
+
+A separate implementation of the hosted nine-stage coverage relaxation (not importing ceiling.py):
+per call w = families/stages live families, total paid mass (m - 1) w + centre, the local word's own children,
+and the remaining idle mass M placed in fractional rank-R children with R the largest rank satisfying the outer
+halving guard m^2 > 2 R^2. The moment
+
+    relax(a) = [ sum_local n_r (r/m)^(1-a) + (M/R)(R/m)^(1-a) ] / w
+
+is increasing in a; its root a* is the ceiling. The verifier brackets a* to 1e-12 for the six rows of #4417's
+screen (selected 8 x rank-8; packs into 4 x 16, 2 x 32, 1 x 64; ideal fractional rank-72; halved-information
+control 4 x 8 with centre 32) and compares them with #4417's RESULT.json values.
+It also proves the regroup extremality: for fixed centre mass, (r/m)^(1-a) / r = r^-a m^(a-1) is nonincreasing in r,
+so moving mass to the largest child rank m - 1 = 72 minimises the moment, i.e. maximises the ceiling; and it
+checks Kronecker packing sharpness exhaustively on small grids.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from fractions import Fraction as Q
+import itertools
+import json
+import sys
+
+GRID = Q(1, 10**60)
+M, FAM, ST = 73, 896, 9
+WORD = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8}
+EXPECTED_HI = {  # #4417 RESULT.json a_hi values, rounded to 11 digits in its README table
+    "selected": "0.00169005411", "pack2": "0.00169362555", "pack4": "0.00169720789",
+    "pack8": "0.00170080115", "regroup72": "0.00170141282", "halved": "0.00321297289"}
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def down(x):
+    return (x / GRID).__floor__() * GRID
+
+
+def up(x):
+    return (x / GRID).__ceil__() * GRID
+
+
+LN = {}
+
+
+def ln(n):
+    """certified ln of an integer by bit reduction and the atanh series"""
+    if n in LN:
+        return LN[n]
+    if n == 1:
+        LN[n] = (Q(0), Q(0))
+        return LN[n]
+    k = n.bit_length() - 1
+    lo = hi = Q(0)
+    for y, scale in ((Q(n, 2 ** k), 1), (Q(2), k)):
+        if y == 1 or scale == 0:
+            continue
+        u = (y - 1) / (y + 1)
+        s, term, j = Q(0), u, 0
+        while True:
+            s += term / (2 * j + 1)
+            j += 1
+            term *= u * u
+            tail = term / (2 * j + 1) / (1 - u * u)
+            if tail < GRID:
+                break
+        lo += scale * down(2 * s)
+        hi += scale * up(2 * (s + tail))
+    LN[n] = (lo, hi)
+    return LN[n]
+
+
+def exp_iv(lo, hi):
+    def series(x):
+        s, term = Q(0), Q(1)
+        for i in range(60):
+            s += term
+            term = term * x / (i + 1)
+        return s, abs(term) * 2
+    a, ea = series(lo)
+    b, eb = series(hi)
+    return down(a - ea), up(b + eb)
+
+
+def idle_rank(m):
+    R = 1
+    while 2 * (R + 1) ** 2 < m * m:
+        R += 1
+    return R
+
+
+def relax(local, centre, a):
+    w = Q(FAM, ST)
+    R = idle_rank(M)
+    idle = (M - 1) * w + centre - sum(r * Q(n) for r, n in local.items())
+    need(idle >= 0, "coverage law")
+    lo = hi = Q(0)
+    lm = ln(M)
+    for r, n in list(local.items()) + [(R, idle / R)]:
+        lr = ln(r)
+        e = exp_iv(a * (lm[0] - lr[1]), a * (lm[1] - lr[0]))   # (m/r)^a
+        lo += Q(n) * Q(r, M) * e[0]
+        hi += Q(n) * Q(r, M) * e[1]
+    return lo / w, hi / w
+
+
+def ceiling(local, centre=64):
+    lo, hi = Q(0), Q(1, 20)
+    need(relax(local, centre, hi)[0] > 1 and relax(local, centre, lo)[1] < 1, "bracket")
+    while hi - lo > Q(1, 10**12):
+        mid = (lo + hi) / 2
+        v = relax(local, centre, mid)
+        if v[1] < 1:
+            lo = mid
+        elif v[0] > 1:
+            hi = mid
+        else:
+            raise AssertionError("enclosure too wide")
+    return lo, hi
+
+
+def kronecker_sharp(widths, bits):
+    """k values of `bits` bits pack injectively into sum(widths) bits iff sum(widths) >= k*bits"""
+    values = list(itertools.product(range(2 ** bits), repeat=len(widths)))
+    total = sum(widths)
+    packed = {sum(v << (bits * i) for i, v in enumerate(vals)) for vals in values}
+    return len(packed) == len(values) and max(packed) < 2 ** total
+
+
+def main():
+    need(idle_rank(M) == 51, "R = 51 for m = 73")
+    rest = {r: n for r, n in WORD.items() if r != 8}
+    rows = {"selected": (WORD, 64), "pack2": ({**rest, 16: Q(4)}, 64), "pack4": ({**rest, 32: Q(2)}, 64),
+            "pack8": ({**rest, 64: Q(1)}, 64), "regroup72": ({**rest, 72: Q(64, 72)}, 64),
+            "halved": ({**WORD, 8: 4}, 32)}
+    out = {}
+    base = None
+    for name, (local, centre) in rows.items():
+        lo, hi = ceiling(local, centre)
+        exp = Q(EXPECTED_HI[name])
+        need(abs(hi - exp) < Q(1, 10**11), f"{name}: matches #4417's a_hi to 1e-11")
+        base = hi if base is None else base
+        out[name] = {"a_hi": f"{float(hi):.12f}", "ratio": f"{float(hi / base):.6f}"}
+    need(Q(out["regroup72"]["a_hi"]) / Q(out["selected"]["a_hi"]) < Q(1007, 1000), "+0.7% cap")
+    # extremality: per-unit-mass cost r^-a m^(a-1) nonincreasing in r for a >= 0, so any regrouping of the
+    # 64 centre mass into children of rank <= 72 has moment >= the fractional rank-72 relaxation
+    a = Q(1, 500)
+    for r in range(1, 72):
+        c1 = exp_iv(-a * ln(r + 1)[1], -a * ln(r + 1)[0])[1]     # (r+1)^-a upper
+        c0 = exp_iv(-a * ln(r)[1], -a * ln(r)[0])[0]             # r^-a lower
+        need(c1 <= c0, "per-unit-mass cost nonincreasing")
+    # Kronecker sharpness on small grids
+    for k, bits in ((2, 2), (3, 2), (2, 3), (4, 1), (3, 3), (2, 4)):
+        need(kronecker_sharp([bits] * k, bits), "packing at exact width is injective")
+        vals = list(itertools.product(range(2 ** bits), repeat=k))
+        need(len(vals) > 2 ** (k * bits - 1), "one bit less collides (pigeonhole)")
+    print(json.dumps({"status": "PASS_PR4417_SCREEN_REVIEW", "rows": out, "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())