diff --git a/.github/workflows/five-stage-493-fixed-prime.yml b/.github/workflows/five-stage-493-fixed-prime.yml new file mode 100644 index 0000000000..e7e8169ced --- /dev/null +++ b/.github/workflows/five-stage-493-fixed-prime.yml @@ -0,0 +1,69 @@ +name: Fixed prime, seven levels and eta 1e-24 on the 493-source five-stage banks +on: + pull_request: + paths: + - 'research/five-stage-493-fixed-prime/**' + - 'research/five-stage-banks-493/**' + - '.github/workflows/five-stage-493-fixed-prime.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + full: + runs-on: ubuntu-24.04 + timeout-minutes: 90 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + repository: CrocSwap/integer-mult-bounds + ref: af3fe331ca60c936229e060681ffccbc1c208678 + path: .dependencies/pr234 + persist-credentials: false + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + repository: eumemic/integer-mult-bounds + ref: 13311491eb74a3a9a443ba4e318c68c263f064f0 + path: .dependencies/pr210 + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.13' + - run: python -m pip install sympy==1.14.0 + - run: python -B research/five-stage-493-fixed-prime/verify.py --pr210-root .dependencies/pr210 --pr234-root .dependencies/pr234 --full + - run: git diff --exit-code + prime-kernel: + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.12' + - name: Install the fixed Lean release in runner temporary storage + run: | + python -m pip install zstandard==0.25.0 + curl -fsSL https://github.com/leanprover/lean4/releases/download/v4.24.0/lean-4.24.0-linux.tar.zst -o "$RUNNER_TEMP/lean.tar.zst" + python - <<'PY' + import hashlib,os,tarfile,zstandard + from pathlib import Path + root=Path(os.environ['RUNNER_TEMP']) + expected='b14f5e5159219dd1a1956c3b806813319f5e94ccd5bdfd56f54520609a5bb5ec' + assert hashlib.sha256((root/'lean.tar.zst').read_bytes()).hexdigest()==expected + with (root/'lean.tar.zst').open('rb') as f: + with zstandard.ZstdDecompressor().stream_reader(f) as reader: + with tarfile.open(fileobj=reader,mode='r|') as archive: + archive.extractall(root,filter='data') + PY + echo "$RUNNER_TEMP/lean-4.24.0-linux/bin" >> "$GITHUB_PATH" + - name: Kernel-check the prime in a separate project copy + env: + MATHLIB_CACHE_DIR: ${{ runner.temp }}/mathlib-cache + run: | + cp -R research/five-stage-493-fixed-prime "$RUNNER_TEMP/prime-proof" + cd "$RUNNER_TEMP/prime-proof" + lake update + lake exe cache get Mathlib.NumberTheory.LucasLehmer + lake env lean Prime.lean diff --git a/.github/workflows/five-stage-banks-493.yml b/.github/workflows/five-stage-banks-493.yml new file mode 100644 index 0000000000..fba88e4780 --- /dev/null +++ b/.github/workflows/five-stage-banks-493.yml @@ -0,0 +1,35 @@ +name: Verify five-stage banks with the 493-source helper +on: + pull_request: + paths: + - 'research/five-stage-banks-493/**' + - '.github/workflows/five-stage-banks-493.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + full: + runs-on: ubuntu-24.04 + timeout-minutes: 90 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + repository: CrocSwap/integer-mult-bounds + ref: af3fe331ca60c936229e060681ffccbc1c208678 + path: .dependencies/pr234 + persist-credentials: false + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + repository: eumemic/integer-mult-bounds + ref: 13311491eb74a3a9a443ba4e318c68c263f064f0 + path: .dependencies/pr210 + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.13' + - run: python -m pip install sympy==1.14.0 + - run: python -B research/five-stage-banks-493/verify.py --pr210-root .dependencies/pr210 --pr234-root .dependencies/pr234 --full + - run: git diff --exit-code diff --git a/.github/workflows/five-stage-banks.yml b/.github/workflows/five-stage-banks.yml new file mode 100644 index 0000000000..9080083b1a --- /dev/null +++ b/.github/workflows/five-stage-banks.yml @@ -0,0 +1,29 @@ +name: Verify five-stage banks +on: + pull_request: + paths: + - 'research/five-stage-banks/**' + - '.github/workflows/five-stage-banks.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + full: + runs-on: ubuntu-24.04 + timeout-minutes: 60 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + repository: CrocSwap/integer-mult-bounds + ref: af3fe331ca60c936229e060681ffccbc1c208678 + path: .dependencies/pr234 + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.13' + - run: python -m pip install sympy==1.14.0 + - run: python -B research/five-stage-banks/verify.py --pr234-root .dependencies/pr234 --full + - run: git diff --exit-code diff --git a/research/five-stage-493-fixed-prime/NOTICE.md b/research/five-stage-493-fixed-prime/NOTICE.md new file mode 100644 index 0000000000..315152ac01 --- /dev/null +++ b/research/five-stage-493-fixed-prime/NOTICE.md @@ -0,0 +1,14 @@ +# Notice + +Fixed prime, seven finite levels and eta = 10^-24 on PR240's banked five-stage bit supplier. Apache-2.0. +Prepared by Rohan Arun (rohanarun) with Anthropic Claude assistance. + +Reused, with credit: +- Gabriele Nespoli, PR235 (OpenAI Codex assistance): the fixed-prime rare-density argument, the seven-level + finite bootstrap, the paid q-power overcharge, `Prime.lean`, `lakefile.toml`, `lean-toolchain` and + `base_two_moment.py` (copied unchanged), applied there to PR237. +- Rohan Arun, PR237/PR240: completed width-120 banks and the 493-source five-stage word (unchanged here). +- hcg890 and Jacob Sussman, PR234: five-stage cover, moment engine, outer-47 assembly and finite bill. +- eumemic, PR210 (with Dugongue, PR216, and sennemmi, PR230): the 493-source helper. +- Evan McKinney (PR197), Chafik Boukhalfa (PR200), Avi Eisenberg (PR193), and every contributor credited by + those packages. Original notices remain in the pinned sources. diff --git a/research/five-stage-493-fixed-prime/Prime.lean b/research/five-stage-493-fixed-prime/Prime.lean new file mode 100644 index 0000000000..4c323ab609 --- /dev/null +++ b/research/five-stage-493-fixed-prime/Prime.lean @@ -0,0 +1,22 @@ +/- Copyright 2026 Gabriele Nespoli. Apache-2.0. Developed with OpenAI Codex. + Lucas-Lehmer criterion and norm_num extension: mathlib contributors. + This verifies prime eligibility only, not the integer multiplication theorem. -/ +import Mathlib.NumberTheory.LucasLehmer + +theorem fixed_prime_prime : (mersenne 127).Prime := + lucas_lehmer_sufficiency _ (by simp) (by norm_num) + +theorem fixed_prime_value : mersenne 127 = 170141183460469231731687303715884105727 := by + norm_num [mersenne] + +theorem fixed_prime_large : 2 ^ 80 < mersenne 127 := by + norm_num [mersenne] + +theorem fixed_prime_density : + (0 : ℚ) < 3456000 / 170141183460469231731687303715884105727 ∧ + (3456000 / 170141183460469231731687303715884105727 : ℚ) < 1 / 10 ^ 16 := by + norm_num + +#print axioms fixed_prime_prime +#print axioms fixed_prime_large +#print axioms fixed_prime_density diff --git a/research/five-stage-493-fixed-prime/README.md b/research/five-stage-493-fixed-prime/README.md new file mode 100644 index 0000000000..b6caba8442 --- /dev/null +++ b/research/five-stage-493-fixed-prime/README.md @@ -0,0 +1,38 @@ +# Fixed prime and seven finite levels on PR240's five-stage banks + +Conditional κ = **709424410568125629699 / 10^24 = 7.09424410568125629699 × 10^-4**. + +That is +3.91 × 10^-12 over PR240 (`28376976266399/(4·10^16)` = 7.09424406659975 × 10^-4). PR240's banked five-stage word, its 493-source helper and all of its checks are unchanged. Only three fixed arithmetic parameters change: + +| Parameter | PR240 | This | +|---|---|---| +| Rare-class density in the paid moment | envelope 10^-16 | proved 2m^3/q with the fixed prime q = 2^127 − 1, full 32m^2 fallback still paid | +| Finite ordinary levels | 3 | 7 | +| Outer-47 backoff η (β = 10^-9 unchanged) | 10^-12 | 10^-24 | + +The first two are PR235's refinement of PR237 (Gabriele Nespoli), applied here to PR240. The third is new: all 47 strict inequalities and 7 margins of PR234's unchanged assembly still hold at η = 10^-24; it adds about 2.1 × 10^-15 on its own. + +## Reproduce + +```sh +git worktree add --detach ../pr210 13311491eb74a3a9a443ba4e318c68c263f064f0 +git worktree add --detach ../pr234 af3fe331ca60c936229e060681ffccbc1c208678 +python3 -m pip install sympy==1.14.0 +python3 -B research/five-stage-493-fixed-prime/verify.py --pr210-root ../pr210 --pr234-root ../pr234 [--full] +``` + +The verifier first runs PR240's own verifier from the same checkout (all F2 and integer columns, telescope, five-stage lowering, geometry, primes, finite bill, 231 charts, 176,915 banks and the 60-colouring) and requires PR240's certificate to be reproduced. Then it: + +- bisects the coarse saving `177482012714287685545103/(2.5·10^26)` on the 10^-27 grid with PR234's engine, checks both sides with an independent atanh engine, and checks that the old 10^-16 density fails at this point; +- runs seven acyclic levels from the retained completed saving 384599/10^10, with PR234's cutoff checks; +- runs the outer-47 assembly on the 10^-24 κ grid and rejects the next grid point; +- reproduces PR240's published κ with η = 10^-12 and three levels; +- recomputes the fully paid q-power constant with PR240's fresh finite-bill values (coefficient 62,150,081,742,953,667,360 < 2^80 < q). + +About 5 minutes; `--full` also runs PR234's fresh verifier (about 10). `certificate.json` holds the key values and the SHA-256 of the complete recomputed record; `--dump PATH` writes the full record. `Prime.lean` kernel-checks q with mathlib's Lucas–Lehmer theorem (CI job `prime-kernel`). + +## Scope + +This is a conditional finite certificate with exactly PR234/PR240's hypotheses. The large fixed prime makes initialization and table constants enormous but finite and paid, as argued in PR235's PROOF.md. No construction changes. + +Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. diff --git a/research/five-stage-493-fixed-prime/base_two_moment.py b/research/five-stage-493-fixed-prime/base_two_moment.py new file mode 100644 index 0000000000..14a90fa0e7 --- /dev/null +++ b/research/five-stage-493-fixed-prime/base_two_moment.py @@ -0,0 +1,63 @@ +#!/usr/bin/env python3 +"""Maintainer arithmetic cross-check of the pinned PR39 certificate. + +Uses no producer/checker imports. Counts are inputs, not proved by this script. +80-term rational logarithms and 12-term exponentials independently enclose +the two moments. The accompanying written review addresses their realization. +""" +import argparse +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +GRID = 10**30 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def log_unit(x): + require(1 <= x <= 2, "logarithm range") + z = (x-1)/(x+1) + lo = 2*sum((z**(2*j+1)/(2*j+1) for j in range(80)), Q(0)) + return lo, lo+2*z**161/(161*(1-z*z)) + + +def log_bounds(x): + k = 0 + while x > 2: + x /= 2 + k += 1 + lo, hi = log_unit(x) + l2, u2 = log_unit(Q(2)) + lo, hi = lo+k*l2, hi+k*u2 + # Outward rational rounding keeps later certificates compact. + return Q((lo*GRID).__floor__(), GRID), Q((hi*GRID).__ceil__(), GRID) + + +def exp_bounds(x): + require(0 <= x < 1, "exponential range") + term = total = Q(1) + for j in range(1, 13): + term *= x/j + total += term + tail = term*x/13/(1-x/14) + return total, total+tail + + +def moment(m, W, entries, saving): + lo = hi = Q(0) + for t, count in entries: + t, count = int(t), int(count) + require(0 < t < m and count > 0, "improper child") + l, u = log_bounds(Q(m, t)) + lower = exp_bounds(saving*l)[0] + upper = exp_bounds(saving*u)[1] + lo += Q(t*count, m*W)*lower + hi += Q(t*count, m*W)*upper + return Q((lo*GRID).__floor__(), GRID), Q((hi*GRID).__ceil__(), GRID) + diff --git a/research/five-stage-493-fixed-prime/certificate.json b/research/five-stage-493-fixed-prime/certificate.json new file mode 100644 index 0000000000..fe54189d87 --- /dev/null +++ b/research/five-stage-493-fixed-prime/certificate.json @@ -0,0 +1,52 @@ +{ + "beta": "1/1000000000", + "coarse": "177482012714287685545103/250000000000000000000000000", + "coarse_grid": 1000000000000000000000000000, + "complex_saving": "29898197786071/40000000000000000", + "controls": [ + "cyclic supplier", + "unattained coarse ordinary leaf", + "corrupt Lucas-Lehmer residue", + "old-density paid moment at new coarse point", + "adjacent coarse and kappa grid points" + ], + "depth": 7, + "eta": "1/1000000000000000000000000", + "excluded_coarse": "709928050857150742180413/1000000000000000000000000000", + "full_record_note": "SHA-256 of the compact sorted JSON of the complete recomputed record; write it out with --dump PATH.", + "full_record_sha256": "de8771e266553c196243a2c979de68d42d5423102c69ccca2eef0b2044d7fb6d", + "gain_over_pr240": "3908150629699/1000000000000000000000000", + "kappa": "709424410568125629699/1000000000000000000000000", + "kappa_decimal": "0.000709424410568125629699", + "kappa_grid": 1000000000000000000000000, + "minimum_strict_constraint": "10832642377581035494695296821178533499673945779813408255286918911514209978022657405185936620440519269216604609649967868394833616688605989605177135955517175213216408326174719786469010781230802601418458882803839/15258789062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "parent_eta": "1/1000000000000", + "parent_eta_seven_level_kappa": "354712205282999181517/500000000000000000000000", + "pr240_certificate_sha256": "9309284d492d5631e794cef134e183c266e96c48715994bdbed7113ce7233362", + "pr240_kappa": "28376976266399/40000000000000000", + "prime": { + "criterion": "Lucas-Lehmer sufficiency, independently kernel-checked in Prime.lean", + "fixed_before_all_widths": true, + "iterations": 125, + "p": 127, + "q": 170141183460469231731687303715884105727 + }, + "prime_residues_sha256": "6cf3fcaaa2a1b05097bab0a570cfb0f9c1b56efb83ec49aa3dff9a08281dfc5a", + "q_power_bound": { + "coefficient": 62150081742953667360, + "enlarged_role_charge": 654573856200, + "low_matrix_power": 14400, + "original_coefficient": 1567472751689902, + "original_copies": 12, + "per_selector_coefficient": 5088069708, + "route_families": 208450, + "selector_calls": 12211167492, + "strict_upper": "q^14401" + }, + "rare_density": "3456000/170141183460469231731687303715884105727", + "relative_gain_over_pr240": "3908150629699/709424406659975000000", + "schema": "five-stage-493-fixed-prime/1", + "six_level_kappa": "354712205284062814807/500000000000000000000000", + "strict_constraints": 47, + "three_level_kappa": "354712205164106803993/500000000000000000000000" +} diff --git a/research/five-stage-493-fixed-prime/lakefile.toml b/research/five-stage-493-fixed-prime/lakefile.toml new file mode 100644 index 0000000000..9a3ab1f712 --- /dev/null +++ b/research/five-stage-493-fixed-prime/lakefile.toml @@ -0,0 +1,6 @@ +name = "fixed_prime_certificate" +version = "0.1.0" +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "f897ebcf72cd16f89ab4577d0c826cd14afaafc7" diff --git a/research/five-stage-493-fixed-prime/lean-toolchain b/research/five-stage-493-fixed-prime/lean-toolchain new file mode 100644 index 0000000000..c00a53503c --- /dev/null +++ b/research/five-stage-493-fixed-prime/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.24.0 diff --git a/research/five-stage-493-fixed-prime/requirements.txt b/research/five-stage-493-fixed-prime/requirements.txt new file mode 100644 index 0000000000..1ca5fd0616 --- /dev/null +++ b/research/five-stage-493-fixed-prime/requirements.txt @@ -0,0 +1 @@ +sympy==1.14.0 diff --git a/research/five-stage-493-fixed-prime/verify.py b/research/five-stage-493-fixed-prime/verify.py new file mode 100644 index 0000000000..e3ef26a4f7 --- /dev/null +++ b/research/five-stage-493-fixed-prime/verify.py @@ -0,0 +1,215 @@ +#!/usr/bin/env python3 +"""Fixed prime, seven finite levels and the assembly backoff eta = 10^-24 on PR240's banked five-stage word. + +Usage (repository root, assertions enabled, sympy==1.14.0): + python3 -B research/five-stage-493-fixed-prime/verify.py --pr210-root --pr234-root [--full] [--write] + +First runs PR240's own verifier (research/five-stage-banks-493, same checkout): the 493-source helper on every +column, telescope, five-stage lowering, geometry, primes, finite bill, 231 charts, 176,915 banks and the coloring, +and requires its stored certificate to be reproduced. Then, on PR240's banked profile unchanged: + +* the fixed prime q = 2^127 - 1 (Lucas-Lehmer here; Prime.lean kernel-checks it), whose proved rare-class density + 2m^3/q replaces the 10^-16 envelope while every rare class still pays the full 32m^2 rank-one fallback; +* the coarse saving on the 10^-27 grid, bracketed by PR234's public engine and an independent atanh engine; +* seven finite ordinary levels a_j = (1-c)c + c a_(j-1) from the retained completed saving 384599/10^10; +* PR234's unchanged outer-47 assembly with eta = 10^-24 (PR234/240 used 10^-12; all 47 strict inequalities and + 7 margins are recomputed) and beta = 10^-9, on the 10^-24 kappa grid; the adjacent grid point is rejected; +* the fully paid prime-dependent constant, with PR240's fresh finite-bill values. + +The fixed-prime argument and the seven levels follow PR235 (Gabriele Nespoli, Apache-2.0, OpenAI Codex), applied here +to PR240's word. Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import argparse, importlib.util, json, subprocess, sys +if sys.flags.optimize: raise SystemExit('Assertions required') +sys.set_int_max_str_digits(0); sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PR240 = ROOT / 'research/five-stage-banks-493' +V8 = 'research/five-stage-source-bound-v8' +DEPTH = 7; GRID = 10 ** 24; COARSE_GRID = 10 ** 27; PRIME = 2 ** 127 - 1 +ETA = Q(1, 10 ** 24); PARENT_ETA = Q(1, 10 ** 12); BETA = Q(1, 10 ** 9) +PR240_KAPPA = Q(28376976266399, 40000000000000000) + + +def require(ok, message): + if not ok: raise ValueError(message) + + +def serial(x): + if isinstance(x, Q): return str(x) + if isinstance(x, dict): return {str(k): serial(v) for k, v in x.items()} + if isinstance(x, (tuple, list)): return [serial(v) for v in x] + return x + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + mod = importlib.util.module_from_spec(spec); spec.loader.exec_module(mod); return mod + + +def point(x, grid=GRID): + z = x * grid; return Q((z.numerator - 1) // z.denominator, grid) + + +def prime_certificate(): + require(all(127 % d for d in range(2, 12)), 'Composite Mersenne exponent') + values = [4] + for _ in range(125): values.append((values[-1] ** 2 - 2) % PRIME) + require(values[-1] == 0 and PRIME > 2 ** 80 and PRIME % 2 == 1, 'Ineligible prime') + return dict(q=PRIME, p=127, iterations=125, residues=values, + criterion='Lucas-Lehmer sufficiency, independently kernel-checked in Prime.lean', fixed_before_all_widths=True) + + +def validate_step(j, predecessor, c, old, a): + require(1 <= j <= DEPTH and predecessor == j - 1, 'Cyclic completed supplier') + require(a == (1 - c) * c + c * old and old < a < c < 1 - a, 'Unpaid finite toll or unattained coarse leaf') + gaps = dict(atom=c - a, borrowing=1 - a - c, remainder=1 - a - c * (1 - old), stock=1 - c) + require(min(gaps.values()) > 0, 'Nonpositive cutoff gap') + return gaps + + +def arithmetic(P234, parent): + public = load('pr234_moment', P234 / V8 / 'code/five_stage_bit_cost_20261009.py') + outer = load('pr234_outer47', P234 / V8 / 'code/paired_cube_assembly.py') + cutoffs = load('pr234_finite_cutoff', P234 / V8 / 'finite_check.py') + independent = load('independent_atanh_moment', HERE / 'base_two_moment.py') + proof = (P234 / V8 / 'proof/three-stage-cover-bit.tex').read_text() + require('bad fraction at most $2m^3/q<10^{-16}$' in proof, 'Detached rare-density bound') + ar = parent['arithmetic']; physical = parent['physical']; finite = parent['checks']['finite'] + prime = prime_certificate() + bp = ar['bit_profile']; m = bp['m']; W = bp['W'] + H = {int(r): n for r, n in bp['histogram'].items()} + E = sum(H.values()); mass = sum(r * n for r, n in H.items()) + require(m == 120 and m * W - mass == bp['deficit'] == 52800 and max(H) < m // 2 and all(0 < r < m and n > 0 for r, n in H.items()), + 'Changed banked profile') + require(parent['checks']['primes']['prime_factors'] == [2, 3, 5, 7] and parent['checks']['primes']['all_remaining_factors_below_2_power_80'], + 'Unverified excluded primes') + require(max(physical['max_num'], physical['max_den']) < 2 ** 80 and physical['conservative_selector_calls'] < 2 ** 40, 'Ineligible bank charts') + require(finite['fallback_children'] == 32 * m * m, 'Fallback count changed') + rho = Q(2 * m ** 3, PRIME); require(0 < rho < Q(1, 10 ** 16), 'Fallback omitted or no density improvement') + fallback = [(1, 32 * m * m * E)] + def paid(a, density=rho): + lo, hi = public.moment(H, m, W, a, False) + l, u = public.logarithm(Q(m)); e, f = public.exponential(a * l, a * u) + bill = density * Q(32 * m * E, W) + return public.floor(lo + bill * e), public.ceil(hi + bill * f) + def separate(a): + lo, hi = independent.moment(m, W, list(H.items()), a) + fl, fu = independent.moment(m, W, fallback, a) + return lo + rho * fl, hi + rho * fu + c0 = Q(ar['bit_coarse_saving']); lo = int(c0 * COARSE_GRID); hi = lo + COARSE_GRID // 10 ** 8 + require(paid(Q(lo, COARSE_GRID))[1] < 1 < paid(Q(hi, COARSE_GRID))[0], 'Coarse bracket') + while hi - lo > 1: + mid = (lo + hi) // 2; l, u = paid(Q(mid, COARSE_GRID)) + if u < 1: lo = mid + elif l > 1: hi = mid + else: raise ValueError('Inconclusive rational moment enclosure') + c = Q(lo, COARSE_GRID); excluded = Q(hi, COARSE_GRID) + pa, pe, ia, ie = paid(c), paid(excluded), separate(c), separate(excluded) + require(pa[1] < 1 < pe[0] and ia[1] < 1 < ie[0], 'Independent paid moment bracket') + require(paid(c, Q(1, 10 ** 16))[0] > 1, 'Improvement does not depend on the certified smaller density') + base = Q(384599, 10 ** 10); b = Q(ar['complex_saving']) + require(Q(ar['ordinary_chain'][0]) == base, 'Changed completed base supplier') + require(Q(ar['complex_moment_interval'][1]) < 1, 'Complex moment') + bridge = dict(proof='PROOF.md', representation='Exact powers with source-bound finite overcharges', + semantic=dict(G=dict(base=2, exponent=30000), E=dict(base=2, exponent=100000), + B_upper=dict(base=2, exponent=100001), C0=dict(base=2, exponent=210000), C1=1, + strict_literal_gap=1, induction_gap_lower=1), + rows=dict(coefficient=20161, degree=10 ** 6, suffix_slope=4 * 10 ** 6, + degree_gap=Q(10 ** 6) - Q(51 * 20161, 25))) + def assemble(a, grid=GRID, eta=ETA): + require(a < (1 - BETA) * b, 'Complex cap became active') + z = a * (1 - 2 * eta); bound = (1 - eta) * z / (1 + z); k = point(bound, grid) + result = outer.assembly(a, b, bridge, k, eta=eta, beta=BETA) + require(len(result['strict_constraints']) == 47 and len(result['margins']) == 7, 'Incomplete outer assembly') + require(all(v > 0 for v in result['strict_constraints'].values()) and all(v > k for v in result['margins'].values()), 'Non-strict outer inequalities') + try: outer.assembly(a, b, bridge, k + Q(1, grid), eta=eta, beta=BETA) + except AssertionError: pass + else: raise ValueError('Adjacent kappa point admitted') + return dict(kappa=k, bound=bound, assembly=result) + chain = [base]; steps = [] + for j in range(1, DEPTH + 1): + old_a = chain[-1]; a = (1 - c) * c + c * old_a; gaps = validate_step(j, j - 1, c, old_a, a) + require(a == c - c ** j * (c - base), 'Recurrence mismatch') + delta = min(gaps.values()); L = cutoffs.cutoff_log2(delta, 1) + require(L * delta ** 2 >= 36 and L * delta >= 8, 'Cutoff arithmetic') + steps.append(dict(level=j, ordinary_predecessor=j - 1, saving=a, gaps=gaps, minimum_gap=delta, cutoff_log2_at_C_equals_1=L)) + chain.append(a) + result = assemble(chain[-1]) + require(assemble(Q(ar['ordinary_chain'][-1]), 10 ** 18, PARENT_ETA)['kappa'] == Q(ar['kappa']) == PR240_KAPPA, 'Published PR240 comparator') + previous = assemble(Q(ar['ordinary_chain'][-1])) + require(result['kappa'] > PR240_KAPPA and result['kappa'] > previous['kappa'], 'No improvement over PR240') + parent_eta_seven = assemble(chain[-1], GRID, PARENT_ETA) + require(result['kappa'] > parent_eta_seven['kappa'], 'Smaller eta does not improve the grid point') + sixth = assemble(chain[6]); third = assemble(chain[3]) + delta1 = 1 - Q(mass, m * W) - rho * Q(32 * m * E, W) + require(delta1 > 0 and 1 - pa[1] > 0, 'Recurrence contraction gap') + base_coefficient = finite['q_power_coefficient']; J = finite['route_and_final_exchange_families'] + d = m * m; N = 2 * m; K = physical['conservative_selector_calls'] + per_selector = 16 * (d + 1) ** 2 + (W + 12 * 24) + 128 * N ** 3 + (8 * m * m + 8) + 1 + enlarged_role_charge = 12 * J * (W + 12 * 24) + coefficient = 12 * base_coefficient + enlarged_role_charge + K * per_selector + require(coefficient < 2 ** 80 < PRIME, 'Invalid banked q-power overcharge') + controls = [] + for name, j, pred, a in [('cyclic supplier', DEPTH, DEPTH, chain[-1]), ('unattained coarse ordinary leaf', DEPTH, DEPTH - 1, c)]: + try: validate_step(j, pred, c, chain[-2], a) + except ValueError: controls.append(name) + else: raise ValueError('Invalid supplier admitted') + corrupted = prime['residues'][:]; corrupted[37] += 1 + require(any(corrupted[i + 1] != (corrupted[i] ** 2 - 2) % PRIME for i in range(125)), 'Corrupt prime residue accepted') + controls += ['corrupt Lucas-Lehmer residue', 'old-density paid moment at new coarse point', 'adjacent coarse and kappa grid points'] + return serial(dict(schema='five-stage-493-fixed-prime/1', scope='Conditional on the unchanged PR234/PR240 all-size and symbolic interfaces', + prime=prime, rare_density=rho, depth=DEPTH, coarse_grid=COARSE_GRID, kappa_grid=GRID, + banked_profile=bp, coarse=c, excluded_coarse=excluded, public_accepted=pa, public_excluded=pe, + independent_accepted=ia, independent_excluded=ie, fallback_histogram=fallback, + delta_linear=delta1, delta_tau_lower=1 - pa[1], ordinary_chain=chain, steps=steps, + eta=ETA, parent_eta=PARENT_ETA, beta=BETA, complex_saving=b, kappa=result['kappa'], + kappa_decimal=public.decimal(result['kappa']), pr240_kappa=PR240_KAPPA, gain_over_pr240=result['kappa'] - PR240_KAPPA, + relative_gain_over_pr240=result['kappa'] / PR240_KAPPA - 1, + parent_eta_seven_level_kappa=parent_eta_seven['kappa'], three_level_kappa=third['kappa'], six_level_kappa=sixth['kappa'], + assembly=result['assembly'], minimum_margin=result['bound'], + q_power_bound=dict(coefficient=coefficient, low_matrix_power=14400, strict_upper='q^14401', original_copies=12, + original_coefficient=base_coefficient, enlarged_role_charge=enlarged_role_charge, + per_selector_coefficient=per_selector, route_families=J, selector_calls=K), + controls=controls)) + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--pr210-root', type=Path, required=True) + ap.add_argument('--pr234-root', type=Path, required=True) + ap.add_argument('--full', action='store_true', help='Pass --full to PR240 (also runs PR234 fresh verifier)') + ap.add_argument('--write', action='store_true') + ap.add_argument('--dump', type=Path, help='Also write the complete recomputed record here') + a = ap.parse_args() + cmd = [sys.executable, '-B', str(PR240 / 'verify.py'), '--pr210-root', str(a.pr210_root), '--pr234-root', str(a.pr234_root)] + if a.full: cmd.append('--full') + print('Running PR240 verifier', flush=True) + subprocess.run(cmd, cwd=ROOT, check=True) + parent = json.loads((PR240 / 'certificate.json').read_text()) + result = arithmetic(a.pr234_root.resolve(), parent) + result['pr240_certificate_sha256'] = sha256((PR240 / 'certificate.json').read_bytes()).hexdigest() + full = json.dumps(result, sort_keys=True, separators=(',', ':')).encode() + if a.dump: a.dump.write_text(json.dumps(result, sort_keys=True, indent=2) + '\n') + keys = ['schema', 'kappa', 'kappa_decimal', 'pr240_kappa', 'gain_over_pr240', 'relative_gain_over_pr240', 'coarse', + 'excluded_coarse', 'rare_density', 'depth', 'eta', 'parent_eta', 'beta', 'complex_saving', 'coarse_grid', + 'kappa_grid', 'parent_eta_seven_level_kappa', 'three_level_kappa', 'six_level_kappa', 'controls', + 'pr240_certificate_sha256'] + summary = {k: result[k] for k in keys} + summary['prime'] = {k: v for k, v in result['prime'].items() if k != 'residues'} + summary['prime_residues_sha256'] = sha256(json.dumps(result['prime']['residues']).encode()).hexdigest() + summary['q_power_bound'] = result['q_power_bound'] + summary['strict_constraints'] = len(result['assembly']['strict_constraints']) + summary['minimum_strict_constraint'] = min(result['assembly']['strict_constraints'].values(), key=lambda x: Q(x)) + summary['full_record_sha256'] = sha256(full).hexdigest() + summary['full_record_note'] = 'SHA-256 of the compact sorted JSON of the complete recomputed record; write it out with --dump PATH.' + path = HERE / 'certificate.json' + if a.write: path.write_text(json.dumps(summary, sort_keys=True, indent=2) + '\n') + else: require(summary == json.loads(path.read_text()), 'Certificate mismatch') + print('PASS kappa=' + result['kappa'] + ' = ' + result['kappa_decimal'], flush=True) + + +if __name__ == '__main__': main() diff --git a/research/five-stage-banks-493/NOTICE b/research/five-stage-banks-493/NOTICE new file mode 100644 index 0000000000..3dbfcd656c --- /dev/null +++ b/research/five-stage-banks-493/NOTICE @@ -0,0 +1,14 @@ +Five-stage completed banks with PR210's 493-source helper. Apache-2.0. +Prepared by Rohan Arun (rohanarun) with Anthropic Claude assistance. + +Reused, with credit: +- eumemic, PR210 at 13311491eb74a3a9a443ba4e318c68c263f064f0 (with Dugongue's PR216 cuts, sennemmi's PR230 frames + and our PR211 frames; OpenAI Codex assistance): the 493-source helper word, its preparation (extra/, targetagg/, + rank/, echelon/) and its complete F2/integer replay with 17 controls, executed unchanged. +- hcg890, PR234 at af3fe331ca60c936229e060681ffccbc1c208678 (ChatGPT assistance) and Jacob Sussman: the five-stage + cover, its physical telescope, global lowering, exact geometry, prime validator, finite bill, moment engine, + bootstrap and outer-47 assembly, and the five-stage complex supplier. telescope493.py adapts PR234's telescope + to PR210's newer replay; helper493.py rebinds PR234's helper-specific constants to fresh values. +- Evan McKinney, PR197: completed-bank packing and the colouring helpers (banks.py byte-identical). +- Rohan Arun, PR205/PR237: completed banks on PR200 and on PR234's five-stage cover. +- Chafik Boukhalfa (PR200), Avi Eisenberg (PR193) and every contributor credited by those packages. diff --git a/research/five-stage-banks-493/README.md b/research/five-stage-banks-493/README.md new file mode 100644 index 0000000000..cc1860f8a3 --- /dev/null +++ b/research/five-stage-banks-493/README.md @@ -0,0 +1,48 @@ +# Five-stage completed banks with PR210's newest 493-source helper + +Under the retained multiplication interfaces, this finite witness certifies + +$$ +T(n)=O\left(n(\log n)^{1-\kappa}\right),\qquad +\kappa=\frac{28376976266399}{40000000000000000}=0.000709424406659975 . +$$ + +That is **+0.119%** over PR237 (0.000708582410781108, five-stage banks on PR234's 471-source helper) and **+0.813%** over PR234 (0.000703701743496697). + +| Construction | Helper | Bit coarse | κ | +|---|---|---:|---:| +| PR234 | PR210 df95878 (471 sources), paid exteriors | 7.041973e-4 | 0.000703701743496697 | +| PR237 | same, width-120 banks | 7.090849e-4 | 0.000708582410781108 | +| **This** | **PR210 1331149 (493 sources, target aggregation/rank/echelon, PR230 frames), width-120 banks** | **7.099280e-4** | **0.000709424406659975** | + +The bit side binds; PR234's five-stage complex supplier (7.47455e-4) is unchanged. + +## What is new + +PR234 builds its five-stage cover from PR210's older helper (`df95878`, 471 borrowed sources). PR210 has since added 22 more source entrances, 82 equal-response target aggregation groups, 7 integer rank-compression groups, 4 signed echelon target transforms and PR230's frame refinements (head `1331149`, 16,621 physical registers instead of 16,643). This package runs that newer helper through PR234's five-stage pipeline and then applies PR237's completed width-120 banks. + +- **Helper (PR210's own code, unchanged).** The package assembles PR210's research package with PR234's pinned PR200 base inputs, derives the 34 terminal records exactly as PR234 does, prepares the helper with PR210's `targetagg/setup.py`, and runs PR210's replay: all 20,141 F2 columns, the literal majorant (24-bit digits), both defining-integer signs, and all 17 corruption controls. +- **Physical telescope.** PR234's frame-tag telescope, adapted to PR210's newer replay (22 tagged event kinds, including aggregation, rank and echelon setup/read/restore). 2,569,922 tagged events; an independent literal projection and its inverse reproduce the all-column F2 endpoint and the event digest. +- **Five-stage lowering and geometry.** PR234's global lowering and exact h24/m120 geometry, with only the helper-specific constants (register count, event count, call count, rank mass) rebound to the fresh values. The five-stage profile is m = 120, W = 23,661, 494,909 calls, rank mass 2,834,920, deficit 4,400. +- **Primes.** All 26,464 used bases have nonzero cleared Gram determinants whose factors outside {2,3,5,7} leave a residual below 2^80. +- **Finite bill.** PR234's formulas with fresh values; the payload-prefix lift needs 101 bits (PR234: 98), still a fixed finite constant. +- **Banks.** Same 231 entrance charts as PR237. 12 copies give 176,915 banks of width 120 (360×(8·11+8·4), 108×(10·12), 39×(20·6), 4,304×(30·4), 172,104×(5·24)) with a proper 60-colouring of 997,260 incidences. W = 12·4v + 176,915 = 261,395; deficit 52,800; largest child 50. +- **Arithmetic.** PR234's interval moment engine certifies coarse saving 709928047185833/10^18; three finite ordinary levels and PR234's outer-47 assembly give κ; the next 10^-18 grid point fails. + +## Verify + +```sh +git fetch https://github.com/CrocSwap/integer-mult-bounds pull/210/head pull/234/head +git worktree add --detach ../pr210 13311491eb74a3a9a443ba4e318c68c263f064f0 +git worktree add --detach ../pr234 af3fe331ca60c936229e060681ffccbc1c208678 +python3 -m pip install sympy==1.14.0 +python3 -B research/five-stage-banks-493/verify.py --pr210-root ../pr210 --pr234-root ../pr234 --full +``` + +About 10 minutes: PR234's own fresh verifier (for the complex supplier, ~3.5 min), PR210's complete helper replay with controls (~3 min), telescope, lowering, geometry, primes, banks and arithmetic. It compares the result with `certificate.json`. + +## Scope + +Conditional, exactly as PR234/PR237: the five-stage physical program and complex symbolic theorems, weighted q-local compiler, complete-stream movement, copied-centre and restored-row interfaces, ordinary leaves, prime supply, precision/recovery and the all-size reduction remain retained hypotheses. PR234's helper-specific checks are reused with recomputed constants rather than re-derived. Not an unconditional multiplication theorem or a speedup claim. + +Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. diff --git a/research/five-stage-banks-493/SOURCE.json b/research/five-stage-banks-493/SOURCE.json new file mode 100644 index 0000000000..ec1dedb631 --- /dev/null +++ b/research/five-stage-banks-493/SOURCE.json @@ -0,0 +1,53 @@ +{ + "pr210": { + "commit": "13311491eb74a3a9a443ba4e318c68c263f064f0", + "repository": "CrocSwap/integer-mult-bounds refs/pull/210/head", + "files": { + "research/coordinated-crossover-pr200/frames/opframe-bases.json": "9a2bba5c72aebc9ee4f21e59b10ce810b2da98a1fa1748fbc44c50a080e584ff", + "research/coordinated-crossover-pr200/joint/joint_word.py": "de37cbed753fc6f13a7e5dc25c8346279cfee5f1868df8c12a5fcb6ca8f631c0", + "research/coordinated-crossover-pr200/joint/pairs.json": "da54b863601b5cbc21d27fc5cd623bf805f974a3e47b81ed29a85aa5bad0fa05", + "research/coordinated-crossover-pr200/joint/joint-selection.json": "13f6420d6c341c22235c9d136d5f7c32896974bb165a893fecd7e583b790d133", + "research/coordinated-crossover-pr200/borrow/selection.json": "6932749407e14b199651f0a7deff02c6de74e2c1be0a1300263f1e164927fb8b", + "research/coordinated-crossover-pr200/gaugeb/selection.json": "b0f9f0e67f94a3c21069f393ea27f9483d315bff2f53f77270163065a6345d1c", + "research/coordinated-crossover-pr200/newg/replay.py": "0cbec81a11e758156e9303f63dc8c617601da69523073fdf2a77394d76acf56a", + "research/coordinated-crossover-pr200/newg/selection.json": "d94ef4e0b8ca98a7385b364cf245816a7cad08f850a60ce8b67aab4c3a89f3f4", + "research/coordinated-crossover-pr200/newg/schedule.json": "ab39d61fff7a2cfcb13e2c10d65f2c603e76a91013d197260d6c7b645ccb27a1", + "research/coordinated-crossover-pr200/extra/setup.py": "a7789d13eda75e78108cee84206692c913f63aafdb9e3e633fddd14640e4678a", + "research/coordinated-crossover-pr200/extra/selection.json": "791f6ddeb19add7026ba37461256c13efe3d35bba0bccf1cb9787a01fc16f0f2", + "research/coordinated-crossover-pr200/targetagg/setup.py": "fd7adf0b12d0769e06438b2ee4322bfcb180d8f73a1104a3eb805ab88c5cc393", + "research/coordinated-crossover-pr200/targetagg/word.py": "293a0babfac7e92ffccfe1cb69971b26a49fe56f67872b1060c3fe49d759a463", + "research/coordinated-crossover-pr200/targetagg/selection.json": "b7a4d5eb2a6d2f7df867f9be5af7da1d1aa99cfbd5214195967b0ff60642d77a", + "research/coordinated-crossover-pr200/rank/selection.json": "5c97c6413f1eb56c7b8f9ba9e839329d212fae7ac3a08c29e9efdee42f5048a0", + "research/coordinated-crossover-pr200/echelon/selection.json": "8e6ce5e257aa7656898ab46bc3421df4a619497b1e9f5956d2c546b3014050a7" + } + }, + "pr234": { + "commit": "af3fe331ca60c936229e060681ffccbc1c208678", + "repository": "CrocSwap/integer-mult-bounds refs/pull/234/head", + "files": { + "research/five-stage-source-bound-v8/expected-math.json": "44426de51a4d096e1987f43faf8e754d1b29abc8b8b5c4c9d81b15db4f73b0bc", + "research/five-stage-source-bound-v8/verify.py": "827c559d949df4ec462691a42067355ebd6d6baff55c48410d5f36247f0ca9a9", + "research/five-stage-source-bound-v8/MANIFEST.json": "fc691fdf74a7b06c9290d6e91e6d63dc1c7e20c6556519dcf9b7f53fa02350de", + "research/five-stage-source-bound-v8/code/five_stage_bit_cost_20261009.py": "9d465c716c6b910ff66e1453e3bf0057608a787b5f5361be93781f42cb3370f7", + "research/five-stage-source-bound-v8/code/paired_cube_assembly.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c", + "research/five-stage-source-bound-v8/code/five_stage_bit_global_lowering_20261009.py": "2f4fd25eebbfdfbf37e2375e23b4827fda62776dff3b3b64e971dd215b2664bc", + "research/five-stage-source-bound-v8/code/five_stage_bit_global_lowering_geometry_20261009.py": "4a619e5d40c05295ef83183ee0d11bee12d0053bab2596ec9cfcd7fea4936157", + "research/five-stage-source-bound-v8/code/prime_witnesses.py": "98cd03bc9582e7bd0ab194c191ea8eea940539e510051443ab9fd3e572a364ab", + "research/five-stage-source-bound-v8/loader/source_loader.py": "e5e19ee6d6899fce8273d0f06a49caf7cd8bfe940a2a9a103dbc9d3a62b6b291", + "research/five-stage-source-bound-v8/loader/source_inputs/base_bit/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "research/five-stage-source-bound-v8/loader/source_inputs/base_bit/NOTICE": "c9850418622aea8d1382a230306c940947b5da818f4854b4b272ed60cf239f6c", + "research/five-stage-source-bound-v8/loader/source_inputs/base_bit/research/paired-cube-diagonal-bit-168/bit/base_word.py": "9fe3a81b7561d2b09c086f63fac4626e88a32369ef8bc5579c94878de1218a89", + "research/five-stage-source-bound-v8/loader/source_inputs/base_bit/research/paired-cube-diagonal-bit-168/bit/word.py": "85822e9cca5b1b2335c3704a3df2f3c6ef01e42d8328daacb33701d30cee80ab", + "research/five-stage-source-bound-v8/loader/source_inputs/base_bit/research/paired-cube-diagonal-bit-168/references/pr168-v4/research/paired-cube-bit/check_paired_cube_bit.py": "4d7c86cd999a1519e0dfb6dcf33a8f26e442a353c3665a0f06881216a260fbf3", + "research/five-stage-source-bound-v8/loader/source_inputs/base_bit/research/paired-cube-diagonal-bit-168/selected/bit/frames_p12.json.gz": "ad8e2705652b68476713d7647a8592505e222f2b3ccd1728dedce153aac6d462", + "research/five-stage-source-bound-v8/loader/source_inputs/base_bit/research/paired-cube-diagonal-bit-168/selected/bit/graph_p12.json": "31a09a55920e64c8bfbac8b845dc01754c112aa6e207812e2fd1f4939d8f64cb", + "research/five-stage-source-bound-v8/loader/source_inputs/base_bit/research/paired-cube-diagonal-bit-168/selected/bit/kchron_p12.json": "0fab548e84cf5ca7c04e8bd19b5810850463f36e0f92180efe73aeff17105e39", + "research/five-stage-source-bound-v8/loader/source_inputs/base_bit/research/paired-cube-diagonal-bit-168/selected/bit/profile_p12.json": "c44ef8640cbcbcc9bac3a30e13373bd79efddde55d7cea514354ca2cdb60d66d", + "research/five-stage-source-bound-v8/loader/source_inputs/base_bit/research/paired-cube-diagonal-bit-168/selected/bit/sinks.json": "c00ff70c564829d4b97740f92796fc6ce14fbcd5ca519663828650552b80249d", + "research/five-stage-source-bound-v8/loader/source_inputs/base_bit/research/paired-cube-diagonal-bit-168/selected/bit/word_p12.json.gz": "1cb7e8ed45cf542e304fddc4b12247dbb248a0dc84dedbd832f336b2d172793a", + "research/five-stage-source-bound-v8/loader/source_inputs/pr210/research/coordinated-crossover-pr200/joint/pairs.json": "da54b863601b5cbc21d27fc5cd623bf805f974a3e47b81ed29a85aa5bad0fa05", + "research/five-stage-source-bound-v8/loader/source_inputs/pr210/research/coordinated-crossover-pr200/joint/joint-selection.json": "13f6420d6c341c22235c9d136d5f7c32896974bb165a893fecd7e583b790d133", + "research/five-stage-source-bound-v8/loader/source_inputs/pr210/research/coordinated-crossover-pr200/gaugeb/selection.json": "b0f9f0e67f94a3c21069f393ea27f9483d315bff2f53f77270163065a6345d1c" + } + } +} diff --git a/research/five-stage-banks-493/arithmetic5.py b/research/five-stage-banks-493/arithmetic5.py new file mode 100644 index 0000000000..e2c96fdc49 --- /dev/null +++ b/research/five-stage-banks-493/arithmetic5.py @@ -0,0 +1,94 @@ +"""(493-helper copy) Exact paid moments, three finite ordinary levels and PR234's outer-47 assembly for the banked five-stage bit +supplier. Uses PR234's own pinned moment, bootstrap and assembly code unchanged. +Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from pathlib import Path +import importlib.util + +PKG = 'research/five-stage-source-bound-v8' +PR234_KAPPA = Q(703701743496697, 10 ** 18) +PR230_KAPPA = Q(694787513005285, 10 ** 18) +PR237_KAPPA = Q(177145602695277, 250000000000000000) # PR237: banks on PR234's 471-source five-stage helper + + +def load(name, path): + s = importlib.util.spec_from_file_location(name, path); m = importlib.util.module_from_spec(s); s.loader.exec_module(m) + return m + + +def build(P234, pr234_math, physical): + """pr234_math: PR234's freshly computed mathematics (bit_profile, complex_profile, assembly parameters).""" + math = load('pr234_moments', P234 / PKG / 'code/five_stage_bit_cost_20261009.py') + outer = load('pr234_outer47', P234 / PKG / 'code/paired_cube_assembly.py') + bp = pr234_math['bit_profile']; cp = pr234_math['complex_profile'] + assert (bp['m'], bp['deficit'], bp['maxchild']) == (120, 4400, 100) + H = {int(k): n for k, n in bp['histogram'].items()} + removed = {int(k): n for k, n in physical['removed_exteriors'].items()} + for r, n in removed.items(): + assert H[r] >= n; H[r] -= n + c = physical['copies']; m = 120 + H = {r: c * n for r, n in H.items() if n} + W = physical['W']; mass = sum(r * n for r, n in H.items()); deficit = m * W - mass + assert deficit == c * bp['deficit'], 'banking preserves the telescoping deficit' + assert max(H) < m // 2 + # Coarse paid saving on the 10^-18 grid, PR234's interval engine with the inherited bad-class envelope. + root = Q(math.certify(H, m, W, True)['lower']); den = 10 ** 18 + lo = Q(int(root * den), den) + while math.moment(H, m, W, lo, True)[1] >= 1: lo -= Q(1, den) + hi = lo + Q(1, den) + while math.moment(H, m, W, hi, True)[0] <= 1: lo = hi; hi = lo + Q(1, den) + assert math.moment(H, m, W, lo, True)[1] < 1 < math.moment(H, m, W, hi, True)[0] + coarse = lo + unbanked = {int(k): n for k, n in bp['histogram'].items()} + old_coarse = Q(pr234_math['contract']['assembly']['bit_coarse']) if 'contract' in pr234_math else None + if old_coarse is not None: + assert math.moment(H, m, W, old_coarse, True)[1] < math.moment(unbanked, m, bp['W'], old_coarse, True)[0], \ + 'banking strictly improves the paid moment at PR234 coarse saving' + chain = [Q(384599, 10 ** 10)] + for _ in range(3): + a = (1 - coarse) * coarse + coarse * chain[-1] + assert chain[-1] < a < coarse < 1 - a + chain.append(a) + bit = chain[-1] + b = Q(pr234_math['assembly']['parameters']['a_complex']) + cm = math.moment({int(k): n for k, n in cp['histogram'].items()}, 110, cp['W'], b, False) + assert cm[1] < 1 + eta = Q(1, 10 ** 12); beta = Q(1, 10 ** 9) + assert bit < (1 - beta) * b + bridge = dict(proof='PROOF.md', representation='Exact powers with source-bound finite overcharges', + semantic=dict(G=dict(base=2, exponent=30000), E=dict(base=2, exponent=100000), + B_upper=dict(base=2, exponent=100001), C0=dict(base=2, exponent=210000), C1=1, + strict_literal_gap=1, induction_gap_lower=1), + rows=dict(coefficient=20161, degree=10 ** 6, suffix_slope=4 * 10 ** 6, + degree_gap=Q(10 ** 6) - Q(51 * 20161, 25))) + q = bit * (1 - 2 * eta); minimum = (1 - eta) * q / (1 + q); ticks = minimum * den + kappa = Q(ticks.numerator // ticks.denominator, den) + if kappa == minimum: kappa -= Q(1, den) + result = outer.assembly(bit, b, bridge, kappa, eta=eta, beta=beta) + assert len(result['strict_constraints']) == 47 and len(result['margins']) == 7 + assert all(x > 0 for x in result['strict_constraints'].values()) + try: outer.assembly(bit, b, bridge, kappa + Q(1, den), eta=eta, beta=beta) + except AssertionError: pass + else: raise AssertionError('adjacent kappa grid point admitted') + assert kappa > PR237_KAPPA > PR234_KAPPA > PR230_KAPPA + controls = [] + try: profile_check({**H, 1: H[1] + 1}, m, W, c * bp['deficit']) + except AssertionError: controls.append('changed rank mass rejected') + else: raise AssertionError('corrupt rank mass accepted') + try: math.moment({**H, m: 1}, m, W, coarse, True) + except AssertionError: controls.append('full-width child rejected') + else: raise AssertionError('full-width child accepted') + return dict(scope='Conditional finite supplier composition; PR234 physical, scalar, prime and analytic dependencies inherited', + bit_profile=dict(m=m, W=W, copies=c, histogram={str(r): n for r, n in sorted(H.items())}, + calls=sum(H.values()), rank_mass=mass, deficit=deficit, maxchild=max(H)), + bit_coarse_saving=coarse, pr234_bit_coarse_saving=old_coarse, ordinary_chain=chain, bit=bit, + complex_saving=b, complex_moment_interval=cm, assembly=result, kappa=kappa, + comparison_pr234_kappa=PR234_KAPPA, relative_gain_over_pr234=kappa / PR234_KAPPA - 1, + comparison_pr230_kappa=PR230_KAPPA, comparison_pr237_kappa=PR237_KAPPA, + relative_gain_over_pr237=kappa / PR237_KAPPA - 1, controls=controls) + + +def profile_check(H, m, W, deficit): + assert m * W - sum(r * n for r, n in H.items()) == deficit + return True diff --git a/research/five-stage-banks-493/banks.py b/research/five-stage-banks-493/banks.py new file mode 100644 index 0000000000..6505ebd37e --- /dev/null +++ b/research/five-stage-banks-493/banks.py @@ -0,0 +1,104 @@ +"""PR197 chart inversion and bank colouring helpers (byte-identical extract of packing.py up to build()). + +Apache-2.0. Prepared with substantial OpenAI Codex assistance. +""" +from array import array +from collections import Counter +from fractions import Fraction as Q +from math import gcd +from pathlib import Path +import hashlib,json,sys + +def inverse_integer(a): + """Fraction-free Gauss-Jordan; return integral C,d with a C = d I.""" + n=len(a) + m=[list(row)+[int(i==j) for j in range(n)] for i,row in enumerate(a)] + previous=1 + factors=[] + for k in range(n): + pivot=next((i for i in range(k,n) if m[i][k]),None) + if pivot is None: + raise ValueError('Singular basis') + m[k],m[pivot]=m[pivot],m[k] + if pivot != k:factors.append(('swap',k,pivot,1,1)) + p=m[k][k] + if p != previous: + ratio=Q(previous,p) + factors.append(('scale',k,k,ratio.numerator,ratio.denominator)) + for i in range(n): + if i==k:continue + u=m[i][k] + if u: + ratio=Q(-u,previous) + factors.append(('add',i,k,ratio.numerator,ratio.denominator)) + for j in range(2*n): + if j==k:continue + value=p*m[i][j]-u*m[k][j] + assert value % previous==0 + m[i][j]=value//previous + m[i][k]=0 + previous=p + d=m[0][0] + assert d and all(m[i][j]==d*int(i==j) for i in range(n) for j in range(n)) + c=[row[n:] for row in m] + common=abs(d) + for row in c: + for x in row:common=gcd(common,x) + d//=common + c=[[x//common for x in row] for row in c] + if d<0:d=-d;c=[[-x for x in row] for row in c] + return c,d,factors + +def color_incidence(left,right,nleft,nright,colors): + """Incremental two-color swaps; parallel edges are identified separately.""" + assert len(left)==len(right) + full=(1< 2 * bound + out['majorant'] = dict(residual_bound=bound, packing_bits=bits) + out['integer'] = [m.replay('Z', d, bits) for d in (1, -1)] + controls = {} + for mutation in ['omit_echelon_setup', 'omit_echelon_inverse', 'flip_echelon_sign', 'omit_rank_setup', 'omit_rank_inverse', + 'repeat_rank_read', 'omit_aggregation_setup', 'omit_aggregation_inverse', 'repeat_aggregation_read', + 'omit_extra_mix', 'omit_extra_compensation', 'omit_early_mix', 'old_adjoint', 'undo_before_restore', + 'omit_gauge_mix', 'omit_gauge_compensation', 'late_phase1_gauge']: + try: m.replay('Z' if mutation == 'flip_echelon_sign' else 'F2', bits=bits, mutation=mutation) + except AssertionError: controls[mutation] = 'REJECTED' + else: raise AssertionError('corruption accepted: ' + mutation) + out['controls'] = controls + f = out['F2']; assert f['formal_columns'] == 2 * m.W.v + len(m.regs) and f['all_targets'] and f['all_source_and_dirty_restored'] + for z in out['integer']: assert z['all_targets'] and z['all_source_and_dirty_restored'] + return out + + +def projection(records, n, v, reverse=False): + """Independent literal F2 replay of the telescope's scalar projection (PR234 scalar_check, constants rebound).""" + def events(): + center = None + for k in (range(len(records) - 6, -1, -6) if reverse else range(0, len(records), 6)): + op, a, b, c, f, z = records[k:k + 6] + if op == 1: + if b == n: assert center is not None; b = center + assert 0 <= a < n and 0 <= b < n and a != b + yield a, b, -c if reverse else c + elif op == (3 if reverse else 2): assert center is None and b == n; center = a + elif op == (2 if reverse else 3): assert center == a and b == n; center = None + assert center is None + cols = [1 << i for i in range(n)]; norms = [1] * n; want = cols[:] + for i in range(v): want[v + i] ^= 1 << i + largest = 1; counts = Counter(); digest = hashlib.sha256(b'['); count = 0 + for a, b, c in events(): + if c & 1: cols[a] ^= cols[b] + norms[a] += abs(c) * norms[b]; largest = max(largest, norms[a]); counts[abs(c)] += 1 + if count: digest.update(b',') + digest.update(json.dumps([a, b, c], separators=(',', ':')).encode()); count += 1 + digest.update(b']') + assert cols == want, 'independent literal all-column endpoint' + return dict(all_formal_columns=n, event_sha256=digest.hexdigest(), weighted_additions=count, + coefficient_counts={str(k): x for k, x in sorted(counts.items())}, + literal_unit_additions=sum(c * x for c, x in counts.items()), max_intermediate_row_l1=largest) + + +def lowering(P234, m, records, tele, raw): + src = (Path(P234) / V8 / 'code/five_stage_bit_global_lowering_20261009.py').read_text() + R = raw['physical_R']; five = raw['five_stage_profile'] + def rep(a, b): + nonlocal src; assert src.count(a) == 1, a; src = src.replace(a, b) + rep("V, R, H, M = 1760, 16643, 24, 120", f"V, R, H, M = 1760, {R}, 24, 120") + rep("assert not copy_open and adds==2569626 and copies==erases==24", f"assert not copy_open and adds=={tele['events']} and copies==erases==24") + rep("assert coefficient=={1:785130,2:1783176,3:1320}", "COEFFICIENTS.append(dict(sorted(coefficient.items())))") + rep("physical=lower.ns['result']; raw=json.loads(RAW.read_text())", "physical=lower.ns['result']; raw=portable_raw") + rep("assert paid==expected and sum(paid.values())==495304", f"assert paid==expected and sum(paid.values())=={five['calls']}") + rep("assert sum(r*n for r,n in paid.items())==2837560 and", f"assert sum(r*n for r,n in paid.items())=={five['rank_mass']} and") + mod = types.ModuleType('fs493_lowering'); mod.__file__ = 'five_stage_bit_global_lowering [493 rebinding]' + mod.COEFFICIENTS = []; mod.portable_raw = raw + exec(compile(src, mod.__file__, 'exec'), mod.__dict__) + physical = dict(categories=tele['categories'], paid_histogram=raw['one_stage_helper_histogram_including_copies'], + tagged_scalar_sha256=tele['tagged_sha256']) + ctx = dict(W=m.W, C=m.C, initial_state=tele['initial_state'], ZERO=m.W.register([]), FULL=m.W.w['full_frame'], result=physical) + lower = mod.Lowerer(records, ctx) + res = mod.verify(lower) + res['stage_coefficients'] = mod.COEFFICIENTS[0] + return mod, lower, res + + +def geometry(P234, mod, m): + src = (Path(P234) / V8 / 'code/five_stage_bit_global_lowering_geometry_20261009.py').read_text() + start = src.index("W,C=ctx['W'],ctx['C']"); stop = src.index("assert all(sha(BASE.parent/p)==h") + body = src[start:stop] + ns = dict(ctx=dict(W=m.W, C=m.C, regs=m.regs), L=mod, sp=__import__('sympy'), array=array, lru_cache=__import__('functools').lru_cache) + exec(compile(body, 'five_stage_bit_global_lowering_geometry [493 context]', 'exec'), ns) + return dict(checked_actual_ports=ns['checked'], checked_actual_entrances=ns['helpers'], + distinct_entrances_noncommuting=bool(ns['sigma'][0] * ns['sigma'][1] != ns['sigma'][1] * ns['sigma'][0])) + + +def primes(P234, m, used): + pw = load('fs493_prime_validator', Path(P234) / V8 / 'code/prime_witnesses.py') + w, c = m.W, m.C + allused = set(used) | set(w.opframe) | set(w.w['source_frame']) | set(w.w['root_frame']) | {w.w['full_frame'], w.register([])} + allused.update(g['frame'] for g in w.gauge.values()) + for e in w.k['entries']: allused.update((e['mix_frame'], e['deliver_frame'])) + for t in range(w.v): allused.add(w.register(w.module.kernel([c.cov[t]], w.h)[0])) + groups = {} + for f in sorted(allused): groups.setdefault(sha(json.dumps(c.B[f], separators=(',', ':')).encode()), f) + factors = set(); largest = 0 + for h_, f in sorted(groups.items()): + B = c.B[f] + if not B: continue + s = list(map(sum, B)) + gram = [[9 * sum(a * b for a, b in zip(x, y)) - s[i] * s[k] for k, y in enumerate(B)] for i, x in enumerate(B)] + det = pw.det(gram); assert det != 0 + powers, residual = pw.factor_witness(det) # asserts residual < 2^80 and the factor identity + factors.update(int(p) for p, e in powers.items() if e); largest = max(largest, abs(det).bit_length()) + return dict(unique_bases=len(groups), current_frame_ids=len(allused), prime_factors=sorted(factors), + maximum_determinant_bits=largest, all_remaining_factors_below_2_power_80=True, + basis_inventory_sha256=sha(json.dumps(sorted(groups), separators=(',', ':')).encode())) + + +def finite(raw, fwd, inv): + """PR234's finite BIT bill, recomputed from fresh values (formulas unchanged).""" + m = 120; v = raw['v']; R = raw['physical_R']; W = 4 * v + R; d = m * m + H = {int(k): n for k, n in raw['five_stage_profile']['histogram'].items()}; E = sum(H.values()) + J = 20 * v + 10 * R + 4 * v; good = 8 * m * m + 8; high = 16 * (d + 1) ** 2; N = 2 * m + unit = 5 * fwd['literal_unit_additions'] + 6 * v + payload = 64 * fwd['max_intermediate_row_l1'] ** 3 * inv['max_intermediate_row_l1'] ** 2 + payload_bits = payload.bit_length(); assert payload_bits <= 128 + fallback = 6 * N * (N - 1) + 3 * N + 6 * (N - 1); assert fallback < 32 * m * m + coefficient = unit + J * high + J * (W + 24) + E * good + E * (128 * N ** 3) + 16 * m ** 3 + 120 + E + 1 + assert coefficient < 2 ** 80 + return dict(m=m, W=W, positive_rank_children=E, unit_expanded_additions=unit, route_and_final_exchange_families=J, + payload_prefix_upper=payload, payload_prefix_bits=payload_bits, q_power_coefficient=coefficient, fallback_children=32 * m * m, + scope='PR234 finite_check formulas with fresh 493-helper values; same retained primitive/tape hypotheses.') + + +def build(P210, P234, progress=lambda s: None): + with tempfile.TemporaryDirectory(prefix='fs493-') as tmp: + tree = assemble_tree(P210, P234, tmp); progress('tree assembled') + m = prepare(tree); progress('PR210 493 helper prepared') + scalar = scalar_proofs(m); progress('F2, majorant, both integer signs and 17 controls passed') + records = array('i') + tele = telescope493.run(m, records, CATEGORIES); progress('physical telescope passed') + v = m.W.v; h = m.W.h; R = len(m.regs); n = 2 * v + R + fwd = projection(records, n, v); inv = projection(records, n, v, True) + assert fwd['event_sha256'] == tele['scalar_sha256'] and fwd['weighted_additions'] == tele['events'] + progress('independent projection and inverse passed') + H = tele['hist'] + ent = Counter(g['dim'] for s, g in m.W.gauge.items() if s not in m.W.donor and s not in m.borrow) + assert dict(ent) == {20: 2200, 18: 13, 12: 18, 13: 48} + assert sum(k * x for k, x in H.items()) == h * R + 2 * v * (h - 1) + 24 * 22 - sum(a * x for a, x in ent.items()) + five = Counter({k: 5 * x for k, x in H.items()}); five.update({k: 2 * v for k in (2 * h - 2, h - 1, 2 * h + 2, 4)}) + for a, x in ent.items(): five[5 * a] += x + Wl = 4 * v + R; mass = sum(k * x for k, x in five.items()) + raw = dict(source_head='13311491eb74a3a9a443ba4e318c68c263f064f0', h=h, v=v, physical_R=R, + source_aliases=len(m.borrow), one_stage_helper_histogram_including_copies={str(k): x for k, x in sorted(H.items())}, + auxiliary_entrance_rank_histogram={str(k): x for k, x in sorted(ent.items())}, + five_stage_profile=dict(m=120, W=Wl, histogram={str(k): x for k, x in sorted(five.items())}, calls=sum(five.values()), + rank_mass=mass, deficit=120 * Wl - mass, maxchild=max(five))) + assert raw['five_stage_profile']['deficit'] == 4 * v - 5 * 24 * 22 == 4400 + mod, lower, glob = lowering(P234, m, records, tele, raw); progress('five-stage global lowering passed') + geo = geometry(P234, mod, m); progress('exact geometry passed') + prime = primes(P234, m, tele['used_frames']); progress('prime determinants passed') + fin = finite(raw, fwd, inv) + summary = dict( + scalar=dict(F2=scalar['F2'], majorant=scalar['majorant'], integer_directions=[z['direction'] for z in scalar['integer']], + controls_rejected=sorted(scalar['controls'])), + telescope=dict(events=tele['events'], categories=dict(sorted(tele['categories'].items())), scalar_sha256=tele['scalar_sha256'], + tagged_sha256=tele['tagged_sha256'], copies=tele['copies'], center_reads=tele['center_reads'], + physical_registers=tele['physical_registers'], local_records=len(records) // 6), + projection=dict(forward=fwd, inverse=inv), + lowering=dict(program_sha256=glob['program_sha256'], paid_calls=glob['paid_calls'], paid_rank_mass=glob['paid_rank_mass'], + deficit=glob['deficit'], opcode_counts={str(k): x for k, x in glob['opcode_counts'].items()}, + stage_coefficients={str(k): x for k, x in glob['stage_coefficients'].items()}, + bank_F2_endpoint_after_terminal_relabel=glob['bank_F2_endpoint_after_terminal_relabel'], + controls_rejected=glob['controls_rejected']), + geometry=dict(ports=[z['port'] for z in geo['checked_actual_ports']], entrances=len(geo['checked_actual_entrances']), + distinct_entrances_noncommuting=geo['distinct_entrances_noncommuting']), + primes=prime, finite=fin) + return raw, summary diff --git a/research/five-stage-banks-493/packing5.py b/research/five-stage-banks-493/packing5.py new file mode 100644 index 0000000000..ef707f380d --- /dev/null +++ b/research/five-stage-banks-493/packing5.py @@ -0,0 +1,212 @@ +"""Exact gauge charts and completed width-120 entrance banks for PR234's five-stage bit helper. + +PR197/PR205's completed-bank construction (Evan McKinney; Rohan Arun) applied to the five-stage cover of +PR234 (hcg890; Jacob Sussman's five-stage layout). Each genuine independent entrance of rank a pays one +bundled exterior child of rank 5a in PR234. Here its five stage residuals I - P_sigma (rank 24 - a each) are +instead routed into completed banks of width m = 120, exactly as PR197 does for the three-stage cover with +width 72. Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. +""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from math import gcd +from pathlib import Path +import gzip, hashlib, json, sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from banks import inverse_integer, color_incidence, check_coloring # PR197 helpers, byte-identical + +H = 24 # local address dimension +STAGES = 5 # PR234 five-stage cover +M = STAGES * H # bank width 120 +COPIES = 12 # data copies; 12 makes the residual volume a whole number of banks +COLORS = STAGES * COPIES +SRC = 'research/five-stage-source-bound-v8/loader/source_inputs' + + +def kernel_basis(A, n): + """Integer basis of {x in Q^n : A x = 0}, by exact RREF.""" + Mx = [[Q(x) for x in row] for row in A]; piv = []; r = 0 + for c in range(n): + p = next((i for i in range(r, len(Mx)) if Mx[i][c]), None) + if p is None: continue + Mx[r], Mx[p] = Mx[p], Mx[r]; inv = 1 / Mx[r][c]; Mx[r] = [x * inv for x in Mx[r]] + for i in range(len(Mx)): + if i != r and Mx[i][c]: f = Mx[i][c]; Mx[i] = [x - f * y for x, y in zip(Mx[i], Mx[r])] + piv.append(c); r += 1 + if r == len(Mx): break + out = [] + for fcol in [c for c in range(n) if c not in piv]: + v = [Q(0)] * n; v[fcol] = Q(1) + for i, pc in enumerate(piv): v[pc] = -Mx[i][fcol] + den = 1 + for x in v: den = den * x.denominator // gcd(den, x.denominator) + iv = [int(x * den) for x in v]; g = 0 + for x in iv: g = gcd(g, abs(x)) + out.append([x // g for x in iv]) + return out + + +def annihilator(B): + """Integer rows spanning the annihilator of row space B (i.e. A with A b = 0 for b in B).""" + return kernel_basis(B, H) + + +def entrance_inventory(P234): + """The genuine independent entrances PR234 bundles into rank-5a exterior children. + + PR200 rank-20 gauges that are not alias recipients, plus PR210's joint shared gauges of ranks 12, 13 + and 18. PR210's three rank-19 joint gauges are source-owned (gaugeb borrowing) and stay unbanked, as in + PR234's own ledger. + """ + src = P234 / SRC + sel = src / 'base_bit/research/paired-cube-diagonal-bit-168/selected/bit' + word = json.loads(gzip.decompress((sel / 'word_p12.json.gz').read_bytes())) + frames = json.loads(gzip.decompress((sel / 'frames_p12.json.gz').read_bytes()))['frames'] + pr210 = src / 'pr210/research/coordinated-crossover-pr200' + pairs = json.loads((pr210 / 'joint/pairs.json').read_text()) + recipients = {b for b, d in pairs} + assert len(recipients) == len(pairs) == 1760 + entries = [] # (role, rank, annihilator rows) + for z in word['gauges']: + if z['role'] in recipients: + assert z['dim'] == 21 + continue + rec = frames[str(z['frame'])] + assert z['dim'] == 20 and rec['dim'] == 20 and len(rec['a']) == 4 + entries.append((z['role'], 20, tuple(map(tuple, rec['a'])))) + owned = {r['role'] for r in json.loads((pr210 / 'gaugeb/selection.json').read_text())} + joint = json.loads((pr210 / 'joint/joint-selection.json').read_text()) + seen_owned = set() + for g in joint: + B = g['gauge_basis']; rank = len(B) + assert len(B) == rank + A = tuple(map(tuple, annihilator(B))) + assert len(A) == H - rank and all(sum(a * b for a, b in zip(x, y)) == 0 for x in A for y in B) + for role in g['roles']: + if role in owned: + assert rank == 19; seen_owned.add(role); continue + entries.append((role, rank, A)) + assert seen_owned == owned and len(owned) == 3 + ranks = Counter(r for _, r, _ in entries) + assert dict(ranks) == {20: 2200, 12: 18, 13: 48, 18: 13}, ranks + assert len({e[0] for e in entries}) == len(entries) == 2279 + return entries + + +def charts(entries): + """Exact charts: G-orthogonal complement 15a - (sum a)1 for G = 9I - J, then a basis of sigma. + + Returns per-frame statistics; every chart's inverse identities and elementary-factor replay are checked. + """ + inventory = Counter(A for _, _, A in entries) + digest = hashlib.sha256(); maxops = maxnum = maxden = 0 + for A, count in sorted(inventory.items()): + source = kernel_basis([list(a) for a in A], H) + assert len(source) == H - len(A) + assert all(sum(x * y for x, y in zip(a, s)) == 0 for a in A for s in source) + residual = [] + for a in A: + row = [15 * x - sum(a) for x in a]; d = gcd(*row); residual.append([x // d for x in row]) + assert all(9 * sum(x * y for x, y in zip(a, b)) - sum(a) * sum(b) == 0 for a in residual for b in source) + B = list(map(list, zip(*(residual + source)))) + C, d, ops = inverse_integer(B) + for left, right in ((B, C), (C, B)): + assert all(sum(x * y for x, y in zip(row, col)) == d * int(i == j) + for i, row in enumerate(left) for j, col in enumerate(zip(*right))) + replay = [list(map(Q, row)) for row in B] + for op, i, j, num, den in ops: + if op == 'swap': replay[i], replay[j] = replay[j], replay[i] + elif op == 'scale': replay[i] = [Q(num, den) * x for x in replay[i]] + else: + assert op == 'add'; replay[i] = [x + Q(num, den) * y for x, y in zip(replay[i], replay[j])] + assert all(x == int(i == j) for i, row in enumerate(replay) for j, x in enumerate(row)) + maxops = max(maxops, len(ops)); maxnum = max(maxnum, max(abs(op[3]) for op in ops)) + maxden = max(maxden, d, max(op[4] for op in ops)) + digest.update(json.dumps([A, count, B, C, d, ops], separators=(',', ':')).encode()) + assert max(maxnum, maxden) < 2 ** 80 + return dict(distinct_charts=len(inventory), chart_sha256=digest.hexdigest(), max_chart_factors=maxops, + max_num=maxnum, max_den=maxden) + + +# Bank patterns of width 120 (residual rank -> multiplicity); every pattern has at most 60 items. +PATTERNS = { + 'r11x8+r4x8': {11: 8, 4: 8}, + 'r12x10': {12: 10}, + 'r6x20': {6: 20}, + 'r4x30': {4: 30}, + 'r24x5': {24: 5}, +} + + +def banks(entries, physical_roles): + """Allocate every residual occurrence (5 stages x 12 copies per physical chain) to a full bank and colour.""" + residual = {role: H - rank for role, rank, _ in entries} + gauge_roles = sorted(residual) + n_full = physical_roles - len(gauge_roles) + assert n_full == physical_roles - 2279 + # chains: gauge chains first, then anonymous full-residual chains (one per remaining physical role) + chain_res = [residual[r] for r in gauge_roles] + [H] * n_full + by_res = defaultdict(list) + for c, res in enumerate(chain_res): by_res[res].append(c) + occ = {res: [c for c in cs for _ in range(COLORS)] for res, cs in by_res.items()} + counts = {res: len(v) for res, v in occ.items()} + plan = Counter() + plan['r11x8+r4x8'] = counts[11] // 8 + plan['r12x10'] = counts[12] // 10 + plan['r6x20'] = counts[6] // 20 + plan['r4x30'] = (counts[4] - 8 * plan['r11x8+r4x8']) // 30 + plan['r24x5'] = counts[24] // 5 + use = Counter() + for name, n in plan.items(): + for res, k in PATTERNS[name].items(): use[res] += n * k + assert dict(use) == counts, (use, counts) + assert all(sum(r * k for r, k in p.items()) == M and sum(p.values()) <= COLORS for p in PATTERNS.values()) + left = []; right = []; offsets = []; cursor = Counter(); bank = 0 + for name in ('r11x8+r4x8', 'r12x10', 'r6x20', 'r4x30', 'r24x5'): + for _ in range(plan[name]): + off = 0 + for res, k in sorted(PATTERNS[name].items(), reverse=True): + for _ in range(k): + c = occ[res][cursor[res]]; cursor[res] += 1 + left.append(c); right.append(bank); offsets.append(off); off += res + assert off == M + bank += 1 + assert all(cursor[r] == counts[r] for r in counts) + nchains = len(chain_res) + labels, stats = color_incidence(left, right, nchains, bank, COLORS) + check_coloring(left, right, labels, nchains, bank, COLORS, full_left=True) + # A deliberately duplicated colour at one chain must be rejected. + first = {}; rejected = False + for e, r in enumerate(left): + if r not in first: first[r] = e; continue + old = labels[e]; labels[e] = labels[first[r]] + try: check_coloring(left, right, labels, nchains, bank, COLORS, full_left=True) + except AssertionError: rejected = True + finally: labels[e] = old + break + assert rejected + inc = hashlib.sha256() + for r, b, c, o in zip(left, right, labels, offsets): inc.update(f'{r},{b},{c},{o}\n'.encode()) + total_width = sum(r * n for r, n in counts.items()) + assert total_width == M * bank + return dict(copies=COPIES, colors=COLORS, banks=bank, plan=dict(plan), residual_occurrences=counts, + incidences=len(left), incidence_sha256=inc.hexdigest(), color_stats=stats, + conflicting_assignment_rejected=rejected, gauge_chains=len(gauge_roles), full_chains=n_full) + + +def build(P234, physical_roles, v=1760): + entries = entrance_inventory(P234) + chart = charts(entries) + bank = banks(entries, physical_roles) + W = COPIES * (STAGES - 1) * v + bank['banks'] + K = 18 * ((W - 1) + physical_roles * M * (chart['max_chart_factors'] + M - 1)) + return dict(status='PASS exact charts and width-120 bank incidence', entrance_ranks={20: 2200, 12: 18, 13: 48, 18: 13}, + removed_exteriors={100: 2200, 60: 18, 65: 48, 90: 13}, W=W, m=M, **chart, **bank, + conservative_selector_calls=K) + + +if __name__ == '__main__': + import time; t = time.time() + r = build(Path(sys.argv[1]), int(sys.argv[2])) + print(json.dumps(r, indent=1), time.time() - t) diff --git a/research/five-stage-banks-493/telescope493.py b/research/five-stage-banks-493/telescope493.py new file mode 100644 index 0000000000..2955dafd9e --- /dev/null +++ b/research/five-stage-banks-493/telescope493.py @@ -0,0 +1,100 @@ +"""Physical frame-tag telescope for the PR210 1331149 helper word (targetagg/word.py replay). +Adapted from PR234's five_stage_source471_physical_telescope (hcg890, ChatGPT assistance).""" +from collections import Counter +import hashlib,json,sys +from array import array +def run(m,records=None,category_names=None): + W,C=m.W,m.C;v=W.v;regs=m.regs;n=2*v+len(regs) + ZERO=W.register([]);FULL=W.w['full_frame'] + state={i:W.w['source_frame'][i]for i in range(v)} + state.update({v+t:ZERO for t in range(v)}) + state.update({2*v+j:W.gauge[r]['frame']if r in W.gauge else ZERO for j,r in enumerate(regs)}) + initial_state=state.copy() + caps={} + for t in range(v): + B,_=W.module.kernel([C.cov[t]],W.h);caps[t]=W.register(B);assert C.dimf[caps[t]]==W.h-1 + used=set(state.values());hist=Counter();cats=Counter();centers=[];sub={} + G=dict(count=0,center=None,moves=0,copies=0) + shs=hashlib.sha256(b'[');ths=hashlib.sha256(b'[') + kind_ids=None if category_names is None else {k:i for i,k in enumerate(category_names)} + def move(i,f): + used.add(f);old=state[i] + if old==f:return + k=old,f + if k not in sub:sub[k]=C.sub(old,f) + assert sub[k],('physical frame descent',i,C.dimf[old],C.dimf[f]) + d=C.dimf[f]-C.dimf[old];assert d>=0 + if records is not None:records.extend((0,i,old,f,d,0)) + if d:hist[d]+=1;G['moves']+=1 + state[i]=f + def dig(h,row,comma): + if comma:h.update(b',') + h.update(json.dumps(row,separators=(',',':')).encode()) + def add(x,c,y,f,kind): + assert isinstance(x,int)and isinstance(y,int)and x!=y + move(x,f);py=y + if kind=='center': + assert G['center'] is not None and G['center']['source']==y and f==ZERO;py=n + else:move(y,f) + if records is not None:records.extend((1,x,py,c,f,kind_ids[kind])) + dig(shs,[x,y,c],G['count']);dig(ths,[x,py,c,f,kind],G['count']);G['count']+=1;cats[kind]+=1 + return x + def center_begin(source,frame): + assert G['center'] is None;move(source,frame);rank=C.dimf[frame];assert rank==22 + G['center']=dict(source=source,frame=frame,rank=rank,first_event=G['count']);hist[rank]+=1;G['copies']+=1 + if records is not None:records.extend((2,source,n,frame,ZERO,rank)) + centers.append(G['center']) + def center_end(): + c=G['center'];assert c is not None + if records is not None:records.extend((3,c['source'],n,c['frame'],ZERO,c['rank'])) + c['after_event']=G['count'];assert c['after_event']>c['first_event'];G['center']=None + text=m.__dict__['__word_text__'] + body=text[text.index('def replay('):] + body=body[:body.index(' if binary:want')] + def rep(old,new,cnt=1): + nonlocal body + assert body.count(old)==cnt,('site',old,body.count(old));body=body.replace(old,new) + rep("unit=(lambda i:1)if major else(lambda i:1< --pr234-root [--full] [--write] + +Always: assemble PR210's package with PR234's pinned PR200 base inputs, prepare the 493-source helper with PR210's +own code, run its F2 / majorant / both defining-integer replays and 17 controls, the physical telescope, an +independent literal projection and inverse, PR234's five-stage global lowering and exact geometry (constants +rebound), all used-basis determinants, the finite bill, 231 charts, 176,915 width-120 banks with a proper +60-colouring, paid moments, three leaf levels and PR234's outer-47 assembly. +--full additionally runs PR234's own fresh verifier (for its complex supplier) and requires its mathematics to +match its pinned expected values. Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from pathlib import Path +import argparse, hashlib, json, subprocess, sys, tempfile, time +if sys.flags.optimize: raise SystemExit('Assertions required') +sys.set_int_max_str_digits(0) +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import helper493, packing5, arithmetic5 + +V8 = 'research/five-stage-source-bound-v8' + + +def serial(x): + if isinstance(x, Q): return str(x) + if isinstance(x, dict): return {str(k): serial(v) for k, v in x.items()} + if isinstance(x, (list, tuple, set)): return [serial(v) for v in x] + return x + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--pr210-root', type=Path, required=True) + ap.add_argument('--pr234-root', type=Path, required=True) + ap.add_argument('--full', action='store_true') + ap.add_argument('--write', action='store_true') + a = ap.parse_args(); assert not a.write or a.full + t0 = time.monotonic(); say = lambda s: print(f'{time.monotonic()-t0:7.1f}s {s}', flush=True) + src = json.loads((HERE / 'SOURCE.json').read_text()) + for key, root in (('pr210', a.pr210_root), ('pr234', a.pr234_root)): + head = subprocess.check_output(['git', '-C', str(root), 'rev-parse', 'HEAD'], text=True).strip() + assert head == src[key]['commit'], ('wrong checkout', key) + for name, digest in src[key]['files'].items(): + assert hashlib.sha256((root / name).read_bytes()).hexdigest() == digest, ('changed input', key, name) + say('source pins passed') + expected = json.loads((a.pr234_root / V8 / 'expected-math.json').read_text())['mathematics'] + if a.full: + with tempfile.TemporaryDirectory(prefix='pr234-fresh-') as tmp: + subprocess.run([sys.executable, '-B', 'verify.py', '--output', str(Path(tmp) / 'run')], cwd=a.pr234_root / V8, check=True) + fresh = json.loads((Path(tmp) / 'run/certificate.json').read_text()) + for key in ('complex_profile', 'complex_moment_interval', 'assembly'): + assert fresh[key] == expected[key], ('PR234 fresh mathematics differ', key) + say('PR234 fresh verifier passed') + raw, checks = helper493.build(a.pr210_root, a.pr234_root, say) + R = raw['physical_R'] + physical = packing5.build(a.pr234_root, R); say('charts, banks and colouring passed') + math234 = dict(expected); math234['bit_profile'] = raw['five_stage_profile'] + result = arithmetic5.build(a.pr234_root, math234, physical); say('moments, bootstrap and outer-47 assembly passed') + record = serial(dict(pr210_commit=src['pr210']['commit'], pr234_commit=src['pr234']['commit'], pr234_fresh_run=a.full, + helper=raw, checks=checks, physical=physical, arithmetic=result)) + path = HERE / 'certificate.json' + if a.write: path.write_text(json.dumps(record, indent=2, sort_keys=True) + '\n') + else: + old = json.loads(path.read_text()); old['pr234_fresh_run'] = a.full + assert record == old, 'certificate differs' + print('PASS 493-source helper (all columns, telescope, five-stage lowering, geometry, primes, finite bill), banks, 47 constraints') + print('conditional kappa = ' + record['arithmetic']['kappa']) + + +if __name__ == '__main__': main() diff --git a/research/five-stage-banks/NOTICE b/research/five-stage-banks/NOTICE new file mode 100644 index 0000000000..4c6a53ede5 --- /dev/null +++ b/research/five-stage-banks/NOTICE @@ -0,0 +1,13 @@ +Five-stage completed entrance banks. Apache-2.0. +Prepared by Rohan Arun (rohanarun) with Anthropic Claude assistance. + +Reused, with credit: +- hcg890, PR234 at af3fe331ca60c936229e060681ffccbc1c208678 (ChatGPT assistance): the five-stage bit and + complex suppliers, their fresh verifier, exact moment engine, bootstrap and outer-47 assembly code, all + consumed unchanged from the pinned checkout. Jacob Sussman: the five-stage layout and complex baseline. +- Evan McKinney, PR197 (OpenAI Codex assistance): completed-bank packing, exact gauge charts and the bank + colouring helpers; banks.py is a byte-identical extract. +- Rohan Arun, PR205: completed banks on PR200's diagonal bit word. +- eumemic, PR210: the source471 helper, joint shared gauges and source borrowing consumed by PR234. +- Chafik Boukhalfa, PR200: the bit word, frames and checkers; Avi Eisenberg, PR193: the complex supplier. +- Every contributor credited by those packages. Original notices remain in the pinned checkouts. diff --git a/research/five-stage-banks/PROOF.md b/research/five-stage-banks/PROOF.md new file mode 100644 index 0000000000..07f178d6c2 --- /dev/null +++ b/research/five-stage-banks/PROOF.md @@ -0,0 +1,52 @@ +# Completed width-120 entrance banks on the five-stage bit supplier + +## 1. Inputs + +PR234 at `af3fe331ca60c936229e060681ffccbc1c208678` freshly verifies a five-stage bit supplier on PR210's +source471 helper (m = 120, W = 23,683, deficit 4,400) and a five-stage complex supplier (saving +747454944651775/10^18). Its bit histogram contains one bundled exterior child of rank 5a for each of the 2,279 +genuine independent entrances (2,200 PR200 rank-20 gauges that are not alias recipients and 79 PR210 joint +gauges of ranks 12, 13, 18). PR210's three rank-19 source-owned gauges, and PR210's source-owned rank-2/4 +entrances, are not banked. Every other child is retained unchanged. + +## 2. Charts + +For each of the 231 distinct entrance frames σ = ker A ⊂ Q^24 use G = 9I − J. Rows 15a − (Σa)1 span the +G-orthogonal complement of σ; place them before an exact integer basis of σ to form B. The checker verifies +G-orthogonality, both identities B·C = C·B = d·I, and an independent replay of the elementary factors of B⁻¹. +In this chart the residual projector I − P_σ is diag(I_{24−a}, 0). Every chart integer is below 2^80, so the +charts stay invertible at every retained prime q > 2^80. They are address charts and change no scalar word. + +## 3. Banks and scheduling + +Take twelve data copies of the five-stage construction. Each physical chain then has 60 residual occurrences, +one per (stage j, copy b). Entrance chains have residual rank 24 − a ∈ {4, 12, 11, 6}; the other 14,364 +physical chains have residual rank 24. The occurrences are partitioned into 177,179 banks of width exactly +120 (patterns in README). The chain/bank multigraph has degree 60 at every chain and at most 30 at every bank, +so it has a proper 60-edge-colouring; the checker verifies it at both ends and rejects a duplicated colour. +Colour j + 5b denotes stage j of copy b: every phase-major stage invocation receives every physical chain +exactly once and uses no bank twice, and each data copy keeps PR234's stage order. + +## 4. Bank endpoint + +After the charts, the residual projectors of a bank occupy disjoint coordinate intervals and sum to I_120. +For disjoint projectors D_P D_Q = D_(P+Q) = D_Q D_P, so the bank's weighted residual involutions commute and +multiply to the full weighted endpoint on arbitrary bank contents (PR197 §4, unchanged). The bank endpoint +therefore supplies exactly the correction each bundled rank-5a exterior child supplied, and those 2,279 +children are removed. This is the same mechanism as PR197/PR205 at width 72; only the number of stage windows +(five) and the bank width (120 = 5·24) change. + +## 5. Profile and arithmetic + +Over twelve copies: W = 12·(4·1760) + 177,179 = 261,659, rank mass 12·(2,837,560 − 226,200), deficit +52,800 = 12·4,400. PR234's moment engine certifies the paid coarse saving 709084856078931/10^18 with the +inherited 10^-16·32m bad-class envelope; the next grid point fails, and banking strictly improves the paid +moment at PR234's own coarse saving. Three finite ordinary levels from PR234's retained 384599/10^10 and PR234's +unchanged outer-47 assembly (η = 10^-12, β = 10^-9, same finite bridge) give κ = 177145602695277/250000000000000000. +The extra routing calls are bounded by 12,227,329,044 < 2^40 and absorbed by the inherited ordinary toll exactly +as in PR197. + +## 6. Limits + +Conditional on every interface PR234 retains. No unconditional all-size theorem, Lean build or measured multiplier +performance is claimed. diff --git a/research/five-stage-banks/README.md b/research/five-stage-banks/README.md new file mode 100644 index 0000000000..126b72e086 --- /dev/null +++ b/research/five-stage-banks/README.md @@ -0,0 +1,52 @@ +# Completed entrance banks on the five-stage bit supplier + +Under the retained multiplication interfaces, this finite witness certifies + +$$ +T(n)=O\left(n(\log n)^{1-\kappa}\right),\qquad +\kappa=\frac{177145602695277}{250000000000000000}=0.000708582410781108 . +$$ + +That is **+0.694%** over PR234 (`703701743496697/10^18`, the five-stage construction) and +1.99% over PR230. + +| Construction | Bit coarse saving | Conditional κ | +|---|---:|---:| +| PR234: five-stage suppliers, paid rank-5a exteriors | 7.04197e-4 | 0.000703701743496697 | +| **This: same suppliers, entrance residuals in width-120 banks** | **7.09085e-4** | **0.000708582410781108** | + +The bit side still binds. PR234's five-stage complex supplier (`747454944651775/10^18`) has about 5% slack. + +## What is new + +PR234 completes each of its 2,279 genuine independent auxiliary entrances with one bundled exterior child of rank 5a: 2,200 of rank 100 (a = 20), 18 of rank 60, 48 of rank 65 and 13 of rank 90. Its own ledger notes these entrances are "not banked". + +PR197 and PR205 showed, for the three-stage cover, that such an exterior correction can be replaced by completed banks: route every residual `I − P_σ` of an entrance chart into a full-width bank whose disjoint residual involutions multiply to the full weighted endpoint. This package applies that construction to the five-stage cover, at bank width m = 120. + +- **Charts.** 231 distinct entrance frames (220 PR200 rank-20 frames and 11 PR210 joint frames of ranks 12, 13 and 18), each with the G-orthogonal complement `15a − (Σa)1` for `G = 9I − J` followed by an exact kernel basis. Each chart is inverted fraction-free and its elementary factors replayed; at most 221 factors, numerators ≤ 40, denominators ≤ 36. +- **Banks.** Twelve data copies, so every physical chain has 60 residual occurrences (5 stages × 12 copies). Residual ranks are 4, 12, 11, 6 (entrances) and 24 (the 14,364 other physical chains). They fill exactly 177,179 banks of width 120: + - 360 banks of 8×11 + 8×4, + - 108 banks of 10×12, + - 39 banks of 20×6, + - 4,304 banks of 30×4, + - 172,368 banks of 5×24. +- **Colouring.** The chain/bank multigraph (998,580 incidences, degree 60 at every chain, at most 30 at a bank) gets a proper 60-edge-colouring, checked at both ends; colour j + 5b is stage j of copy b. A duplicated colour is rejected. +- **Profile.** Remove exactly the 2,279 exterior children; keep every other child. Over 12 copies, W = 12·4v + 177,179 = 261,659 at m = 120, with deficit 52,800 = 12·4,400 (unchanged per copy) and largest child 50. +- **Arithmetic.** PR234's own interval moment engine (with the inherited 10⁻¹⁶ bad-class envelope) certifies the coarse saving `709084856078931/10^18`; the next 10⁻¹⁸ point fails. Three finite ordinary levels from PR234's retained ordinary saving, and PR234's unchanged outer-47 assembly with its η = 10⁻¹², β = 10⁻⁹ and bridge, give κ. All 47 strict inequalities and 7 margins pass; the adjacent grid point is rejected. +- **Routing.** The conservative additional selector-call bound is 18·((W−1) + R·120·(221+119)) = 12,227,329,044 < 2⁴⁰, absorbed by the inherited ordinary toll as in PR197. + +## Verify + +```sh +git fetch https://github.com/CrocSwap/integer-mult-bounds pull/234/head +git worktree add --detach ../pr234 af3fe331ca60c936229e060681ffccbc1c208678 +python3 -m pip install sympy==1.14.0 +python3 -B research/five-stage-banks/verify.py --pr234-root ../pr234 --full +``` + +`--full` first runs PR234's own fresh verifier (all six mandatory stages, a few minutes) and requires its freshly computed mathematics to match; then it rebuilds the 231 charts, all banks and the colouring, and recomputes the moments and assembly, comparing with `certificate.json`. Without `--full`, PR234's pinned expected mathematics is used. + +## Scope + +A conditional finite construction and composition, not an unconditional multiplication theorem. Every PR234 dependency remains: the five-stage physical/scalar/prime checks, complex scalar theorems, weighted q-local compiler, complete-stream movement, copied-centre and restored-row interfaces, ordinary leaves, prime supply, precision/recovery and the all-size reduction. The bank endpoint argument is PR197's (disjoint residual involutions commute and multiply to the full endpoint, on arbitrary dirty contents), applied at width 120 with one colour per (stage, copy). Source-owned PR210 gauges are not banked, as in PR234. + +Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. diff --git a/research/five-stage-banks/SOURCE.json b/research/five-stage-banks/SOURCE.json new file mode 100644 index 0000000000..5c2880d6b1 --- /dev/null +++ b/research/five-stage-banks/SOURCE.json @@ -0,0 +1,16 @@ +{ + "pr234_commit": "af3fe331ca60c936229e060681ffccbc1c208678", + "pr234_repository": "CrocSwap/integer-mult-bounds (refs/pull/234/head)", + "pr234_files": { + "research/five-stage-source-bound-v8/expected-math.json": "44426de51a4d096e1987f43faf8e754d1b29abc8b8b5c4c9d81b15db4f73b0bc", + "research/five-stage-source-bound-v8/code/five_stage_bit_cost_20261009.py": "9d465c716c6b910ff66e1453e3bf0057608a787b5f5361be93781f42cb3370f7", + "research/five-stage-source-bound-v8/code/paired_cube_assembly.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c", + "research/five-stage-source-bound-v8/verify.py": "827c559d949df4ec462691a42067355ebd6d6baff55c48410d5f36247f0ca9a9", + "research/five-stage-source-bound-v8/MANIFEST.json": "fc691fdf74a7b06c9290d6e91e6d63dc1c7e20c6556519dcf9b7f53fa02350de", + "research/five-stage-source-bound-v8/loader/source_inputs/base_bit/research/paired-cube-diagonal-bit-168/selected/bit/word_p12.json.gz": "1cb7e8ed45cf542e304fddc4b12247dbb248a0dc84dedbd832f336b2d172793a", + "research/five-stage-source-bound-v8/loader/source_inputs/base_bit/research/paired-cube-diagonal-bit-168/selected/bit/frames_p12.json.gz": "ad8e2705652b68476713d7647a8592505e222f2b3ccd1728dedce153aac6d462", + "research/five-stage-source-bound-v8/loader/source_inputs/pr210/research/coordinated-crossover-pr200/joint/pairs.json": "da54b863601b5cbc21d27fc5cd623bf805f974a3e47b81ed29a85aa5bad0fa05", + "research/five-stage-source-bound-v8/loader/source_inputs/pr210/research/coordinated-crossover-pr200/joint/joint-selection.json": "13f6420d6c341c22235c9d136d5f7c32896974bb165a893fecd7e583b790d133", + "research/five-stage-source-bound-v8/loader/source_inputs/pr210/research/coordinated-crossover-pr200/gaugeb/selection.json": "b0f9f0e67f94a3c21069f393ea27f9483d315bff2f53f77270163065a6345d1c" + } +} diff --git a/research/five-stage-banks/arithmetic5.py b/research/five-stage-banks/arithmetic5.py new file mode 100644 index 0000000000..cfdbf5d1a5 --- /dev/null +++ b/research/five-stage-banks/arithmetic5.py @@ -0,0 +1,92 @@ +"""Exact paid moments, three finite ordinary levels and PR234's outer-47 assembly for the banked five-stage bit +supplier. Uses PR234's own pinned moment, bootstrap and assembly code unchanged. +Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from pathlib import Path +import importlib.util + +PKG = 'research/five-stage-source-bound-v8' +PR234_KAPPA = Q(703701743496697, 10 ** 18) +PR230_KAPPA = Q(694787513005285, 10 ** 18) + + +def load(name, path): + s = importlib.util.spec_from_file_location(name, path); m = importlib.util.module_from_spec(s); s.loader.exec_module(m) + return m + + +def build(P234, pr234_math, physical): + """pr234_math: PR234's freshly computed mathematics (bit_profile, complex_profile, assembly parameters).""" + math = load('pr234_moments', P234 / PKG / 'code/five_stage_bit_cost_20261009.py') + outer = load('pr234_outer47', P234 / PKG / 'code/paired_cube_assembly.py') + bp = pr234_math['bit_profile']; cp = pr234_math['complex_profile'] + assert (bp['m'], bp['W'], bp['deficit'], bp['maxchild']) == (120, 23683, 4400, 100) + H = {int(k): n for k, n in bp['histogram'].items()} + removed = {int(k): n for k, n in physical['removed_exteriors'].items()} + for r, n in removed.items(): + assert H[r] >= n; H[r] -= n + c = physical['copies']; m = 120 + H = {r: c * n for r, n in H.items() if n} + W = physical['W']; mass = sum(r * n for r, n in H.items()); deficit = m * W - mass + assert deficit == c * bp['deficit'], 'banking preserves the telescoping deficit' + assert max(H) < m // 2 + # Coarse paid saving on the 10^-18 grid, PR234's interval engine with the inherited bad-class envelope. + root = Q(math.certify(H, m, W, True)['lower']); den = 10 ** 18 + lo = Q(int(root * den), den) + while math.moment(H, m, W, lo, True)[1] >= 1: lo -= Q(1, den) + hi = lo + Q(1, den) + while math.moment(H, m, W, hi, True)[0] <= 1: lo = hi; hi = lo + Q(1, den) + assert math.moment(H, m, W, lo, True)[1] < 1 < math.moment(H, m, W, hi, True)[0] + coarse = lo + unbanked = {int(k): n for k, n in bp['histogram'].items()} + old_coarse = Q(pr234_math['contract']['assembly']['bit_coarse']) if 'contract' in pr234_math else None + if old_coarse is not None: + assert math.moment(H, m, W, old_coarse, True)[1] < math.moment(unbanked, m, bp['W'], old_coarse, True)[0], \ + 'banking strictly improves the paid moment at PR234 coarse saving' + chain = [Q(384599, 10 ** 10)] + for _ in range(3): + a = (1 - coarse) * coarse + coarse * chain[-1] + assert chain[-1] < a < coarse < 1 - a + chain.append(a) + bit = chain[-1] + b = Q(pr234_math['assembly']['parameters']['a_complex']) + cm = math.moment({int(k): n for k, n in cp['histogram'].items()}, 110, cp['W'], b, False) + assert cm[1] < 1 + eta = Q(1, 10 ** 12); beta = Q(1, 10 ** 9) + assert bit < (1 - beta) * b + bridge = dict(proof='PROOF.md', representation='Exact powers with source-bound finite overcharges', + semantic=dict(G=dict(base=2, exponent=30000), E=dict(base=2, exponent=100000), + B_upper=dict(base=2, exponent=100001), C0=dict(base=2, exponent=210000), C1=1, + strict_literal_gap=1, induction_gap_lower=1), + rows=dict(coefficient=20161, degree=10 ** 6, suffix_slope=4 * 10 ** 6, + degree_gap=Q(10 ** 6) - Q(51 * 20161, 25))) + q = bit * (1 - 2 * eta); minimum = (1 - eta) * q / (1 + q); ticks = minimum * den + kappa = Q(ticks.numerator // ticks.denominator, den) + if kappa == minimum: kappa -= Q(1, den) + result = outer.assembly(bit, b, bridge, kappa, eta=eta, beta=beta) + assert len(result['strict_constraints']) == 47 and len(result['margins']) == 7 + assert all(x > 0 for x in result['strict_constraints'].values()) + try: outer.assembly(bit, b, bridge, kappa + Q(1, den), eta=eta, beta=beta) + except AssertionError: pass + else: raise AssertionError('adjacent kappa grid point admitted') + assert kappa > PR234_KAPPA > PR230_KAPPA + controls = [] + try: profile_check({**H, 1: H[1] + 1}, m, W, c * bp['deficit']) + except AssertionError: controls.append('changed rank mass rejected') + else: raise AssertionError('corrupt rank mass accepted') + try: math.moment({**H, m: 1}, m, W, coarse, True) + except AssertionError: controls.append('full-width child rejected') + else: raise AssertionError('full-width child accepted') + return dict(scope='Conditional finite supplier composition; PR234 physical, scalar, prime and analytic dependencies inherited', + bit_profile=dict(m=m, W=W, copies=c, histogram={str(r): n for r, n in sorted(H.items())}, + calls=sum(H.values()), rank_mass=mass, deficit=deficit, maxchild=max(H)), + bit_coarse_saving=coarse, pr234_bit_coarse_saving=old_coarse, ordinary_chain=chain, bit=bit, + complex_saving=b, complex_moment_interval=cm, assembly=result, kappa=kappa, + comparison_pr234_kappa=PR234_KAPPA, relative_gain_over_pr234=kappa / PR234_KAPPA - 1, + comparison_pr230_kappa=PR230_KAPPA, controls=controls) + + +def profile_check(H, m, W, deficit): + assert m * W - sum(r * n for r, n in H.items()) == deficit + return True diff --git a/research/five-stage-banks/banks.py b/research/five-stage-banks/banks.py new file mode 100644 index 0000000000..6505ebd37e --- /dev/null +++ b/research/five-stage-banks/banks.py @@ -0,0 +1,104 @@ +"""PR197 chart inversion and bank colouring helpers (byte-identical extract of packing.py up to build()). + +Apache-2.0. Prepared with substantial OpenAI Codex assistance. +""" +from array import array +from collections import Counter +from fractions import Fraction as Q +from math import gcd +from pathlib import Path +import hashlib,json,sys + +def inverse_integer(a): + """Fraction-free Gauss-Jordan; return integral C,d with a C = d I.""" + n=len(a) + m=[list(row)+[int(i==j) for j in range(n)] for i,row in enumerate(a)] + previous=1 + factors=[] + for k in range(n): + pivot=next((i for i in range(k,n) if m[i][k]),None) + if pivot is None: + raise ValueError('Singular basis') + m[k],m[pivot]=m[pivot],m[k] + if pivot != k:factors.append(('swap',k,pivot,1,1)) + p=m[k][k] + if p != previous: + ratio=Q(previous,p) + factors.append(('scale',k,k,ratio.numerator,ratio.denominator)) + for i in range(n): + if i==k:continue + u=m[i][k] + if u: + ratio=Q(-u,previous) + factors.append(('add',i,k,ratio.numerator,ratio.denominator)) + for j in range(2*n): + if j==k:continue + value=p*m[i][j]-u*m[k][j] + assert value % previous==0 + m[i][j]=value//previous + m[i][k]=0 + previous=p + d=m[0][0] + assert d and all(m[i][j]==d*int(i==j) for i in range(n) for j in range(n)) + c=[row[n:] for row in m] + common=abs(d) + for row in c: + for x in row:common=gcd(common,x) + d//=common + c=[[x//common for x in row] for row in c] + if d<0:d=-d;c=[[-x for x in row] for row in c] + return c,d,factors + +def color_incidence(left,right,nleft,nright,colors): + """Incremental two-color swaps; parallel edges are identified separately.""" + assert len(left)==len(right) + full=(1< multiplicity); every pattern has at most 60 items. +PATTERNS = { + 'r11x8+r4x8': {11: 8, 4: 8}, + 'r12x10': {12: 10}, + 'r6x20': {6: 20}, + 'r4x30': {4: 30}, + 'r24x5': {24: 5}, +} + + +def banks(entries, physical_roles): + """Allocate every residual occurrence (5 stages x 12 copies per physical chain) to a full bank and colour.""" + residual = {role: H - rank for role, rank, _ in entries} + gauge_roles = sorted(residual) + n_full = physical_roles - len(gauge_roles) + assert n_full == 14364 + # chains: gauge chains first, then anonymous full-residual chains (one per remaining physical role) + chain_res = [residual[r] for r in gauge_roles] + [H] * n_full + by_res = defaultdict(list) + for c, res in enumerate(chain_res): by_res[res].append(c) + occ = {res: [c for c in cs for _ in range(COLORS)] for res, cs in by_res.items()} + counts = {res: len(v) for res, v in occ.items()} + plan = Counter() + plan['r11x8+r4x8'] = counts[11] // 8 + plan['r12x10'] = counts[12] // 10 + plan['r6x20'] = counts[6] // 20 + plan['r4x30'] = (counts[4] - 8 * plan['r11x8+r4x8']) // 30 + plan['r24x5'] = counts[24] // 5 + use = Counter() + for name, n in plan.items(): + for res, k in PATTERNS[name].items(): use[res] += n * k + assert dict(use) == counts, (use, counts) + assert all(sum(r * k for r, k in p.items()) == M and sum(p.values()) <= COLORS for p in PATTERNS.values()) + left = []; right = []; offsets = []; cursor = Counter(); bank = 0 + for name in ('r11x8+r4x8', 'r12x10', 'r6x20', 'r4x30', 'r24x5'): + for _ in range(plan[name]): + off = 0 + for res, k in sorted(PATTERNS[name].items(), reverse=True): + for _ in range(k): + c = occ[res][cursor[res]]; cursor[res] += 1 + left.append(c); right.append(bank); offsets.append(off); off += res + assert off == M + bank += 1 + assert all(cursor[r] == counts[r] for r in counts) + nchains = len(chain_res) + labels, stats = color_incidence(left, right, nchains, bank, COLORS) + check_coloring(left, right, labels, nchains, bank, COLORS, full_left=True) + # A deliberately duplicated colour at one chain must be rejected. + first = {}; rejected = False + for e, r in enumerate(left): + if r not in first: first[r] = e; continue + old = labels[e]; labels[e] = labels[first[r]] + try: check_coloring(left, right, labels, nchains, bank, COLORS, full_left=True) + except AssertionError: rejected = True + finally: labels[e] = old + break + assert rejected + inc = hashlib.sha256() + for r, b, c, o in zip(left, right, labels, offsets): inc.update(f'{r},{b},{c},{o}\n'.encode()) + total_width = sum(r * n for r, n in counts.items()) + assert total_width == M * bank + return dict(copies=COPIES, colors=COLORS, banks=bank, plan=dict(plan), residual_occurrences=counts, + incidences=len(left), incidence_sha256=inc.hexdigest(), color_stats=stats, + conflicting_assignment_rejected=rejected, gauge_chains=len(gauge_roles), full_chains=n_full) + + +def build(P234, physical_roles, v=1760): + entries = entrance_inventory(P234) + chart = charts(entries) + bank = banks(entries, physical_roles) + W = COPIES * (STAGES - 1) * v + bank['banks'] + K = 18 * ((W - 1) + physical_roles * M * (chart['max_chart_factors'] + M - 1)) + return dict(status='PASS exact charts and width-120 bank incidence', entrance_ranks={20: 2200, 12: 18, 13: 48, 18: 13}, + removed_exteriors={100: 2200, 60: 18, 65: 48, 90: 13}, W=W, m=M, **chart, **bank, + conservative_selector_calls=K) + + +if __name__ == '__main__': + import time; t = time.time() + r = build(Path(sys.argv[1]), int(sys.argv[2])) + print(json.dumps(r, indent=1), time.time() - t) diff --git a/research/five-stage-banks/verify.py b/research/five-stage-banks/verify.py new file mode 100644 index 0000000000..231b340565 --- /dev/null +++ b/research/five-stage-banks/verify.py @@ -0,0 +1,65 @@ +#!/usr/bin/env python3 +"""Verify completed width-120 entrance banks on PR234's five-stage bit supplier. + +Usage (repository root, assertions enabled): + python3 -B research/five-stage-banks/verify.py --pr234-root [--full] [--write] + +--full first runs PR234's own fresh verifier (all six mandatory stages) into a new temporary directory and +uses its freshly computed mathematics; without it, PR234's pinned expected-math.json is used. +Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from pathlib import Path +import argparse, hashlib, json, subprocess, sys, tempfile +if sys.flags.optimize: raise SystemExit('Assertions required') +sys.set_int_max_str_digits(0) +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import packing5, arithmetic5 + +PKG = 'research/five-stage-source-bound-v8' + + +def serial(x): + if isinstance(x, Q): return str(x) + if isinstance(x, dict): return {str(k): serial(v) for k, v in x.items()} + if isinstance(x, (list, tuple)): return [serial(v) for v in x] + return x + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--pr234-root', type=Path, required=True) + ap.add_argument('--full', action='store_true') + ap.add_argument('--write', action='store_true') + a = ap.parse_args(); assert not a.write or a.full + P = a.pr234_root.resolve(); source = json.loads((HERE / 'SOURCE.json').read_text()) + head = subprocess.check_output(['git', '-C', str(P), 'rev-parse', 'HEAD'], text=True).strip() + assert head == source['pr234_commit'], 'wrong PR234 checkout' + for name, digest in source['pr234_files'].items(): + assert hashlib.sha256((P / name).read_bytes()).hexdigest() == digest, ('changed PR234 input', name) + expected = json.loads((P / PKG / 'expected-math.json').read_text())['mathematics'] + if a.full: + with tempfile.TemporaryDirectory(prefix='pr234-fresh-') as tmp: + out = Path(tmp) / 'run' + subprocess.run([sys.executable, '-B', 'verify.py', '--output', str(out)], cwd=P / PKG, check=True) + fresh = json.loads((out / 'certificate.json').read_text()) + for key in ('bit_profile', 'complex_profile', 'kappa', 'assembly'): + assert fresh[key] == expected[key], ('PR234 fresh mathematics differ', key) + pr234 = fresh + else: + pr234 = expected + R = pr234['bit_profile']['W'] - 4 * 1760 + physical = packing5.build(P, R) + result = arithmetic5.build(P, pr234, physical) + record = serial(dict(pr234_commit=head, pr234_fresh_run=a.full, physical=physical, arithmetic=result)) + path = HERE / 'certificate.json' + if a.write: path.write_text(json.dumps(record, indent=2, sort_keys=True) + '\n') + else: + old = json.loads(path.read_text()); old['pr234_fresh_run'] = a.full + assert record == old, 'certificate differs' + print('PASS 231 exact charts, 177179 width-120 banks with a proper 60-colouring, paid moments, 3 leaf levels, 47 constraints') + print('conditional kappa = ' + record['arithmetic']['kappa']) + + +if __name__ == '__main__': main()