diff --git a/research/pr4417-centre-review/README.md b/research/pr4417-centre-review/README.md new file mode 100644 index 0000000000..034786dadf --- /dev/null +++ b/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. diff --git a/research/pr4417-centre-review/SOURCES.json b/research/pr4417-centre-review/SOURCES.json new file mode 100644 index 0000000000..fcfba8aa31 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/pr4417-centre-review/TASK.json b/research/pr4417-centre-review/TASK.json new file mode 100644 index 0000000000..ab77118b48 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/pr4417-centre-review/VERIFY.json b/research/pr4417-centre-review/VERIFY.json new file mode 100644 index 0000000000..36703d7a2f --- /dev/null +++ b/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." + } + ] +} diff --git a/research/pr4417-centre-review/verify.py b/research/pr4417-centre-review/verify.py new file mode 100644 index 0000000000..393cb0a39d --- /dev/null +++ b/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())