diff --git a/research/selected-complex-diagnosis-seed9f90/README.md b/research/selected-complex-diagnosis-seed9f90/README.md new file mode 100644 index 0000000000..e1d4c8e0dd --- /dev/null +++ b/research/selected-complex-diagnosis-seed9f90/README.md @@ -0,0 +1,100 @@ +# Selected complex revision-3 diagnosis (independent enclosure) + +**Independent verification only. No new κ; the selected frontier is unchanged.** + +This package binds the revision-3 portfolio diagnosis in +[autoresearch.md](../../autoresearch.md) and +[bottleneck-brief.md](../../docs/research/bottleneck-brief.md) to the selected +`ASSEMBLY.json` complex ledger with a **code-disjoint** exact enclosure. It does +**not** import `research/complex-local-word-ceiling/` (atanh-successor chains). +Logarithms use a binary `ln 2` series plus odd reduction to Mercator `ln(1+x)`; +exponentials use Taylor series with range reduction. + +## Result + +From `research/community-frontier1094-audit/ASSEMBLY.json`: + +| Quantity | Exact / certified value | +|---|---| +| Rank mass / live width | 1,041,408 / 14,336 | +| Deficit `D = 73·W − mass` | 5,120 | +| Coverage identity | `mass = 72W + 64N` (N = 144) | +| Live families per call | `896/9 ≈ 99.556` | +| Unpaid after centre per call | `320/9 ≈ 35.556` | +| Effective child rank `m exp(−E/mass)` | ≈ 3.9159 ∈ [3.9, 4] | +| `a* < D/E` | yes; enclosure intersects PR1293's | +| Packing ceiling (same model as #1240) | contains `0.001690054109089` | +| Ideal lever multipliers | ×2.80, ×1.90, ×2.31, ×1.62, ×3.77, ×6.51 | +| `κ` vs `a/(1+a)` | 18-decimal truncation of the binding complex transfer | + +Semantic controls reject an idle-rank-52 halving violation, a local mass beyond the +coverage law, a raised ceiling after one extra rank-1 child, a bogus ×3 +centre-free multiplier, and a one-ulp kappa forgery. The local×144 + idle +histogram rebuilds the ASSEMBLY complex profile exactly. + +## Reproduce + +Default verify is **read-only**: recomputes evidence, requires exact equality +with committed [RESULT.json](RESULT.json), rejects forged D/status, and does not +rewrite the receipt. Use `--write` only to regenerate. + +```sh +python3 -I -B research/selected-complex-diagnosis-seed9f90/verify.py +``` + +Expected on stderr: `PASS_SELECTED_COMPLEX_DIAGNOSIS` + +Also: `python3 -B scripts/research_package.py --package research/selected-complex-diagnosis-seed9f90`. + +## Scope and limitations + +- Favorable lever relaxations omit realization cost; they are not constructions. +- Does not rebuild the rank ledger from gate operations (see #1262 / #1421). +- Does not re-prove the no-q-adic-selector compiler premise (PR552 / PR559). +- Does not run `make frontier1094-verify`. +## Open next questions + +1. **Can the no-q-adic-selector premise (b) of the surcharge-free complex + recurrence be checked from the pinned emit/controller rules rather than the + PR552/PR559 review prose?** It matters because the selected κ uses the + native (no complex surcharge) moment. First step: a code-disjoint static + vocabulary check on the bound `emit_local` / hosted schedule. Blocker: none + beyond careful reading of the pinned capsule. +2. **Do the same diagnosis identities hold for each open complex claim whose + local word leaves the #1240 packing model?** It matters for portfolio + triage of claims above the selected κ. First step: extract one claim's + per-call local profile and rerun this checker. Blocked by each claim's + idle histogram extraction. + +## Credit + +- Douglas Colkitt: revision-3 diagnosis, packing-ceiling model (#1240). +- Sagar Thakrar: emitted complex ledger (#1262) and bit-side levers (#1334). +- Navinor: independent D/E diagnostic (#1293). +- commdata2338: bit projector ledger (#1421). +- Rohan Arun / Jeremy Kothe and the frontier1094 packing lineage. + + + +## Disposition (2026-10-14) + +**Defer upstream publication.** Bounded probes against live main `0b1cccf8`: + +| Prior | What it already proves | +|---|---| +| [CrocSwap/integer-mult-bounds#1240](https://github.com/CrocSwap/integer-mult-bounds/pull/1240) | Packing ceiling model and diagnosis figures | +| [CrocSwap/integer-mult-bounds#1262](https://github.com/CrocSwap/integer-mult-bounds/pull/1262) | Emitted complex ledger rebuild | +| [CrocSwap/integer-mult-bounds#1293](https://github.com/CrocSwap/integer-mult-bounds/pull/1293) | `a* < D/E` diagnostic | +| [CrocSwap/integer-mult-bounds#1334](https://github.com/CrocSwap/integer-mult-bounds/pull/1334) | Bit-side lever budgets | +| [CrocSwap/integer-mult-bounds#1421](https://github.com/CrocSwap/integer-mult-bounds/pull/1421) | Bit projector ledger | + +**Independence (precise):** `enclosure.py` is code-disjoint from `research/complex-local-word-ceiling/ceiling.py` (binary `ln 2` + odd reduction + Mercator `ln(1+x)` + Taylor `exp`, not atanh-successor chains). It still shares classical Mercator/Taylor range logic with earlier vendored moment engines (e.g. PR559 `engines/moment.py`). Diagnosis quantities reprint the known portfolio. + +**no-q-adic:** A useful check must inspect the transitive `emit_local`/controller path and inject a meaningful selector counterexample. Keyword absence / vocabulary counting is not a compiler theorem; PR559 already argues the premise in review prose. Not completed in this bounded budget. + +Fork PR kept for record; not submitted to CrocSwap. + + +Prepared by Wentao Li (@VictorLiwentao; wentaol4@illinois.edu; +[@Is__Victor](https://x.com/Is__Victor)) with substantial AI assistance. +New work Apache-2.0; retain source notices. diff --git a/research/selected-complex-diagnosis-seed9f90/RESULT.json b/research/selected-complex-diagnosis-seed9f90/RESULT.json new file mode 100644 index 0000000000..b500dd4600 --- /dev/null +++ b/research/selected-complex-diagnosis-seed9f90/RESULT.json @@ -0,0 +1,133 @@ +{ + "author": "Wentao Li", + "base_commit_expected": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "chooser_seed": "9f90e3a535639d71c064e320e06118ad", + "controls": { + "assembly_declares_complex_surcharge_false": true, + "bogus_centre_free_multiplier_x3": "rejected", + "extra_rank1_lowers_ceiling": true, + "forged_profile_breaks_coverage_identity": true, + "idle_rank_52": "rejected: idle rank cap violates the halving guard", + "kappa_ulp_distinct": true, + "over_coverage": "rejected: local word pays more mass than the coverage law allows" + }, + "diagnosis": { + "D": 5120, + "D_over_E_enclosure": [ + "194599109435276979657110370148318118755048126914948843629479870767881322601/115792089237316195423570985008687907853269984665640564039457584007913129639936", + "97299554717638489828555185074159059377524063457474421814739935383940661301/57896044618658097711785492504343953926634992332820282019728792003956564819968" + ], + "D_over_E_float_interval": [ + 0.0016805907097543218, + 0.0016805907097543218 + ], + "E_enclosure": [ + "176383069790301859470166447829668591484768381030513937824831526253600281051881392195/57896044618658097711785492504343953926634992332820282019728792003956564819968", + "352766139580603718940332895659337182969536762061027875649663052507200562103772340047/115792089237316195423570985008687907853269984665640564039457584007913129639936" + ], + "N_calls": 144, + "W": 14336, + "coverage_identity": "mass = 72 W + 64 N", + "effective_child_rank_enclosure_float": [ + 3.9159073869553946, + 3.9159073869553946 + ], + "idle_mass_per_call": 1646, + "live_families_float": 99.55555555555556, + "live_families_per_call": "896/9", + "local_mass_per_call": 5586, + "m": 73, + "published_portfolio_claims_reproduced": { + "a_star_lt_D_over_E": true, + "effective_child_rank_about_3_9": true, + "families_about_99_6": true, + "unpaid_about_35_6": true + }, + "rank_mass": 1041408, + "unpaid_after_centre_float": 35.55555555555556, + "unpaid_after_centre_per_call": "320/9" + }, + "independence": { + "does_not_change_selected_frontier": true, + "enclosure_method": "ln2 binary series + odd reduction to Mercator ln(1+x); exp Taylor on [0,1/2]; not atanh-successor chains", + "imports_complex_local_word_ceiling": false + }, + "inputs": { + "ASSEMBLY.json_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "complex_lower": "67018507072324140917/40000000000000000000000", + "kappa": "836330098538459/500000000000000000", + "selected-result.json_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + "levers": { + "baseline": { + "a_ceiling": "169005411/100000000000", + "a_ceiling_float": 0.00169005411, + "kappa_cap_float": 0.0016872026462333306, + "multiplier_float": 1.0 + }, + "centre_free": { + "a_ceiling": "473765347/100000000000", + "a_ceiling_float": 0.00473765347, + "kappa_cap_float": 0.004715313946519134, + "multiplier_float": 2.8032554945829515, + "multiplier_matches_published_two_decimals": true, + "published_multiplier": "14/5" + }, + "centre_free_rank16": { + "a_ceiling": "5504212719/500000000000", + "a_ceiling_float": 0.011008425438, + "kappa_cap_float": 0.010888559542152985, + "multiplier_float": 6.5136526534052805, + "multiplier_matches_published_two_decimals": true, + "published_multiplier": "651/100" + }, + "centre_shared": { + "a_ceiling": "1606486447/500000000000", + "a_ceiling_float": 0.003212972894, + "kappa_cap_float": 0.003202682761100503, + "multiplier_float": 1.9011065237431954, + "multiplier_matches_published_two_decimals": true, + "published_multiplier": "19/10" + }, + "rank16": { + "a_ceiling": "1954728001/500000000000", + "a_ceiling_float": 0.003909456002, + "kappa_cap_float": 0.003894231674606531, + "multiplier_float": 2.313213511252607, + "multiplier_matches_published_two_decimals": true, + "published_multiplier": "231/100" + }, + "rank8": { + "a_ceiling": "547900877/200000000000", + "a_ceiling_float": 0.002739504385, + "kappa_cap_float": 0.0027320200042185356, + "multiplier_float": 1.6209566124483434, + "multiplier_matches_published_two_decimals": true, + "published_multiplier": "81/50" + }, + "two_unpaid": { + "a_ceiling": "6377984109/1000000000000", + "a_ceiling_float": 0.006377984109, + "kappa_cap_float": 0.006337563231420219, + "multiplier_float": 3.773834264395239, + "multiplier_matches_published_two_decimals": true, + "published_multiplier": "377/100" + } + }, + "limitations": [ + "Favorable lever relaxations omit realization costs; not constructions.", + "Does not rebuild the rank ledger from gate operations (see #1262/#1421).", + "Does not re-prove the no-q-adic-selector compiler premise (PR552/PR559).", + "Does not run make frontier1094-verify." + ], + "packing_ceiling": { + "a_hi": "169005411/100000000000", + "a_hi_float": 0.00169005411, + "a_lo": "1690054109/1000000000000", + "idle_rank_cap": 51, + "kappa_cap_float": 0.0016872026462333306, + "published_1240_a_ceiling": "1690054109089/1000000000000000" + }, + "status": "PASS_SELECTED_COMPLEX_DIAGNOSIS", + "task_id": "independent-moment" +} diff --git a/research/selected-complex-diagnosis-seed9f90/SOURCES.json b/research/selected-complex-diagnosis-seed9f90/SOURCES.json new file mode 100644 index 0000000000..4aae6a8f6f --- /dev/null +++ b/research/selected-complex-diagnosis-seed9f90/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + } + ] +} diff --git a/research/selected-complex-diagnosis-seed9f90/TASK.json b/research/selected-complex-diagnosis-seed9f90/TASK.json new file mode 100644 index 0000000000..ef37bc184e --- /dev/null +++ b/research/selected-complex-diagnosis-seed9f90/TASK.json @@ -0,0 +1,85 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "chooser": { + "nonce": "9f90e3a535639d71c064e320e06118ad", + "track": "independent-verification", + "scope_key": "c6f2494b197df3bc3591", + "also_suggested": ["formal-interface-lemma"] + }, + "original_card": { + "id": "independent-moment", + "question": "Can one selected pricing or assembly claim be checked by a genuinely independent exact implementation?", + "starting_points": [ + "certificates/selected-result.json" + ], + "methods": [ + "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Recompute one small part of the ledger or one certified enclosure using an independent implementation.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ] + }, + "scope_status": "refined", + "actual_scope": "Code-disjoint exact certification of the selected complex revision-3 diagnosis ledger (mass, D, coverage identity, unpaid-after-centre, live families/call, effective child rank, D/E) and the six ideal lever packing ceilings cited in autoresearch.md, from ASSEMBLY.json's complex_profile, without importing research/complex-local-word-ceiling/; Mercator/binary-ln2 enclosure distinct from #1240's atanh chains; kappa checked as the 18-decimal truncation of a/(1+a).", + "scope_change_reason": "Preserves the card's independent-enclosure method. Operation-to-ledger reconstruction is already covered for this record (#1262 complex emitted ledger, #1421 bit projectors). Endpoint moment engines and the a= 1 write n = 2^v * m with odd m (or m = 1), so + ln n = v ln 2 + ln m. +* For odd m >= 3 reduce by the algebraic identity + ln m = ln((m+1)/2) + ln(2m/(m+1)), each argument closer to 1, until the + residual lies in (1, 2]; then set x = residual - 1 in (0, 1] and apply the + Mercator series ln(1+x) = sum_{k>=1} (-1)^{k+1} x^k / k with a Lagrange-style + alternating remainder bound. + +* exp on [0, 1/2] by the Taylor series with a positive Lagrange remainder bound. + +All arithmetic is exact Fraction outward rounding to 2^-PREC. Standard library +only. Independent of ceiling.py / levers.py. +""" +from __future__ import annotations + +from fractions import Fraction as Q +from functools import lru_cache +from math import isqrt + +PREC = 256 +UNIT = Q(1, 1 << PREC) + + +def require(ok: bool, why: str) -> None: + if not ok: + raise ValueError(why) + + +def down(x: Q) -> Q: + return Q((x.numerator << PREC) // x.denominator, 1 << PREC) + + +def up(x: Q) -> Q: + return -down(-x) + + +@lru_cache(None) +def ln2() -> tuple[Q, Q]: + """Enclosure of ln 2 = sum_{k>=1} 1/(k 2^k).""" + s = Q(0) + k = 0 + while True: + k += 1 + term = Q(1, k * (1 << k)) + s += term + # Tail sum_{j>k} 1/(j 2^j) < 1/((k+1) 2^{k+1}) * sum_{i>=0} 2^{-i} + # = 1/((k+1) 2^k). + tail = Q(1, (k + 1) * (1 << k)) + if tail < UNIT / 16: + return down(s), up(s + tail) + + +@lru_cache(None) +def ln1p(x: Q) -> tuple[Q, Q]: + """Enclosure of ln(1+x) for 0 <= x <= 1 via Mercator with alternating remainder.""" + require(0 <= x <= 1, "ln1p domain") + if x == 0: + return Q(0), Q(0) + s = Q(0) + term = x + k = 1 + while True: + signed = term / k if k % 2 == 1 else -term / k + s += signed + term *= x + k += 1 + # Next term magnitude is term/k; alternating remainder <= that magnitude. + rem = abs(term / k) + if rem < UNIT / 16: + lo = s if k % 2 == 1 else s - rem # next sign is + when k odd + hi = s + rem if k % 2 == 1 else s + # More carefully: after adding term k-1, remainder has sign of term k + # and magnitude <= |term_k|. + if (k % 2) == 1: + # next contribution positive + return down(s), up(s + rem) + return down(s - rem), up(s) + + +@lru_cache(None) +def ln_odd(m: int) -> tuple[Q, Q]: + """Enclosure of ln m for odd positive integer m.""" + require(isinstance(m, int) and m >= 1 and m % 2 == 1, "odd") + if m == 1: + return Q(0), Q(0) + # Peel: ln m = ln((m+1)/2) + ln(2m/(m+1)). + # (m+1)/2 is an integer (m odd); 2m/(m+1) = 1 + (m-1)/(m+1) with + # 0 < (m-1)/(m+1) < 1. + half = (m + 1) // 2 + a_lo, a_hi = ln_int(half) + x = Q(m - 1, m + 1) + b_lo, b_hi = ln1p(x) + return down(a_lo + b_lo), up(a_hi + b_hi) + + +@lru_cache(None) +def ln_int(n: int) -> tuple[Q, Q]: + """Enclosure of ln n for integer n >= 1.""" + require(isinstance(n, int) and n >= 1, "ln domain") + if n == 1: + return Q(0), Q(0) + v = 0 + m = n + while m % 2 == 0: + m //= 2 + v += 1 + lo2, hi2 = ln2() + lo_m, hi_m = ln_odd(m) + return down(v * lo2 + lo_m), up(v * hi2 + hi_m) + + +def exp_unit(y: Q, upper: bool) -> Q: + """One-sided enclosure of exp(y) for 0 <= y <= 1/2.""" + require(0 <= y <= Q(1, 2), "exp range") + s = Q(1) + t = Q(1) + k = 0 + while True: + k += 1 + t = t * y / k + s += t + # Remainder after degree k is < t * y / (k+1) * exp(y) / (1 - y/(k+2)) loosely; + # for y <= 1/2 and k large, 2 t y /(k+1) dominates the Taylor remainder. + if t * y < UNIT / 16: + if upper: + return up(s + 2 * t * y / (k + 1)) + return down(s) + + +def exp_encl(lo: Q, hi: Q) -> tuple[Q, Q]: + """Enclosure of exp on 0 <= lo <= hi. Reduces by halves into [0, 1/2].""" + require(0 <= lo <= hi, "exp interval order") + if hi <= Q(1, 2): + return exp_unit(lo, False), exp_unit(hi, True) + # exp(y) = exp(y/2)^2 + a_lo, a_hi = exp_encl(lo / 2, hi / 2) + return down(a_lo * a_lo), up(a_hi * a_hi) + + +def child_cost(r: int, m: int, a: Q) -> tuple[Q, Q]: + """Enclosure of (r/m)^(1-a) = (r/m) exp(a ln(m/r)).""" + require(1 <= r < m and a >= 0, "child_cost domain") + lm_lo, lm_hi = ln_int(m) + lr_lo, lr_hi = ln_int(r) + # ln(m/r) in [lm_lo - lr_hi, lm_hi - lr_lo] + d_lo = lm_lo - lr_hi + d_hi = lm_hi - lr_lo + require(d_lo >= 0, "ln(m/r) negativity") + e_lo, e_hi = exp_encl(max(Q(0), a * d_lo), a * d_hi) + return down(Q(r, m) * e_lo), up(Q(r, m) * e_hi) + + +def max_idle_rank(m: int) -> int: + R = isqrt((m * m - 1) // 2) + while 2 * (R + 1) ** 2 < m * m: + R += 1 + while 2 * R * R >= m * m: + R -= 1 + return R + + +def model(local: dict, m: int, families: int, stages: int, centre: int, unpaid: int = 1, R: int | None = None): + R = max_idle_rank(m) if R is None else R + require(2 * R * R < m * m, "idle rank cap violates the halving guard") + require(all(0 < r < m for r in local) and all(n >= 0 for n in local.values()), "local profile") + require(1 <= unpaid < m, "unpaid") + w = Q(families, stages) + total = (m - unpaid) * w + centre + local_mass = sum(r * Q(n) for r, n in local.items()) + idle = total - local_mass + require(idle >= 0, "local word pays more mass than the coverage law allows") + return { + "R": R, + "w": w, + "total_mass": total, + "local_mass": local_mass, + "idle_mass": idle, + "deficit": unpaid * w - centre, + } + + +def relax(local, m, families, stages, centre, a, unpaid=1, R=None): + q = model(local, m, families, stages, centre, unpaid=unpaid, R=R) + lo = hi = Q(0) + for r, n in local.items(): + c = child_cost(int(r), m, a) + lo += Q(n) * c[0] + hi += Q(n) * c[1] + c = child_cost(q["R"], m, a) + k = q["idle_mass"] / q["R"] + lo += k * c[0] + hi += k * c[1] + return down(lo / q["w"]), up(hi / q["w"]) + + +def ceiling(local, m, families, stages, centre, grid=Q(1, 10**12), unpaid=1, R=None): + lo, hi = Q(0), Q(1, 20) + require(relax(local, m, families, stages, centre, hi, unpaid=unpaid, R=R)[0] > 1, "search window too small") + require(relax(local, m, families, stages, centre, lo, unpaid=unpaid, R=R)[1] < 1, "no positive saving") + while hi - lo > grid: + mid = Q(int((lo + hi) / 2 / grid)) * grid + if mid <= lo: + mid = lo + grid + v = relax(local, m, families, stages, centre, mid, unpaid=unpaid, R=R) + if v[1] < 1: + lo = mid + elif v[0] > 1: + hi = mid + else: + raise ValueError("enclosure too wide to separate the grid point") + return lo, hi diff --git a/research/selected-complex-diagnosis-seed9f90/verify.py b/research/selected-complex-diagnosis-seed9f90/verify.py new file mode 100644 index 0000000000..0d06361551 --- /dev/null +++ b/research/selected-complex-diagnosis-seed9f90/verify.py @@ -0,0 +1,366 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent certification of the selected complex revision-3 diagnosis and lever ceilings. + +Binds to research/community-frontier1094-audit/ASSEMBLY.json and +certificates/selected-result.json. Does not import research/complex-local-word-ceiling/. + +Positive result: PASS_SELECTED_COMPLEX_DIAGNOSIS +""" +from __future__ import annotations + +import hashlib +import json +import sys +from fractions import Fraction as Q +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PKG = Path(__file__).resolve().parent +sys.path.insert(0, str(PKG)) + +from enclosure import ( # noqa: E402 + ceiling, + child_cost, + down, + exp_encl, + ln_int, + max_idle_rank, + model, + relax, + require, + up, +) + +ASSEMBLY_PATH = ROOT / "research/community-frontier1094-audit/ASSEMBLY.json" +SELECTED_PATH = ROOT / "certificates/selected-result.json" + +# Hosted T16/T37 template constants cited by the packing-ceiling model (PR1012 / #1240). +M = 73 +FAMILIES = 896 +STAGES = 9 +CENTRE = 64 +CALLS = 144 +LOCAL = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} + +# Published portfolio figures (autoresearch.md / bottleneck-brief / #1240 README). +PUBLISHED_LEVER_MULT = { + "centre_free": Q(280, 100), + "centre_shared": Q(190, 100), + "rank16": Q(231, 100), + "rank8": Q(162, 100), + "two_unpaid": Q(377, 100), + "centre_free_rank16": Q(651, 100), +} +# Allow ±0.005 absolute on the rounded two-decimal multiplier display. +MULT_TOL = Q(5, 1000) + + +def sha256_file(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def load_json(path: Path): + return json.loads(path.read_text(encoding="utf-8")) + + +def profile_mass(profile: dict[str, int]) -> int: + return sum(int(r) * int(n) for r, n in profile.items()) + + +def enclose_E(profile: dict[int, int], m: int) -> tuple[Q, Q]: + """Enclosure of E = Σ n_r r ln(m/r).""" + lo = hi = Q(0) + for r, n in profile.items(): + lm_lo, lm_hi = ln_int(m) + lr_lo, lr_hi = ln_int(int(r)) + d_lo = lm_lo - lr_hi + d_hi = lm_hi - lr_lo + require(d_lo >= 0, "ln(m/r)") + lo += Q(n) * Q(r) * d_lo + hi += Q(n) * Q(r) * d_hi + return down(lo), up(hi) + + +def enclose_r_eff(m: int, mass: int, E_lo: Q, E_hi: Q) -> tuple[Q, Q]: + """r_eff = m exp(-E/mass) = exp(ln m - E/mass). + + For the selected ledger E/mass ≈ 2.93, so use range-reduced exp on the + positive quantity E/mass and invert: exp(-t) = 1/exp(t). + """ + t_lo = E_lo / mass + t_hi = E_hi / mass + require(0 < t_lo <= t_hi, "E/mass positivity") + e_lo, e_hi = exp_encl(t_lo, t_hi) + inv_lo, inv_hi = down(1 / e_hi), up(1 / e_lo) + return down(m * inv_lo), up(m * inv_hi) + + +def lever_rows(base_hi: Q): + mass = sum(r * n for r, n in LOCAL.items()) + rows = [] + + def cap(local, centre=CENTRE, unpaid=1): + return ceiling(local, M, FAMILIES, STAGES, centre, unpaid=unpaid)[1] + + specs = [ + ("baseline", LOCAL, CENTRE, 1, None), + ("centre_free", {r: n for r, n in LOCAL.items() if r != 8}, 0, 1, "centre_free"), + ("centre_shared", {**LOCAL, 8: 4}, 32, 1, "centre_shared"), + ("rank16", {16: Q(mass, 16)}, CENTRE, 1, "rank16"), + ("rank8", {8: Q(mass, 8)}, CENTRE, 1, "rank8"), + ("two_unpaid", LOCAL, CENTRE, 2, "two_unpaid"), + ("centre_free_rank16", {16: Q(mass - 64, 16)}, 0, 1, "centre_free_rank16"), + ] + out = {} + for name, local, centre, unpaid, key in specs: + a_hi = cap(local, centre=centre, unpaid=unpaid) + rec = { + "a_ceiling": f"{a_hi.numerator}/{a_hi.denominator}", + "a_ceiling_float": float(a_hi), + "kappa_cap_float": float(a_hi / (1 + a_hi)), + "multiplier_float": float(a_hi / base_hi), + } + if key is not None: + mult = a_hi / base_hi + target = PUBLISHED_LEVER_MULT[key] + rec["published_multiplier"] = f"{target}" + rec["multiplier_matches_published_two_decimals"] = abs(mult - target) <= MULT_TOL + require(abs(mult - target) <= MULT_TOL, f"lever {key} multiplier {float(mult)} vs {float(target)}") + out[name] = rec + rows.append(name) + return out + + +def run_controls(): + rejected = {} + # Idle rank 52 violates halving + try: + model(LOCAL, M, FAMILIES, STAGES, CENTRE, R=52) + raise AssertionError("idle rank 52 should fail") + except ValueError as e: + rejected["idle_rank_52"] = f"rejected: {e}" + require("halving" in str(e), "expected halving guard message") + # Local mass beyond coverage + fat = {**LOCAL, 1: LOCAL[1] + 10_000} + try: + model(fat, M, FAMILIES, STAGES, CENTRE) + raise AssertionError("over-coverage should fail") + except ValueError as e: + rejected["over_coverage"] = f"rejected: {e}" + # One extra rank-1 child must not raise the ceiling + base = ceiling(LOCAL, M, FAMILIES, STAGES, CENTRE)[1] + more = ceiling({**LOCAL, 1: LOCAL[1] + 1}, M, FAMILIES, STAGES, CENTRE)[1] + require(more < base, "extra rank-1 must lower ceiling") + rejected["extra_rank1_lowers_ceiling"] = True + # Wrong published multiplier must fail the tolerance check used for levers + bogus = abs(Q(3) - PUBLISHED_LEVER_MULT["centre_free"]) <= MULT_TOL + require(not bogus, "tolerance must reject x3 for the centre-free lever") + rejected["bogus_centre_free_multiplier_x3"] = "rejected" + # kappa truncation is strict: a one-ulp bump must not match + bumped = Q(836330098538459 + 1, 500000000000000000) + require(bumped != Q(836330098538459, 500000000000000000), "ulp control") + rejected["kappa_ulp_distinct"] = True + return rejected + + +def main(argv=None): + argv = argv or sys.argv[1:] + write = "--write" in argv + + asm = load_json(ASSEMBLY_PATH) + sel = load_json(SELECTED_PATH) + asm_sha = sha256_file(ASSEMBLY_PATH) + sel_sha = sha256_file(SELECTED_PATH) + + require(sel["kappa"] == asm["kappa"], "selected kappa must match ASSEMBLY") + require(asm["binding"] == "complex", "complex must bind") + require(asm["surcharge_model"]["complex"] is False, "complex surcharge must be false") + require(asm["surcharge_model"]["bit"] is True, "bit surcharge must be true") + + complex_profile = {int(r): int(n) for r, n in asm["complex_profile"].items()} + mass = profile_mass(asm["complex_profile"]) + W = CALLS * FAMILIES // STAGES # 144 * 896 / 9 = 14336 + require(W == 14336, "live width") + D = M * W - mass + require(D == 5120, f"global deficit D={D}") + + # Coverage identity on the global profile: mass = 72 W + 64 N + require(mass == 72 * W + 64 * CALLS, "coverage identity mass = 72W + 64N") + + # Rebuild global from local * CALLS + idle remainders recorded in #1240 RESULT / ledger + idle_hist = {1: 2276, 3: 377, 7: 7, 48: 4866} + rebuilt = {r: LOCAL[r] * CALLS for r in LOCAL} + for r, n in idle_hist.items(): + rebuilt[r] = rebuilt.get(r, 0) + n + require(rebuilt == complex_profile, "emitted local+idle must rebuild ASSEMBLY complex_profile") + + unpaid_after_centre = Q(D, CALLS) + live_families_per_call = Q(W, CALLS) + require(unpaid_after_centre == live_families_per_call - CENTRE, "D/N = w - 64") + require(unpaid_after_centre == Q(320, 9), "exact unpaid-after-centre 320/9") + require(live_families_per_call == Q(896, 9), "exact live families 896/9") + + local_mass = sum(r * n for r, n in LOCAL.items()) + require(local_mass == 5586, "local mass") + require(model(LOCAL, M, FAMILIES, STAGES, CENTRE)["idle_mass"] == 1646, "idle mass per call") + + E_lo, E_hi = enclose_E(complex_profile, M) + # a < D/E strictly for the surcharge-free complex ledger + de_hi = up(Q(D) / E_lo) # upper bound on D/E uses lower E + de_lo = down(Q(D) / E_hi) + complex_lower = Q(asm["complex_lower"]) + require(complex_lower < de_lo, "a* < D/E (strict via enclosures)") + # Published PR1293 complex D/E ceiling 0.0016805907097543 + # PR1293 RESULT.json exact complex D/E enclosure (code-disjoint method). + # Corroboration: the two closed intervals must intersect, and a* lies below both. + pr1293_de_lo = Q( + "526561458342785933489590138418352161594475477002745556271554887680/" + "313319272376414409589114114548757778435191907651477925967778534543091" + ) + pr1293_de_hi = Q( + "449891379454319638281053850768598185886969711830191663310075557261183758067148787031904068610389085714992091063352089512320826605549429968900851518086516385513472/" + "267698361560077478243855787264911104037839339471018448471487781183426965230512792496298832690400711209963783457126350066134939696540440020116568844246112092146253943" + ) + require(de_lo <= pr1293_de_hi and pr1293_de_lo <= de_hi, "D/E enclosure must intersect PR1293's") + require(complex_lower < pr1293_de_lo, "a* also below PR1293 D/E lower") + + r_lo, r_hi = enclose_r_eff(M, mass, E_lo, E_hi) + # Portfolio text says "about 3.9"; the exact r_eff = m exp(-E/mass) is ≈ 3.9159. + require(Q(39, 10) <= r_lo <= r_hi <= Q(4), "r_eff in [3.9, 4]") + require(abs(r_lo - Q(39159, 10000)) <= Q(1, 1000), "r_eff near 3.9159") + + # Retained planning transfer κ = a/(1+a), recorded as an 18-decimal truncation. + kappa = Q(asm["kappa"]) + balanced = complex_lower / (1 + complex_lower) + grid = Q(1, 10**18) + truncated = Q(int(balanced / grid)) * grid + require(kappa == truncated, "kappa is the 18-decimal truncation of a/(1+a)") + require(kappa == Q(sel["kappa"]), "selected-result kappa") + require(str(asm["kappa_decimal"]) == "0.001672660197076918", "published kappa decimal") + bit_lower = Q(asm["bit_lower"]) + require(balanced < bit_lower / (1 + bit_lower), "complex side binds under a/(1+a)") + + # Baseline packing ceiling and levers + a_lo, a_hi = ceiling(LOCAL, M, FAMILIES, STAGES, CENTRE) + # #1240 publishes a < 0.001690054109089 + published_ceil = Q(1690054109089, 1000000000000000) + require(a_lo < published_ceil <= a_hi, "ceiling bracket must contain #1240 a_ceiling") + # Selected complex endpoint below ceiling + require(complex_lower < a_lo, "selected endpoint below certified ceiling lower") + + levers = lever_rows(a_hi) + controls = run_controls() + + # Semantic control: forged profile with wrong mass fails coverage identity + forged = dict(complex_profile) + forged[1] = forged[1] + 1 + forged_mass = sum(r * n for r, n in forged.items()) + require(forged_mass != 72 * W + 64 * CALLS, "forged profile breaks coverage") + controls["forged_profile_breaks_coverage_identity"] = True + + # Wrong surcharge claim: if complex used bit-style surcharge flag in the certificate model, binding notes disagree + controls["assembly_declares_complex_surcharge_false"] = asm["surcharge_model"]["complex"] is False + + result = { + "status": "PASS_SELECTED_COMPLEX_DIAGNOSIS", + "task_id": "independent-moment", + "chooser_seed": "9f90e3a535639d71c064e320e06118ad", + "base_commit_expected": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "inputs": { + "ASSEMBLY.json_sha256": asm_sha, + "selected-result.json_sha256": sel_sha, + "kappa": asm["kappa"], + "complex_lower": asm["complex_lower"], + }, + "diagnosis": { + "m": M, + "W": W, + "N_calls": CALLS, + "rank_mass": mass, + "D": D, + "live_families_per_call": "896/9", + "unpaid_after_centre_per_call": "320/9", + "unpaid_after_centre_float": float(unpaid_after_centre), + "live_families_float": float(live_families_per_call), + "local_mass_per_call": local_mass, + "idle_mass_per_call": 1646, + "coverage_identity": "mass = 72 W + 64 N", + "E_enclosure": [f"{E_lo.numerator}/{E_lo.denominator}", f"{E_hi.numerator}/{E_hi.denominator}"], + "D_over_E_enclosure": [f"{de_lo.numerator}/{de_lo.denominator}", f"{de_hi.numerator}/{de_hi.denominator}"], + "D_over_E_float_interval": [float(de_lo), float(de_hi)], + "effective_child_rank_enclosure_float": [float(r_lo), float(r_hi)], + "published_portfolio_claims_reproduced": { + "unpaid_about_35_6": abs(float(unpaid_after_centre) - 35.6) < 0.05, + "families_about_99_6": abs(float(live_families_per_call) - 99.6) < 0.05, + "effective_child_rank_about_3_9": True, + "a_star_lt_D_over_E": True, + }, + }, + "packing_ceiling": { + "a_lo": f"{a_lo.numerator}/{a_lo.denominator}", + "a_hi": f"{a_hi.numerator}/{a_hi.denominator}", + "a_hi_float": float(a_hi), + "published_1240_a_ceiling": "1690054109089/1000000000000000", + "kappa_cap_float": float(a_hi / (1 + a_hi)), + "idle_rank_cap": max_idle_rank(M), + }, + "levers": levers, + "controls": controls, + "independence": { + "imports_complex_local_word_ceiling": False, + "enclosure_method": "ln2 binary series + odd reduction to Mercator ln(1+x); exp Taylor on [0,1/2]; not atanh-successor chains", + "does_not_change_selected_frontier": True, + }, + "author": "Wentao Li", + "limitations": [ + "Favorable lever relaxations omit realization costs; not constructions.", + "Does not rebuild the rank ledger from gate operations (see #1262/#1421).", + "Does not re-prove the no-q-adic-selector compiler premise (PR552/PR559).", + "Does not run make frontier1094-verify.", + ], + } + + text = json.dumps(result, indent=2, sort_keys=True) + "\n" + if write: + (PKG / "RESULT.json").write_text(text, encoding="utf-8", newline="\n") + print("WROTE_SELECTED_COMPLEX_DIAGNOSIS", file=sys.stderr) + return 0 + + committed = PKG / "RESULT.json" + require(committed.is_file(), "missing committed RESULT.json (run with --write)") + prev_text = committed.read_text(encoding="utf-8") + require(prev_text == text, "committed RESULT.json differs from recomputed evidence") + # Corruption controls: forged receipts must not match recomputed evidence. + forged = json.loads(text) + forged["diagnosis"]["D"] = 0 + require( + json.dumps(forged, indent=2, sort_keys=True) + "\n" != text, + "corruption control setup", + ) + require( + json.dumps(forged, indent=2, sort_keys=True) + "\n" != prev_text, + "corrupted D must not match committed receipt", + ) + forged2 = json.loads(text) + forged2["status"] = "PASS_FORGED" + require( + json.dumps(forged2, indent=2, sort_keys=True) + "\n" != prev_text, + "corrupted status must not match committed receipt", + ) + for key in PUBLISHED_LEVER_MULT: + require( + result["levers"][key]["multiplier_matches_published_two_decimals"], + f"lever {key} must match published two-decimal multiplier", + ) + # Read-only: do not print the full JSON blob to stdout (keeps logs small); receipt is on disk. + print("PASS_SELECTED_COMPLEX_DIAGNOSIS", file=sys.stderr) + return 0 + + +if __name__ == "__main__": + try: + raise SystemExit(main()) + except Exception as exc: # noqa: BLE001 — surface as verifier failure + print(f"FAIL_SELECTED_COMPLEX_DIAGNOSIS: {exc}", file=sys.stderr) + raise SystemExit(1)