diff --git a/research/r437-pooled-moment-ceiling/README.md b/research/r437-pooled-moment-ceiling/README.md new file mode 100644 index 0000000000..e338e6b0b7 --- /dev/null +++ b/research/r437-pooled-moment-ceiling/README.md @@ -0,0 +1,135 @@ +# Moment ceiling of the pooled R437 carrier profile + +**Finite exact certificate for a fixed profile. No new κ, supplier admission +or frontier change.** This contribution is produced by Nick Petalas. + +ToikY's [PR #5810](https://github.com/CrocSwap/integer-mult-bounds/pull/5810) +(`research/r437-unpooled-budget-obstruction`) shows that the unpooled #4067 +host fails the retained moment test at the admitted BIT target `17/5000`. It +leaves other invoices open: "a different invoice, productive normalization, +target allocation ... needs its own bound". Chris R / Clear1nsight's +[PR #4176](https://github.com/CrocSwap/integer-mult-bounds/pull/4176) +(`research/r437-carrier-integration`) fixes the pooled profiles C (original +R437 with the 63 pooled owner moves) and D (the #4067 carrier with the same +moves). Its BILL.md says "No new decimal root is needed". This package computes +that root as a certified ceiling. + +## Result + +Use #5810's moment with every added charge omitted: + + M(c) = Σ_r n_r · r/(64·28416) · (64/r)^c. + +Every rank in C and D is below 64, so each term increases with `c`. A +nonnegative surcharge `S(c)` only raises the left side of `M(c)+S(c) <= 1`. +The certificate proves `M(lo) < 1 < M(hi)` exactly. Therefore **every +`c >= hi` fails for every nonnegative surcharge**, and the fixed contract cannot +pass above the ceiling `hi`. + +| Profile | Source | Certified crossing bracket of M | +|---|---|---| +| U, unpooled #4067 host | #5810 README | (0.0017366903544672, 0.0017366903544673) | +| C, pooled original | #4176 `PROFILE_C` | (0.0017367386530996, 0.0017367386530997) | +| **D, pooled carrier** | #4176 `PROFILE_D` | **(0.0017367829682417, 0.0017367829682418)** | + +- **The carrier keeps its gain under pooling.** The D ceiling exceeds C by + 4.4315142e-8 (exact interval in RESULT.json). The C ceiling exceeds U by + 4.83e-8. +- **The admitted BIT target is out of reach at this normalization.** For D, + `M(17/5000)` lies in an interval around `1.005440413297699` and exceeds 1. +- **The required width is 28571.** With D's paid profile unchanged, `M(17/5000) <= 1` + holds exactly when the productive normalization is at least + `Σ n_r r (64/r)^{17/5000} / 64`. The certificate places that number strictly + between 28570 and 28571. The smallest integer width is **28571**, 155 more + than 28416. C and U give the same integer. + +All three profiles have 903456 paid calls, rank mass 1808352 and +`M(0) = 18837/18944`. That matches #5810's constant `A`. + +**Consistency with reported values.** Two reported values should lie below +these ceilings, since their invoices include surcharges that this package +omits. Both do. #4067's passing grid point 0.001736690352456612377607 lies +2.0e-12 below the U bracket. Rohan Arun's closed #3959 pooled crossing +0.001736738651088946052684 lies 2.0e-12 below the C bracket. Neither +predecessor was replayed. + +## Method + +`verify.py` uses only the standard library and exact `Fraction` intervals. +Every endpoint is rounded outward to the grid `2^-256`. + +- `log 2, log 3, log 5, log 7, log 13` come from `atanh(1/q)` series for + `q = 3, 5, 9, 15, 25`, each with an explicit geometric tail bound. + `log(64/r)` is assembled by factoring `r`. +- `exp(t)` on `0 <= t <= 1/2` uses the Taylor partial sum. The Lagrange tail is + bounded by twice the next term. +- The profiles are read from #4176's `numerical.py` with `ast` and from #5810's + README text. No predecessor code is executed. Both files are pinned by + SHA256 in the verifier and in SOURCES.json. The verifier also checks the + call count, rank mass, the #4176 normalization `W = 28416` and `M = 64`. + +Controls must reject: +- D's bracket applied to C; +- the physical width 28425 in place of the productive width 28416; +- one D rank-42 call moved to rank 1; +- the carrier delta `{1:+288, 2:-576, 3:+288}` reversed on D. + +The log intervals are also checked against floating-point `log` and must be +narrower than `10^-60`. The normal run requires byte equality with the +committed [RESULT.json](RESULT.json); `--emit` prints the recomputation. + +## Reproduce + +From the repository root, CPython 3.12, standard library only: + +```sh +python3.12 -B research/r437-pooled-moment-ceiling/verify.py +python3.12 -O -B research/r437-pooled-moment-ceiling/verify.py +python3.12 -B scripts/research_package.py --package research/r437-pooled-moment-ceiling +``` + +Each direct run prints `PASS_R437_POOLED_MOMENT_CEILING` and takes under one +second. + +## Scope and limits + +- This is a **ceiling for one fixed moment test**. It assumes #5810's contract: + productive normalization `64·28416` and the retained gate `M + S <= 1`. It is + not a runtime lower bound, and it does not price D's complete invoice. It is + not admission of the pooled compiler, physical caller, precision or stock + boundaries, which #4176 and the family status keep open. +- The width threshold is a statement about normalization only. Adding productive + columns would change the word, the caller and the paid profile. No such + construction is proposed. +- The R437 line is not the selected supplier. The selected conditional κ stays + `0.00310045` (#5599). The BIT budget there is admitted at `.0034` from a + different supplier. + +## Open next questions + +1. **What is D's complete pooled crossing?** It matters because the ceiling + omits the 864 added ADDs, the finite invoice term and the pooled-routing + premise that #4176 retains. First step: add #4176's complete D invoice + charges to `M(c)` and bisect with the same interval arithmetic. Blocked by + #4176's retained absolute 77-factor routing premise, which has no + source-bound proof. +2. **Which change of paid profile could close the gap to `17/5000`?** It + matters because one carrier exchange per call moves the ceiling by only + about 4.4e-8, while D still needs `M(17/5000)` lowered by about 0.544%. + First step: compute the exact per-call moment change of each available + local exchange at `c = 17/5000`, then compare the needed total with the + 903456 paid calls. Blocked by: no inventory of further exchange-eligible + calls beyond #4067's 288. + +Structured versions are in [TASK.json](TASK.json). + +## Credit + +ToikY (#5810) supplied the fixed moment contract, the unpooled profile and the +open pooled question. Chris R / Clear1nsight supplied the #4067 carrier, the +#4176 pooled C/D profiles and normalization, and the earlier pooled-allocation +audit. Rohan Arun supplied the #3959 pooled crossing. The retained R437 lineage +credited in those packages is unchanged: ai-nanachi/#3647, Ali Romman/#1043, +Sagar Thakrar/#3700, unpaidmoon/#4147, zxv/#3690 and others. The new work is +the certified pooled ceilings, the carrier gain under pooling and the +width threshold. Apache-2.0. diff --git a/research/r437-pooled-moment-ceiling/RESULT.json b/research/r437-pooled-moment-ceiling/RESULT.json new file mode 100644 index 0000000000..ee5d53b7fc --- /dev/null +++ b/research/r437-pooled-moment-ceiling/RESULT.json @@ -0,0 +1,103 @@ +{ + "ceiling_gain_C_minus_U": [ + "482986323/10000000000000000", + "19319453/400000000000000" + ], + "ceiling_gain_D_minus_C": [ + "22157571/500000000000000", + "221575711/5000000000000000" + ], + "controls_rejected": [ + "D bracket applied to C", + "physical width 28425 instead of productive 28416", + "one D rank-42 call moved to rank 1", + "carrier delta reversed on D", + "log intervals tight and consistent with float log" + ], + "normalization": "64*28416", + "profiles": { + "C": { + "M0": "18837/18944", + "M_at_target_interval_decimal": [ + "1.005440697467206", + "1.005440697467206" + ], + "crossing_bracket": [ + "0.0017367386530996", + "0.0017367386530997" + ], + "extra_productive_columns": 155, + "min_productive_width_at_target": 28571, + "profile": { + "1": 380160, + "14": 1, + "2": 400877, + "3": 22176, + "4": 26592, + "42": 403, + "5": 29376, + "6": 17375, + "7": 26496 + } + }, + "D": { + "M0": "18837/18944", + "M_at_target_interval_decimal": [ + "1.005440413297699", + "1.005440413297699" + ], + "crossing_bracket": [ + "0.0017367829682417", + "0.0017367829682418" + ], + "extra_productive_columns": 155, + "min_productive_width_at_target": 28571, + "profile": { + "1": 380448, + "14": 1, + "2": 400301, + "3": 22464, + "4": 26592, + "42": 403, + "5": 29376, + "6": 17375, + "7": 26496 + } + }, + "U": { + "M0": "18837/18944", + "M_at_target_interval_decimal": [ + "1.005441005045044", + "1.005441005045044" + ], + "crossing_bracket": [ + "0.0017366903544672", + "0.0017366903544673" + ], + "extra_productive_columns": 155, + "min_productive_width_at_target": 28571, + "profile": { + "1": 380448, + "2": 400288, + "26": 32, + "3": 22464, + "4": 26592, + "42": 384, + "5": 29376, + "6": 17376, + "7": 26496 + } + } + }, + "reported_3959_pooled_crossing": { + "below_ceiling_of": "C", + "gap_to_bracket_lo": "502663486829/250000000000000000000000", + "value": "0.001736738651088946052684" + }, + "reported_4067_unpooled_grid_point": { + "below_ceiling_of": "U", + "gap_to_bracket_lo": "2010587622393/1000000000000000000000000", + "value": "0.001736690352456612377607" + }, + "target": "17/5000" +} diff --git a/research/r437-pooled-moment-ceiling/SOURCES.json b/research/r437-pooled-moment-ceiling/SOURCES.json new file mode 100644 index 0000000000..d35e593306 --- /dev/null +++ b/research/r437-pooled-moment-ceiling/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/r437-carrier-integration/numerical.py", + "usage": "input", + "git_blob": "d3411758be96f22f8d64e02ba278dc46b21639c5", + "sha256": "83f2b60a90ab2d0354c5c84f48af246ab416605c3ae4bd62368bbe5f23bb53bb" + }, + { + "path": "research/r437-unpooled-budget-obstruction/README.md", + "usage": "input", + "git_blob": "6b1a2a36a7f0dd69261a25bb32faf131a60126f8", + "sha256": "f41669bda70e75a91471539303011766b7348353e88a3ef9774865d3dd24e512" + } + ] +} diff --git a/research/r437-pooled-moment-ceiling/TASK.json b/research/r437-pooled-moment-ceiling/TASK.json new file mode 100644 index 0000000000..a6010885f2 --- /dev/null +++ b/research/r437-pooled-moment-ceiling/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "r437-carrier-integration", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "r437-carrier-integration", + "question": "Can the paid R437 two-window carrier improvement be admitted by the actual pooled compiler and physical caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/r437-two-window-carrier/README.md", + "research/r437-reverse-row-coefficient/README.md" + ], + "methods": [ + "Close one compiler/request, caller or precision/stock implication for the pinned paid exchange.", + "Falsify that exact interface with an arbitrary-dirty-state or chronology counterexample." + ], + "acceptance_gate": "Pin the complete source and destination contracts, exact paid and scalar deltas, and all remaining assumptions. A local moment gain is not a physical or all-size supplier admission.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Choose one unclaimed obligation: pooled compiler codebook/request alignment, actual physical caller, or precision/stock envelope using the already reported reverse coefficient. Pin the input and receiver, preserve dirty/source windows, and test one binding with a rejection control. Stop at unresolved dependencies; do not rederive the coefficient or quote the local moment as a completed bound.", + "bottleneck_link": "The exchange changes the paid profile; integration must establish that its gain survives the complete caller.", + "allowed_variations": [ + "One compiler rebind, one actual caller boundary, or one precision/stock implication." + ], + "scope_change_triggers": [ + "Ignoring added ADDs, retaining an obsolete reverse coefficient, or declaring global admission from the local histogram." + ], + "overlap_terms": [ + "R437", + "two-window carrier", + "4067", + "4147", + "pooled compiler", + "request alignment", + "reverse row coefficient" + ], + "existing_checks": [ + { + "scope": "PR #4067: source-bound two-window carrier with (2,2) to (1,3) paid exchange and fixed OQ4 host.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Pooled compiler/request rebind, physical caller and precision/stock admission.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4147: reverse row coefficient follow-up.", + "evidence": "research/r437-reverse-row-coefficient/README.md", + "remaining": "Use the exact coefficient in a caller-bound precision/stock proof rather than repeat the arithmetic.", + "status": "author-checked", + "source_commit": "72e7bb797adf82aeb525a399f56ab8adbab8e93c", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Certified ceiling of the retained fixed moment test (PR #5810 contract, productive normalization 64*28416, surcharges omitted) for the pooled R437 C and D profiles fixed by PR #4176, with the unpooled #4067 host as a comparison row and the smallest productive normalization at which D's paid profile could meet the admitted BIT target 17/5000.", + "scope_change_reason": "The card asks for admission of the carrier through the pooled compiler and caller. This package settles one necessary pricing implication of that admission, the pooled moment ceiling that PR #4176 left uncomputed, and does not attempt compiler, caller, precision or stock admission.", + "bottleneck_link": "Side result on a non-selected BIT supplier: it shows that the pooled carrier keeps its moment gain (+4.43e-8 over pooled C) and that no surcharge allocation lets the fixed pooled profile reach the current admitted BIT budget 17/5000 without about 155 more productive columns.", + "budget_minutes": 60, + "stop_rule": "Stop after the first exact interval certificate for the D ceiling and the width threshold; do not search for a changed allocation or price the complete invoice.", + "outcome": "completed", + "evidence": "Exact outward-rounded rational interval certificate: M_D(0.0017367829682417) < 1 < M_D(0.0017367829682418); M_D(17/5000) > 1; 28570 < sum n_r r (64/r)^(17/5000)/64 < 28571. Same certificates for C and U; four rejecting mutation controls; RESULT.json byte equality.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the complete crossing of the pooled D invoice once its 864 added ADDs, finite invoice term and pooled-routing premise are charged?", + "why_it_matters": "The certified ceiling omits every surcharge; only the complete invoice gives D's actual fixed-contract crossing.", + "first_step": "Add PR #4176's complete D invoice charges to M(c) and bisect with the same interval arithmetic.", + "blocked_by": "PR #4176 retains an absolute 77-factor routing/primitive premise without a source-bound proof." + }, + { + "question": "Which change of paid profile could close the gap between the pooled D profile and 17/5000?", + "why_it_matters": "One carrier exchange per call moves the ceiling by about 4.4e-8, while D still needs M(17/5000) lowered by about 0.544%.", + "first_step": "Compute the exact per-call moment change of each available local exchange at c = 17/5000 and compare the needed total with the 903456 paid calls.", + "blocked_by": "No inventory of further exchange-eligible calls beyond #4067's 288." + } + ] +} diff --git a/research/r437-pooled-moment-ceiling/VERIFY.json b/research/r437-pooled-moment-ceiling/VERIFY.json new file mode 100644 index 0000000000..01344719c3 --- /dev/null +++ b/research/r437-pooled-moment-ceiling/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/r437-carrier-integration/numerical.py", + "research/r437-unpooled-budget-obstruction/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned C/D/U profiles and normalization; exact interval brackets for each crossing; M(17/5000)>1; width threshold 28571; reported #4067/#3959 values below ceilings; four rejecting mutation controls; RESULT.json byte equality." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same certificate under -O; the verifier uses explicit Fail checks, not assert." + } + ] +} diff --git a/research/r437-pooled-moment-ceiling/verify.py b/research/r437-pooled-moment-ceiling/verify.py new file mode 100644 index 0000000000..8a871dba62 --- /dev/null +++ b/research/r437-pooled-moment-ceiling/verify.py @@ -0,0 +1,295 @@ +"""Exact moment ceilings for the pooled R437 C/D profiles of PR #4176. + +The fixed moment contract is ToikY's PR #5810 (research/r437-unpooled-budget- +obstruction): M(c) = sum_r n_r * r/(64*28416) * (64/r)**c, with every added +nonnegative charge omitted. The pooled C and D profiles are read, without +executing any predecessor code, from Chris R / Clear1nsight's PR #4176 +research/r437-carrier-integration/numerical.py. The unpooled #4067 profile is +read from the #5810 README as a comparison row. + +All bounds use exact rational interval arithmetic with outward rounding. +Nick Petalas. Apache-2.0. +""" + +from __future__ import annotations + +import argparse +import ast +import hashlib +import json +import math +import re +import sys +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +NUMERICAL = ROOT / "research/r437-carrier-integration/numerical.py" +UNPOOLED_README = ROOT / "research/r437-unpooled-budget-obstruction/README.md" +RESULT = HERE / "RESULT.json" + +PINS = { + NUMERICAL: "83f2b60a90ab2d0354c5c84f48af246ab416605c3ae4bd62368bbe5f23bb53bb", + UNPOOLED_README: "f41669bda70e75a91471539303011766b7348353e88a3ef9774865d3dd24e512", +} + +DIM = 64 +SCALE = 2**256 # outward-rounding grid for every interval endpoint +TARGET = Fraction(17, 5000) # admitted BIT saving of the selected record + +# Claimed crossing brackets (lo, hi): M(lo) < 1 < M(hi). +BRACKETS = { + "U": ("0.0017366903544672", "0.0017366903544673"), + "C": ("0.0017367386530996", "0.0017367386530997"), + "D": ("0.0017367829682417", "0.0017367829682418"), +} +# #4067's reported rational moment-grid point for the unpooled host. +GRID_4067 = "0.001736690352456612377607" +# Rohan Arun's #3959 reported pooled crossing (closed PR), compared to C. +REPORTED_3959 = "0.001736738651088946052684" + + +class Fail(Exception): + pass + + +def need(cond: bool, msg: str) -> None: + if not cond: + raise Fail(msg) + + +# ---------- inputs ---------- + +def sha256(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def literal_assignments(path: Path) -> dict[str, object]: + """Module-level literal assignments, read through ast only.""" + tree = ast.parse(path.read_text(encoding="utf-8")) + out: dict[str, object] = {} + for node in tree.body: + if not isinstance(node, ast.Assign): + continue + for target in node.targets: + if isinstance(target, ast.Name): + try: + out[target.id] = ast.literal_eval(node.value) + except ValueError: + pass + elif isinstance(target, ast.Tuple) and isinstance(node.value, ast.Tuple): + for name, val in zip(target.elts, node.value.elts): + if isinstance(name, ast.Name): + out[name.id] = ast.literal_eval(val) + return out + + +def unpooled_profile(path: Path) -> dict[int, int]: + text = path.read_text(encoding="utf-8") + match = re.search(r"paid profile:\s*```\s*(\{[^`]*\})\s*```", text) + need(match is not None, "unpooled profile block in #5810 README") + body = re.sub(r"\s+", "", match.group(1)) + return {int(k): int(v) for k, v in (kv.split(":") for kv in body[1:-1].split(","))} + + +def load_inputs() -> tuple[dict[str, dict[int, int]], int]: + for path, digest in PINS.items(): + need(sha256(path) == digest, f"pinned bytes: {path.relative_to(ROOT)}") + lits = literal_assignments(NUMERICAL) + need(lits.get("W") == 28416 and lits.get("M") == DIM, "#4176 normalization W=28416, M=64") + need(lits.get("REQUESTS") == 903456, "#4176 request count") + profiles = {"U": unpooled_profile(UNPOOLED_README), "C": lits["PROFILE_C"], "D": lits["PROFILE_D"]} + for name, prof in profiles.items(): + need(sum(prof.values()) == 903456, f"{name}: paid calls 903456") + need(sum(r * n for r, n in prof.items()) == 1808352, f"{name}: rank mass 1808352") + need(all(1 <= r < DIM and n > 0 for r, n in prof.items()), f"{name}: ranks below 64") + return profiles, lits["W"] + + +# ---------- outward-rounded rational intervals ---------- + +def down(x: Fraction) -> Fraction: + return Fraction(math.floor(x * SCALE), SCALE) + + +def up(x: Fraction) -> Fraction: + return Fraction(math.ceil(x * SCALE), SCALE) + + +def atanh_inv(q: int) -> tuple[Fraction, Fraction]: + """Interval for atanh(1/q), q >= 3: alternating-free positive series.""" + y = Fraction(1, q) + total, term, k = Fraction(0), y, 0 + while True: + total += term / (2 * k + 1) + k += 1 + term *= y * y + tail = term / (2 * k + 1) / (1 - y * y) # bounds the remaining sum + if tail < Fraction(1, SCALE): + return down(total), up(total + tail) + + +def log_intervals() -> dict[int, tuple[Fraction, Fraction]]: + """log p for the primes needed by ranks <= 42 (and 26 = 2*13).""" + def add(*parts): + return down(sum(p[0] for p in parts)), up(sum(p[1] for p in parts)) + + def scale(k, iv): + return (k * iv[0], k * iv[1]) if k >= 0 else (k * iv[1], k * iv[0]) + + a3, a5, a9, a15, a25 = (atanh_inv(q) for q in (3, 5, 9, 15, 25)) + log2 = scale(2, a3) # log 2 = 2 atanh(1/3) + log3 = add(log2, scale(2, a5)) # log(3/2) = 2 atanh(1/5) + log5 = add(scale(2, log2), scale(2, a9)) # log(5/4) = 2 atanh(1/9) + log7 = add(scale(3, log2), scale(-2, a15)) # log(8/7) = 2 atanh(1/15) + log13 = add(scale(2, log2), log3, scale(2, a25)) # log(13/12) = 2 atanh(1/25) + return {2: log2, 3: log3, 5: log5, 7: log7, 13: log13} + + +def log_ratio(r: int, logs) -> tuple[Fraction, Fraction]: + """Interval for log(64/r).""" + lo = 6 * logs[2][0] + hi = 6 * logs[2][1] + n = r + for p in (2, 3, 5, 7, 13): + while n % p == 0: + n //= p + lo -= logs[p][1] + hi -= logs[p][0] + need(n == 1, f"rank {r} factors over 2,3,5,7,13") + return down(lo), up(hi) + + +def exp_interval(tl: Fraction, th: Fraction) -> tuple[Fraction, Fraction]: + """exp on [tl, th] with 0 <= tl <= th <= 1/2.""" + need(0 <= tl <= th <= Fraction(1, 2), "exp argument range") + lo = hi = Fraction(0) + tlk = thk = Fraction(1) + k = 0 + while True: + lo += tlk + hi += thk + k += 1 + tlk = tlk * tl / k + thk = thk * th / k + if 2 * thk < Fraction(1, SCALE): + return down(lo), up(hi + 2 * thk) # Lagrange tail < 2 * th^k / k! + + +def moment(profile: dict[int, int], c: Fraction, width: int, logs) -> tuple[Fraction, Fraction]: + """Interval for sum n_r * r/(64*width) * exp(c * log(64/r)).""" + lo = hi = Fraction(0) + for r, n in profile.items(): + ll, lh = log_ratio(r, logs) + el, eh = exp_interval(c * ll, c * lh) + lo += n * r * el + hi += n * r * eh + denom = DIM * width + return down(lo / denom), up(hi / denom) + + +# ---------- certificate ---------- + +def certify(profiles, width, logs) -> dict[str, object]: + out: dict[str, object] = {"normalization": f"64*{width}", "target": "17/5000", "profiles": {}} + brackets = {} + for name in ("U", "C", "D"): + prof = profiles[name] + lo_s, hi_s = BRACKETS[name] + lo, hi = Fraction(lo_s), Fraction(hi_s) + need(0 < lo < hi, f"{name}: ordered bracket") + m_lo = moment(prof, lo, width, logs) + m_hi = moment(prof, hi, width, logs) + need(m_lo[1] < 1, f"{name}: M(lo) < 1") + need(m_hi[0] > 1, f"{name}: M(hi) > 1") + m_t = moment(prof, TARGET, width, logs) + need(m_t[0] > 1, f"{name}: M(17/5000) > 1") + # smallest productive width W' with M(17/5000; W') <= 1 + s_lo, s_hi = m_t[0] * width, m_t[1] * width + need(math.floor(s_hi) == math.floor(s_lo), f"{name}: width threshold resolved") + w_min = math.floor(s_lo) + 1 + m0_exact = Fraction(sum(r * n for r, n in prof.items()), DIM * width) + m0 = moment(prof, Fraction(0), width, logs) + need(m0[0] <= m0_exact <= m0[1] and m0_exact < 1, f"{name}: M(0) < 1") + brackets[name] = (lo, hi) + out["profiles"][name] = { + "profile": {str(r): n for r, n in sorted(prof.items())}, + "M0": str(m0_exact), + "crossing_bracket": [lo_s, hi_s], + "M_at_target_interval_decimal": [f"{float(m_t[0]):.15f}", f"{float(m_t[1]):.15f}"], + "min_productive_width_at_target": w_min, + "extra_productive_columns": w_min - width, + } + gain_dc = (brackets["D"][0] - brackets["C"][1], brackets["D"][1] - brackets["C"][0]) + gain_cu = (brackets["C"][0] - brackets["U"][1], brackets["C"][1] - brackets["U"][0]) + need(gain_dc[0] > 0 and gain_cu[0] > 0, "strict ceiling order U < C < D") + out["ceiling_gain_D_minus_C"] = [str(gain_dc[0]), str(gain_dc[1])] + out["ceiling_gain_C_minus_U"] = [str(gain_cu[0]), str(gain_cu[1])] + # Reported passing values include surcharges, so each must lie below the ceiling. + for key, value, name in (("reported_4067_unpooled_grid_point", GRID_4067, "U"), + ("reported_3959_pooled_crossing", REPORTED_3959, "C")): + point = Fraction(value) + need(point < brackets[name][0], f"{key} below the {name} ceiling") + out[key] = {"value": value, "below_ceiling_of": name, + "gap_to_bracket_lo": str(brackets[name][0] - point)} + return out + + +def controls(profiles, width, logs) -> list[str]: + """Each mutation must make certify() reject.""" + passed = [] + cases = { + "D bracket applied to C": ({**profiles, "D": profiles["C"]}, width), + "physical width 28425 instead of productive 28416": (profiles, 28425), + "one D rank-42 call moved to rank 1": ( + {**profiles, "D": {**profiles["D"], 42: profiles["D"][42] - 1, 1: profiles["D"][1] + 1}}, + width), + "carrier delta reversed on D": ( + {**profiles, "D": {**profiles["D"], 1: profiles["D"][1] - 288, + 2: profiles["D"][2] + 576, 3: profiles["D"][3] - 288}}, + width), + } + for label, (prof, w) in cases.items(): + try: + certify(prof, w, logs) + except Fail: + passed.append(label) + continue + raise Fail(f"control accepted: {label}") + # interval sanity against floating point + for r in (1, 2, 3, 5, 7, 14, 26, 42): + lo, hi = log_ratio(r, logs) + need(lo <= Fraction(math.log(64 / r)) + Fraction(1, 10**12) and + Fraction(math.log(64 / r)) - Fraction(1, 10**12) <= hi and hi - lo < Fraction(1, 10**60), + f"log interval sanity r={r}") + passed.append("log intervals tight and consistent with float log") + return passed + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + parser.add_argument("--emit", action="store_true", help="print the recomputed RESULT.json and exit") + args = parser.parse_args() + try: + profiles, width = load_inputs() + logs = log_intervals() + result = certify(profiles, width, logs) + result["controls_rejected"] = controls(profiles, width, logs) + text = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.emit: + sys.stdout.write(text) + return 0 + need(RESULT.read_text(encoding="utf-8") == text, "RESULT.json matches recomputation") + except Fail as exc: + print(f"FAIL: {exc}") + return 1 + d = result["profiles"]["D"] + print("PASS_R437_POOLED_MOMENT_CEILING " + f"D_bracket={d['crossing_bracket'][0]}..{d['crossing_bracket'][1]} " + f"min_width_at_17/5000={d['min_productive_width_at_target']} no_new_kappa") + return 0 + + +if __name__ == "__main__": + sys.exit(main())