diff --git a/.github/workflows/cascade-frames-bit.yml b/.github/workflows/cascade-frames-bit.yml new file mode 100644 index 0000000000..87b349e674 --- /dev/null +++ b/.github/workflows/cascade-frames-bit.yml @@ -0,0 +1,42 @@ +name: Verify cascade-optimized bit frames +on: + pull_request: + paths: + - 'research/cascade-frames-bit/**' + - 'research/source-assisted-v4/**' + - 'research/source-assisted/**' + - 'scripts/paired_cube_assembly.py' + - '.github/workflows/cascade-frames-bit.yml' + push: + paths: + - 'research/cascade-frames-bit/**' + - '.github/workflows/cascade-frames-bit.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + full: + runs-on: ubuntu-24.04 + timeout-minutes: 45 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + repository: CrocSwap/integer-mult-bounds + ref: a1175449f34d39ff933d9d8ab23ced1f32b290ec + path: .dependencies/pr200 + persist-credentials: false + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + repository: CrocSwap/integer-mult-bounds + ref: 187e1010ac8b259af8e9b5166f68b64bc27b4b47 + path: .dependencies/pr193 + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.13' + - run: python -m pip install -r .dependencies/pr193/research/source-assisted/requirements-round13.txt + - run: python -B research/cascade-frames-bit/verify.py --complex-root .dependencies/pr193 --bit-root .dependencies/pr200 --full + - run: git diff --exit-code diff --git a/.github/workflows/packed-diagonal-bit.yml b/.github/workflows/packed-diagonal-bit.yml new file mode 100644 index 0000000000..b00ddc44b8 --- /dev/null +++ b/.github/workflows/packed-diagonal-bit.yml @@ -0,0 +1,38 @@ +name: Verify packed diagonal bit supplier +on: + pull_request: + paths: + - 'research/packed-diagonal-bit/**' + - 'research/source-assisted-v4/**' + - 'research/source-assisted/**' + - 'scripts/paired_cube_assembly.py' + - '.github/workflows/packed-source-assisted-bit.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + full: + runs-on: ubuntu-24.04 + timeout-minutes: 30 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + repository: CrocSwap/integer-mult-bounds + ref: a1175449f34d39ff933d9d8ab23ced1f32b290ec + path: .dependencies/pr200 + persist-credentials: false + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + repository: CrocSwap/integer-mult-bounds + ref: 187e1010ac8b259af8e9b5166f68b64bc27b4b47 + path: .dependencies/pr193 + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.13' + - run: python -m pip install -r .dependencies/pr193/research/source-assisted/requirements-round13.txt + - run: python -B research/packed-diagonal-bit/verify.py --complex-root .dependencies/pr193 --bit-root .dependencies/pr200 --full + - run: git diff --exit-code diff --git a/research/cascade-frames-bit/NOTICE b/research/cascade-frames-bit/NOTICE new file mode 100644 index 0000000000..bd9cdf7779 --- /dev/null +++ b/research/cascade-frames-bit/NOTICE @@ -0,0 +1,4 @@ + + +Finite stopped-leaf extension (2026-10-10) +This follow-up reuses PR211's cascade-optimized frame supplier (Rohan Arun, with Claude assistance) and adds two exact fixed-depth composition levels following PR185/187/210. The fourth- and fifth-level recurrences, exact certificate update, and independent audit were prepared with OpenAI Codex assistance. No authorship is claimed for PR211's frame layout, PR200's bit word/checkers, PR197's banks, PR193's complex supplier, or their inherited interfaces. diff --git a/research/cascade-frames-bit/PR-STATEMENT.md b/research/cascade-frames-bit/PR-STATEMENT.md new file mode 100644 index 0000000000..349c57ffeb --- /dev/null +++ b/research/cascade-frames-bit/PR-STATEMENT.md @@ -0,0 +1,45 @@ +# Five-level finite bootstrap on the PR211 cascade-frame supplier + +## Result + +Starting from open PR211's exact conditional exponent `683847872495777/10^18`, this follow-up adds two fixed stopped-leaf levels and obtains + +```text +kappa = 683847872497761/10^18 + = 0.000683847872497761. +``` + +The exact gain over PR211 is `1984/10^18`. The fifth level adds the last `10^-18` grid step over the four-level version. The bit supplier still binds. The regenerated certificate stores all 47 exact positive assembly margins, and the independent audit rejects the adjacent final grid point. + +## Mechanism and inherited construction + +The finite supplier and physical frames are PR211's frozen cascade-optimized PR200 bit word: 6,191 changed operation frames, the same terminal-modified word, 1,760 compensated aliases, completed banks, and PR193 complex supplier. We do not overwrite that layout with an older frame candidate. In an explicit comparison, PR211 already uses the same first-frame minimum joins at all 17 pairs found in our prior local search, while its second frames are smaller than that earlier candidate. The stronger cascade schedule is retained intact. + +Let `c` be the newly priced packed bit saving and let `a_0` be the fully paid ordinary saving from the admitted PR200 word. Five fixed recurrences use + +```text +a_j = (1-c)c + c a_(j-1), j=1,2,3,4,5. +``` + +The exact rational verifier checks every recurrence, `a_(j-1) < a_j < c < 1-a_j`, the two-supplier paid moments, and the unchanged 47-constraint assembly with `eta=beta=10^-24` and weakening `10^-30`. The finite depth is five, independent of input size. For the fixed suppliers, the exact assembly ceiling at the unattained limit `a=c` has the same `10^-18` grid floor as the fifth level; since every finite `a_j checkout 187e1010ac8b259af8e9b5166f68b64bc27b4b47 +git -C checkout a1175449f34d39ff933d9d8ab23ced1f32b290ec +python -B research/cascade-frames-bit/verify.py --complex-root --bit-root --full +``` + +The full run takes about 6 minutes on two cores. It re-runs PR193's complex verifier, re-admits every frame through PR200's exact checkers, rebuilds charts and banks, and reproduces `certificate.json` byte for byte. Without `--full`, it re-derives the arithmetic from the stored physical record. + +## Scope + +This is a conditional finite supplier certificate. It inherits, without proving, the same all-size compiler, the completed weighted/restored selector, routing, precision, the fixed analytic tape, and the finite bridge hypotheses as PR193/197/200/205/207. The frame search is a heuristic local optimum with no optimality claim. The search scripts are not needed for verification: only the frozen frame list is a mathematical input. + +## Credits + +- PR200 (Chafik Boukhalfa): word and checkers. +- PR193: complex supplier. +- PR197 (Evan McKinney): bank packing. +- PR185/187: finite composition. +- PR207 (Dugongue): first showed that frame re-optimization pays and how to admit frames through PR200's checkers. + +Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. diff --git a/research/cascade-frames-bit/SOURCE.json b/research/cascade-frames-bit/SOURCE.json new file mode 100644 index 0000000000..a0c824a744 --- /dev/null +++ b/research/cascade-frames-bit/SOURCE.json @@ -0,0 +1,24 @@ +{ + "bit_commit": "a1175449f34d39ff933d9d8ab23ced1f32b290ec", + "bit_files": { + "research/paired-cube-diagonal-bit-168/arithmetic/interval_moment.py": "9d3d1d28bfb3375958995205179b171fb65c70a3792cf9f7a21ef5ee54f5460b", + "research/paired-cube-diagonal-bit-168/certificate.json": "853afa75980e11ce16b333c28311c4f635e84065867c049fda9916c2419091ed", + "research/paired-cube-diagonal-bit-168/selected/bit/frames_p12.json": "aec2f09df5b42165a353a9233d9c8549bf091167915f6b044689c4bfb189d406", + "research/paired-cube-diagonal-bit-168/selected/bit/sinks.json": "c00ff70c564829d4b97740f92796fc6ce14fbcd5ca519663828650552b80249d", + "research/paired-cube-diagonal-bit-168/selected/bit/word_p12.json": "0728ed1c7320430a87709b1034485cbabefec85d532b48897f74136cf3954218" + }, + "bit_manifest_sha256": "015abe3342d08d08a9c4a764f103cafc1be1fe7f23d7a72471bd87412c57c2df", + "comparison": { + "pr197": "Evan McKinney, packing on PR187", + "pr202": "Chafik Boukhalfa, kappa = 6768823/10^10", + "pr204": "maxime-fleury, modelled 6.83061299e-4" + }, + "complex_commit": "187e1010ac8b259af8e9b5166f68b64bc27b4b47", + "complex_files": { + "research/source-assisted-v4/SOURCE.json": "99024e5c8296ad03b6e499c3c4e1e9e879bf6a5954d8558cc39abd557edf79d6", + "research/source-assisted-v4/certificate.json": "d84406d2fcc6990deba2b135509e6d86600e57123d88f9b21f7b7240e1aeb513", + "research/source-assisted/global/FINITE_BRIDGE.txt": "66d8f4ea8752abd89952d6674a636575a0db16e18b1c16e293f48f64242f0c46", + "scripts/paired_cube_assembly.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + }, + "frames_sha256": "56b2ed0f6b867e8cafdc32ac70419cfda36d02838844572098b3fc77f8026e58" +} diff --git a/research/cascade-frames-bit/arithmetic.py b/research/cascade-frames-bit/arithmetic.py new file mode 100644 index 0000000000..f8fd6873df --- /dev/null +++ b/research/cascade-frames-bit/arithmetic.py @@ -0,0 +1,107 @@ +"""Exact paid moments, finite ordinary-leaf composition and the balanced assembly. + +Adapted from PR197's arithmetic.py (Evan McKinney; PR185/187 finite bootstrap, PR193 balanced bridge inherited): +the bit supplier is PR200's terminal-modified diagonal-circuit word instead of PR187's. +Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from pathlib import Path +import importlib.util, json + +BIT_PACKAGE = 'research/paired-cube-diagonal-bit-168' +PR207_KAPPA = Q(1366380910073, 2 * 10 ** 15) # PR207: 302 coordinated frames + completed banks on PR200 +PR205_KAPPA = Q(683061299399923, 10 ** 18) # PR205: completed banks on PR200 +PR211_KAPPA = Q(683847872495777, 10 ** 18) # PR211: cascade-optimized frames with three finite levels + + +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(ROOT, BIT, physical, admitted): + im = load('interval_moment', BIT / BIT_PACKAGE / 'arithmetic/interval_moment.py') + assembly = load('frontier_assembly', ROOT / 'scripts/paired_cube_assembly.py') + p = physical + c191 = json.loads((ROOT / 'research/source-assisted-v4/certificate.json').read_text()) + b200 = admitted + + def profile(m, W, H, delta): + H = {int(r): int(n) for r, n in H.items()} + return dict(m=m, W=W, child_multiplicities=H, N=delta, L=0, total_rank=sum(r * n for r, n in H.items()), maxchild=max(H)) + cp = c191['complex_profile']; cp = profile(cp['m'], cp['W_per_vertex'], cp['child_histogram'], cp['deficit_per_vertex']) + bp = b200['profile'] + unpacked = profile(bp['m'], bp['W_per_vertex'], bp['child_histogram'], bp['deficit_per_vertex']) + assert unpacked['total_rank'] == bp['rank_per_vertex'] and unpacked['maxchild'] == bp['maxchild'] == 60 + packed = profile(72, p['W'], p['child_histogram'], p['deficit']) + + def paid(row, a, bit): + result = im.moment(row, a) + if bit: + l, u = im.log_interval(Q(row['m'])); e, f = im.exp_interval(a * l, a * u) + w = Q(1, 10 ** 16) * Q(32 * row['m'] * sum(row['child_multiplicities'].values()), row['W']) + result.update(lower=result['lower'] + w * e, upper=result['upper'] + w * f) + return result + + def certify(row, bit): + den = 10 ** 18; lo = 0; hi = den // 100 + assert paid(row, Q(lo, den), bit)['upper'] < 1 < paid(row, Q(hi, den), bit)['lower'] + while hi - lo > 1: + mid = (lo + hi) // 2; v = paid(row, Q(mid, den), bit) + if v['upper'] < 1: lo = mid + elif v['lower'] > 1: hi = mid + else: raise AssertionError('Interval inconclusive') + a = Q(lo, den); b = Q(hi, den) + return dict(saving=a, accepted=paid(row, a, bit), next_excluded=paid(row, b, bit)) + + complex_cert = certify(cp, False) + original = certify(unpacked, True); new = certify(packed, True) + assert original['saving'] == Q(b200['coarse']['coarse_saving']) + assert new['saving'] > original['saving'] + assert paid(packed, original['saving'], True)['upper'] < paid(unpacked, original['saving'], True)['lower'] + # Finite-depth ordinary supplier composition, as in PR185/187/197, from PR200's completed ordinary supplier. + old = Q(b200['coarse']['ordinary_saving']); coarse = new['saving']; chain = [old] + for _ in range(5): + a = (1 - coarse) * coarse + coarse * chain[-1] + assert chain[-1] < a < coarse < 1 - a + chain.append(a) + assert 0 < p['conservative_selector_calls'] < 2 ** 40 + # Additional chart/router calls use the inherited completed ordinary selector; their exponent is at most the + # atom exponent coarse, which is below 1 - ordinary. + assert coarse < 1 - chain[-1] + bridge = c191['assembly']['finite_bridge']; bridge['rows']['degree_gap'] = Q(bridge['rows']['degree_gap']) + beta = eta = Q(1, 10 ** 24); weak = Q(1, 10 ** 30); den = 10 ** 18 + + def assemble(bit_saving): + b = complex_cert['saving']; a = min(bit_saving, (1 - beta) * b - weak) + q = a * (1 - 2 * eta); bound = (1 - eta) * q / (1 + q); z = bound * den + k = Q((z.numerator - 1) // z.denominator, den) + out = assembly.assembly(a, b, bridge, k, eta=eta, beta=beta) + assert len(out['strict_constraints']) == 47 and len(out['margins']) == 7 + try: assembly.assembly(a, b, bridge, k + Q(1, den), eta=eta, beta=beta) + except AssertionError: pass + else: raise AssertionError('Next final grid accepted') + constraints = out['strict_constraints'] + out['strict_constraint_count'] = len(constraints) + out['minimum_constraint'] = min(constraints.values()) + return dict(kappa=k, assembly=out, binding='complex' if a == (1 - beta) * b - weak else 'bit') + before = assemble(old); after = assemble(chain[-1]) + del before['assembly'] + assert before['kappa'] < after['kappa'] and after['binding'] == 'bit' + assert after['kappa'] > PR207_KAPPA and after['kappa'] > PR205_KAPPA and after['kappa'] > PR211_KAPPA + controls = [] + bad = dict(packed, total_rank=packed['total_rank'] + 1) + try: paid(bad, coarse, True) + except ValueError: controls.append('changed rank mass') + else: raise AssertionError('Corrupt mass accepted') + + return dict(scope='Conditional composition; physical and finite bridge proof dependencies are separate', + source_commits=dict(complex='187e1010ac8b259af8e9b5166f68b64bc27b4b47', bit='a1175449f34d39ff933d9d8ab23ced1f32b290ec'), + complex_profile=cp, unpacked_profile=unpacked, packed_profile=packed, complex=complex_cert, + bit_before=original, bit_after=new, bit_coarse_relative_gain=new['saving'] / original['saving'] - 1, + stock_relative_reduction=1 - Q(p['W'], 3 * unpacked['W']), ordinary_chain=chain, + extra_selector_calls=p['conservative_selector_calls'], selector_toll_gap=1 - chain[-1] - coarse, + comparison_pr207_kappa=PR207_KAPPA, comparison_pr205_kappa=PR205_KAPPA, comparison_pr211_kappa=PR211_KAPPA, + before_packing=before, after_packing=after, + kappa_gain_from_packing=after['kappa'] - before['kappa'], + relative_gain_over_pr207=after['kappa'] / PR207_KAPPA - 1, controls=controls) diff --git a/research/cascade-frames-bit/audit.py b/research/cascade-frames-bit/audit.py new file mode 100644 index 0000000000..158616089a --- /dev/null +++ b/research/cascade-frames-bit/audit.py @@ -0,0 +1,85 @@ +"""Independent exact moment and finite-leaf audit; no optimizer imports. + +PR197's audit.py (Evan McKinney, Apache-2.0), with the PR200 inventory constants. Adapted by Rohan Arun with +Anthropic Claude assistance.""" +from fractions import Fraction as Q +from functools import lru_cache +from math import factorial +ROUND=2**192 + +def lower(value): + return Q((value * ROUND).numerator // (value * ROUND).denominator, ROUND) + +def upper(value): + x = value * ROUND + return Q(-((-x.numerator) // x.denominator), ROUND) + +@lru_cache(None) +def logarithm(x): + """Independent base-two reduction, 64 atanh terms and geometric remainder.""" + assert x >= 1 + power = 0 + while x >= 2: + x /= 2 + power += 1 + def small(y): + z = (y - 1) / (y + 1) + s = 2 * sum((z**(2*j+1) / (2*j+1) for j in range(64)), Q(0)) + return s, s + 2*z**129 / (129*(1-z*z)) + l, u = small(x) + l2, u2 = small(Q(2)) + return lower(l + power*l2), upper(u + power*u2) + +def exponential(l, u): + assert 0 <= l <= u < Q(1, 4) + def polynomial(x): + return sum((x**j / factorial(j) for j in range(17)), Q(0)) + tail = u**17 / (factorial(17)*(1-u/18)) + return lower(polynomial(l)), upper(polynomial(u) + tail) + + +def moment(row,a,bit): + m,W=row['m'],row['W'];H={int(r):n for r,n in row['child_multiplicities'].items()} + assert sum(r*n for r,n in H.items())==row['total_rank']==m*W-row['N'] + lo=hi=Q(0) + for r,n in H.items(): + l,u=logarithm(Q(m,r));e,f=exponential(a*l,a*u) + lo+=Q(r*n,m*W)*e;hi+=Q(r*n,m*W)*f + if bit: + l,u=logarithm(Q(m));e,f=exponential(a*l,a*u) + weight=Q(32*m*sum(H.values()),10**16*W) + lo+=weight*e;hi+=weight*f + return lo,hi + + +def run(record,original): + original=dict(original,child_multiplicities={int(r):n for r,n in original['child_multiplicities'].items()}) + intervals={} + for name,row,bit in (('complex',record['complex_profile'],False),('bit_before',original,True),('bit_after',record['packed_profile'],True)): + a=Q(record[name]['saving']);lo,hi=moment(row,a,bit);next_lo,next_hi=moment(row,a+Q(1,10**18),bit) + assert hi<1Q(record['comparison_pr207_kappa']) + assert Q(record['after_packing']['kappa'])>Q(record['comparison_pr205_kappa']) + assert Q(record['after_packing']['kappa'])>Q(record['comparison_pr211_kappa']) + constraints=record['after_packing']['assembly']['strict_constraints'] + assert len(constraints)==47 and all(Q(v)>0 for v in constraints.values()) + return dict(status='PASS',moment_intervals=intervals,finite_leaf_levels=5,adjacent_final_grids_checked=2) diff --git a/research/cascade-frames-bit/banks.py b/research/cascade-frames-bit/banks.py new file mode 100644 index 0000000000..6505ebd37e --- /dev/null +++ b/research/cascade-frames-bit/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< 22 for r in H) + W = 2 * profile['v'] * copies + bank; mass = sum(r * n for r, n in H.items()) + assert 72 * W - mass == copies * profile['deficit_per_vertex'] == 5808 + K = 18 * ((W - 1) + len(physical) * 72 * (maxops + 71)) + return dict(status='PASS exact actual-chain chart and incidence checks', source_package=PACKAGE, + word_sha256=word_sha, physical_roles=len(physical), interior_splices=len(recipients), + terminal_sinks=len(sink_roles), gauge_roles=len(selected), distinct_gauges=len(inventory), copies=copies, + banks=bank, patterns=[dict(rank4=6, rank24=2, count=small), dict(rank4=0, rank24=3, count=large)], + incidences=len(left), W=W, m=72, rank_mass=mass, deficit=5808, maxchild=max(H), + child_histogram=dict(sorted(H.items())), chart_sha256=digest.hexdigest(), + incidence_sha256=incidence.hexdigest(), max_chart_factors=maxops, max_num=maxnum, max_den=maxden, + conservative_selector_calls=K, color_stats=stats, conflicting_assignment_rejected=rejected) + + +if __name__ == '__main__': + import time; t = time.time() + r = build(Path(sys.argv[1])) + print(json.dumps({k: v for k, v in r.items() if k != 'child_histogram'}, indent=1), time.time() - t) diff --git a/research/cascade-frames-bit/verify.py b/research/cascade-frames-bit/verify.py new file mode 100644 index 0000000000..b8e9497546 --- /dev/null +++ b/research/cascade-frames-bit/verify.py @@ -0,0 +1,66 @@ +#!/usr/bin/env python3 +"""Verify PR200's bit word with cascade-optimized frames and completed banks, composed with PR193's complex supplier. + +Adapted from this author's PR205 verify.py (itself from PR197's, Evan McKinney, Apache-2.0). +Prepared by Rohan Arun with Anthropic Claude assistance. +""" +from pathlib import Path +from fractions import Fraction as Q +import argparse, hashlib, json, os, subprocess, sys +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 frames, packing, arithmetic, audit, controls + +BIT_PACKAGE = 'research/paired-cube-diagonal-bit-168' + + +def serial(value): + if isinstance(value, Q): return str(value) + if isinstance(value, dict): return {str(k): serial(v) for k, v in value.items()} + if isinstance(value, (list, tuple)): return [serial(v) for v in value] + return value + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--complex-root', type=Path, required=True, help='Checkout of the pinned PR193 commit') + parser.add_argument('--bit-root', type=Path, required=True, help='Checkout of the pinned PR200 commit') + parser.add_argument('--full', action='store_true', help='Run the complex verifier, re-admit all frames and rebuild banks') + parser.add_argument('--write', action='store_true', help='Regenerate certificate; requires --full') + args = parser.parse_args(); assert not args.write or args.full + ROOT = args.complex_root.resolve(); bit = args.bit_root.resolve() + source = json.loads((HERE / 'SOURCE.json').read_text()) + assert subprocess.check_output(['git', '-C', str(ROOT), 'rev-parse', 'HEAD'], text=True).strip() == source['complex_commit'] + for name, expected in source['complex_files'].items(): + assert hashlib.sha256((ROOT / name).read_bytes()).hexdigest() == expected, ('Changed source', name) + inherited = json.loads((ROOT / 'research/source-assisted-v4/SOURCE.json').read_text()) + for name, expected in inherited['files'].items(): + assert hashlib.sha256((ROOT / name).read_bytes()).hexdigest() == expected, ('Changed complex dependency', name) + assert subprocess.check_output(['git', '-C', str(bit), 'rev-parse', 'HEAD'], text=True).strip() == source['bit_commit'] + manifest_path = bit / BIT_PACKAGE / 'SOURCE.json' + assert hashlib.sha256(manifest_path.read_bytes()).hexdigest() == source['bit_manifest_sha256'] + manifest = json.loads(manifest_path.read_text()) + for name, expected in list(manifest['files'].items()) + list(source['bit_files'].items()): + assert hashlib.sha256((bit / name).read_bytes()).hexdigest() == expected, ('Changed bit dependency', name) + assert hashlib.sha256((HERE / 'opframe-bases.json').read_bytes()).hexdigest() == source['frames_sha256'] + if args.full: + subprocess.run([sys.executable, '-B', str(ROOT / 'research/source-assisted-v4/verify.py')], cwd=ROOT, check=True, + env=dict(os.environ, PYTHONDONTWRITEBYTECODE='1')) + admitted = serial(frames.admit(bit)) + physical = packing.build(bit, admitted['profile']) + else: + old = json.loads((HERE / 'certificate.json').read_text()); admitted = old['admitted']; physical = old['physical'] + result = arithmetic.build(ROOT, bit, physical, admitted) + independent = audit.run(result, result['unpacked_profile']) + record = dict(admitted=admitted, physical=physical, arithmetic=result, independent=independent, + bank_controls=controls.run(), pinned_bit_files=len(manifest['files'])) + out = serial(record) + if args.write: (HERE / 'certificate.json').write_text(json.dumps(out, indent=2, sort_keys=True) + '\n') + else: assert out == json.loads((HERE / 'certificate.json').read_text()), 'Certificate differs' + print('PASS PR200 frame/terminal/prime re-admission, exact charts and banks, two moment engines, finite leaf composition, 47 constraints') + print('conditional kappa = ' + out['arithmetic']['after_packing']['kappa']) + + +if __name__ == '__main__': main() diff --git a/research/packed-diagonal-bit/NOTICE b/research/packed-diagonal-bit/NOTICE new file mode 100644 index 0000000000..9edc257237 --- /dev/null +++ b/research/packed-diagonal-bit/NOTICE @@ -0,0 +1,18 @@ +Packed diagonal bit supplier. Apache-2.0. +Prepared by Rohan Arun (rohanarun) with Anthropic Claude assistance. + +Reused, with credit: +- Evan McKinney, PR197 (OpenAI Codex assistance): completed-bank packing, exact + gauge charts, nine-colour bank incidence, routing bound, arithmetic, audit + and endpoint controls. banks.py and controls.py are byte-identical extracts; + packing.py, arithmetic.py, audit.py and verify.py are adaptations to PR200. +- Chafik Boukhalfa, PR200 at a1175449f34d39ff933d9d8ab23ced1f32b290ec (Anthropic + Claude and OpenAI Codex assistance): the fixed-coordinate/face-diagonal bit + word, physical layer, terminal sinks, prime witnesses and package verifier. +- Avi Eisenberg, PR193 at 187e1010ac8b259af8e9b5166f68b64bc27b4b47: the v4 + source-assisted complex supplier and balanced assembly bridge; icekylinx for + the source-assisted method (PR184) and the paired-cube framework (PR144). +- maxime-fleury, PR204: the model of this lever and its predicted value. +- eumemic (PR168 lineage), jamesyc (PR166 terminal lemma), PR185/187 finite + ordinary-leaf composition, and every contributor credited by those packages. +Original notices remain in the pinned checkouts. diff --git a/research/packed-diagonal-bit/PROOF.md b/research/packed-diagonal-bit/PROOF.md new file mode 100644 index 0000000000..f8287b66ba --- /dev/null +++ b/research/packed-diagonal-bit/PROOF.md @@ -0,0 +1,69 @@ +# Completed entrance banks on the PR200 bit word + +This applies PR197's construction (see its PROOF.md, sections 1-7) verbatim. The only change is the source word: PR200's terminal-modified bit word instead of PR187's. This file lists only what changes. Every argument not restated here is PR197's, with the same inherited interfaces. + +## 1. Actual physical chains + +PR200 at `a1175449f34d39ff933d9d8ab23ced1f32b290ec` emits and fully checks its bit word: 18,908 logical auxiliary roles, 1,760 donor/recipient splices and 34 PR166 terminal sinks, hence 17,114 physical chains. Its verifier checks the F2 identity on all formal columns, the integer decoder, the exact frames, the prime witnesses for all 24,401 used frames, and the terminal substitution. + +There are 3,960 logical gauges: + +- 1,760 rank-21 gauges are recipient starts internal to the paid splices; +- 2,200 rank-20 gauges, on 220 distinct frames, start otherwise unpaired chains. + +The packing checker verifies all of the following from the frozen word: + +- no donor is gauged; +- donors and recipients are disjoint; +- every recipient is gauged; +- no sink role is a donor, a recipient or gauged. + +Deleted sink registers have no residual. The 2,200 rank-20 gauges supply rank-4 entrance residuals, and every other physical chain has a rank-24 residual. + +## 2. Charts + +Each distinct rank-20 frame is given by four integer annihilator rows `A` in PR200's frame table. The checker computes an exact integer basis of `ker A` (20 vectors) and the G-orthogonal complement `15a-(sum a)1` (`G=9I-J`). It checks orthogonality and both inverse identities of the 24×24 chart, and replays its fraction-free elementary factors. The largest chart has 171 factors. Numerators are at most 5, denominators at most 18, and every nonzero integer is below 2^80, so the charts remain invertible at every allowed prime `q > 2^80`. + +## 3. Banks and scheduling + +There are three full copies, and each physical chain occurs nine times: + +``` +6·3300 = 9·2200, 2·3300 + 3·42542 = 9·(17114 − 2200). +``` + +The chain/bank multigraph (154,026 incidences, degree 9 at each chain and at most 8 at each bank) receives a proper 9-edge-colouring. An independent check verifies every incidence, and a duplicated colour is rejected. Scheduling, the cover bijection and the endpoint identity are PR197's sections 3 and 4. + +## 4. Profile, routing and moments + +Take three copies of PR200's recounted histogram and remove its 6,600 rank-60 exterior children; everything else is retained. Then: + +- `W = 3·2·1760 + 45,842 = 56,402`; +- deficit `72W − mass = 5,808`; +- maximum child 22. + +The conservative extra selector bound is `18((W−1) + 17114·72·(171+71)) = 5,368,513,266`. It is paid as in PR197 section 5. + +The packed coarse saving is `683528191056257/10^18`; the next grid point fails under two independent rational enclosures. Three finite ordinary-leaf levels start from PR200's completed ordinary supplier `a_0 = 677340914792209011107/10^24` (its certified θ-wrapper) and give `a_3`. All gaps `a_j < c < 1 − a_j` are positive. + +## 5. Assembly + +PR193's complex supplier, `700918443859411/10^18`, does not bind. With `eta = beta = 10^-24`, the unchanged 47-constraint balanced assembly certifies + +``` +kappa = 683061299399923/10^18. +``` + +The next `10^-18` point fails for these fixed suppliers and parameters. + +## 6. Limits + +The finite checks establish the charts, banks, profile, moments, leaf recurrence and assembly arithmetic. As in PR197, the following remain inherited assumptions: + +- the completed-core contract; +- the general Clifford interface; +- uniform weighted compilation; +- restored rows; +- fixed-tape transfer. + +PR193's disclosed limitations on the complex side are also retained. diff --git a/research/packed-diagonal-bit/README.md b/research/packed-diagonal-bit/README.md new file mode 100644 index 0000000000..d413e7d373 --- /dev/null +++ b/research/packed-diagonal-bit/README.md @@ -0,0 +1,79 @@ +# Completed banks on PR200's diagonal bit word + +Under the retained multiplication interfaces, this finite witness certifies + +$$ +T(n)=O\left(n(\log n)^{1-\kappa}\right),\qquad +\kappa=\frac{683061299399923}{10^{18}}=0.000683061299399923 . +$$ + +That is **+0.913%** over PR202 (`6768823/10^10`) and above PR199's priced composition of the same two suppliers (`1693287/2500000000`). It is the construction PR204 modelled but did not build. This package builds it, and it lands exactly on PR204's predicted value `6.83061299e-4`. + +| Construction | Bit coarse saving | Conditional kappa | +|---|---:|---:| +| PR202 as published | 6.77774e-4 | 0.0006768823 | +| PR200 bit + PR193 complex, unpacked | 6.77774e-4 | 0.000676882434624733 | +| **Same suppliers, PR200 word packed into completed banks** | **6.83528e-4** | **0.000683061299399923** | + +## What is new + +Two existing pieces are combined: + +- Evan McKinney's PR197 packs completed scratch residuals into rank-72 banks, so the rank-60 exterior corrections of the rank-20 entrance gauges disappear. PR197 applied this to PR187's bit word. +- Chafik Boukhalfa's PR200 has the strongest certified bit word: a fixed-coordinate and face-diagonal local circuit with 34 terminal sinks. + +This package carries out PR197's construction on PR200's actual emitted word. + +| PR200 bit word, per copy | Value | +|---|---:| +| Logical auxiliary roles | 18,908 | +| Donor/recipient splices | 1,760 | +| Terminal sinks | 34 | +| Physical chains | 17,114 | +| Unpaired rank-20 entrance gauges | 2,200 (220 distinct frames) | + +**Charts.** Every distinct gauge frame gets an exact chart. The chart is the G-orthogonal complement (`15a-(sum a)1` for `G=9I-J`) followed by an exact integer kernel basis. Each chart is inverted fraction-free, and its elementary factors are replayed. The worst chart has 171 factors, with every numerator at most 5 and every denominator at most 18. + +**Banks.** Across three copies there are: + +- 3,300 banks of six rank-4 and two rank-24 items; +- 42,542 banks of three rank-24 items. + +The 154,026 chain/bank incidences get a proper 9-edge-colouring, so each stage and copy receives every chain exactly once. The colouring is independently rechecked, and a conflicting assignment is rejected. + +**Packed profile.** Three copies of PR200's independently recounted histogram, minus its 6,600 rank-60 children. Total stock is `W = 56,402` (8.9% less), deficit `5,808 = 3·1,936`, largest child 22. + +**Paid moment.** The bit coarse saving rises from `677773948354561/10^18` to `683528191056257/10^18` (+0.849%). The 10^-16 rare-class fallback is included, and the next 10^-18 point is excluded by two independent moment engines. + +**Leaf composition.** Three finite ordinary-leaf levels (PR185/187/197) start from PR200's completed ordinary supplier, `a_0 = 6.77341e-4`, and reach `a_3 = 6.835282e-4`. + +**Assembly.** The PR193 v4 source-assisted complex supplier (`700918443859411/10^18`) has slack. The bit branch binds, and PR193's unchanged balanced 47-constraint assembly certifies κ. The next 10^-18 κ point is rejected. + +Extra address-chart routing costs at most `5,368,513,266` selector calls. These are paid through the inherited ordinary selector inside the strict row/adapter toll, as in PR197. + +## Verify + +```sh +git fetch https://github.com/CrocSwap/integer-mult-bounds a1175449f34d39ff933d9d8ab23ced1f32b290ec +git worktree add --detach ../packed-bit-pr200 a1175449f34d39ff933d9d8ab23ced1f32b290ec +git fetch https://github.com/CrocSwap/integer-mult-bounds 187e1010ac8b259af8e9b5166f68b64bc27b4b47 +git worktree add --detach ../packed-complex-pr193 187e1010ac8b259af8e9b5166f68b64bc27b4b47 +python3 -m pip install -r ../packed-complex-pr193/research/source-assisted/requirements-round13.txt +python3.13 -B research/packed-diagonal-bit/verify.py --complex-root ../packed-complex-pr193 --bit-root ../packed-bit-pr200 --full +``` + +`--full` runs PR193's and PR200's unchanged package verifiers (about 5.5 minutes in all). It then rebuilds every chart and the bank colouring from PR200's frozen word, and recomputes the arithmetic, the independent audit and the bank endpoint controls. Without `--full`, the saved physical receipt is used, and only the pins and the arithmetic run. + +## Scope and credit + +This is a conditional finite construction and composition, not an unconditional multiplication theorem or a speedup claim. The all-size compiler, analytic, precision, restored-row and fixed-tape hypotheses are inherited exactly as in PR197 and PR200. + +No new packing mechanism is claimed. Credit goes to: + +- Evan McKinney (PR197) for the completed-bank packing, its charts, colouring, routing bound and code (reused byte-identically in `banks.py`, and adapted in `packing.py`, `arithmetic.py`, `audit.py` and `verify.py`); +- Chafik Boukhalfa (PR200) for the bit word and its verifier; +- Avi Eisenberg (PR193) for the complex supplier, and icekylinx for the source-assisted method; +- maxime-fleury (PR204) for modelling exactly this lever and pinning the target; +- eumemic and the PR168 lineage, and PR185/187 for the finite leaf composition. + +Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. diff --git a/research/packed-diagonal-bit/SOURCE.json b/research/packed-diagonal-bit/SOURCE.json new file mode 100644 index 0000000000..b5b05c90e7 --- /dev/null +++ b/research/packed-diagonal-bit/SOURCE.json @@ -0,0 +1,23 @@ +{ + "bit_commit": "a1175449f34d39ff933d9d8ab23ced1f32b290ec", + "bit_files": { + "research/paired-cube-diagonal-bit-168/arithmetic/interval_moment.py": "9d3d1d28bfb3375958995205179b171fb65c70a3792cf9f7a21ef5ee54f5460b", + "research/paired-cube-diagonal-bit-168/certificate.json": "853afa75980e11ce16b333c28311c4f635e84065867c049fda9916c2419091ed", + "research/paired-cube-diagonal-bit-168/selected/bit/frames_p12.json": "aec2f09df5b42165a353a9233d9c8549bf091167915f6b044689c4bfb189d406", + "research/paired-cube-diagonal-bit-168/selected/bit/sinks.json": "c00ff70c564829d4b97740f92796fc6ce14fbcd5ca519663828650552b80249d", + "research/paired-cube-diagonal-bit-168/selected/bit/word_p12.json": "0728ed1c7320430a87709b1034485cbabefec85d532b48897f74136cf3954218" + }, + "bit_manifest_sha256": "015abe3342d08d08a9c4a764f103cafc1be1fe7f23d7a72471bd87412c57c2df", + "comparison": { + "pr197": "Evan McKinney, packing on PR187", + "pr202": "Chafik Boukhalfa, kappa = 6768823/10^10", + "pr204": "maxime-fleury, modelled 6.83061299e-4" + }, + "complex_commit": "187e1010ac8b259af8e9b5166f68b64bc27b4b47", + "complex_files": { + "research/source-assisted-v4/SOURCE.json": "99024e5c8296ad03b6e499c3c4e1e9e879bf6a5954d8558cc39abd557edf79d6", + "research/source-assisted-v4/certificate.json": "d84406d2fcc6990deba2b135509e6d86600e57123d88f9b21f7b7240e1aeb513", + "research/source-assisted/global/FINITE_BRIDGE.txt": "66d8f4ea8752abd89952d6674a636575a0db16e18b1c16e293f48f64242f0c46", + "scripts/paired_cube_assembly.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + } +} diff --git a/research/packed-diagonal-bit/arithmetic.py b/research/packed-diagonal-bit/arithmetic.py new file mode 100644 index 0000000000..58dd57d75e --- /dev/null +++ b/research/packed-diagonal-bit/arithmetic.py @@ -0,0 +1,106 @@ +"""Exact paid moments, finite ordinary-leaf composition and the balanced assembly. + +Adapted from PR197's arithmetic.py (Evan McKinney; PR185/187 finite bootstrap, PR193 balanced bridge inherited): +the bit supplier is PR200's terminal-modified diagonal-circuit word instead of PR187's. +Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from pathlib import Path +import importlib.util, json + +BIT_PACKAGE = 'research/paired-cube-diagonal-bit-168' +PR202_KAPPA = Q(6768823, 10 ** 10) # PR202: v4 source-assisted complex + PR200 bit, theta wrapper +PR199_KAPPA = Q(1693287, 2500000000) # PR199: PR200 bit priced with PR193 complex, finite leaf composition + + +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(ROOT, BIT, physical): + im = load('interval_moment', BIT / BIT_PACKAGE / 'arithmetic/interval_moment.py') + assembly = load('frontier_assembly', ROOT / 'scripts/paired_cube_assembly.py') + p = physical + c191 = json.loads((ROOT / 'research/source-assisted-v4/certificate.json').read_text()) + b200 = json.loads((BIT / BIT_PACKAGE / 'certificate.json').read_text())['bit'] + + def profile(m, W, H, delta): + H = {int(r): int(n) for r, n in H.items()} + return dict(m=m, W=W, child_multiplicities=H, N=delta, L=0, total_rank=sum(r * n for r, n in H.items()), maxchild=max(H)) + cp = c191['complex_profile']; cp = profile(cp['m'], cp['W_per_vertex'], cp['child_histogram'], cp['deficit_per_vertex']) + bp = b200['profile'] + unpacked = profile(bp['m'], bp['W_per_vertex'], bp['child_histogram'], bp['deficit_per_vertex']) + assert unpacked['total_rank'] == bp['rank_per_vertex'] and unpacked['maxchild'] == bp['maxchild'] == 60 + packed = profile(72, p['W'], p['child_histogram'], p['deficit']) + + def paid(row, a, bit): + result = im.moment(row, a) + if bit: + l, u = im.log_interval(Q(row['m'])); e, f = im.exp_interval(a * l, a * u) + w = Q(1, 10 ** 16) * Q(32 * row['m'] * sum(row['child_multiplicities'].values()), row['W']) + result.update(lower=result['lower'] + w * e, upper=result['upper'] + w * f) + return result + + def certify(row, bit): + den = 10 ** 18; lo = 0; hi = den // 100 + assert paid(row, Q(lo, den), bit)['upper'] < 1 < paid(row, Q(hi, den), bit)['lower'] + while hi - lo > 1: + mid = (lo + hi) // 2; v = paid(row, Q(mid, den), bit) + if v['upper'] < 1: lo = mid + elif v['lower'] > 1: hi = mid + else: raise AssertionError('Interval inconclusive') + a = Q(lo, den); b = Q(hi, den) + return dict(saving=a, accepted=paid(row, a, bit), next_excluded=paid(row, b, bit)) + + complex_cert = certify(cp, False) + original = certify(unpacked, True); new = certify(packed, True) + assert original['saving'] == Q(b200['coarse']['coarse_saving']) + assert new['saving'] > original['saving'] + assert paid(packed, original['saving'], True)['upper'] < paid(unpacked, original['saving'], True)['lower'] + # Finite-depth ordinary supplier composition, as in PR185/187/197, from PR200's completed ordinary supplier. + old = Q(b200['coarse']['ordinary_saving']); coarse = new['saving']; chain = [old] + for _ in range(3): + a = (1 - coarse) * coarse + coarse * chain[-1] + assert chain[-1] < a < coarse < 1 - a + chain.append(a) + assert 0 < p['conservative_selector_calls'] < 2 ** 40 + # Additional chart/router calls use the inherited completed ordinary selector; their exponent is at most the + # atom exponent coarse, which is below 1 - ordinary. + assert coarse < 1 - chain[-1] + bridge = c191['assembly']['finite_bridge']; bridge['rows']['degree_gap'] = Q(bridge['rows']['degree_gap']) + beta = eta = Q(1, 10 ** 24); weak = Q(1, 10 ** 30); den = 10 ** 18 + + def assemble(bit_saving): + b = complex_cert['saving']; a = min(bit_saving, (1 - beta) * b - weak) + q = a * (1 - 2 * eta); bound = (1 - eta) * q / (1 + q); z = bound * den + k = Q((z.numerator - 1) // z.denominator, den) + out = assembly.assembly(a, b, bridge, k, eta=eta, beta=beta) + assert len(out['strict_constraints']) == 47 and len(out['margins']) == 7 + try: assembly.assembly(a, b, bridge, k + Q(1, den), eta=eta, beta=beta) + except AssertionError: pass + else: raise AssertionError('Next final grid accepted') + constraints = out.pop('strict_constraints') + out['strict_constraint_count'] = len(constraints) + out['minimum_constraint'] = min(constraints.values()) + return dict(kappa=k, assembly=out, binding='complex' if a == (1 - beta) * b - weak else 'bit') + before = assemble(old); after = assemble(chain[-1]) + del before['assembly'] + assert before['kappa'] < after['kappa'] and after['binding'] == 'bit' + assert after['kappa'] > PR202_KAPPA and after['kappa'] > PR199_KAPPA + controls = [] + bad = dict(packed, total_rank=packed['total_rank'] + 1) + try: paid(bad, coarse, True) + except ValueError: controls.append('changed rank mass') + else: raise AssertionError('Corrupt mass accepted') + + return dict(scope='Conditional composition; physical and finite bridge proof dependencies are separate', + source_commits=dict(complex='187e1010ac8b259af8e9b5166f68b64bc27b4b47', bit='a1175449f34d39ff933d9d8ab23ced1f32b290ec'), + complex_profile=cp, unpacked_profile=unpacked, packed_profile=packed, complex=complex_cert, + bit_before=original, bit_after=new, bit_coarse_relative_gain=new['saving'] / original['saving'] - 1, + stock_relative_reduction=1 - Q(p['W'], 3 * unpacked['W']), ordinary_chain=chain, + extra_selector_calls=p['conservative_selector_calls'], selector_toll_gap=1 - chain[-1] - coarse, + comparison_pr202_kappa=PR202_KAPPA, comparison_pr199_kappa=PR199_KAPPA, + before_packing=before, after_packing=after, + kappa_gain_from_packing=after['kappa'] - before['kappa'], + relative_gain_over_pr202=after['kappa'] / PR202_KAPPA - 1, controls=controls) diff --git a/research/packed-diagonal-bit/audit.py b/research/packed-diagonal-bit/audit.py new file mode 100644 index 0000000000..5cd81d208b --- /dev/null +++ b/research/packed-diagonal-bit/audit.py @@ -0,0 +1,82 @@ +"""Independent exact moment and finite-leaf audit; no optimizer imports. + +PR197's audit.py (Evan McKinney, Apache-2.0), with the PR200 inventory constants. Adapted by Rohan Arun with +Anthropic Claude assistance.""" +from fractions import Fraction as Q +from functools import lru_cache +from math import factorial +ROUND=2**192 + +def lower(value): + return Q((value * ROUND).numerator // (value * ROUND).denominator, ROUND) + +def upper(value): + x = value * ROUND + return Q(-((-x.numerator) // x.denominator), ROUND) + +@lru_cache(None) +def logarithm(x): + """Independent base-two reduction, 64 atanh terms and geometric remainder.""" + assert x >= 1 + power = 0 + while x >= 2: + x /= 2 + power += 1 + def small(y): + z = (y - 1) / (y + 1) + s = 2 * sum((z**(2*j+1) / (2*j+1) for j in range(64)), Q(0)) + return s, s + 2*z**129 / (129*(1-z*z)) + l, u = small(x) + l2, u2 = small(Q(2)) + return lower(l + power*l2), upper(u + power*u2) + +def exponential(l, u): + assert 0 <= l <= u < Q(1, 4) + def polynomial(x): + return sum((x**j / factorial(j) for j in range(17)), Q(0)) + tail = u**17 / (factorial(17)*(1-u/18)) + return lower(polynomial(l)), upper(polynomial(u) + tail) + + +def moment(row,a,bit): + m,W=row['m'],row['W'];H={int(r):n for r,n in row['child_multiplicities'].items()} + assert sum(r*n for r,n in H.items())==row['total_rank']==m*W-row['N'] + lo=hi=Q(0) + for r,n in H.items(): + l,u=logarithm(Q(m,r));e,f=exponential(a*l,a*u) + lo+=Q(r*n,m*W)*e;hi+=Q(r*n,m*W)*f + if bit: + l,u=logarithm(Q(m));e,f=exponential(a*l,a*u) + weight=Q(32*m*sum(H.values()),10**16*W) + lo+=weight*e;hi+=weight*f + return lo,hi + + +def run(record,original): + original=dict(original,child_multiplicities={int(r):n for r,n in original['child_multiplicities'].items()}) + intervals={} + for name,row,bit in (('complex',record['complex_profile'],False),('bit_before',original,True),('bit_after',record['packed_profile'],True)): + a=Q(record[name]['saving']);lo,hi=moment(row,a,bit);next_lo,next_hi=moment(row,a+Q(1,10**18),bit) + assert hi<1Q(record['comparison_pr202_kappa']) + assert Q(record['after_packing']['kappa'])>Q(record['comparison_pr199_kappa']) + return dict(status='PASS',moment_intervals=intervals,finite_leaf_levels=3,adjacent_final_grids_checked=2) diff --git a/research/packed-diagonal-bit/banks.py b/research/packed-diagonal-bit/banks.py new file mode 100644 index 0000000000..6505ebd37e --- /dev/null +++ b/research/packed-diagonal-bit/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< 22 for r in H) + W = 2 * profile['v'] * copies + bank; mass = sum(r * n for r, n in H.items()) + assert 72 * W - mass == copies * profile['deficit_per_vertex'] == 5808 + K = 18 * ((W - 1) + len(physical) * 72 * (maxops + 71)) + return dict(status='PASS exact actual-chain chart and incidence checks', source_package=PACKAGE, + word_sha256=word_sha, physical_roles=len(physical), interior_splices=len(recipients), + terminal_sinks=len(sink_roles), gauge_roles=len(selected), distinct_gauges=len(inventory), copies=copies, + banks=bank, patterns=[dict(rank4=6, rank24=2, count=small), dict(rank4=0, rank24=3, count=large)], + incidences=len(left), W=W, m=72, rank_mass=mass, deficit=5808, maxchild=max(H), + child_histogram=dict(sorted(H.items())), chart_sha256=digest.hexdigest(), + incidence_sha256=incidence.hexdigest(), max_chart_factors=maxops, max_num=maxnum, max_den=maxden, + conservative_selector_calls=K, color_stats=stats, conflicting_assignment_rejected=rejected) + + +if __name__ == '__main__': + import time; t = time.time() + r = build(Path(sys.argv[1])) + print(json.dumps({k: v for k, v in r.items() if k != 'child_histogram'}, indent=1), time.time() - t) diff --git a/research/packed-diagonal-bit/verify.py b/research/packed-diagonal-bit/verify.py new file mode 100644 index 0000000000..47f7e6ab8f --- /dev/null +++ b/research/packed-diagonal-bit/verify.py @@ -0,0 +1,73 @@ +#!/usr/bin/env python3 +"""Verify the packed PR200 bit supplier with PR193's complex supplier. + +Adapted from PR197's verify.py (Evan McKinney, Apache-2.0) by Rohan Arun with Anthropic Claude assistance. +""" +from pathlib import Path +from fractions import Fraction as Q +import argparse, hashlib, json, os, subprocess, sys +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 packing, arithmetic, audit, controls + +BIT_PACKAGE = 'research/paired-cube-diagonal-bit-168' + + +def serial(value): + if isinstance(value, Q): return str(value) + if isinstance(value, dict): return {str(k): serial(v) for k, v in value.items()} + if isinstance(value, (list, tuple)): return [serial(v) for v in value] + return value + + +def run(root, script, *args): + subprocess.run([sys.executable, '-B', str(root / script), *args], cwd=root, check=True, + env=dict(os.environ, PYTHONDONTWRITEBYTECODE='1')) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--complex-root', type=Path, required=True, help='Checkout of the pinned PR193 commit') + parser.add_argument('--bit-root', type=Path, required=True, help='Checkout of the pinned PR200 commit') + parser.add_argument('--full', action='store_true', help='Run both inherited verifiers, then rebuild charts and banks') + parser.add_argument('--write', action='store_true', help='Regenerate certificate; requires --full') + args = parser.parse_args(); assert not args.write or args.full + ROOT = args.complex_root.resolve() + source = json.loads((HERE / 'SOURCE.json').read_text()) + head = subprocess.check_output(['git', '-C', str(ROOT), 'rev-parse', 'HEAD'], text=True).strip() + assert head == source['complex_commit'], 'Wrong complex checkout commit' + for name, expected in source['complex_files'].items(): + assert hashlib.sha256((ROOT / name).read_bytes()).hexdigest() == expected, ('Changed source', name) + inherited = json.loads((ROOT / 'research/source-assisted-v4/SOURCE.json').read_text()) + for name, expected in inherited['files'].items(): + assert hashlib.sha256((ROOT / name).read_bytes()).hexdigest() == expected, ('Changed complex dependency', name) + bit = args.bit_root.resolve() + head = subprocess.check_output(['git', '-C', str(bit), 'rev-parse', 'HEAD'], text=True).strip() + assert head == source['bit_commit'], 'Wrong bit checkout commit' + manifest_path = bit / BIT_PACKAGE / 'SOURCE.json' + assert hashlib.sha256(manifest_path.read_bytes()).hexdigest() == source['bit_manifest_sha256'] + manifest = json.loads(manifest_path.read_text()) + for name, expected in manifest['files'].items(): + assert hashlib.sha256((bit / name).read_bytes()).hexdigest() == expected, ('Changed bit dependency', name) + for name, expected in source['bit_files'].items(): + assert hashlib.sha256((bit / name).read_bytes()).hexdigest() == expected, ('Changed bit word', name) + if args.full: + run(ROOT, 'research/source-assisted-v4/verify.py') + run(bit, BIT_PACKAGE + '/verify.py') + physical = packing.build(bit) + else: + physical = json.loads((HERE / 'certificate.json').read_text())['physical'] + result = arithmetic.build(ROOT, bit, physical) + independent = audit.run(result, result['unpacked_profile']) + record = dict(physical=physical, arithmetic=result, independent=independent, + bank_controls=controls.run(), pinned_bit_files=len(manifest['files'])) + out = serial(record) + if args.write: (HERE / 'certificate.json').write_text(json.dumps(out, indent=2, sort_keys=True) + '\n') + else: assert out == json.loads((HERE / 'certificate.json').read_text()), 'Certificate differs' + print('PASS exact charts and banks on PR200, two moment engines, finite leaf composition, 47 constraints and seven margins') + print('conditional kappa = ' + out['arithmetic']['after_packing']['kappa']) + + +if __name__ == '__main__': main()