From 4bbf9f961016210cfdd15fa0e01dd63e114b3fd9 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 01:53:30 -0400 Subject: [PATCH 1/2] Bound selected packing ceiling with fixed data-route child boundaries Exact rank-48 idle relaxation for the selected #1094 word when the 112-port data-route children stay fixed: kappa < 0.001679270178313 (at most 0.395% above selected), against #1240's rank-51 cap. Prepared by OpenAI Codex in offline session 14 of an overnight run; committed and published by the Claude coordinator. Co-Authored-By: Claude Opus 5.5 --- .../README.md | 45 +++ .../RESULT.json | 46 +++ .../SOURCES.json | 60 ++++ .../TASK.json | 68 +++++ .../VERIFY.json | 27 ++ .../verify.py | 288 ++++++++++++++++++ 6 files changed, 534 insertions(+) create mode 100644 research/frontier1094-fixed-route-packing-cap/README.md create mode 100644 research/frontier1094-fixed-route-packing-cap/RESULT.json create mode 100644 research/frontier1094-fixed-route-packing-cap/SOURCES.json create mode 100644 research/frontier1094-fixed-route-packing-cap/TASK.json create mode 100644 research/frontier1094-fixed-route-packing-cap/VERIFY.json create mode 100644 research/frontier1094-fixed-route-packing-cap/verify.py diff --git a/research/frontier1094-fixed-route-packing-cap/README.md b/research/frontier1094-fixed-route-packing-cap/README.md new file mode 100644 index 0000000000..c8ae5375d9 --- /dev/null +++ b/research/frontier1094-fixed-route-packing-cap/README.md @@ -0,0 +1,45 @@ +# Selected #1094 fixed-route packing cap + +**Scoped exact upper bound, no new κ.** For the selected local word and the selected data-route child inventory, any whole-helper owner reassignment that hosts into those same children has complex primitive saving `a < 0.001682094870065`. Under the retained balanced conversion `κ = a/(1+a)`, this gives the planning cap `κ < 0.001679270178313`, at most **0.395178%** above the selected `0.001672660197076918`. The selected κ is at least 99.606% of this favorable cap. This does not assert an attainable packing or the exact seven-step outer-grid ceiling. + +## Fixed inventory and proof + +The source-bound route is `research/direct-delivery504-global/inputs/data-base/work/complex-nine-native/DATA-PHASES.json`. It is pinned by the selected `SELECTED-SOURCE.json` and byte-identical to the same member in `selected-replay.tar.gz`. The verifier recomputes GF(2) rank from every `orthogonal_axes` list. Each of the 112 port recipes has two rank-0, six rank-8, four rank-16, four rank-32, and four rank-48 children. Thus **no existing data-route child has rank above 48**. The selected manifest also pins the [parent T16 hosting proof](../gauge44-slots-t16/hosting/PROOF.md): a pending child has capacity `C_g`, hosting occupies a prefix of total width `U_g`, and its remaining suffix has rank `C_g−U_g`. The selected plan explicitly lifts that eight-replica geometry to sixteen replicas. Therefore a remainder after whole-helper hosting into one of these fixed children has rank at most 48. This is the extra premise beyond [the predecessor's rank-51 relaxation](../complex-local-word-ceiling/README.md). Axis transfer or repartitioning across child boundaries can make a rank above 48 without changing the total parent space, and is excluded. + +The selected replay's `spec_sha256` binds the T16 `SPEC.json`; its `data.plan_sha256` binds `PLAN.json`. The plan and replay give 144 calls, 14,336 live families and the same complete profile. Subtracting the replay's idle profile and dividing by 144 gives the local profile per call `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}`. The complete rank mass is `1,041,408 = 72·14,336 + 64·144`; local mass is `5,586·144`, so idle mass is `237,024 = 4,938·48`. + +For `0 0, 'invalid route axis') + while value: + pivot = value.bit_length() - 1 + if pivot not in basis: + basis[pivot] = value + break + value ^= basis[pivot] + return len(basis) + + +def route_ranks(route): + need(route['m'] == 73 and route['ports'] == 112, 'route geometry') + recipes = route['recipes'] + need(len(recipes) == 112 and {r['port'] for r in recipes} == set(range(112)), 'route port coverage') + total = Counter() + for recipe in recipes: + counts = Counter() + for child in recipe['idle_children']: + rank, axes = child['rank'], child['orthogonal_axes'] + need(type(rank) is int and rank >= 0, 'invalid route rank') + need(rank == len(axes) == gf2_rank(axes), 'route rank/axes mismatch') + counts[rank] += 1 + need(dict(counts) == RANKS, 'route child inventory changed') + total.update(counts) + return dict(sorted(total.items())) + + +def profile(replay, plan): + calls, live = replay['complete_invocations'], plan['live'] + need((calls, live) == (144, 14336), 'selected calls/live changed') + lift = plan['replica_lift'] + need((lift['source_replicas'], lift['replicas']) == (8, 16), 'selected replica lift changed') + need(plan['profile'] == replay['complex_profile'] and plan['deficit'] == 5120, + 'plan/replay profile binding') + complete = {int(r): n for r, n in replay['complex_profile'].items()} + idle = {int(r): n for r, n in replay['idle_remainder_profile'].items()} + local = {} + for rank in set(complete) | set(idle): + n = complete.get(rank, 0) - idle.get(rank, 0) + need(n >= 0 and n % calls == 0, 'local profile split') + if n: + local[rank] = n // calls + need(local == LOCAL, 'selected local word changed') + need(sum(r*n for r, n in complete.items()) == 72*live + 64*calls, + 'selected coverage identity') + mass = sum(r*n for r, n in idle.items()) + need(mass == 237024 and max(idle) <= 48, 'selected idle profile') + return calls, live, local, mass, idle + + +def atanh(z): + """Rational enclosure of atanh(z), 0 <= z <= 1/3.""" + need(0 <= z <= Q(1, 3), 'atanh domain') + summation, power = Q(0), z + for k in range(40): + summation += power / (2*k + 1) + power *= z*z + return summation, summation + power / (81*(1-z*z)) + + +@lru_cache(None) +def ln(integer): + """Reduce integer to [1,2), then use atanh; unlike predecessor's ln(k-1) chain.""" + need(type(integer) is int and integer >= 1, 'log domain') + if integer == 1: + return Q(0), Q(0) + j = integer.bit_length() - 1 + y = Q(integer, 1 << j) + z = (y-1)/(y+1) + zlo, zhi = atanh(z) + tlo, thi = atanh(Q(1, 3)) # ln 2 = 2 atanh(1/3) + return 2*(j*tlo+zlo), 2*(j*thi+zhi) + + +@lru_cache(None) +def log_ratio(m, r): + ml, mh = ln(m) + rl, rh = ln(r) + return ml-rh, mh-rl + + +def exp_interval(low, high): + need(0 <= low <= high < Q(1, 2), 'exp domain') + def series(x): + s = term = Q(1) + for k in range(1, 17): + term *= x/k + s += term + next_term = term*x/17 + return s, s + next_term/(1-x/18) + return series(low)[0], series(high)[1] + + +def cost(rank, saving): + lo, hi = log_ratio(73, rank) + elo, ehi = exp_interval(saving*lo, saving*hi) + return Q(rank, 73)*elo, Q(rank, 73)*ehi + + +def moment(local, calls, live, mass, cap, saving): + low = high = Q(0) + for rank, count in local.items(): + clo, chi = cost(rank, saving) + low += calls*count*clo + high += calls*count*chi + clo, chi = cost(cap, saving) + return (low+Q(mass, cap)*clo)/live, (high+Q(mass, cap)*chi)/live + + +def bracket(local, calls, live, mass, cap): + left, right = 0, 50_000_000_000_000 # a in [0, 0.05] + need(moment(local, calls, live, mass, cap, 0)[1] < 1, 'root lower sign') + need(moment(local, calls, live, mass, cap, right*GRID)[0] > 1, 'root upper sign') + while right-left > 1: + mid = (left+right)//2 + low, high = moment(local, calls, live, mass, cap, mid*GRID) + if high < 1: + left = mid + elif low > 1: + right = mid + else: + raise ValueError('interval cannot separate grid sign') + return left*GRID, right*GRID + + +def display(x): + digits = 18 + scaled = x.numerator*10**digits//x.denominator + return f'{scaled//10**digits}.{scaled%10**digits:0{digits}d}' + + +def result(selected, replay, route, plan): + ranks = route_ranks(route) + calls, live, local, mass, idle = profile(replay, plan) + low, high = bracket(local, calls, live, mass, 48) + old_low, old_high = bracket(local, calls, live, mass, 51) + need((low, high) == (Q(1682094870064, 10**15), Q(1682094870065, 10**15)), 'rank-48 root') + need((old_low, old_high) == (Q(1690054109088, 10**15), Q(1690054109089, 10**15)), + 'rank-51 predecessor root') + need(moment(local, calls, live, mass, 48, low)[1] < 1 and + moment(local, calls, live, mass, 48, high)[0] > 1, 'strict endpoint signs') + kappa = Q(selected['kappa']) + bit, complex_a = Q(replay['bit_lower']), Q(replay['complex_lower']) + need(complex_a < low < high < bit, 'supplier ordering') + cap_k = high/(1+high) + old_cap_k = old_high/(1+old_high) + need(kappa < cap_k < old_cap_k, 'kappa cap ordering') + return { + 'status': 'PASS_FRONTIER1094_FIXED_ROUTE_PACKING_CAP', + 'scope': 'Selected fixed 112-port data-route children and local word; PR1012 coverage; whole-helper hosting into existing children; retained balanced transfer. Relaxation only, no new kappa.', + 'route_sha256': sha((ROOT/ROUTE).read_bytes()), + 'route_rank_counts': {str(r): n for r, n in ranks.items()}, + 'calls': calls, 'live_families': live, + 'local_per_call': {str(r): n for r, n in sorted(local.items())}, + 'selected_idle': {str(r): n for r, n in sorted(idle.items())}, + 'idle_mass': mass, 'ideal_rank48_children': str(Q(mass, 48)), + 'a_root_bracket': [str(low), str(high)], + 'a_upper_decimal': display(high), + 'kappa_planning_upper_decimal': display(cap_k), + 'selected_fraction_of_cap_decimal': display(kappa/cap_k), + 'max_gain_over_selected_percent_decimal': display(100*(cap_k/kappa-1)), + 'rank51_a_root_bracket': [str(old_low), str(old_high)], + 'rank51_kappa_upper_decimal': display(old_cap_k), + 'selected_kappa': str(kappa), + 'selected_complex_primitive_lower': str(complex_a), + 'bit_primitive_lower': str(bit), + } + + +def controls(replay, route, plan): + wrong = copy.deepcopy(route) + wrong['recipes'][0]['idle_children'][0]['rank'] += 1 + try: + route_ranks(wrong) + except ValueError as exc: + need('rank/axes' in str(exc), 'wrong rank control reason') + else: + raise ValueError('rank mismatch accepted') + wrong = copy.deepcopy(route) + child = next(c for c in wrong['recipes'][0]['idle_children'] if c['rank'] == 48) + child['rank'] = 49 + child['orthogonal_axes'].append(1 << 1024) + try: + route_ranks(wrong) + except ValueError as exc: + need('inventory changed' in str(exc), 'rank-49 control rejected for wrong reason') + else: + raise ValueError('rank-49 route accepted') + wrong = copy.deepcopy(replay) + wrong['complex_profile']['1'] += 288 + wrong['complex_profile']['2'] -= 144 + try: + profile(wrong, plan) + except ValueError: + pass + else: + raise ValueError('mass-preserving local drift accepted') + + +def main(): + need(not sys.flags.optimize, 'run without -O') + selected, replay, route, plan = sources() + controls(replay, route, plan) + output = result(selected, replay, route, plan) + encoded = (json.dumps(output, indent=2, sort_keys=True)+'\n').encode() + path = HERE/'RESULT.json' + if sys.argv[1:] == ['--write']: + path.write_bytes(encoded) + else: + need(not sys.argv[1:], 'usage: verify.py [--write]') + need(path.read_bytes() == encoded, 'RESULT.json differs from exact replay') + print(output['status'], 'max_idle_rank=48', 'a_upper='+output['a_upper_decimal'], + 'kappa_cap='+output['kappa_planning_upper_decimal'], 'controls=3') + + +if __name__ == '__main__': + main() From 691534353b8c5172f5c157e79496686d8c80f196 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 05:52:38 -0400 Subject: [PATCH 2/2] Source-bind fixed-route child capacities and fix packing-cap controls Check the selected T16 window capacities against the route child ranks, check that the selected owner map's hosted offsets tile capacity prefixes and reproduce the replay idle profile, and make the mass-preserving local-word control fail at the local-word check (it previously failed at the plan/replay binding). Add capacity and offset controls, refresh overlap (PR1276/PR1387 merged, PR1685) and update credit. Review and fixes by Claude (session 18) of OpenAI Codex's offline session 14 package. Co-Authored-By: Claude Opus 5.5 --- .../README.md | 8 +- .../RESULT.json | 2 + .../SOURCES.json | 6 + .../TASK.json | 6 +- .../VERIFY.json | 3 +- .../verify.py | 117 +++++++++++++----- 6 files changed, 106 insertions(+), 36 deletions(-) diff --git a/research/frontier1094-fixed-route-packing-cap/README.md b/research/frontier1094-fixed-route-packing-cap/README.md index c8ae5375d9..d3d0241883 100644 --- a/research/frontier1094-fixed-route-packing-cap/README.md +++ b/research/frontier1094-fixed-route-packing-cap/README.md @@ -4,7 +4,7 @@ ## Fixed inventory and proof -The source-bound route is `research/direct-delivery504-global/inputs/data-base/work/complex-nine-native/DATA-PHASES.json`. It is pinned by the selected `SELECTED-SOURCE.json` and byte-identical to the same member in `selected-replay.tar.gz`. The verifier recomputes GF(2) rank from every `orthogonal_axes` list. Each of the 112 port recipes has two rank-0, six rank-8, four rank-16, four rank-32, and four rank-48 children. Thus **no existing data-route child has rank above 48**. The selected manifest also pins the [parent T16 hosting proof](../gauge44-slots-t16/hosting/PROOF.md): a pending child has capacity `C_g`, hosting occupies a prefix of total width `U_g`, and its remaining suffix has rank `C_g−U_g`. The selected plan explicitly lifts that eight-replica geometry to sixteen replicas. Therefore a remainder after whole-helper hosting into one of these fixed children has rank at most 48. This is the extra premise beyond [the predecessor's rank-51 relaxation](../complex-local-word-ceiling/README.md). Axis transfer or repartitioning across child boundaries can make a rank above 48 without changing the total parent space, and is excluded. +The source-bound route is `research/direct-delivery504-global/inputs/data-base/work/complex-nine-native/DATA-PHASES.json`. It is pinned by the selected `SELECTED-SOURCE.json` and byte-identical to the same member in `selected-replay.tar.gz`. The verifier recomputes GF(2) rank from every `orthogonal_axes` list. Each of the 112 port recipes has two rank-0, six rank-8, four rank-16, four rank-32, and four rank-48 children. Thus **no existing data-route child has rank above 48**. The selected manifest also pins the [parent T16 hosting proof](../gauge44-slots-t16/hosting/PROOF.md): a pending-child group `g=(owner replica, child, port)` has capacity `C_g`, hosting occupies a prefix of total width `U_g`, and its remaining suffix has rank `C_g−U_g`. The selected plan explicitly lifts that eight-replica geometry to sixteen replicas. The verifier checks this premise against the selected sources rather than the proof text alone. All 288 `(owner replica, child)` window entries of the selected `PLAN.json` have capacity equal to the route rank of that child at every port (the two route children of rank 0 have no window). Every one of the 69,120 hosted helpers in the selected `OWNERS.json.gz` lies in its group's window. In each of the 32,256 groups, the hosted offsets tile `[0,U_g)` with `U_g ≤ C_g`. The remainders `C_g−U_g` reproduce the replay's idle profile `{1:2276, 3:377, 7:7, 48:4866}` exactly. Therefore a remainder after whole-helper hosting into one of these fixed children has rank at most `max C_g = 48`. This is the extra premise beyond [the predecessor's rank-51 relaxation](../complex-local-word-ceiling/README.md). Axis transfer or repartitioning across child boundaries can make a rank above 48 without changing the total parent space, and is excluded. The selected replay's `spec_sha256` binds the T16 `SPEC.json`; its `data.plan_sha256` binds `PLAN.json`. The plan and replay give 144 calls, 14,336 live families and the same complete profile. Subtracting the replay's idle profile and dividing by 144 gives the local profile per call `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}`. The complete rank mass is `1,041,408 = 72·14,336 + 64·144`; local mass is `5,586·144`, so idle mass is `237,024 = 4,938·48`. @@ -16,7 +16,7 @@ This is a favorable mass relaxation; the hypothetical 4,938 rank-48 idle childre The same engine independently reproduces the predecessor's rank-51 bracket `0.001690054109088 < root < 0.001690054109089`; its implied κ cap is `0.001687202645326`. The bit primitive lower exceeds the complex cap, so it does not bind this planning comparison. -Two open results have narrower or different domains. [PR1276](https://github.com/CrocSwap/integer-mult-bounds/pull/1276) bounds within-group idle-axis repartitions while allowing child ranks up to 51; [PR1387](https://github.com/CrocSwap/integer-mult-bounds/pull/1387) sharpens a selected idle-axis relaxation and gives a counterexample to an inherited admission check. Those analyses do not cover arbitrary whole-helper reassignment among the *unchanged* selected child bins. Their tighter numerical ceilings must not be combined with this cap without satisfying both scopes. The counterexample is also a reason to treat any proposed owner or axis edit as requiring fresh semantic admission. +Two merged results have narrower or different domains. [PR1276](https://github.com/CrocSwap/integer-mult-bounds/pull/1276) bounds within-group idle-axis repartitions while allowing child ranks up to 51; [PR1387](https://github.com/CrocSwap/integer-mult-bounds/pull/1387) sharpens a selected idle-axis relaxation and gives a counterexample to an inherited admission check. Those analyses do not cover arbitrary whole-helper reassignment among the *unchanged* selected child bins. Their tighter numerical ceilings must not be combined with this cap without satisfying both scopes. The counterexample is also a reason to treat any proposed owner or axis edit as requiring fresh semantic admission. The open [PR1685](https://github.com/CrocSwap/integer-mult-bounds/pull/1685) shows that at `a=0.00169`, at most 1,603 of the 237,024 idle mass units may sit at ranks ≤ 48. It leaves legal residual groups as its next question. This package answers that question for the fixed-route class: every legal remainder has rank ≤ 48, so the fixed route cannot reach `a=0.00169`, consistent with the rank-48 root above. Overlap was refreshed on 2026-10-14 at about 05:50 EDT (446 open PRs, 418 discussions). ## Reproduce @@ -27,7 +27,7 @@ python3.12 -I -B research/frontier1094-fixed-route-packing-cap/verify.py python3.12 scripts/research_package.py --package research/frontier1094-fixed-route-packing-cap ``` -The first command takes about 6 seconds on the local macOS host. It checks source hashes; selected record, review and replay paths; manifest, archive, spec and plan bindings; all 112 recipes' axes and ranks; profile splitting and the PR1012 coverage identity; exact endpoint signs; `RESULT.json`; and three failure controls. The controls reject a changed rank without matching axes, a rank-49 route child, and a mass-preserving change to the local word. Pinned sources are unchanged, so the selected cold replay is not part of this package check. +The first command takes about 4 seconds on the local macOS host. It checks source hashes; selected record, review and replay paths; manifest, archive, spec, plan and owner-map bindings; all 112 recipes' axes and ranks; window capacities against route ranks; the selected owner map's prefix offsets and idle remainders; profile splitting and the PR1012 coverage identity; exact endpoint signs; `RESULT.json`; and five failure controls, each of which must fail at its intended check. The controls reject a changed rank without matching axes, a rank-49 route child, a mass-preserving change to the local word applied consistently to plan and replay, a window capacity raised to 49, and an overlapping hosted offset. Pinned sources are unchanged, so the selected cold replay is not part of this package check. ## Scope and limitations @@ -42,4 +42,4 @@ The first command takes about 6 seconds on the local macOS host. It checks sourc ## Credit -Douglas Colkitt's [complex-local-word-ceiling](../complex-local-word-ceiling/README.md) supplies the rank-51 model and coverage-law application; PR1012 supplies the coverage identity. Rohan Arun's #1094 and Jeremy Kothe's T16 lineage supply the selected word and packing. The selected review credits the underlying data route, controller, bit supplier and outer composition. Prepared by Josie Elliston with substantial OpenAI Codex assistance. No independent human review is claimed. Apache-2.0. +Douglas Colkitt's [complex-local-word-ceiling](../complex-local-word-ceiling/README.md) supplies the rank-51 model and coverage-law application; PR1012 supplies the coverage identity. Rohan Arun's #1094 and Jeremy Kothe's T16 lineage supply the selected word and packing. The selected review credits the underlying data route, controller, bit supplier and outer composition. Prepared by Josie Elliston with substantial AI assistance: drafted by OpenAI Codex (offline session 14 of a donated overnight run), then reviewed, fixed and published by Claude (Anthropic). Claude added the source-bound capacity and offset checks and corrected a control that had been rejected for the wrong reason. No independent human review is claimed. Apache-2.0. diff --git a/research/frontier1094-fixed-route-packing-cap/RESULT.json b/research/frontier1094-fixed-route-packing-cap/RESULT.json index 4b1074bacc..b0a6aa20c3 100644 --- a/research/frontier1094-fixed-route-packing-cap/RESULT.json +++ b/research/frontier1094-fixed-route-packing-cap/RESULT.json @@ -19,6 +19,8 @@ "8": 8 }, "max_gain_over_selected_percent_decimal": "0.395177768158804506", + "max_pending_child_capacity": 48, + "pending_child_groups": 32256, "rank51_a_root_bracket": [ "52814190909/31250000000000", "1690054109089/1000000000000000" diff --git a/research/frontier1094-fixed-route-packing-cap/SOURCES.json b/research/frontier1094-fixed-route-packing-cap/SOURCES.json index 9fd91ee10a..78932cba62 100644 --- a/research/frontier1094-fixed-route-packing-cap/SOURCES.json +++ b/research/frontier1094-fixed-route-packing-cap/SOURCES.json @@ -38,6 +38,12 @@ "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" }, + { + "path": "research/complex-t16-rare-pattern-exchanges/data/OWNERS.json.gz", + "usage": "input", + "git_blob": "d3ba33d7e703a3229d9fb8a360f69d2f318bbb70", + "sha256": "87902c528dfab7d503dcf8a784260e3ab6fb7424c418a1820f7261f25be7b6bc" + }, { "path": "research/complex-t16-rare-pattern-exchanges/data/PLAN.json", "usage": "input", diff --git a/research/frontier1094-fixed-route-packing-cap/TASK.json b/research/frontier1094-fixed-route-packing-cap/TASK.json index b4face5367..2fb391e6f1 100644 --- a/research/frontier1094-fixed-route-packing-cap/TASK.json +++ b/research/frontier1094-fixed-route-packing-cap/TASK.json @@ -46,11 +46,11 @@ "scope_change_reason": "The selected-packing card allows an exact relaxation for a named residual problem. This fixes the data-route child inventory and proves a rank-48 cap, narrower than the predecessor rank-51 halving relaxation; it does not search for a new owner map.", "bottleneck_link": "The complex supplier binds the selected conditional result. The fixed-route cap leaves at most 0.395178% relative kappa headroom for owner packing of this word under the retained conversion, versus 0.86942% for the generic rank-51 relaxation.", "budget_minutes": 225, - "stop_rule": "Stop after source-binding the 112 route recipes, exact rank-48 and predecessor rank-51 root brackets, three negative controls, and package replay. Do not search another owner map.", + "stop_rule": "Stop after source-binding the 112 route recipes, exact rank-48 and predecessor rank-51 root brackets, five negative controls, and package replay. Do not search another owner map.", "outcome": "completed", - "evidence": "RESULT.json: all 112 route recipes have maximal child rank 48 (GF(2) rank recomputed); exact root a in (0.001682094870064,0.001682094870065); retained-transfer kappa cap 0.001679270178313; selected fraction of cap 99.606%; three controls. Source/archive/spec/plan chain checked.", + "evidence": "RESULT.json: all 112 route recipes have maximal child rank 48 (GF(2) rank recomputed); exact root a in (0.001682094870064,0.001682094870065); retained-transfer kappa cap 0.001679270178313; selected fraction of cap 99.606%; window capacities equal route ranks and selected owner offsets reproduce the replay idle profile; five controls. Source/archive/spec/plan/owner-map chain checked.", "author": "Josie Elliston", - "ai_assistance": "Substantial OpenAI Codex assistance in task refinement, proof analysis, verifier implementation and documentation. No independent human review.", + "ai_assistance": "Substantial AI assistance: OpenAI Codex (offline session 14) for task refinement, proof analysis, verifier implementation and documentation; Claude (Anthropic) for review, source-bound capacity/offset checks, control fixes and publication. No independent human review.", "open_questions": [ { "question": "Can the fixed route's per-child capacities and helper widths sharpen the rank-48 mass cap?", diff --git a/research/frontier1094-fixed-route-packing-cap/VERIFY.json b/research/frontier1094-fixed-route-packing-cap/VERIFY.json index 7753595251..9b727382be 100644 --- a/research/frontier1094-fixed-route-packing-cap/VERIFY.json +++ b/research/frontier1094-fixed-route-packing-cap/VERIFY.json @@ -9,6 +9,7 @@ "research/community-frontier1094-audit/SELECTED-SOURCE.json", "research/community-frontier1094-audit/selected-replay.tar.gz", "research/direct-delivery504-global/inputs/data-base/work/complex-nine-native/DATA-PHASES.json", + "research/complex-t16-rare-pattern-exchanges/data/OWNERS.json.gz", "research/complex-t16-rare-pattern-exchanges/data/PLAN.json", "research/complex-t16-rare-pattern-exchanges/data/SPEC.json", "research/gauge44-slots-t16/hosting/PROOF.md" @@ -21,7 +22,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Selected source/archive and parent hosting proof binding, 112-port binary ranks, local/idle split and coverage mass, independent rational interval root, rank-51 predecessor cross-check, three negative controls" + "checks": "Selected source/archive, owner-map and parent hosting proof binding, 112-port binary ranks, window capacities equal to route child ranks, selected owner offsets tile capacity prefixes and reproduce the replay idle profile, local/idle split and coverage mass, independent rational interval root, rank-51 predecessor cross-check, five negative controls" } ] } diff --git a/research/frontier1094-fixed-route-packing-cap/verify.py b/research/frontier1094-fixed-route-packing-cap/verify.py index 51b8a3ced8..76c96e5d83 100644 --- a/research/frontier1094-fixed-route-packing-cap/verify.py +++ b/research/frontier1094-fixed-route-packing-cap/verify.py @@ -1,9 +1,10 @@ #!/usr/bin/env python3 """Exact fixed-route rank-48 ceiling, independently of predecessor ceiling.py. -Apache-2.0. Josie Elliston, with substantial OpenAI Codex assistance. +Apache-2.0. Josie Elliston, with substantial AI assistance (OpenAI Codex draft; Claude review and fixes). """ import copy +import gzip import hashlib import json import sys @@ -18,6 +19,7 @@ ROUTE = 'research/direct-delivery504-global/inputs/data-base/work/complex-nine-native/DATA-PHASES.json' PLAN = 'research/complex-t16-rare-pattern-exchanges/data/PLAN.json' SPEC = 'research/complex-t16-rare-pattern-exchanges/data/SPEC.json' +OWNERS = 'research/complex-t16-rare-pattern-exchanges/data/OWNERS.json.gz' HOSTING_PROOF = 'research/gauge44-slots-t16/hosting/PROOF.md' ARCHIVE = 'research/community-frontier1094-audit/selected-replay.tar.gz' MEMBER = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' @@ -54,16 +56,19 @@ def sources(): need(manifest['files'][ROUTE] == sha(route_bytes), 'route not pinned by selected manifest') need(manifest['files'][PLAN] == sha((ROOT/PLAN).read_bytes()), 'plan not pinned by selected manifest') need(manifest['files'][SPEC] == sha((ROOT/SPEC).read_bytes()), 'spec not pinned by selected manifest') + owners_bytes = (ROOT/OWNERS).read_bytes() + need(manifest['files'][OWNERS] == sha(owners_bytes), 'owner map not pinned by selected manifest') need(manifest['files'][HOSTING_PROOF] == sha((ROOT/HOSTING_PROOF).read_bytes()), 'parent hosting proof not pinned by selected manifest') replay = read('research/community-frontier1094-audit/REPLAY.json') spec = read(SPEC) need(replay['spec_sha256'] == sha((ROOT/SPEC).read_bytes()), 'replay/spec binding') need(spec['data']['plan_sha256'] == sha((ROOT/PLAN).read_bytes()), 'spec/plan binding') + need(spec['data']['owners_sha256'] == sha(owners_bytes), 'spec/owner-map binding') with tarfile.open(ROOT / ARCHIVE, 'r:gz') as archive: member = archive.extractfile(MEMBER) need(member is not None and member.read() == route_bytes, 'selected archive route mismatch') - return selected, replay, json.loads(route_bytes), read(PLAN) + return selected, replay, json.loads(route_bytes), read(PLAN), json.loads(gzip.decompress(owners_bytes)) def gf2_rank(vectors): @@ -96,6 +101,53 @@ def route_ranks(route): return dict(sorted(total.items())) +def hosting(route, plan, owners, replay): + """Selected pending-child capacities are the route ranks; hosting is a prefix. + + Every T16 pending-child group g = (owner replica, child, port) takes its + capacity C_g from the selected plan's window catalogue. Check C_g against + the route child rank, check that each hosted helper lies in its group's + window, that hosted offsets tile the prefix [0, U_g) with U_g <= C_g, and + that the remainders C_g - U_g reproduce the replay's idle profile. + """ + rank = {(r['port'], i): c['rank'] for r in route['recipes'] + for i, c in enumerate(r['idle_children'])} + windows = {} + for key, (capacity, times) in plan['windows'].items(): + owner, child = map(int, key.split(',')) + windows[owner, child] = capacity, set(times) + lift = plan['replica_lift']['replicas'] + children = {child for _, child in windows} + need(set(windows) == {(o, c) for o in range(lift) for c in children}, 'window catalogue coverage') + for (owner, child), (capacity, _) in windows.items(): + for port in range(route['ports']): + need(capacity == rank[port, child], 'window capacity differs from route rank') + need(all(rank[port, child] == 0 for port in range(route['ports']) + for child in range(len(route['recipes'][0]['idle_children'])) if child not in children), + 'positive-rank route child missing from windows') + need(len(owners) == 144*480, 'selected owner-map size') + occupied = {} + for item in owners: + key = (item['owner_replica'], item['child'], item['port']) + need((key[0], key[1]) in windows and 0 <= key[2] < route['ports'], 'owner outside catalogue') + need(item['time'] in windows[key[0], key[1]][1], 'hosted call outside window') + need(type(item['width']) is int and item['width'] > 0, 'hosted width') + occupied.setdefault(key, []).append((item['offset'], item['width'])) + idle = Counter() + for (owner, child), (capacity, _) in windows.items(): + for port in range(route['ports']): + prefix = 0 + for offset, width in sorted(occupied.get((owner, child, port), [])): + need(offset == prefix, 'hosted offsets are not a disjoint prefix') + prefix += width + need(prefix <= capacity, 'hosted width exceeds child capacity') + if capacity > prefix: + idle[capacity-prefix] += 1 + need(dict(idle) == {int(r): n for r, n in replay['idle_remainder_profile'].items()}, + 'capacity minus hosted prefix differs from replay idle profile') + return max(c for c, _ in windows.values()), len(windows)*route['ports'] + + def profile(replay, plan): calls, live = replay['complete_invocations'], plan['live'] need((calls, live) == (144, 14336), 'selected calls/live changed') @@ -200,8 +252,10 @@ def display(x): return f'{scaled//10**digits}.{scaled%10**digits:0{digits}d}' -def result(selected, replay, route, plan): +def result(selected, replay, route, plan, owners): ranks = route_ranks(route) + max_capacity, groups = hosting(route, plan, owners, replay) + need(max_capacity == max(ranks) == 48, 'maximal pending-child capacity') calls, live, local, mass, idle = profile(replay, plan) low, high = bracket(local, calls, live, mass, 48) old_low, old_high = bracket(local, calls, live, mass, 51) @@ -221,6 +275,8 @@ def result(selected, replay, route, plan): 'scope': 'Selected fixed 112-port data-route children and local word; PR1012 coverage; whole-helper hosting into existing children; retained balanced transfer. Relaxation only, no new kappa.', 'route_sha256': sha((ROOT/ROUTE).read_bytes()), 'route_rank_counts': {str(r): n for r, n in ranks.items()}, + 'pending_child_groups': groups, + 'max_pending_child_capacity': max_capacity, 'calls': calls, 'live_families': live, 'local_per_call': {str(r): n for r, n in sorted(local.items())}, 'selected_idle': {str(r): n for r, n in sorted(idle.items())}, @@ -238,41 +294,46 @@ def result(selected, replay, route, plan): } -def controls(replay, route, plan): - wrong = copy.deepcopy(route) - wrong['recipes'][0]['idle_children'][0]['rank'] += 1 +def rejects(why, function, *args): try: - route_ranks(wrong) + function(*args) except ValueError as exc: - need('rank/axes' in str(exc), 'wrong rank control reason') + need(why in str(exc), f'control rejected for wrong reason: {exc} (wanted {why})') else: - raise ValueError('rank mismatch accepted') + raise ValueError('control accepted: ' + why) + + +def controls(replay, route, plan, owners): + wrong = copy.deepcopy(route) + wrong['recipes'][0]['idle_children'][0]['rank'] += 1 + rejects('rank/axes', route_ranks, wrong) wrong = copy.deepcopy(route) child = next(c for c in wrong['recipes'][0]['idle_children'] if c['rank'] == 48) child['rank'] = 49 child['orthogonal_axes'].append(1 << 1024) - try: - route_ranks(wrong) - except ValueError as exc: - need('inventory changed' in str(exc), 'rank-49 control rejected for wrong reason') - else: - raise ValueError('rank-49 route accepted') - wrong = copy.deepcopy(replay) - wrong['complex_profile']['1'] += 288 - wrong['complex_profile']['2'] -= 144 - try: - profile(wrong, plan) - except ValueError: - pass - else: - raise ValueError('mass-preserving local drift accepted') + rejects('inventory changed', route_ranks, wrong) + # Mass-preserving local-word drift, applied consistently to plan and replay + # so that the plan/replay binding passes and the local-word check must fire. + wrong_replay, wrong_plan = copy.deepcopy(replay), copy.deepcopy(plan) + for profile_ in (wrong_replay['complex_profile'], wrong_plan['profile']): + profile_['1'] += 288 + profile_['2'] -= 144 + rejects('local word changed', profile, wrong_replay, wrong_plan) + wrong = copy.deepcopy(plan) + key = next(k for k, (c, _) in wrong['windows'].items() if c == 48) + wrong['windows'][key][0] = 49 + rejects('window capacity differs', hosting, route, wrong, owners, replay) + wrong = copy.deepcopy(owners) + item = next(i for i in wrong if i['offset'] > 0) + item['offset'] -= 1 + rejects('disjoint prefix', hosting, route, plan, wrong, replay) def main(): need(not sys.flags.optimize, 'run without -O') - selected, replay, route, plan = sources() - controls(replay, route, plan) - output = result(selected, replay, route, plan) + selected, replay, route, plan, owners = sources() + controls(replay, route, plan, owners) + output = result(selected, replay, route, plan, owners) encoded = (json.dumps(output, indent=2, sort_keys=True)+'\n').encode() path = HERE/'RESULT.json' if sys.argv[1:] == ['--write']: @@ -281,7 +342,7 @@ def main(): need(not sys.argv[1:], 'usage: verify.py [--write]') need(path.read_bytes() == encoded, 'RESULT.json differs from exact replay') print(output['status'], 'max_idle_rank=48', 'a_upper='+output['a_upper_decimal'], - 'kappa_cap='+output['kappa_planning_upper_decimal'], 'controls=3') + 'kappa_cap='+output['kappa_planning_upper_decimal'], 'controls=5') if __name__ == '__main__':