diff --git a/research/rank7-idle-star-exchanges-t740/AUDIT.json b/research/rank7-idle-star-exchanges-t740/AUDIT.json new file mode 100644 index 0000000000..7b5fbcff94 --- /dev/null +++ b/research/rank7-idle-star-exchanges-t740/AUDIT.json @@ -0,0 +1,30 @@ +{ + "fill_rebound": true, + "gain_over_pr3148": "411566555253748209/1000000000000000000000000", + "kappa": "17301890612338507600949999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "moves": 125706, + "profile": { + "1": 16376940, + "2": 4821840, + "3": 1567431, + "4": 679320, + "42": 45543, + "45": 34620, + "48": 76700, + "5": 147075, + "51": 125706, + "8": 53280 + }, + "rejected_controls": { + "axis_moved_twice": "axis moved twice", + "centre_is_leaf": "centre is also a leaf", + "foreign_axis": "foreign axis", + "hosted_child": "centre/leaf must be idle children of the group", + "next_root_grid": "moment < 1 at lower endpoint", + "non_commuting_axis": "axis does not commute with leaf axes", + "reused_leaf": "leaf reused", + "two_axes_only": "exactly three distinct axes", + "wrong_profile": "declared profile" + }, + "status": "PASS_IDLE48_STAR_EXCHANGE_AUDIT" +} diff --git a/research/rank7-idle-star-exchanges-t740/CLAIM.json b/research/rank7-idle-star-exchanges-t740/CLAIM.json new file mode 100644 index 0000000000..e0582d711b --- /dev/null +++ b/research/rank7-idle-star-exchanges-t740/CLAIM.json @@ -0,0 +1,27 @@ +{ + "kappa": "17301890612338507600949999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "kappa_decimal": "0.0017301890612338507600949999999999999999999998999999999999999999999999", + "root": [ + "17301890612338507600957/10000000000000000000000000", + "8650945306169253800479/5000000000000000000000000" + ], + "baseline": "PR3148 (open; Jeremy Diviney) head f2927a4b8", + "baseline_kappa": "17297774946785970118859999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "gain": "411566555253748209/1000000000000000000000000", + "profile": { + "1": 16376940, + "2": 4821840, + "3": 1567431, + "4": 679320, + "5": 147075, + "8": 53280, + "42": 45543, + "45": 34620, + "48": 76700, + "51": 125706 + }, + "T": 740, + "changed_hypothesis": "idle capacity moved between completely idle capacity-48 children of one (replica, port) by PR1252-rule star exchanges", + "status": "author-checked conditional candidate; complete T74/T740 native admission and outer release with the overlay not rerun", + "credits": "PR1252 Gonzalo-Mier; frontier1094-idle-star-ceiling Gueorgui Maissouradze; PR3148 Jeremy Diviney; PR3133/PR3042 dcharb78; PR2979 Marius-Paul Dumitrean; OpenCode (Space bunny free); Anthropic Claude" +} \ No newline at end of file diff --git a/research/rank7-idle-star-exchanges-t740/IDLE-48-BINS.json.gz b/research/rank7-idle-star-exchanges-t740/IDLE-48-BINS.json.gz new file mode 100644 index 0000000000..8503480124 Binary files /dev/null and b/research/rank7-idle-star-exchanges-t740/IDLE-48-BINS.json.gz differ diff --git a/research/rank7-idle-star-exchanges-t740/README.md b/research/rank7-idle-star-exchanges-t740/README.md new file mode 100644 index 0000000000..4742d06a7e --- /dev/null +++ b/research/rank7-idle-star-exchanges-t740/README.md @@ -0,0 +1,139 @@ +# Idle rank-48 star exchanges on PR3148's T740 fill: conditional κ = 0.001730189061233850760095 − 10⁻⁴⁶ − 10⁻⁷⁰ + +**Author-checked conditional candidate; not maintainer-reviewed.** The selected record +on `main` remains #1094 (κ = 0.001672660197076918). This package stacks on the open, +unreviewed PR3148 (Jeremy Diviney: PR3133's words at their T740 packing cap) and does not +change its words, helpers, fill rows, order or dispatch. + +```text + complex root bracket (1e-25) κ headline +PR3148 (baseline) [0.0017297774946785970118869, ...8870] 0.001729777494678597011886 − 1e-46 − 1e-70 +this package [0.0017301890612338507600957, ...0958] 0.001730189061233850760095 − 1e-46 − 1e-70 +gain +4.11566555253748209e-7 (+0.0238%) +``` + +## Changed hypothesis + +PR3133's fixed-capacity relaxation cap (RELAX-CAP) and PR3148's cap-attaining fill both +charge **one idle child per bin, of rank `capacity − used`**. They never move idle +capacity *between* bins. In PR3148's fill, **282,569** capacity-48 bins are completely +idle: no helper row touches them. They lie in 82,880 (replica, port) groups of sizes +`{1: 414, 2: 19103, 3: 9503, 4: 53860}`. + +Gonzalo-Mier's PR1252 showed on #1094 that two such children can exchange three axes, +`48 + 48 → 45 + 51`. The move is legal when every moved axis commutes with all of the +receiver's axes, every stage entry/exit X and Y translation, the terminal Y translation +and both children's terminal translations. The group's total axis set, and hence its Z4 +phase polynomial, is unchanged. `research/frontier1094-idle-star-ceiling` (Guéorgui +Maissouradze) extended this to **stars**: one centre sends three axes to each of several +leaves. + +**The data needed for this rule is on main.** The rank-seven T74/T740 lineage uses the +same exact data-phase recipe as #1094 (`DATA-PHASES.json`, SHA-256 +`c5916ff3…e8251fa`; GLOBAL-TEMPLATE `exact_data_phase_recipe_sha256`). Its per-port idle +children carry the orthogonal axis sets. For all 4,866 #1094 idle rank-48 children, these +axes equal the hosted `IDLE-REMAINDER-FRAMES` that PR1252 used, so legality is a +port-local property. It does not depend on the replica or on the local word. + +## Result + +The exhaustive per-group star optimum covers every role assignment of the idle children +(untouched, centre, or leaf of one centre). Each candidate is checked by an exact +disjoint 3-axis matching: + +| Group shape after exchange | Groups | +|---|---:| +| `[51,51,48,42]` | 37,080 | +| `[48,48]` (no movable axes) | 19,083 | +| `[51,51,45,45]` | 16,780 | +| `[51,51,42]` | 8,463 | +| `[51,48,45]` | 1,040 | +| `[48]` (singleton) | 414 | +| `[51,45]` | 20 | + +The search makes 125,706 three-axis moves and changes 205,869 children. The idle bill +`{48: 282569}` becomes `{42: 45543, 45: 34620, 48: 76700, 51: 125706}`. The rank mass +`65088·740` is unchanged. The maximum child rank is 51, and the finite halving guard still +holds: `73² = 5329 > 2·51² = 5202`. + +The complete paid profile is +`{1:16376940, 2:4821840, 3:1567431, 4:679320, 5:147075, 8:53280, 42:45543, 45:34620, 48:76700, 51:125706}`. + +The complex side still binds: the bit supplier is #589 at 0.001733427… > 0.00173019. The +within-group ceiling (any repartition of each group, `51^(k−1), 51−3k`) has root +0.00173069001404…. The star class captures 45% of that headroom. + +## Reproduce + +```sh +# baseline input: PR3148's own deterministic materializer (head f2927a4b) +python3 -B research/coupled-carrier-cap740/materialize.py --output /tmp/t740 # on PR3148's branch +python3 -B research/rank7-idle-star-exchanges-t740/build.py --fill /tmp/t740/COMPOSED-FILL.json.gz +python3 -B research/rank7-idle-star-exchanges-t740/verify.py --fill /tmp/t740/COMPOSED-FILL.json.gz +``` + +`build.py` authenticates DATA-PHASES and the decoded PR3148 fill payload +(`8f4d6965…`). It then derives `IDLE-48-BINS.json.gz` and `STAR-MOVES.json.gz`, and +writes `RESULT.json` with an exact rational root bracket. That bracket reproduces +PR3148's published one exactly for the baseline profile. Building takes about 15 s. + +`verify.py` does not import `build.py`. It works from the committed files and does not +need the fill; the optional `--fill` flag rebinds the idle bins. It re-derives: + +- every moved axis's commuting rule; +- disjoint stars, single-use axes and single-centre leaves; +- orthonormal, independent final axis sets; +- unchanged per-group axis multisets; +- the rank cap and halving guard; +- the complete profile and rank mass; +- the root bracket, using its own directed-rounding interval arithmetic (10⁻⁷²); +- the headline κ, gated above PR3148 and PR3143. + +All nine mutation controls are rejected: non-commuting axis, axis moved twice, reused +leaf, foreign axis, centre that is also a leaf, hosted child, two-axis move, wrong profile +and the next root grid point. The receipt is `AUDIT.json`; the run takes about 3.5 min. + +## Scope and remaining obligations + +What is established: a literal, port-local axis overlay on PR3148's untouched idle +children. Every move satisfies PR1252's commuting rule, and the exact complete-profile +root with the lineage's headline convention is computed. + +What is **not** run here: + +- PR3148/PR3133's complete native admission, controller/owner audit and modern outer + release with this overlay. That audit, `audit_mixed.py` in the T74 release chain, must + be generalized to read idle axis overlays, as PR1252 did for the #1094 async auditor. +- Re-pinning the outer finite check `halving_integer_inequality = [5329, 4608]` to + `[5329, 5202]`. + +Soundness of the star class is inherited from PR1252's pair argument (unchanged group +axis set and phase polynomial, commuting moved axes), as in the star-ceiling package. All +inherited all-size compiler, realization, hosting, precision/tape, recovery and +analytic-transfer obligations of the lineage remain. PR3148 itself is an unreviewed +author claim; if it is not admitted, the same overlay applies to PR3133's T74 fill. + +## Open next questions + +- **Does the star overlay pass the T74 controller/owner audit and outer release?** Only then + is this κ an admitted finite candidate. First step: generalize the T74 `audit_mixed.py` to + read the idle-axis overlay and rerun PR3148's release. Blocked by: the release chain has no + overlay reader. +- **Partially hosted remainders as donors** (PR3190) push the complex root past the bit side. + +## Credit + +- Gonzalo-Mier (PR1252): the idle exchange move, its commuting rule and its pricing + recipe. +- Guéorgui Maissouradze (PatatePatatePatate): the star class and the per-group optimum + (`frontier1094-idle-star-ceiling`). +- Jeremy Diviney (PR3148): the T740 cap-attaining fill. +- dcharb78 (PR3133, PR3042): the words. +- Marius-Paul Dumitrean (PR2979). +- Jeremy Kothe (PR3015). +- Nick Petalas (PR3024 lift). +- The credited rank-seven, T37-envelope and data-phase lineage. + +Prepared by Rohan Arun. This was done with help from **OpenCode (Space bunny free)**, +which identified the idle-exchange lever and proposed porting it to the rank-seven line, +and with substantial Anthropic Claude assistance. Apache-2.0. diff --git a/research/rank7-idle-star-exchanges-t740/RESULT.json b/research/rank7-idle-star-exchanges-t740/RESULT.json new file mode 100644 index 0000000000..08fdf8c278 --- /dev/null +++ b/research/rank7-idle-star-exchanges-t740/RESULT.json @@ -0,0 +1,117 @@ +{ + "status": "PASS_IDLE48_STAR_EXCHANGES_T740", + "T": 740, + "idle48": 282569, + "groups": 82880, + "group_sizes": { + "1": 414, + "2": 19103, + "3": 9503, + "4": 53860 + }, + "movable_axis_counts": { + "0": 448, + "3": 280, + "15": 616 + }, + "moves": 125706, + "changed_children": 205869, + "shapes": [ + [ + [ + 51, + 51, + 48, + 42 + ], + 37080 + ], + [ + [ + 48, + 48 + ], + 19083 + ], + [ + [ + 51, + 51, + 45, + 45 + ], + 16780 + ], + [ + [ + 51, + 51, + 42 + ], + 8463 + ], + [ + [ + 51, + 48, + 45 + ], + 1040 + ], + [ + [ + 48 + ], + 414 + ], + [ + [ + 51, + 45 + ], + 20 + ] + ], + "baseline_profile": { + "1": 16376940, + "2": 4821840, + "3": 1567431, + "4": 679320, + "5": 147075, + "8": 53280, + "48": 282569 + }, + "profile": { + "1": 16376940, + "2": 4821840, + "3": 1567431, + "4": 679320, + "5": 147075, + "8": 53280, + "42": 45543, + "45": 34620, + "48": 76700, + "51": 125706 + }, + "baseline_root": [ + "17297774946785970118869/10000000000000000000000000", + "1729777494678597011887/1000000000000000000000000" + ], + "root": [ + "17301890612338507600957/10000000000000000000000000", + "8650945306169253800479/5000000000000000000000000" + ], + "root_decimal": [ + "17301890612338507600957e-25", + "17301890612338507600958e-25" + ], + "kappa": "17301890612338507600949999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "pr3148_kappa": "17297774946785970118859999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "gain_over_pr3148": "411566555253748209/1000000000000000000000000", + "within_group_ceiling_root_lower": "17306900140466462208079/10000000000000000000000000", + "max_child_rank": 51, + "halving": [ + 5329, + 5202 + ] +} diff --git a/research/rank7-idle-star-exchanges-t740/SOURCES.json b/research/rank7-idle-star-exchanges-t740/SOURCES.json new file mode 100644 index 0000000000..b6bd6d61d4 --- /dev/null +++ b/research/rank7-idle-star-exchanges-t740/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "research/adaptive-kernel-demotion/inputs/DATA-PHASES.json", + "usage": "input", + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + { + "path": "research/frontier1094-idle-star-ceiling/README.md", + "usage": "provenance", + "git_blob": "dc62e4569948a9e10bb1c72731a9ddfdc81fe0cd", + "sha256": "2f640127f48be627f10a8db1d224d8a75219772525b3c0d5d3251dc8dc57b121" + } + ] +} diff --git a/research/rank7-idle-star-exchanges-t740/STAR-MOVES.json.gz b/research/rank7-idle-star-exchanges-t740/STAR-MOVES.json.gz new file mode 100644 index 0000000000..ef209aa4a9 Binary files /dev/null and b/research/rank7-idle-star-exchanges-t740/STAR-MOVES.json.gz differ diff --git a/research/rank7-idle-star-exchanges-t740/TASK.json b/research/rank7-idle-star-exchanges-t740/TASK.json new file mode 100644 index 0000000000..0b82da3552 --- /dev/null +++ b/research/rank7-idle-star-exchanges-t740/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "selected-packing", + "priority_revision": 6, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "original_card": { + "id": "selected-packing", + "question": "Is there a genuinely unsearched, explicitly bounded improvement to the selected packing?", + "starting_points": [ + "certificates/selected-result.json", + "research/heterogeneous-owner-assembly/README.md", + "research/complex-local-word-ceiling/README.md" + ], + "methods": [ + "Search a named unclaimed canonical candidate domain with a reproducible partition.", + "Prove a stronger scoped relaxation or exact optimum for one named residual subproblem." + ], + "acceptance_gate": "Check live PR overlap first, price both suppliers and distinguish a search best from an optimum. Report the word's packing cap from ceiling.ceiling() and the fraction of it realized; label packing gains as such.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Locate the selected packing source in the review and check live PRs for the same residual problem.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Define an unclaimed canonical domain and a favorable bound before starting a new search.", + "bottleneck_link": "An actual paid-profile gain can improve the frontier up to the other supplier cap.", + "allowed_variations": [ + "One bounded residual packing instance or exact relaxation.", + "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": [ + "Rerunning an existing search with only a different seed as a separate mathematical contribution." + ], + "overlap_terms": [ + "T16", + "owner exchange", + "packing" + ], + "existing_checks": [ + { + "scope": "Packing-independent ceiling for the selected paid profile under the one-unpaid-coordinate coverage and halving guard.", + "evidence": "docs/research/community-efficient1000-review.md", + "remaining": "A changed word or model requires new pricing; a local packing search must name uncovered scope.", + "status": "reviewed", + "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Changed residual subproblem on the open PR3148 T740 fill of PR3133's words (not the selected #1094 packing): the 282,569 completely idle capacity-48 children; PR1252-rule star exchanges with the exact per-group star optimum.", + "scope_change_reason": "The card targets the selected packing; this applies the same idle-repartition mechanism (PR1252 / frontier1094-idle-star-ceiling) to the open rank-seven T740 line, whose relaxation cap charges one idle child per bin.", + "bottleneck_link": "Repartitioning idle children changes the paid histogram and so moves the exact complex endpoint.", + "budget_minutes": 120, + "stop_rule": "Stop after the exact overlay, pricing and an independent structural verifier; no controller/outer admission in this session.", + "outcome": "partial", + "evidence": "RESULT.json, IDLE-48-BINS.json.gz, STAR-MOVES.json.gz (125,706 moves), AUDIT.json (9/9 controls rejected).", + "author": "Rohan Arun", + "ai_assistance": "Substantial Anthropic Claude (Claude Code) assistance; idea seeded with help from OpenCode (Space bunny free).", + "open_questions": [ + { + "question": "Does the star overlay pass the T74 controller/owner audit and outer release?", + "why_it_matters": "Only then is the kappa an admitted finite candidate rather than a priced structural lead.", + "first_step": "Generalize the T74 audit_mixed.py to read the idle-axis overlay and rerun PR3148's release.", + "blocked_by": "No overlay reader in the T74 release chain." + } + ] +} diff --git a/research/rank7-idle-star-exchanges-t740/VERIFY.json b/research/rank7-idle-star-exchanges-t740/VERIFY.json new file mode 100644 index 0000000000..11f36c8941 --- /dev/null +++ b/research/rank7-idle-star-exchanges-t740/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/adaptive-kernel-demotion/inputs/DATA-PHASES.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Independent of build.py: commuting rule for every moved axis, disjoint stars and axes, orthonormal final sets, unchanged group multisets, rank cap and halving guard, profile and rank mass, exact root bracket with its own interval arithmetic, kappa gates over PR3148/PR3143; 9 mutation controls rejected." + } + ] +} diff --git a/research/rank7-idle-star-exchanges-t740/build.py b/research/rank7-idle-star-exchanges-t740/build.py new file mode 100644 index 0000000000..74e23e93b0 --- /dev/null +++ b/research/rank7-idle-star-exchanges-t740/build.py @@ -0,0 +1,245 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Build idle rank-48 star exchanges on PR3148's T740 fill of PR3133's words. + +Inputs (both authenticated by SHA-256 of their decoded payload): + * DATA-PHASES.json on main (exact data-phase recipe c5916ff3..., shared by the + #1094 lineage and the T74/T740 rank-seven lineage); + * PR3148's COMPOSED-FILL.json.gz, regenerated by its own materialize.py. + +Outputs (deterministic): IDLE-48-BINS.json.gz, STAR-MOVES.json.gz, RESULT.json. + +The move and its commuting rule are Gonzalo-Mier's PR1252; the star class and its +exhaustive per-group optimum follow research/frontier1094-idle-star-ceiling. +""" +import argparse, gzip, hashlib, itertools, json, math +from collections import Counter, defaultdict +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PHASES = ROOT / 'research/adaptive-kernel-demotion/inputs/DATA-PHASES.json' +PHASES_SHA = 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' +FILL_PAYLOAD_SHA = '8f4d6965ba573ff2b71fd7bf6b552643e086739d90bd73c55889502077638e00' +T = 740 +# PR3148 complete paid profile (CLAIM.json 'profile'): 6,660 local bills + idle bill. +PR3148_PROFILE = {1: 16376940, 2: 4821840, 3: 1567431, 4: 679320, 5: 147075, 8: 53280, 48: 282569} +PR3148_KAPPA = Q('17297774946785970118859999999999999999999998999999999999999999999999/' + '10000000000000000000000000000000000000000000000000000000000000000000000') +CAP48 = (8, 10, 12, 13) + + +def need(ok, why): + if not ok: + raise SystemExit('FAIL: ' + why) + + +def dot(a, b): + return (a & b).bit_count() & 1 + + +def portable_gzip(obj): + raw = json.dumps(obj, sort_keys=True, separators=(',', ':')).encode() + data = bytearray(gzip.compress(raw, mtime=0)); data[9] = 255 + return bytes(data) + + +# ---------------- exact pricing (rational interval arithmetic) ---------------- +SCALE = 10 ** 60 + + +def down(x): return Q(math.floor(x * SCALE), SCALE) +def up(x): return Q(math.ceil(x * SCALE), SCALE) + + +def ln_ratio(r): + """enclosure of ln(73/r) for integer 1 <= r <= 73 via atanh series.""" + x = Q(73, r); k = 0 + while x > 2: x /= 2; k += 1 + z = (x - 1) / (x + 1); s = Q(0); p = z + for j in range(80): + s += p / (2 * j + 1); p *= z * z + tail = 2 * p / (161 * (1 - z * z)) + ln2_lo, ln2_hi = ln2() + return down(2 * s + k * ln2_lo), up(2 * s + tail + k * ln2_hi) + + +def ln2(): + z = Q(1, 3); s = Q(0); p = z + for j in range(120): + s += p / (2 * j + 1); p *= z * z + return 2 * s, 2 * s + 2 * p / (241 * (1 - z * z)) + + +def exp_enc(lo, hi): + def series(x): + s = Q(0); t = Q(1) + for n in range(1, 40): + s += t; t = t * x / n + return s, t # remainder bounded by 2*t for 0<=x<=1 + a, ta = series(lo); b, tb = series(hi) + return down(a), up(b + 2 * tb) + + +LN = {} + + +def moment(profile, b, W): + lo = hi = Q(0) + for r, n in profile.items(): + if r not in LN: LN[r] = ln_ratio(r) + L0, L1 = LN[r] + e0, e1 = exp_enc(b * L0, b * L1) + lo += n * r * e0; hi += n * r * e1 + return lo / (73 * W), hi / (73 * W) + + +def root(profile, digits=25): + W = 896 * T + need(sum(r * n for r, n in profile.items()) == 65088 * T, 'complete rank mass 65088*T') + need(73 * 73 > 2 * max(profile) ** 2, 'halving guard') + # float start, then exact bisection on the 10^-digits grid + f = lambda b: sum(n * r * (73 / r) ** b for r, n in profile.items()) / (73 * W) - 1 + a, c = 0.0, 0.01 + for _ in range(200): + m = (a + c) / 2 + if f(m) < 0: a = m + else: c = m + g = 10 ** digits + k0 = int(a * g) - 10 ** 10; k1 = int(a * g) + 10 ** 10 + need(moment(profile, Q(k0, g), W)[1] < 1 and moment(profile, Q(k1, g), W)[0] > 1, 'bracket start') + while k1 - k0 > 1: + k = (k0 + k1) // 2 + mlo, mhi = moment(profile, Q(k, g), W) + if mhi < 1: k0 = k + elif mlo > 1: k1 = k + else: raise SystemExit('interval too wide at ' + str(k)) + return Q(k0, g), Q(k1, g) + + +def headline(lo): + """lineage convention (PR2857 ... PR3148): floor(root_lower, 24 digits) - 1e-46 - 1e-70.""" + return Q(math.floor(lo * 10 ** 24), 10 ** 24) - Q(1, 10 ** 46) - Q(1, 10 ** 70) + + +# ---------------- moves ---------------- +def recipes(): + raw = PHASES.read_bytes(); need(hashlib.sha256(raw).hexdigest() == PHASES_SHA, 'DATA-PHASES pin') + return {r['port']: r for r in json.loads(raw)['recipes']} + + +def movable(rc, d, r): + ys = [int(s[k]) for s in rc['stage_alignment'] for k in ('entry_Y', 'exit_Y')] + [int(rc['terminal_Y_translation'])] + xs = [int(s[k]) for s in rc['stage_alignment'] for k in ('entry_X', 'exit_X')] + tr = [int(rc['idle_children'][c]['translation_after']) for c in (d, r)] + ra = [int(v) for v in rc['idle_children'][r]['orthogonal_axes']] + return [int(v) for v in rc['idle_children'][d]['orthogonal_axes'] + if all(dot(int(v), x) == 0 for x in ra + ys + xs + tr)] + + +def H(r, b=0.00173): return r * (73.0 / r) ** b + + +def best_star(MV, kids): + """exhaustive role assignment (none / centre / leaf-of-centre); leaves get exactly 3 axes; + stars disjoint; a centre's moved axes disjoint across its leaves.""" + kids = sorted(kids); best = [len(kids) * H(48), []] + + def match(c, leaves): + opts = [MV[c, l] for l in leaves] + if any(len(o) < 3 for o in opts): return None + def go(k, used): + if k == len(leaves): return [] + for trip in itertools.combinations([v for v in opts[k] if v not in used], 3): + rest = go(k + 1, used | set(trip)) + if rest is not None: return [(c, leaves[k], list(trip))] + rest + return None + return go(0, set()) + + def assign(i, roles): + if i == len(kids): + leaves = defaultdict(list) + for c in kids: + if isinstance(roles[c], tuple): leaves[roles[c][1]].append(c) + cents = [c for c in kids if roles[c] == 'c'] + if any(not leaves[c] for c in cents) or any(roles[x] != 'c' for x in leaves): return + moves = [] + for c in cents: + m = match(c, leaves[c]) + if m is None: return + moves += m + ranks = [48 - 3 * len(leaves[c]) if roles[c] == 'c' else 51 if isinstance(roles[c], tuple) else 48 for c in kids] + cost = sum(H(x) for x in ranks) + if cost < best[0] - 1e-12: best[0], best[1] = cost, moves + return + c = kids[i] + for opt in ['n', 'c'] + [('l', d) for d in kids if d != c]: + roles[c] = opt; assign(i + 1, roles) + del roles[c] + assign(0, {}) + return best[1] + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--fill', type=Path, required=True, help="PR3148's materialized COMPOSED-FILL.json.gz") + a = ap.parse_args() + raw = gzip.decompress(a.fill.read_bytes()) + need(hashlib.sha256(raw).hexdigest() == FILL_PAYLOAD_SHA, 'PR3148 fill payload pin') + fill = json.loads(raw); rec = recipes() + need(fill['columns'] == ['time', 'helper', 'owner_replica', 'child', 'port', 'offset'], 'fill columns') + need(fill['dispatch_overrides'] == [], 'no dispatch overrides') + touched = {(rep, child, port) for _, _, rep, child, port, _ in fill['rows']} + need(all(rec[p]['idle_children'][c]['rank'] == 48 for p in rec for c in CAP48), 'four capacity-48 children per port') + groups = [] + for rep in range(T): + for p in range(112): + kids = [c for c in CAP48 if (rep, c, p) not in touched] + if kids: groups.append([rep, p, kids]) + n48 = sum(len(g[2]) for g in groups) + need(n48 == PR3148_PROFILE[48], 'idle rank-48 count equals PR3148 idle bill') + MV = {(p, d, r): movable(rec[p], d, r) for p in rec for d in CAP48 for r in CAP48 if d != r} + cache, moves, shapes = {}, [], Counter() + for rep, p, kids in groups: + key = (p, tuple(kids)) + if key not in cache: + cache[key] = best_star({(d, r): MV[p, d, r] for d in kids for r in kids if d != r}, kids) + rk = Counter({c: 48 for c in kids}) + for c, l, ax in cache[key]: + moves.append([rep, p, c, l, ax]); rk[c] -= 3; rk[l] += 3 + shapes[tuple(sorted(rk.values(), reverse=True))] += 1 + idle = Counter() + for s, n in shapes.items(): + for r in s: idle[r] += n + profile = Counter(PR3148_PROFILE); del profile[48]; profile.update(idle) + profile = dict(sorted(profile.items())) + lo, hi = root(profile) + blo, bhi = root(PR3148_PROFILE) + kappa = headline(lo) + need(kappa > PR3148_KAPPA, 'exceeds PR3148') + # context prices: pair class (no centre with two leaves) and the within-group ceiling + ceiling = Counter(PR3148_PROFILE); del ceiling[48] + for rep, p, kids in groups: + k = len(kids) + if k == 1: ceiling[48] += 1 + else: ceiling[51] += k - 1; ceiling[51 * 1 + 48 * k - 51 * k] += 1 + clo, _ = root(dict(ceiling)) + (HERE / 'IDLE-48-BINS.json.gz').write_bytes(portable_gzip(dict(T=T, fill_payload_sha256=FILL_PAYLOAD_SHA, groups=groups))) + (HERE / 'STAR-MOVES.json.gz').write_bytes(portable_gzip(dict(columns=['replica', 'port', 'centre_child', 'leaf_child', 'moved_axes'], moves=moves))) + result = dict(status='PASS_IDLE48_STAR_EXCHANGES_T740', T=T, idle48=n48, groups=len(groups), + group_sizes={str(k): v for k, v in sorted(Counter(len(g[2]) for g in groups).items())}, + movable_axis_counts={str(k): v for k, v in sorted(Counter(map(len, MV.values())).items())}, + moves=len(moves), changed_children=len({(m[0], m[1], m[2]) for m in moves} | {(m[0], m[1], m[3]) for m in moves}), + shapes=[[list(s), n] for s, n in shapes.most_common()], + baseline_profile={str(k): v for k, v in PR3148_PROFILE.items()}, profile={str(k): v for k, v in profile.items()}, + baseline_root=[str(blo), str(bhi)], root=[str(lo), str(hi)], + root_decimal=[f'{lo.numerator * 10**25 // lo.denominator}e-25', f'{hi.numerator * 10**25 // hi.denominator}e-25'], + kappa=str(kappa), pr3148_kappa=str(PR3148_KAPPA), gain_over_pr3148=str(kappa - PR3148_KAPPA), + within_group_ceiling_root_lower=str(clo), max_child_rank=max(profile), halving=[73 * 73, 2 * max(profile) ** 2]) + (HERE / 'RESULT.json').write_text(json.dumps(result, indent=1) + '\n') + print('PASS', float(lo), float(kappa - PR3148_KAPPA), result['shapes']) + + +if __name__ == '__main__': + main() diff --git a/research/rank7-idle-star-exchanges-t740/verify.py b/research/rank7-idle-star-exchanges-t740/verify.py new file mode 100644 index 0000000000..fbe7039b8e --- /dev/null +++ b/research/rank7-idle-star-exchanges-t740/verify.py @@ -0,0 +1,249 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent verifier for the idle rank-48 star exchanges on PR3148's T740 fill. + +Does not import build.py. From the committed IDLE-48-BINS / STAR-MOVES, the +pinned DATA-PHASES recipe and PR3148's complete paid profile it re-derives: +every moved axis's commuting rule, disjointness of stars and axes, orthonormal +final axis sets, unchanged per-group axis multisets (hence each group's Z4 phase +polynomial), the rank cap 51 and halving guard, the complete changed profile and +rank mass, and an exact rational root bracket with its own interval arithmetic. +Optional --fill re-derives IDLE-48-BINS from PR3148's materialized fill. +Mutation controls must all be rejected. +""" +import argparse, copy, gzip, hashlib, json, sys +from collections import Counter, defaultdict +from fractions import Fraction as F +from pathlib import Path + +PKG = Path(__file__).resolve().parent +PHASES = PKG.parents[1] / 'research/adaptive-kernel-demotion/inputs/DATA-PHASES.json' +PHASES_SHA = 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' +FILL_PAYLOAD_SHA = '8f4d6965ba573ff2b71fd7bf6b552643e086739d90bd73c55889502077638e00' +T = 740 +BASE = {1: 16376940, 2: 4821840, 3: 1567431, 4: 679320, 5: 147075, 8: 53280, 48: 282569} +GATES = { + 'PR3148': F('17297774946785970118859999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000'), + 'PR3143': F('172977608940512033423846781989357386829999999999999999999998999999999999999999999999/100000000000000000000000000000000000000000000000000000000000000000000000000000000000000'), +} + + +class Reject(Exception): + pass + + +def req(ok, why): + if not ok: + raise Reject(why) + + +def load(p): + b = Path(p).read_bytes() + return json.loads(gzip.decompress(b) if b[:2] == b'\x1f\x8b' else b) + + +def parity(a, b): + return bin(a & b).count('1') % 2 + + +def gf2_rank(vs): + rows = [] + for v in vs: + for r in rows: + v = min(v, v ^ r) + if v: + rows.append(v) + return len(rows) + + +def check_moves(rec, bins, moves): + groups = {(g[0], g[1]): list(g[2]) for g in bins['groups']} + req(len(groups) == len(bins['groups']), 'duplicate group') + req(all(set(k) <= {8, 10, 12, 13} and k == sorted(set(k)) and k for k in groups.values()), 'group children') + req(all(0 <= r < T and 0 <= p < 112 for r, p in groups), 'group index range') + req(sum(map(len, groups.values())) == BASE[48], 'idle rank-48 count') + per = defaultdict(list) + for m in moves: + rep, p, c, l, ax = m + req((rep, p) in groups, 'move outside an idle group') + req(c in groups[rep, p] and l in groups[rep, p] and c != l, 'centre/leaf must be idle children of the group') + req(isinstance(ax, list) and len(ax) == 3 and len(set(ax)) == 3, 'exactly three distinct axes') + per[rep, p].append((c, l, [int(v) for v in ax])) + ranks = Counter() + for (rep, p), kids in groups.items(): + rc = rec[p] + axes = {c: [int(v) for v in rc['idle_children'][c]['orthogonal_axes']] for c in kids} + for c in kids: + req(rc['idle_children'][c]['rank'] == 48 and len(axes[c]) == 48, 'rank-48 source child') + ys = {int(s['entry_Y']) for s in rc['stage_alignment']} | {int(s['exit_Y']) for s in rc['stage_alignment']} | {int(rc['terminal_Y_translation'])} + xs = {int(s['entry_X']) for s in rc['stage_alignment']} | {int(s['exit_X']) for s in rc['stage_alignment']} + mv = per.get((rep, p), []) + centres = {c for c, _, _ in mv}; leaves = [l for _, l, _ in mv] + req(len(leaves) == len(set(leaves)), 'leaf reused') + req(not centres & set(leaves), 'centre is also a leaf') + seen = set() + final = {c: list(axes[c]) for c in kids} + for c, l, ax in mv: + trans = {int(rc['idle_children'][c]['translation_after']), int(rc['idle_children'][l]['translation_after'])} + for v in ax: + req((c, v) not in seen, 'axis moved twice') + seen.add((c, v)) + req(v in axes[c], 'foreign axis') + req(all(parity(v, x) == 0 for x in axes[l]), 'axis does not commute with leaf axes') + req(all(parity(v, x) == 0 for x in ys | xs | trans), 'axis does not commute with stage/terminal translations') + final[c].remove(v); final[l].append(v) + for c in kids: + fs = final[c] + req(len(fs) <= 51, 'rank above 51') + req(all(parity(v, v) == 1 for v in fs), 'unit axis') + req(all(parity(a, b) == 0 for i, a in enumerate(fs) for b in fs[i + 1:]), 'final axes orthogonal') + req(gf2_rank(fs) == len(fs), 'independent final axes') + ranks[len(fs)] += 1 + req(sorted(v for c in kids for v in final[c]) == sorted(v for c in kids for v in axes[c]), 'group axis multiset unchanged') + return ranks + + +# -------- independent exact moment: directed rounding at 10^-72 -------- +Q72 = 10 ** 72 + + +def rd(x): + return F(x.numerator * Q72 // x.denominator, Q72) + + +def ru(x): + return F(-((-x.numerator * Q72) // x.denominator), Q72) + + +def log_box(y): + """[lo, hi] for ln(y), y rational >= 1, argument reduction by 2 then atanh series.""" + k = 0 + while y >= 2: + y = y / 2; k += 1 + def atanh2(z, n): + acc, pw = F(0), z + for j in range(n): + acc += pw / (2 * j + 1); pw *= z * z + return 2 * acc, 2 * pw / ((2 * n + 1) * (1 - z * z)) + a, ea = atanh2((y - 1) / (y + 1), 90) + l2, e2 = atanh2(F(1, 3), 130) + return rd(a + k * l2), ru(a + ea + k * (l2 + e2)) + + +def exp_box(x0, x1): + def taylor(x): + s, t = F(1), F(1) + for n in range(1, 34): + t = t * x / n; s += t + return s, t * x / 34 * 3 # Lagrange tail, 0 <= x <= 1 + a, _ = taylor(x0); b, e = taylor(x1) + return rd(a), ru(b + e) + + +def moment_box(profile, b): + W = 896 * T; lo = hi = F(0) + for r, n in sorted(profile.items()): + L0, L1 = log_box(F(73, r)) + e0, e1 = exp_box(b * L0, b * L1) + lo += n * r * e0; hi += n * r * e1 + return lo / (73 * W), hi / (73 * W) + + +def verify_root(profile, root): + lo, hi = F(root[0]), F(root[1]) + req(hi - lo == F(1, 10 ** 25), 'root bracket width 1e-25') + req(moment_box(profile, lo)[1] < 1, 'moment < 1 at lower endpoint') + req(moment_box(profile, hi)[0] > 1, 'moment > 1 at upper endpoint') + return lo + + +def run(rec, bins, moves, result): + ranks = check_moves(rec, bins, moves) + prof = Counter(BASE); del prof[48]; prof.update(ranks) + prof = dict(sorted(prof.items())) + req({str(k): v for k, v in prof.items()} == result['profile'], 'declared profile') + req(sum(r * n for r, n in prof.items()) == 65088 * T, 'complete rank mass 65088*T') + req(73 * 73 > 2 * max(prof) ** 2 and max(prof) == 51, 'halving guard 5329 > 5202') + lo = verify_root(prof, result['root']) + kappa = F(lo.numerator * 10 ** 24 // lo.denominator, 10 ** 24) - F(1, 10 ** 46) - F(1, 10 ** 70) + req(kappa == F(result['kappa']), 'headline kappa') + for name, g in GATES.items(): + req(kappa > g, 'kappa must exceed ' + name) + return prof, kappa + + +def controls(rec, bins, moves, result): + rej = {} + mv = moves['moves'] + rep, p, c, l, ax = mv[0] + rc = rec[p] + bad = [int(v) for v in rc['idle_children'][c]['orthogonal_axes'] if int(v) not in ax + and any(parity(int(v), int(x)) for x in rc['idle_children'][l]['orthogonal_axes'])] + def m(f): + x = copy.deepcopy(mv); f(x); return x + cases = { + 'non_commuting_axis': m(lambda x: x[0][4].__setitem__(0, bad[0])), + 'axis_moved_twice': m(lambda x: x.append([rep, p, c, next(k for k in [8, 10, 12, 13] if k not in (c, l)), list(ax)])), + 'reused_leaf': m(lambda x: x.append(list(x[0]))), + 'foreign_axis': m(lambda x: x[0][4].__setitem__(0, 1 << 80)), + 'centre_is_leaf': m(lambda x: x.append([rep, p, l, c, [int(v) for v in rc['idle_children'][l]['orthogonal_axes']][:3]])), + 'hosted_child': m(lambda x: x.__setitem__(0, [rep, p, c, next(k for k in [8, 10, 12, 13] if k not in dict.fromkeys( + {(g[0], g[1]): g[2] for g in bins['groups']}[rep, p])) if len({(g[0], g[1]): g[2] for g in bins['groups']}[rep, p]) < 4 else 99, ax])), + 'two_axes_only': m(lambda x: x[0].__setitem__(4, ax[:2])), + } + for name, x in cases.items(): + try: + run(rec, bins, x, result) + except Reject as e: + rej[name] = str(e) + else: + raise SystemExit('mutation accepted: ' + name) + r2 = copy.deepcopy(result); r2['profile']['51'] += 1; r2['profile']['48'] -= 1 + try: run(rec, bins, mv, r2) + except Reject as e: rej['wrong_profile'] = str(e) + else: raise SystemExit('mutation accepted: wrong_profile') + r3 = copy.deepcopy(result); lo = F(result['root'][0]) + F(1, 10 ** 25) + r3['root'] = [str(lo), str(lo + F(1, 10 ** 25))] + try: run(rec, bins, mv, r3) + except Reject as e: rej['next_root_grid'] = str(e) + else: raise SystemExit('mutation accepted: next_root_grid') + return rej + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--fill', type=Path, help="optional PR3148 COMPOSED-FILL.json.gz to rebind IDLE-48-BINS") + ap.add_argument('--write', action='store_true', help='rewrite the committed AUDIT.json receipt') + a = ap.parse_args() + if not __debug__: + raise SystemExit('assertions required') + raw = PHASES.read_bytes() + req(hashlib.sha256(raw).hexdigest() == PHASES_SHA, 'DATA-PHASES pin') + rec = {r['port']: r for r in json.loads(raw)['recipes']} + bins = load(PKG / 'IDLE-48-BINS.json.gz'); moves = load(PKG / 'STAR-MOVES.json.gz'); result = load(PKG / 'RESULT.json') + req(bins['T'] == T and bins['fill_payload_sha256'] == FILL_PAYLOAD_SHA, 'bins provenance') + rebound = False + if a.fill: + data = gzip.decompress(a.fill.read_bytes()) + req(hashlib.sha256(data).hexdigest() == FILL_PAYLOAD_SHA, 'PR3148 fill payload') + touched = {(row[2], row[3], row[4]) for row in json.loads(data)['rows']} + derived = [[r, p, [c for c in (8, 10, 12, 13) if (r, c, p) not in touched]] for r in range(T) for p in range(112)] + req([g for g in derived if g[2]] == bins['groups'], 'IDLE-48-BINS equals untouched capacity-48 bins of the fill') + rebound = True + prof, kappa = run(rec, bins, moves['moves'], result) + rej = controls(rec, bins, moves, result) + out = dict(status='PASS_IDLE48_STAR_EXCHANGE_AUDIT', moves=len(moves['moves']), profile={str(k): v for k, v in prof.items()}, + kappa=str(kappa), gain_over_pr3148=str(kappa - GATES['PR3148']), fill_rebound=rebound, + rejected_controls=rej) + if a.write: (PKG / 'AUDIT.json').write_text(json.dumps(out, indent=1, sort_keys=True) + '\n') + else: + strip = lambda d: {k: v for k, v in d.items() if k != 'fill_rebound'} + req(strip(load(PKG / 'AUDIT.json')) == strip(json.loads(json.dumps(out))), 'committed AUDIT.json receipt') + print('PASS_IDLE48_STAR_EXCHANGE_AUDIT moves=%d controls=%d kappa=%s' % (len(moves['moves']), len(rej), float(kappa))) + + +if __name__ == '__main__': + try: + main() + except Reject as e: + raise SystemExit('FAIL: ' + str(e))