diff --git a/.github/workflows/e8-direct-source.yml b/.github/workflows/e8-direct-source.yml new file mode 100644 index 0000000000..56ef7d228e --- /dev/null +++ b/.github/workflows/e8-direct-source.yml @@ -0,0 +1,31 @@ +name: E8 direct-source provider +on: + pull_request: + paths: + - 'research/e8-direct-source/**' + - '.github/workflows/e8-direct-source.yml' + push: + paths: + - 'research/e8-direct-source/**' + - '.github/workflows/e8-direct-source.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + verify: + runs-on: ubuntu-24.04 + timeout-minutes: 5 + strategy: + fail-fast: false + matrix: + python: ['3.11', '3.13'] + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: ${{ matrix.python }} + - run: python -B -I research/e8-direct-source/verify.py --check research/e8-direct-source/RESULTS.json + - run: python -B -I research/e8-direct-source/test_verify.py + - run: git diff --exit-code diff --git a/research/e8-direct-source/.gitattributes b/research/e8-direct-source/.gitattributes new file mode 100644 index 0000000000..cbdafe08e6 --- /dev/null +++ b/research/e8-direct-source/.gitattributes @@ -0,0 +1,3 @@ +# Preserve immutable predecessor bytes, including the mixed-line-ending notice. +vendor/* -text +vendor/pr647_NOTICE.md whitespace=blank-at-eol,blank-at-eof,space-before-tab,cr-at-eol diff --git a/research/e8-direct-source/CLAIM.json b/research/e8-direct-source/CLAIM.json new file mode 100644 index 0000000000..f8b0358331 --- /dev/null +++ b/research/e8-direct-source/CLAIM.json @@ -0,0 +1,30 @@ +{ + "seed": 26, + "seed_source": "OS randomness via secrets.randbelow(100)", + "track": "Complex supplier", + "base": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "started_at": "2026-10-13T04:02:24Z", + "claimed_at": "2026-10-13T04:05:12.066614+00:00", + "finish_target": "2026-10-13T04:25:00Z", + "verification_reserved_from": "2026-10-13T04:19:00Z", + "scope": "Depth-one PR647 paid-copy E8 core: remove the 120 root input helpers by feeding sources directly, with arbitrary-dirt forward and inverse-adjoint restoration and complete paid profile.", + "method": "Exact symbolic live-column replay, chronological binary-projector checks, complete invoice and rational moment; no parameter search.", + "deliverable": "One source-bound construction note and runnable certificate; no multiplication kappa or frontier change.", + "source_pr": 647, + "source_head": "956bb581e7f97328e1b53baa5aca3d2490f2f607", + "candidates": [ + "Direct source inputs replace root copies: chosen after favorable complete profile screen", + "Use target registers for root outputs: deferred because center reads require the zero-frame target before cap writes", + "Reduce private old-response tableau scalar work: incorporated only as a necessary consequence of chosen direct-source scope, not a separate project" + ], + "selection": "Seed 26 selects source port 26 for adversarial misroute/drop controls. The object was selected after a favorable full-cost screen; no randomized search.", + "overlap": "504 open PR titles inspected through #684; PR647 body, exact construction and checker inspected. No pinned coordination issue; local claim. #682 audits the unchanged tensor profile and is not this construction.", + "verification_started": "2026-10-13T04:15:32Z", + "result": { + "updated_at": "2026-10-13T04:19:01.775135+00:00", + "status": "Completed finite construction and exact certificate; packaging PR", + "link": "https://github.com/swbiggart/integer-mult-bounds/tree/research/seed26-direct-source-e8/research/e8-direct-source", + "finding": "120 fewer live helpers, 720 fewer global recursive children, 7088 columns verified both directions, Gaussian-RAM saving 1/14100 admitted while predecessor profile fails it. No multiplication kappa.", + "overlap": "512 open PRs through #692; PR647 unchanged; no pinned coordination issue." + } +} diff --git a/research/e8-direct-source/NOTICE.md b/research/e8-direct-source/NOTICE.md new file mode 100644 index 0000000000..a1b4378b96 --- /dev/null +++ b/research/e8-direct-source/NOTICE.md @@ -0,0 +1,27 @@ +# Attribution and license + +Prepared by Scott Woolsey Biggart (@swbiggart) with substantial OpenAI Codex +assistance in construction, proof, code and verification. New material uses +the repository's Apache-2.0 license. No independent human referee or +proof-assistant certification is claimed. + +This is a variant of Artus / @artuskg's PR647 at +956bb581e7f97328e1b53baa5aca3d2490f2f607. Its retained provider proof credits +OpenAI Pro for the construction, Codex for recovery and scrutiny, and a +separate Codex referee for the packaged checker. We credit that work for +the E8 paid-copy architecture, complete arbitrary-dirt compensation, +phase charts, owner routes, private-memory proof and all-size RAM compiler. + +`vendor/pr647_verify.py` and `vendor/pr647_NOTICE.md` preserve the exact source +bytes and full attribution. The new checker imports the former's binary +linear algebra, exact phase checker and rational log upper bound. It does not +claim these functions as new or as independent verification. The new direct +source constructor, symbolic chronology, modular physical interpreter, +changed invoice and moment certificate are this contribution's additions. + +The predecessor credits Jacob Sussman's E8 and phase-frame/cover work; +Chafik Boukhalfa's explicit programs; eumemic's batched recursion; Ryan Shea's +transfer work; and the P390/P401/paired-cube lineage. The complete retained +notice remains authoritative for that ancestry. No novelty claim is made +for eliminating copies in general, E8 geometry, inverse adjoints, or Fourier +transfer. No Fourier-transfer implementation is added here. diff --git a/research/e8-direct-source/PROOF.md b/research/e8-direct-source/PROOF.md new file mode 100644 index 0000000000..02313213e8 --- /dev/null +++ b/research/e8-direct-source/PROOF.md @@ -0,0 +1,198 @@ +# Remove root copies by reading the sources at their actual frames + +This changes only the depth-one paid-copy provider of PR647, pinned at +`956bb581e7f97328e1b53baa5aca3d2490f2f607`. Its root labels, E8 coefficients, +positive Gaussian charts, three-stage cover and RAM model are retained. +This is an alternative supplier improvement, not a multiplication frontier. + +## Construction and the removed expense + +Use the predecessor's 120 ports p_t in F2^9, rank-eight factorization +K+BA=I, source charts P_t=p_t p_t^T, and target caps I-P_t. The real +coefficients A, B and K are rebuilt from the root formulas. The old core +allocated 120 dirty root input helpers, moved them from zero to P_t and +added source x_t. Those helpers supplied all pair and gather reads; each +source separately moved from P_t to FULL after its last use. + +In the new word the source register itself supplies those reads. For each +pair K_ts != 0, while source s is still at P_s: + +1. Move its pair helper from zero to P_s and add source s. +2. Move the pair helper to I-P_t, add K_ts times it to output helper t, + then finish it at FULL. + +K_ts != 0 implies p_t dot p_s=0, so the intermediate move is legal. After +**all** pair reads, grow source s from P_s to FULL and perform its eight +possible A_js gather updates at FULL. No earlier source read remains. +The output helpers stay at their caps; gathers and all consumed helpers +finish at FULL. No source-access oracle or uncharged source descent is used. + +There are 120 output helpers, 6720 pair helpers and eight gathers: +R=6848, down from 6968. Every target is still at zero when the copied centers +are decoded; it then grows to its cap, receives its output helper, and that +helper finishes at FULL. Sources are already FULL at cleanup. + +## Arbitrary dirt and the two orientations + +Disregarding charts, let the complete core act on sources and helpers as + + x -> x, H -> L H + V x. + +Here L is the helper-only word consisting of the 6720 pair-to-output adds. +The other 7456 adds read the actual sources: 6720 pair loads and 736 gathers. +Let J read the outputs plus the B combination of the eight centers. Since +K+BA=I, JV=I. L is an explicit invertible shear word; no inverse oracle is used. + +Before the core, at frame zero, copy the R helpers to an initialized private +tableau, execute L there, and subtract JL H from the targets. Decode B with +120 initialized private intermediates and 456 adds. Clear the tableau and +intermediates. Neither sources nor source copies are read by this macro. + +After the core, copy each of the eight FULL centers to its own private array, +pay its FULL-to-zero child, and apply the B decoder to the zero-frame targets. +Clear the intermediates and center bank. Then perform the cap/output reads. +The net logical target change is J(LH+Vx)-JLH=x. At FULL, execute the entire +core ADD list in reverse order with negated coefficients, including the source +reads. This restores H exactly and leaves x unchanged. Thus + + F: (x,y,H) -> (x,y+x,H). + +For the backward orientation apply inverse adjoint to the **complete live +macros**, preserving chronological order. A scalar `t += c*s` becomes +`s -= c*t`; unitary frame transitions remain unchanged. The old-response +macro becomes H += L^T J^T y, implemented by a private tableau seeded with +J^T y, the reversed transpose helper-only list, and R additions into H. +The center macro computes B^T y at zero, pays eight zero-to-FULL children, +subtracts into the live centers, and clears the private bank. It is not the +transpose of a CLEAR instruction. Cleanup is the transposed original core +list in reverse order. The same endpoint charts give + + B: (x,y,H) -> (x-y,y,H). + +The local charts may all carry a common orthogonal background Q in a cover +invocation. Scalar gates commute with T_Q, private copies retain that background, +and an initialized zero private array may be assigned its chart. Center children +change only the local window. Thus this rewrite preserves the source +background/whole-helper interface as well as the zero-background calculation. + +Sources can be targets of backward ADDs. Each transposed ADD has equal +operand frames, so this does not require a free frame change. All helper +off-diagonal and helper/data residuals vanish. `verify.py` checks these two +identities symbolically on every one of the 7088 independent live columns. +It also checks every chronological move/ADD frame and every endpoint. + +For a transition projector P, the source's pinned exact basis/phase checker +checks a positive C_rank child with two address permutations and its binary +translation, on a determining set for the quadratic phase. Downward transport +includes the additional diag(P) translation. The pinned utilities are reused +and attributed, not described as independently reimplemented. Optimized +Python is rejected because those utilities use assertions. + +## Complete finite price + +| Quantity | PR647 depth one | Direct source | +| --- | ---: | ---: | +| Live helpers R | 6968 | 6848 | +| Live columns W=R+240 | 7208 | 7088 | +| Core ADDs | 14176 | 14176 | +| Helper-only old-response ADDs | 14176 | 6720 | +| Local forward ADDs | 44160 | 36464 | +| Local backward ADDs | 51136 | 43320 | +| Local forward COPYs | 6976 | 6856 | +| Local backward COPYs | 0 | 0 | +| CLEARs per orientation | 7216 | 7096 | +| Private tableau/decoder/center arrays | 7096 | 6976 | +| Local recursive children | 20896 | 20656 | +| Global recursive children | 62928 | 62208 | + +Forward ADDs are 6720+2*14176+2*456+4*120=36464: the helper-only old +response, main and cleanup, both decoders, and their/root-output target reads. +Backward adds R+8 because the inverse adjoints of the forward copies add into +live arrays. COPYs are R+8; CLEARs are R+2*120+8. The private namespaces are +disjoint, initialized, and cleared. A single additional permutation work array +is explicitly owned. Each permutation is a scatter/copy-back/clear, charged +linearly in its array length. Pointwise ADDs pay coefficient multiplication, +addition, source/target reads and target writes; COPY/CLEAR pay their accesses. + +The whole cover uses forward/backward/forward. Per owner it therefore has +116248 ADDs, 13712 COPYs and 21288 CLEARs, plus at most twice the child count +in address permutations, one translation per child, 120 final translations +and 120 signed exchanges. Workspace initialization is bounded by 6977 zero +writes per entry per cover owner (a conservative bound: the bank is cleared +and reused between complete invocations). Address-table construction, role +routing and loop/index work are charged as in the fixed-depth predecessor. +No private buffer is a borrowed zero input. During a center child the other +nonzero center buffers remain in the caller's protected segment, disjoint from +the child's fresh workspace; the tableau and decoder buffers are zero. + +The old local histogram loses 120 rank-one loads and 120 rank-eight moves. +The latter cancellation compares the old input-helper climb plus late source +climb to the new single source climb. Multiplying by three gives + + H = {1:40680, 2:240, 7:20160, 8:1080, 9:48}, + m=27, W=7088, sum s H(s)=191352=27*7088-24. + +The center-copy bill remains 24 rank-nine global children; none is removed. +Both source and target endpoints, all cleanup, and 240 final rank-two children +are included. The positive deficit stays 24. The improvement is a smaller paid +profile and live width, not a larger deficit. + +## Exact moment and full cost recurrence + +At eta=1/14100, exact rational log/exponential bounds give + + 27W - sum_s s H(s) (27/s)^eta > 11/100. + +For the old histogram and W=7208, a rational **lower** bound on its moment +gives negative slack at the same eta. Thus the larger admitted value is a +consequence of this new word, not finer rounding of the old profile's exponent. +The source's earlier explicit certified eta was 1/15000. Eta here is a +Gaussian-RAM provider saving; it is not integer-multiplication kappa. + +The endpoint maps F/B and all data charts are unchanged. Drop precisely the +120 input-helper role types from each owner in the source's three-stage cover; +the remaining helpers use its same block-swap routing. Each still undergoes +one independently restored full-window transform in each of the three blocks. +The source's explicit route identities and signed final exchange therefore +continue to give C_27 on every live input. No helper-sharing hypothesis changes. +This proof reuses the pinned all-owner argument; it does not enumerate O(27,2). + +For completeness the inherited padding/recursion price can be restated with +the new numbers. Set a=27^2+ceil(log2 W)=742, L=2^a, and G=|O(27,2)|. Enumerate +matrix labels directly, with orthogonality tests; no group-ranking oracle is +needed. All L-GW unused matrix/role slots contain actual input and each pays +an ordinary full-window transform. If + + B_s = G H(s) + (L-GW) * 1_(s=27), + +then the normalized moment is strictly below one by more than + + 11 / (100 * 27 * 2^742), + +because G>=1. For input exponent ell=a+27k+b, 0<=b<27, first pay ordinary +butterflies on the a+b role/remainder bits. Dilate the explicit finite word. +For t(ell)=T(ell)/2^ell its complete recursive cost satisfies + + t(ell) <= A + sum_s (B_s/L) t(sk). + +A is a finite architecture constant paying every scalar, copy, clear, adapter, +source access, allocation, address table and routing operation listed above. +All child exponents sk<=ell-a-b ZERO. + bank=[z[r]*pow(full,-1,p)%p for r in data['centers']] + for t in range(120):z[120+t]=(z[120+t]+sum(B[t][j]*bank[j] for j in range(8)))%p + else: + # B^T y at zero, then actual ZERO -> FULL children. + bank=[sum(B[t][j]*z[120+t] for t in range(120))*full%p for j in range(8)] + for j,r in enumerate(data['centers']):z[r]=(z[r]-bank[j])%p + expected=[a*phase(c.I)%p for a in initial] + for t in range(120): + logical_x=initial[t]*pow(phase(data['initial'][t]),-1,p)%p + cap=phase(c.ref.bitadd(c.I,c.ref.outer(data['ports'][t],9))) + if direction=='forward': + expected[t]=logical_x*phase(c.I)%p + expected[120+t]=(initial[120+t]+logical_x)*cap%p + else: + expected[t]=(logical_x-initial[120+t])*phase(c.I)%p + expected[120+t]=initial[120+t]*cap%p + return z==expected + + +class Checks(unittest.TestCase): + @classmethod + def setUpClass(cls):cls.data=c.build() + + def test_physical_character_replay(self): + chars=[0]+[1<. No publication, push or external message is performed by the supplied scripts. diff --git a/research/e8-direct-source/vendor/pr647_verify.py b/research/e8-direct-source/vendor/pr647_verify.py new file mode 100644 index 0000000000..147026e9f9 --- /dev/null +++ b/research/e8-direct-source/vendor/pr647_verify.py @@ -0,0 +1,578 @@ +"""Independent referee checks. Only Python standard library; never imports candidate code. + +All mathematical decisions use integers/Fraction. Decimal is display only. +The tests corroborate the universal arguments in REFEREE-REPORT.md; they +are not a runtime realization of the enormous padded E8 algorithm. +""" +from fractions import Fraction as Q +from functools import lru_cache +from itertools import combinations, product +from collections import Counter +from pathlib import Path +import hashlib, json, math, time +from decimal import Decimal, localcontext + +import argparse,sys +if not __debug__: + raise SystemExit('Refusing optimized Python: exact checks require assertions; no result was written.') +ROOT=Path(__file__).resolve().parent +RESULT={'checker_origin':'Packaged adaptation of the independent Codex adversarial referee checker; mathematical constructors preserved; no contributor imports','checks':{}} + +def record(name, data): + RESULT['checks'][name] = data + print(name + ': PASS', flush=True) + +def trim(a): + a=list(a) + while a and not a[-1]: a.pop() + return a + +def pa(a,b): + r=[Q(0)]*max(len(a),len(b)) + for i,x in enumerate(a): r[i]+=x + for i,x in enumerate(b): r[i]+=x + return trim(r) + +def pm(a,b): + if not a or not b: return [] + r=[Q(0)]*(len(a)+len(b)-1) + for i,x in enumerate(a): + if x: + for j,y in enumerate(b): + if y: r[i+j]+=x*y + return trim(r) + +def pd(a,b): + a=trim(a);b=trim(b); assert b + r=[Q(0)]*max(0,len(a)-len(b)+1) + while len(a)>=len(b): + j=len(a)-len(b); c=a[-1]/b[-1];r[j]=c + for i,x in enumerate(b): a[i+j]-=c*x + a=trim(a) + return trim(r),a + +@lru_cache(None) +def phi(n): + a=[Q(-1)]+[Q(0)]*(n-1)+[Q(1)] + for d in range(1,n): + if n%d==0: + a,rem=pd(a,phi(d)); assert not rem + return tuple(a) + +class Field: + def __init__(self,n): + self.n=n;self.mod=phi(n);self.degree=len(self.mod)-1 + self.zero=self.v(0);self.one=self.v(1);self.z=self.v([0,1]) + def v(self,a): + if isinstance(a,E): assert a.f is self; return a + if isinstance(a,(int,Q)): a=[Q(a)] + return E(self,tuple(pd(list(a),self.mod)[1])) + +class E: + __slots__=('f','a') + def __init__(self,f,a):self.f=f;self.a=a + def __add__(self,b):b=self.f.v(b);return self.f.v(pa(self.a,b.a)) + __radd__=__add__ + def __neg__(self):return self.f.v([-x for x in self.a]) + def __sub__(self,b):return self+-self.f.v(b) + def __rsub__(self,b):return self.f.v(b)+-self + def __mul__(self,b):b=self.f.v(b);return self.f.v(pm(self.a,b.a)) + __rmul__=__mul__ + def inv(self): + assert self.a + r0=list(self.f.mod);r1=list(self.a);s0=[];s1=[Q(1)] + while r1: + q,r=pd(r0,r1);r0,r1=r1,r;s0,s1=s1,pa(s0,[-x for x in pm(q,s1)]) + assert len(r0)==1 and r0[0] + return self.f.v([x/r0[0] for x in s0]) + def __truediv__(self,b):return self*self.f.v(b).inv() + def __rtruediv__(self,b):return self.f.v(b)*self.inv() + def __pow__(self,k): + if k<0:return self.inv()**(-k) + a=self;r=self.f.one + while k: + if k&1:r=r*a + a=a*a;k//=2 + return r + def __eq__(self,b):return self.a==self.f.v(b).a + def conj(self): + return sum((x*self.f.z**(-j) for j,x in enumerate(self.a)),self.f.zero) + +def mm(A,B): + return [[sum((A[i][k]*B[k][j] for k in range(len(B))),0) for j in range(len(B[0]))] for i in range(len(A))] +def mt(A):return list(map(list,zip(*A))) +def eye(n,one=Q(1)):return [[one if i==j else 0*one for j in range(n)] for i in range(n)] +def diag(a):return [[a[i] if i==j else 0*a[i] for j in range(len(a))] for i in range(len(a))] + +def authentication(): + source=json.loads((ROOT/'SOURCE.json').read_text()) + rows=source['included_proof_sources'] + blobs=[] + for row in rows: + data=(ROOT/row['file']).read_bytes() + digest=hashlib.sha256(data).hexdigest() + assert digest==row['sha256'],row['file'] + if 'git_blob' in row: + got=hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() + assert got==row['git_blob'],row['file'] + blobs.append({'file':row['file'],'git_blob':got}) + manifest=ROOT/'SHA256SUMS.json' + if manifest.exists(): + for name,wanted in json.loads(manifest.read_text()).items(): + assert hashlib.sha256((ROOT/name).read_bytes()).hexdigest()==wanted,name + record('source_byte_authentication',{'included_source_blobs':blobs,'verbatim_Pro_provider_proof':True}) + +def shears(): + f=Field(4);i=f.z;a=(1+i)/2;C=[[a,(1-i)/2],[(1-i)/2,a]];S=diag([f.one,i]);H=[[f.one,f.one],[f.one,-f.one]] + assert mm(mm(S,C),S)==[[a*v for v in row] for row in H] + K=mm(mm(mm(mm(H,diag([f.v(2),f.one])),H),diag([f.v(-3),f.one])),H) + assert K==[[f.v(-8),f.v(-10)],[f.zero,f.v(-6)]] + def upper(t): + assert t!=0 + D=diag([4*t/5,f.one]);inv=diag([5/(4*t),f.one]) + return mm(mm(mm(D,diag([f.v(Q(-1,8)),f.v(Q(-1,6))])),K),inv) + count=0 + for d in [1,2,5]: + for r,s in product(range(-4,5),repeat=2): + mu=f.v(Q(r,d))+Q(s,d)*i + t1=1+mu*mu.conj();t2=mu-t1 + assert t1!=0 and t2!=0 + assert mm(upper(t1),upper(t2))==[[f.one,mu],[f.zero,f.one]] + count+=1 + D=diag([f.one,-i]);assert [[a*x for x in row] for row in mm(mm(D,H),D)]==C + assert mm(C,C)==[[f.zero,f.one],[f.one,f.zero]] + record('fixed_six_C_phase_and_zero_shear',{'coefficients':count,'positive_C':True,'WHT_identity':True}) + +def newton_toeplitz(): + widths=[];roots=0;chunks=0 + for r in range(1,13): + f=Field(r) + for exponent in range(1,r+1): + if math.gcd(exponent,r)!=1:continue + u=f.z**exponent;F=[[u**(j*k) for k in range(r)] for j in range(r)] + h=[f.one] + for j in range(1,r):h.append(h[-1]*(1-u**j));assert h[-1]!=0 + N=[[math.prod([u**j-u**s for s in range(k)],start=f.one) if j>=k else f.zero for k in range(r)] for j in range(r)] + T=[[1/h[j-k] if j>=k else f.zero for k in range(r)] for j in range(r)] + right=[(-1)**k*u**(k*(k-1)//2) for k in range(r)] + assert mm(mm(diag(h),T),diag(right))==N + assert mm(mm(N,diag([1/N[j][j] for j in range(r)])),mt(N))==F + coeff=[1/x for x in h];g=[1/coeff[0]] + for j in range(1,r):g.append(-sum((coeff[s]*g[j-s] for s in range(1,j+1)),f.zero)/coeff[0]) + Ti=[[g[j-k] if j>=k else f.zero for k in range(r)] for j in range(r)] + assert mm(T,Ti)==eye(r,f.one) + if r>1: + p=r//2 + E0=[[sum((coeff[j-nu]*g[nu-k] for nu in range(k,p)),f.zero) for k in range(p)] for j in range(p,r)] + for row in range(p+1,r): + for col in range(1,p): + assert E0[row-p][col]-E0[row-p-1][col-1]==-coeff[row-p]*g[p-col] + # All rectangles, not just a single principal chunk. + for lo,hi in combinations(range(r-p+1),2): + for left,rightend in combinations(range(p+1),2): + M=[x[left:rightend] for x in E0[lo:hi]];a=len(M);e=len(M[0]) + disp=[[M[j][k]-(M[j-1][k-1] if j and k else f.zero) for k in range(e)] for j in range(a)] + v=[-coeff[lo+j] for j in range(a)];w=[g[p-left-k] for k in range(e)] + R=[[disp[j][k]-v[j]*w[k] for k in range(e)] for j in range(a)] + assert all(R[j][k]==0 for j in range(1,a) for k in range(1,e)) + terms=[(v,w),([f.one]+[f.zero]*(a-1),R[0]),([R[j][0] if j else f.zero for j in range(a)],[f.one]+[f.zero]*(e-1))] + assert [[sum((sum((vv[j-l]*ww[k-l] for l in range(min(j,k)+1)),f.zero) for vv,ww in terms),f.zero) for k in range(e)] for j in range(a)]==M + chunks+=1 + roots+=1 + widths.append(r) + record('primitive_newton_triangular_inverse_displacement',{'widths':widths,'primitive_roots':roots,'all_rectangles':chunks,'no_cyclic_inverse_substitution':True}) + +def sparse_add(dst,src,c=Q(1)): + for k,v in list(src.items()): + new=dst.get(k,Q(0))+c*v + if new:dst[k]=new + else:dst.pop(k,None) + +def dag_replay(): + cases=0;negative=0 + for g in range(1,18): + e=3;a=4 + edges=[] + for v in range(g): + edges.append([(v%(e+v),Q((-1)**v*(v+1),3)),((2*v+1)%(e+v),Q(v+2,5))]) + outputs=[0,e+g-1,1,e+g//2] + source=[{j:Q(1)} for j in range(e)];target=[{e+j:Q(1)} for j in range(a)];dirty=[{e+a+j:Q(1)} for j in range(g)] + def sweep(z, suppress=False, undo=False): + for v in (reversed(range(g)) if undo else range(g)): + for j,c in (reversed(edges[v]) if undo else edges[v]): + if suppress and j=e:sparse_add(y[v],z[j-e],-1) + sweep(z,suppress=True,undo=True) + assert z==dirty + expect=[dict(d) for d in target] + for j in range(a):sparse_add(expect[j],desired[j]) + assert y==expect + cases+=1 + assert negative>0 + record('dirty_DAG_all_symbolic_columns',{'DAGs':cases,'arbitrary_helpers':True,'direct_source_reads':True,'omitted_compensation_negative_controls':negative}) + +def popcount(x):return bin(x).count('1') +def bitdot(x,y):return popcount(x&y)%2 +def bitmv(A,y):return sum(bitdot(row,y)<>k)&1)<>j)&1) for row in A) +def xor_many(it): + v=0 + for x in it:v^=x + return v +def biteye(n):return tuple(1<>j)&1 else 0 for j in range(n)) +def bdiag(A):return sum(((x>>j)&1)<>j)&1 for b in B) + assert (popcount(col)-total)%2==0 + delta|=(((popcount(col)-total)//2)%2)<0 + record('E8_depth_one_core_dirty_both_orientations',{'ports':v,'nonzero_counts':counts,'helpers':R,'core_ADDs':len(adds),'independent_symbolic_live_columns':R+2*v,'global_histogram':dict(sorted(globalhist.items())),'rank_mass':sum(s*c for s,c in globalhist.items()),'defect':27*7208-sum(s*c for s,c in globalhist.items()),'distinct_phase_projectors':len(unique),'nonzero_phase_translations':with_phase,'private_arrays':R+120+8}) + # Exact owner geometry, including literal nonsymmetric port-basis construction. + m=27;I27=biteye(m);H0=tuple((1<>j)&1) + swap=list(I) + swap[0],swap[zero]=swap[zero],swap[0] + w=p^(1<=1 + shifts=0 + while x>2:x/=2;shifts+=1 + def unit(y): + u=(y-1)/(y+1) + series=sum((2*u**(2*j+1)/Q(2*j+1) for j in range(terms)),Q(0)) + tail=2*u**(2*terms+1)/((2*terms+1)*(1-u*u)) + return series+tail + val=unit(x)+shifts*unit(Q(2)) + # Upward dyadic round is another exact inequality. + d=1<<100;return Q((val.numerator*d+val.denominator-1)//val.denominator,d) + +def moment(hist): + kappa=Q(1,15000);m=27;W=7208 + upper=Q(0) + for s,c in hist.items(): + z=kappa*log_upper(Q(m,s));assert 0<=z<1 + exp=sum((z**j/Q(math.factorial(j)) for j in range(5)),Q(0))+z**5/(120*(1-z/6)) + upper+=s*c*exp + slack=m*W-upper;assert slack>1 + p=1-kappa;a=m*m+(W-1).bit_length();assert a==742 + # Gap normalized by row padding without needing |O(27,2)|. + gap_lower=Q(1,m*(1<=1','all_padding_roles_are_actual_inputs':True}) + +def sector_checks(): + f=Field(4);C=[[(1+f.z)/2,(1-f.z)/2],[(1-f.z)/2,(1+f.z)/2]] + cases=[[[[1,0]]],[[[2,0],[1]],[[1,0]]],[[[3,1],[0],[2]],[[2,0],[1]]],[[[2,0],[3,1]],[[0],[2,1]],[[1,0]]]] + # Exhaust all order/pair-position choices on small two-axis layouts. + for a in range(2,6): + for b in range(2,6): + cases.append([[[a-1,0]]+[[j] for j in range(1,a-1)],[[b-1,0]]+[[j] for j in range(1,b-1)]]) + maxR=0;columns=0 + for blocks in cases: + rad=[sum(map(len,axis)) for axis in blocks];R=math.prod(rad);maxR=max(R,maxR) + tau=[math.prod(rad[j+1:]) for j in range(len(rad))] + mapping={};sectors=[];prefixnodes=sum(math.prod(rad[:j]) for j in range(len(rad)+1));assert prefixnodes<2*R + for selected in product(*blocks): + q=[len(B) for B in selected];S=0;Qprefix=1 + for j,B in enumerate(selected): + previous=sum(len(A) for A in blocks[j][:blocks[j].index(B)]) + S+=Qprefix*previous*tau[j];Qprefix*=len(B) + for t in product(*[range(len(B)) for B in selected]): + Iaddr=0;o=0 + for j,tt in enumerate(t):Iaddr=Iaddr*rad[j]+selected[j][tt];o=o*q[j]+tt + mapping[Iaddr]=S+o + sectors.append((S,Qprefix,q.count(2))) + assert sorted(mapping.values())==list(range(R)) + assert sorted(j for S,w,k in sectors for j in range(S,S+w))==list(range(R)) + inv={v:k for k,v in mapping.items()} + # Exact operator comparison on every independent input column. + for Iaddr in range(R): + digits=[];x=Iaddr + for r in reversed(rad):digits.append(x%r);x//=r + digits=digits[::-1];choices=[] + for j,d in enumerate(digits): + B=next(B for B in blocks[j] if d in B) + choices.append([(out,C[B.index(out)][B.index(d)]) for out in B] if len(B)==2 else [(d,f.one)]) + direct={} + for selected in product(*choices): + out=0;c=f.one + for j,(d,z) in enumerate(selected):out=out*rad[j]+d;c=c*z + direct[out]=c + packed=mapping[Iaddr];S,w,k=next(sec for sec in sectors if sec[0]<=packed=2 and all(p%d for d in range(2,math.isqrt(p)+1)) +def working(N): + primes=[];r=1;p=3 + while True: + if isprime(p): + if r*p>2*N:break + r*=p;primes.append(p) + p+=2 + q=1 + while r*q<2*N:q*=2 + L=r*q;aux=1<<((16*L-1).bit_length());D=2*N*L*aux + return primes,p,q,L,D,aux + +def roots_crt(): + lengths=list(range(1,4097))+[2**j-1 for j in range(13,81)]+[2**j for j in range(13,81)]+[10**j+7 for j in range(4,45)] + exhaustive=0;phasepairs=0;records=[] + for N in lengths: + primes,nextp,q,L,D,aux=working(N) + assert 2*N<=L<4*N and q<2*nextp + assert D<1024*N**3 and D%(2*N)==0 and D%L==0 + factors=primes+([q] if q>1 else []) + for r in factors: + assert D%r==0 + for power in range(0,(8*r).bit_length()): + order=1<=3 and fourier(x,zeta.inv())!=direct:wrong_sign+=1 + checked.append({'N':N,'L':L,'cyclotomic_order':order,'degree':f.degree}) + assert wrong_sign>0 + record('exact_three_transform_chirp',{'cases':checked,'negative_root_convention_detected':wrong_sign,'fixed_kernel_forward_transform_charged':True}) + +def exponent_scope(): + alpha=Q(14999,15000);beta=4-alpha;saving=Q(1,30000) + assert beta==Q(45001,15000) and (1-saving)-alpha==saving + # An explicit absorption range: u=log log N, beta log u <= u/30000. + # For u>=10^7, log u <= sqrt(u), and sqrt(u)>=30000 beta is + # sufficient; choosing u>=10^10 is a conservative exact threshold. + assert 10**10>=(30000*beta)**2 + f=Field(3);assert f.z*f.z+f.z+1==0 + record('exponents_root_scope',{'alpha':str(alpha),'beta':str(beta),'eventual_log_exponent':str(1-saving),'absorption_sufficient':'log log N >= 10^10 (natural logs); no practical crossover claim','root_free_F3_obstruction':'zeta_3 has nonrational imaginary part sqrt(3)/2; Q(i) closed under field operations'}) + +def main(): + ap=argparse.ArgumentParser(description=__doc__) + ap.add_argument('--check',action='store_true',help='compare the deterministic complete receipt with RESULTS.json') + ap.add_argument('--write',type=Path,help='write a fresh receipt; does not alter package sources') + args=ap.parse_args() + if args.check and args.write:ap.error('choose --check or --write') + for func in [authentication,shears,dag_replay,e8_provider,sector_checks,roots_crt,newton_toeplitz,chirp,exponent_scope]:func() + RESULT['status']='ALL_EXACT_CHECKS_PASSED' + canonical=json.dumps(RESULT,indent=2,sort_keys=True)+'\n' + if args.write: + args.write.write_text(canonical) + else: + expected=json.loads((ROOT/'RESULTS.json').read_text()) + assert json.loads(canonical)==expected,'complete deterministic receipt changed' + print('ALL_EXACT_CHECKS_PASSED',flush=True) + +if __name__=='__main__':main() diff --git a/research/e8-direct-source/verify.py b/research/e8-direct-source/verify.py new file mode 100644 index 0000000000..3756a99c6c --- /dev/null +++ b/research/e8-direct-source/verify.py @@ -0,0 +1,313 @@ +#!/usr/bin/env python3 +"""Depth-one E8 direct-source construction and complete finite checks.""" +import argparse +from collections import Counter +from fractions import Fraction as Q +import hashlib +import importlib.util +from itertools import combinations +import json +import math +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +if not __debug__: + raise SystemExit('Refusing optimized Python: pinned phase utilities require assertions.') + + +def require(ok, why): + if not ok: + raise ValueError(why) + + +def load_reference(): + source = json.loads((HERE/'SOURCE.json').read_text()) + for record in source['files'].values(): + if 'vendored_path' in record: + data = (HERE/record['vendored_path']).read_bytes() + require(hashlib.sha256(data).hexdigest()==record['sha256'],'source SHA256') + require(hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() + == record['git_blob'],'source Git blob') + spec = importlib.util.spec_from_file_location('pr647',HERE/'vendor/pr647_verify.py') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +ref = load_reference() +I, ZERO = ref.biteye(9), (0,)*9 + + +def plus(target,source,c=Q(1)): + for col,value in source.items(): + updated = target.get(col,Q(0))+c*value + if updated: + target[col] = updated + else: + target.pop(col,None) + + +def geometry(): + ports, roots = [],[] + for triple in combinations(range(9),3): + ports.append(sum(1<=240: + helper_adds.append((t,s,c)) + outputs = [alloc() for _ in ports] + for t,r in enumerate(outputs): + move(r,ref.bitadd(I,ref.outer(ports[t],9))) + for t in range(120): + for s in range(120): + if K[t][s]: + z=alloc();move(z,ref.outer(ports[s],9)) + add(z,s,Q(1)) + move(z,ref.bitadd(I,ref.outer(ports[t],9))) + add(outputs[t],z,K[t][s]);move(z,I) + centers=[alloc() for _ in range(8)] + for z in centers:move(z,I) + for s in range(120): + move(s,I) + for j in range(8): + if A[j][s]:add(centers[j],s,A[j][s]) + require(len(allocations)==6848 and len(adds)==14176 and len(helper_adds)==6720, + 'literal core counts') + return {'ports':ports,'A':A,'B':B,'outputs':outputs,'centers':centers, + 'core':events,'adds':adds,'helper_adds':helper_adds, + 'initial':initial,'core_final':frames,'helpers':allocations} + + +def word(data,direction): + # Macros have explicit frame, scratch and primitive invoices below/in PROOF.md. + events=[('old',direction)]+list(data['core'])+[('centers',direction)] + for t,r in enumerate(data['outputs']): + events += [('move',120+t,ref.bitadd(I,ref.outer(data['ports'][t],9))), + ('output',120+t,r,Q(1)),('move',r,I)] + for t,s,c in reversed(data['adds']): + events.append(('cleanup',t,s,-c)) + return events + + +def check_frames(data,events,direction): + frames=list(data['initial']);hist=Counter();projectors=set();count=Counter() + for event in events: + kind=event[0] + if kind=='move': + _,r,P=event;old=frames[r] + require(ref.bitmm(old,P)==old and ref.bitmm(P,old)==old,'chronological nesting') + diff=ref.bitadd(old,P);rank=len(ref.indep(ref.bitmt(diff))) + if rank:hist[rank]+=1;projectors.add(diff) + frames[r]=P + elif kind in ('add','output','cleanup'): + _,t,s,c=event + require(frames[t]==frames[s],f'{kind}: unequal frames at {t},{s}') + count[kind]+=1 + elif kind=='old': + require(all(frames[r]==ZERO for r in data['helpers']),'old helper frame') + require(all(frames[120+t]==ZERO for t in range(120)),'old target frame') + count['old']+=1 + elif kind=='centers': + require(event[1]==direction,'wrong center orientation') + require(all(frames[r]==I for r in data['centers']),'center full frame') + require(all(frames[120+t]==ZERO for t in range(120)),'center target frame') + hist[9]+=8;projectors.add(I);count['centers']+=1 + else: + raise ValueError('unknown event') + require(all(frames[r]==I for r in data['helpers']),'helper endpoint') + require(all(frames[t]==I for t in range(120)),'source endpoint') + require(all(frames[120+t]==ref.bitadd(I,ref.outer(data['ports'][t],9)) + for t in range(120)),'target endpoint') + require(count=={'old':1,'centers':1,'add':14176,'output':120,'cleanup':14176}, + 'complete word event counts') + return hist,projectors + + +def read_response(data,z): + out=[dict(z[r]) for r in data['outputs']] + for t in range(120): + for j,r in enumerate(data['centers']): + if data['B'][t][j]:plus(out[t],z[r],data['B'][t][j]) + return out + + +def old_response(data,z,direction,omit=False): + if omit:return + tmp=[{} for _ in z] # Namespace model: only helper rows are populated/owned. + if direction=='forward': + for r in data['helpers']:tmp[r]=dict(z[r]) + for t,s,c in data['helper_adds']:plus(tmp[t],tmp[s],c) + for t,response in enumerate(read_response(data,tmp)):plus(z[120+t],response,-1) + else: + for t,r in enumerate(data['outputs']):plus(tmp[r],z[120+t]) + for j,r in enumerate(data['centers']): + for t in range(120): + if data['B'][t][j]:plus(tmp[r],z[120+t],data['B'][t][j]) + for t,s,c in reversed(data['helper_adds']):plus(tmp[s],tmp[t],c) + for r in data['helpers']:plus(z[r],tmp[r]) + # tmp is initialized, exclusively owned, and cleared; charged in the invoice. + for row in tmp:row.clear() + + +def run(data,events,direction,omit_old=False): + z=[{j:Q(1)} for j in range(len(data['initial']))] + for event in events: + kind=event[0] + if kind=='old':old_response(data,z,direction,omit_old) + elif kind=='centers': + if direction=='forward': + for t in range(120): + for j,r in enumerate(data['centers']): + if data['B'][t][j]:plus(z[120+t],z[r],data['B'][t][j]) + else: + for j,r in enumerate(data['centers']): + for t in range(120): + if data['B'][t][j]:plus(z[r],z[120+t],-data['B'][t][j]) + elif kind in ('add','output','cleanup'): + _,t,s,c=event + if direction=='backward':t,s,c=s,t,-c + plus(z[t],z[s],c) + expected=[{j:Q(1)} for j in range(len(z))] + for t in range(120): + if direction=='forward':expected[120+t][t]=Q(1) + else:expected[t][120+t]=Q(-1) + require(z==expected,'symbolic arbitrary-dirt endpoint') + return len(z) + + +def moment(hist,W,k): + upper=Q(0);lower=Q(0) + for s,c in hist.items(): + x=Q(27,s);y=x;shifts=0 + while y>2:y/=2;shifts+=1 + def partial(a): + u=(a-1)/(a+1) + return sum((2*u**(2*j+1)/Q(2*j+1) for j in range(36)),Q(0)) + lo=partial(y)+shifts*partial(Q(2)) + z=k*ref.log_upper(x) + require(0<=z<1,'moment exponential domain') + upper+=s*c*(1+z+z*z/(2*(1-z/3))) + lower+=s*c*(1+k*lo) + return 27*W-upper,27*W-lower + + +def phases(projectors): + count=0 + for P in projectors: + ref.check_phase(P);count+=1 + # Downward lowering = positive child plus diag(P) translation. + diag=ref.bdiag(P) + probes=[0]+[1<Q(11,100),'strict new moment') + old=Counter({1:41040,2:240,7:20160,8:1440,9:48}) + _,old_slack=moment(old,7208,Q(1,14100));require(old_slack<0,'old-profile exclusion') + # Concrete instruction counts, including both private macro evaluations. + forward_adds=6720+2*14176+2*456+4*120 + require(forward_adds==36464,'forward scalar invoice') + R=6848 + return {'schema':1,'status':'PASS_E8_DIRECT_SOURCE','source_head':'956bb581e7f97328e1b53baa5aca3d2490f2f607', + 'word_sha256':{name:hashlib.sha256(json.dumps(events,default=str,separators=(',',':')).encode()).hexdigest() for name,events in [('forward',forward),('backward',backward)]}, + 'seed':26,'scope':'depth-one paid-copy complex RAM provider; no multiplication kappa', + 'helpers':R,'live_columns':7088,'independent_symbolic_columns_by_orientation':columns, + 'core_adds':len(data['adds']),'helper_only_old_response_adds':len(data['helper_adds']), + 'source_accesses_in_core':len(data['adds'])-len(data['helper_adds']), + 'local_histogram':dict(sorted(local.items())),'global_histogram':dict(sorted(hist.items())), + 'global_children':sum(hist.values()),'rank_mass':sum(s*c for s,c in hist.items()),'deficit':24, + 'phase_projectors_checked':phases(projectors), + 'private_arrays':R+120+8,'permutation_work_arrays':1, + 'local_invoice':{'forward_add':forward_adds,'backward_add':forward_adds+R+8, + 'forward_copy':R+8,'backward_copy':0,'clear_each_orientation':R+240+8}, + 'global_invoice':{'add':3*forward_adds+R+8,'copy':2*(R+8),'clear':3*(R+240+8), + 'children':sum(hist.values()),'permutation_upper':2*sum(hist.values()), + 'child_translation_upper':sum(hist.values()),'final_translation':120, + 'signed_exchange':120,'initial_private_zero_writes_upper_per_cover_owner':R+120+9}, + 'gaussian_ram_saving':'1/14100','moment_rank_mass_slack_lower':str(slack), + 'old_profile_slack_upper_at_same_saving':str(old_slack), + 'global_rank_two_phase_checked':True,'padding_bits':742,'normalized_gap_lower':str(Q(11,100*27*(1<<742))), + 'negative_controls':controls(data,forward)} + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output',type=Path);parser.add_argument('--check',type=Path) + args=parser.parse_args();result=receipt() + payload=json.dumps(result,indent=2,sort_keys=True)+'\n' + if args.check:require(args.check.read_bytes()==payload.encode(),'receipt mismatch') + if args.output:args.output.write_text(payload) + print('PASS_E8_DIRECT_SOURCE: 7088 columns in both directions; 120 fewer helpers; 7 negative controls') + +if __name__=='__main__':main()