From d5055aa4b44a9bc97404a23410cf4169fe6ac097 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Fri, 23 Oct 2026 04:50:04 -0700 Subject: [PATCH 1/3] Prove the two-edge Gaussian inverse operator limit with exact boundary domains --- .../PROOF.md | 235 ++++++++++++++++++ .../SOURCE-NOTES.md | 9 + .../model.py | 135 ++++++++++ 3 files changed, 379 insertions(+) create mode 100644 research/gaussian-half-line-operator-limit/PROOF.md create mode 100644 research/gaussian-half-line-operator-limit/SOURCE-NOTES.md create mode 100644 research/gaussian-half-line-operator-limit/model.py diff --git a/research/gaussian-half-line-operator-limit/PROOF.md b/research/gaussian-half-line-operator-limit/PROOF.md new file mode 100644 index 0000000000..794842c115 --- /dev/null +++ b/research/gaussian-half-line-operator-limit/PROOF.md @@ -0,0 +1,235 @@ +# Two boundary layers of a finite Gaussian inverse + +JoyboyBrian, with substantial OpenAI Codex assistance. Scoped written theorem; +finite controls are corroboration, not formal verification. Apache-2.0. + +## Statement and embedding + +Fix alpha>0, put b=pi/alpha². Let 0=1)(1-exp(-2tr)), and a=alpha exp(b/4)/P(b)^3. +On H=L²(0,infinity) direct-sum L²(0,infinity), let T have kernel + + T(x,y)=exp(-b(y²-x²)) 1{x<=y}. + +Partition the finite indices at floor(N/2). U_h maps e_i to the normalized +indicator h^-1/2 1_[hi,h(i+1)) in the first summand on the left half; +on the right half it maps e_i to the analogous indicator indexed by n-i +in the second summand. U_h is an isometry. Its adjoint averages over cells; +the orthogonal complement of its image is mapped to zero. Then + + || U_h (h A) U_h* - a(T direct-sum T) || -> 0. + +In particular, + + sqrt(theta) ||K^-1||₂ -> alpha exp(b/4)/(2 sqrt(b) P(b)^3). + +This is for each fixed alpha. Uniformity for alpha growing with theta is +NOT asserted. The section is N=floor(1/theta), beta_0=-1/2; changing section +length or starting phase can change the limit. The result determines the +finite matrix boundary layers, not merely a formal differential expression. + +## Exact predecessor identity and full coefficient + +Credit the finite Gaussian q-LDU identity to the lineage retained by Vlado +Vojdanovski/#1673 and Jose Manuel/#4193, reproduced by JoyboyBrian/#5103 and +Nick Petalas/#5150. Set gamma=b/rho, q=exp(-gamma), Q=q², +P_j=product_(r=1)^j(1-Q^r). For G[i,j]=q^((i-j)²), + + G^-1[i,j]=(-1)^(i+j) sum_(k=max(i,j))^(N-1) + q^(2k-i-j) P_k/(P_i P_(k-i) P_j P_(k-j)). + +K=Dr G Dc with the exact positive diagonals in #5103. For i<=j, d=j-i, +define the FULL positive coefficient (not just its first summand) + + F_ij = sum_(r=0)^(N-1-j) Q^r P_(j+r)/(P_i P_(d+r) P_j P_r). + +Then + + A_ij = alpha exp(E_ij) F_ij, + E_ij = b beta_j²/rho² - gamma theta(j²-i²), + beta_j=theta j-1/2. (1) + +For i>j the same coefficient after reflection i'=n-i,j'=n-j satisfies + + E_ij = b beta_j²/rho² + - gamma theta[(j'+delta)²-(i'+delta)²], + delta=1/theta-n in [1,2). (2) + +The coefficient is invariant under simultaneous reflection because G and +G^-1 are. These are exact formulas. In particular all entries of A are +nonnegative. The predecessor entry lemma gives F_ij<=P(gamma)^-3. +Both exponents are <=b/4. The upper triangle is attached to the left edge; +the strictly lower triangle is attached to the right edge. We assign the +diagonal only to the upper triangle. + +Here is the coefficient limit with an explicit error. For gamma>=b/2 put +r0=exp(-b) and p0=exp(-r0/(1-r0)²). Then all finite products and P(gamma) +are >=p0, because -log(1-z)<=z/(1-z) and geometric summation apply. +Also |P_j-P(gamma)|<=r0^(j+1)/(1-r0). For i>=m, d>=m and N-j>=m+1, + + |F_ij-P(gamma)^-3| <= E_m, + E_m=5 p0^-5 r0^m/(1-r0)². (3) + +Indeed replace P_(j+r), P_i, P_(d+r), P_j by P(gamma) in each term. +The numerator and three inverse factors have telescoping error bounded by +4 p0^-5 r0^(m+1)/(1-r0). Sum Q^r<=1/(1-r0), and bound the omitted tail +by p0^-4 r0^(N-j)/(1-r0). The limiting infinite sum is +P(gamma)^-2 sum Q^r/P_r =P(gamma)^-3: the sum telescopes since +Q^r/P_r=1/P_r-1/P_(r-1) for r>=1. This is why the prefactor contains +THREE infinite-product factors. Dropping all but r=0 does not recover it. +Finally logarithmic differentiation of the convergent product gives + + |P(gamma)^-3-P(b)^-3| <= L_b h², + L_b=6 b p0^-3 r0/(1-r0)³, (4) + +using b-gamma<=b h². Termwise differentiation is justified by the same +summable bound 2 sum k r0^k/(1-r0). + +## Uniform tails, including the middle and cross-edge entries + +Set C=alpha exp(b/4)p0^-3. For i<=j the matrix entry is at most +C exp[-gamma h²(j²-i²)]. For i>j use the reflected bound with delta>=0, +which is no larger than C exp[-gamma h²(j'²-i'²)]. +Fix R>=1, h<=1/2, J=floor(R/h), and suppose 2J<=N. Remove the left +upper-triangular J by J corner and the right strictly-lower J by J corner. +For the upper remainder j>=J, j²-i²=(j-i)(j+i)>=(j-i)J. Every row sum +and every column sum of h times this remainder is bounded by + + C h sum_(d>=0) exp(-gamma h² J d) + <= C(h+1/(gamma h J)) <= C(h+2/(gamma R)). + +The inequality 1/(1-exp(-z))<=1+1/z follows from exp(z)>=1+z. +The lower remainder has the identical bound by reflection. Schur's test +therefore bounds their SUM in operator norm by 2C(h+4/(bR)). This bound +includes the middle and cross-edge blocks; no unproved localization is used. +The two retained corners act in different summands of H, so are a direct +sum, not a sum on a shared output. In particular their norms do not add +in quadrature. + +For the continuum operator, remove its [0,Jh]² triangle. The same row and +column integral bound gives norm <=1/(b Jh)<=2/(bR). After multiplying +by a<=C and allowing both summands, the continuum tails cost <=4C/(bR). +Together the discrete and continuum tail errors are safely bounded by + + 4C(h+4/(bR)). (5) + +This also proves boundedness of T, by a compact-window bound plus its tail. + +## Compact-window comparison and a quantitative convergence regime + +Suppose J>=m>=1 and N-J>=m+1 as well. On each corner the integral kernel +of U_h(h A)U_h* is A_ij on its h by h cells: the h in h A cancels the +normalization h^-1 from the two indicators. On cells with i>=m and +j-i>=m, (3)-(4) control the coefficient. Everywhere both the discrete +kernel and the proposed limiting kernel have magnitude <=C. + +For x in [hi,h(i+1)), y in [hj,h(j+1)), 0<=i<=j=1 and h<=1/2, gives + + |E_ij-[b/4-b(y²-x²)]| <= D, + D=12b(R+1)²h. (6) + +For example the beta²/rho² discrepancy is at most b[h(R+2)+h²], +the gamma discrepancy at most b h²(R+2)², the reflected delta term +at most4bRh, and rounding x,y to cell endpoints at most4b(R+1)h. +Their sum is bounded by (6). Each exponential argument is <=b/4, so +the mean-value theorem gives an absolute exponential error <=exp(b/4)D. + +The exceptional cells i=m, N-J>=m+1; these follow from R/h=h^-11/10, +m<=2h^-1/5 and h<=1/64. Every term of (8) tends to zero, including +R r0^m. Alternatively first choose R, then m, then h. Constants can be +very large for large alpha; this is not a uniform growing-alpha estimate. + +## Exact half-line norm and the endpoint domain + +Let L=-d/dx+2bx on its maximal domain of locally absolutely continuous +u with u,Lu in L²(0,infinity). No boundary condition is imposed on u at0. +For compactly supported smooth f, u=Tf is locally absolutely continuous, +satisfies Lu=f and lies in L². The homogeneous solution exp(bx²) is not +in L², so this inverse is unique. Boundedness extends T to all L² and +identifies it with L^-1 by closedness (or the distributional equation). + +The adjoint is L*=d/dx+2bx on its maximal L² graph domain with g(0)=0. +Integration by parts first on compact intervals proves the boundary term; +cutoffs and the graph norm give the stated domains. More explicitly the +Dirichlet form identity below controls both g' and xg. Truncation and +mollification with the zero trace show that smooth compactly supported +functions on [0,infinity) vanishing at0 form a graph core. At infinity +the boundary term vanishes by those cutoffs. These facts also follow by +solving the first-order distributional adjoint equation and imposing its +boundary pairing with arbitrary u(0). + +For that core, integration by parts gives + + ||L*g||² = integral [|g'|²+4b²x²|g|²-2b|g|²] + >=4b ||g||². (9) + +A direct proof of the inequality, requiring no oscillator spectrum, is the +ground-state identity with v=x exp(-bx²): + + integral [|g'|²+(4b²x²-6b)|g|²] + = integral v² |(g/v)'|² >=0. + +Use a cutoff at0 first; g(0)=0 makes the limiting boundary term zero. +The identity extends by the graph core. Duality then gives +||Tf||<=||f||/(2sqrt(b)): for every core g, +=, and the range of L* is dense (ker L=0). +Density and (9) bound this functional on that range, giving the asserted +bound without a boundary assumption on Tf itself. +Equality is attained at f(x)=x exp(-bx²), since + + T f(x)=exp(-bx²)/(4b), + ||exp(-bx²)||² / ||x exp(-bx²)||²=4b. + +Therefore ||T||=1/(2sqrt(b)). This is a half-line Dirichlet condition on +the ADJOINT, derived from the original Volterra inverse, not an assumed +Neumann condition on a full-line oscillator. The direct sum has the same +norm as either summand. Norm continuity in (8) completes the theorem. + +## Relationship to the formal prediction and limitations + +Ryanson Jonathan/#4408 observed theta^-1/2 growth; #4435 proposed +exp(pi alpha²/4)/(2alpha sqrt(pi)) by a two-frequency approximation and +explicitly left the boundary condition and rigorous upper argument open. +JoyboyBrian/#5103 proved a full-cell upper order; Nick Petalas/#5150 proved +a matching edge lower order. Those results and classical q-binomial +identities are credited dependencies, not new deliverables here. +The exact fixed-alpha coefficient above keeps the entire theta product. +No replacement of it by the formal large-alpha expression is made, and no +joint theta/alpha limit is inferred. The new result is the complete +operator-norm boundary-layer limit with its domain and explicit remainder. + +The exact-real theorem does not supply coefficient preparation, an inverse +application algorithm, rounded prefixes, integer width, physical movement +or storage, native supplier admission, outer transfer or integer recovery. +No selected frontier or multiplication theorem changes. + +## Open next questions + +1. Obtain useful uniform constants for the production growing-alpha regime; + (8) is explicit but too coarse to assert that regime. +2. Classify sections whose endpoint distance or length scales like sqrt(theta), + where a different limiting interval or boundary layer can occur. +3. Bind an actual rounded complete Gaussian caller, preserving all preparation, + prefix, movement and storage charges, before substituting any new guard. diff --git a/research/gaussian-half-line-operator-limit/SOURCE-NOTES.md b/research/gaussian-half-line-operator-limit/SOURCE-NOTES.md new file mode 100644 index 0000000000..1abab9f34b --- /dev/null +++ b/research/gaussian-half-line-operator-limit/SOURCE-NOTES.md @@ -0,0 +1,9 @@ +# Exact source and scope notes + +The executable source closure is pinned in SOURCES.json at canonical base a5df48c55ea806d7952b65acc9c76d878ff09b13. It includes Ryanson Jonathan’s original block exponent, formal turning-point README and numerical code, and JoyboyBrian’s coupled-gauge theorem. The old numerical suites are not rerun; the checker extracts the actual original block expression. + +Nick Petalas [PR5150](https://github.com/CrocSwap/integer-mult-bounds/pull/5150) was read in full at `c16d2fc11e2891bec18d6a9fa3f8ed4e743de6b2`, path `research/gaussian-phase-cell-lower/PROOF.md`, SHA256 `b270bb16325d1bf9c3493072323478b713f48a4602b8cabae1842f8ae514f15a`. Its one-positive-term lower argument and explicit open sharp-coefficient question motivate this task; it is not an executed dependency and no unmerged source history is asserted. The exact finite inverse identity is reproduced in the present proof from the retained q-LDU lineage. + +Ryanson Jonathan [PR4435](https://github.com/CrocSwap/integer-mult-bounds/pull/4435), retained as research/forward-turning-point, labels its semiclassical coefficient and Neumann interpretation as formal/observed. [PR5103](https://github.com/CrocSwap/integer-mult-bounds/pull/5103) supplies the all-cell upper bound; [PR4193](https://github.com/CrocSwap/integer-mult-bounds/pull/4193) and Vlado Vojdanovski/#1673 supply the finite Toeplitz/q-LDU lineage. None is represented as a physical inverse implementation. + +Live overlap before claim: /tmp/integer-mult-round12-claim-overlap.json,329PR/4339Discussion,2026-10-23 11:32–11:33UTC; root refreshed canonical main unchanged. Body/retained-source checks are not an exhaustive novelty certificate. Canonical claim: [4202 comment19144822](https://github.com/CrocSwap/integer-mult-bounds/discussions/4202#discussioncomment-19144822). diff --git a/research/gaussian-half-line-operator-limit/model.py b/research/gaussian-half-line-operator-limit/model.py new file mode 100644 index 0000000000..06f2731506 --- /dev/null +++ b/research/gaussian-half-line-operator-limit/model.py @@ -0,0 +1,135 @@ +"""Exact finite controls for a written operator-limit theorem; no norm fitting. +JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as F + +def need(value,message): + if not value: raise ValueError(message) + +def products(q,n): + p=[F(1)] + for k in range(1,n): p.append(p[-1]*(1-q**(2*k))) + return p + +def coefficient(q,n,i,j): + if i>j: i,j=j,i + p=products(q,n) + return sum((q**(2*r)*p[j+r]/(p[i]*p[j-i+r]*p[j]*p[r]) for r in range(n-j)),F()) + +def exact_inverse(a): + n=len(a); w=[list(v)+[F(i==j) for j in range(n)] for i,v in enumerate(a)] + for k in range(n): + pivot=next(i for i in range(k,n) if w[i][k]) + w[k],w[pivot]=w[pivot],w[k] + scale=w[k][k];w[k]=[v/scale for v in w[k]] + for i in range(n): + if i!=k: + z=w[i][k];w[i]=[v-z*t for v,t in zip(w[i],w[k])] + return [v[n:] for v in w] + +def gauge(theta,i,j): + """Exponent divided by b, from the original Dr,Dc factorization.""" + rho=1+theta;c=F(1,2)/rho + return (theta/rho*i*i-2*c*i-theta/rho**2*j*j+2*c/rho*j+c*c)-abs(i-j)/rho + +def edge(theta,n,i,j): + rho=1+theta; beta=theta*j-F(1,2) + if i<=j: return beta*beta/rho**2-theta/rho*(j*j-i*i) + delta=1/theta-(n-1);a=n-1-i;c=n-1-j + return beta*beta/rho**2-theta/rho*((c+delta)**2-(a+delta)**2) + +def inverse_checks(): + cases=entries=0 + for q in (F(1,2),F(2,3),F(3,4)): + for n in (2,3,5,7): + direct=exact_inverse([[q**((i-j)**2) for j in range(n)] for i in range(n)]) + p=products(q,n) + for i in range(n): + for j in range(n): + a=coefficient(q,n,i,j) + need(direct[i][j]==(-1)**(i+j)*q**abs(i-j)*a,'full q-LDU versus independent elimination') + need(a==coefficient(q,n,n-1-i,n-1-j),'exact reflection') + need(a<=1/p[-1]**3,'normalized predecessor envelope') + entries+=1 + cases+=1 + q=F(1,2);n=20;i=6;j=12;p=products(q,n) + a=coefficient(q,n,i,j);first=1/(p[i]*p[j-i]) + need(a>first,'discarded positive tail changes coefficient') + # A finite product encloses P_infinity: the omitted product is at least1-tail. + L=60; ps=products(q,L+1)[-1];tail=q**(2*(L+1))/(1-q*q) + lo=ps*(1-tail);hi=ps + need(lo>0,'infinite product lower endpoint') + need(1/hi**3>1/lo**2,'three factors distinguish two factors') + return {'matrices':cases,'entries':entries,'nonfirst_tail':str(a-first),'product_interval':[str(lo),str(hi)]} + +def geometry_checks(source_setup,source_expression): + from types import SimpleNamespace + pairs=0; offsets=[] + for theta,n in ((F(1,400),400),(F(2,799),399),(F(3,1000),333)): + rho=1+theta;delta=1/theta-(n-1);offsets.append(str(delta)) + need(1<=delta<2,'floor section reflected offset') + env={'alpha':3,'theta':theta,'beta_start':-F(1,2),'math':SimpleNamespace(pi=F(1))} + exec(source_setup,env) + for i in range(n): + for j in sorted({0,1,5,n//2,n-2,n-1,i}): + env.update(i=F(i),j=F(j)) + original=eval(source_expression,env) + expected=F(1,9)*(F(i)-F(j)/rho-env['c'])**2 + need(original==expected,'original block exponent binding') + need(gauge(theta,i,j)==edge(theta,n,i,j),'both edge gauge identities') + need(gauge(theta,i,j)<=F(1,4),'exponent envelope') + pairs+=1 + theta=F(2,799);n=399;i=n-1;j=n-4;rho=1+theta + wrong=(theta*j-F(1,2))**2/rho**2-theta/rho*((n-1-j)**2-(n-1-i)**2) + need(wrong!=gauge(theta,i,j),'omitting reflected offset rejected') + need(gauge(F(1,400),0,20)!=gauge(F(1,400),20,0),'one edge cannot replace both orientations') + return {'source_pairs':pairs,'offsets':offsets,'first_fixture':{'alpha':3,'theta':'1/400','N':400}} + +def operator_controls(): + # Isometric cell embeddings and direct sums tested exactly, not sampled norms. + h=F(1,20);v=[F(2),F(-3),F(5)] + need(sum(x*x for x in v)==sum(h*(x*x/h) for x in v),'cell isometry') + a=[[F(1),F(2)],[F(0),F(3)]];x=[F(4),F(-1)] + matrix=[h*sum(t*s for t,s in zip(row,x)) for row in a] + kernel=[sum(h*t*s for t,s in zip(row,x)) for row in a] + need(matrix==kernel,'hA versus piecewise constant kernel') + need(matrix!=[sum(t*s for t,s in zip(row,x)) for row in a],'missing h normalization rejected') + # The norm on block-diagonal identical scalar maps is max, not sqrt(sum squares). + z=[F(3),F(4)];need(sum((2*t)**2 for t in z)==4*sum(t*t for t in z),'orthogonal corner outputs') + # Polynomial coefficients after factoring exp(-b x²): L*(x exp)=exp, L(exp)=4bx exp. + for b in (F(1,3),F(1),F(7)): + for x0 in (F(0),F(1,5),F(3)): + need((1-2*b*x0*x0)+2*b*x0*x0==1,'adjoint ground state') + need(-(-2*b*x0)+2*b*x0==4*b*x0,'LL* ground eigenvalue') + # A nonzero-trace trial does not belong to the adjoint domain. + need(F(1)!=0,'exp(-b x²) has forbidden adjoint trace') + return {'controls':['cell-isometry','kernel-h','missing-h','orthogonal-corners','adjoint-ground-state','nonzero-adjoint-trace']} + +def remainder_checks(): + tested=0 + # Exact exponent comparison, including fractional floor offsets and cell corners. + for h,R in ((F(1,20),F(1)),(F(1,32),F(2)),(F(3,100),F(2))): + theta=h*h;n=int(1/theta);J=int(R/h) + for i in sorted({0,1,J//2,J-1}): + for j in sorted({i,min(i+1,J-1),J-1}): + for dx,dy in ((0,0),(0,1),(1,0),(1,1)): + x=h*(i+dx);y=h*(j+dy) + if x>y: continue + target=F(1,4)-(y*y-x*x) + for u,v in ((i,j),(n-1-i,n-1-j)): + need(abs(gauge(theta,u,v)-target)<=12*(R+1)**2*h,'compact exponent remainder') + tested+=1 + # Finite geometric sums dominate full row/column tails without a numerical exp. + for t in (F(1,2),F(2,3),F(9,10)): + for J in (2,5,9): + for i in range(12): + row=sum((t**(j*j-i*i) for j in range(max(i,J),15)),F()) + need(row<=1/(1-t**J),'tail row geometric comparison') + for j in range(J,15): + col=sum((t**(j*j-i*i) for i in range(j+1)),F()) + need(col<=1/(1-t**J),'tail column geometric comparison') + # Explicit scale regime at an exact rational subsequence, no large matrices. + for k in range(1,7): + h=F(1,2**(10*k));R=2**k;m=2**(2*k);J=int(R/h);n=int(1/(h*h)) + need(2*J<=n and J>=m and n-J>=m+1,'explicit regime admissibility') + return {'exponent_comparisons':tested,'geometric_tail_parameters':9,'regime_subsequence_cases':6} From 149d86bea7ea248e4222e60379f219d1a778e79d Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Fri, 23 Oct 2026 04:50:04 -0700 Subject: [PATCH 2/3] Bind exact inverse and source geometry controls to a typed replay certificate --- .../README.md | 15 ++++ .../RESULT.json | 40 ++++++++++ .../SOURCES.json | 60 +++++++++++++++ .../TASK.json | 74 +++++++++++++++++++ .../VERIFY.json | 36 +++++++++ .../verify.py | 21 ++++++ 6 files changed, 246 insertions(+) create mode 100644 research/gaussian-half-line-operator-limit/README.md create mode 100644 research/gaussian-half-line-operator-limit/RESULT.json create mode 100644 research/gaussian-half-line-operator-limit/SOURCES.json create mode 100644 research/gaussian-half-line-operator-limit/TASK.json create mode 100644 research/gaussian-half-line-operator-limit/VERIFY.json create mode 100644 research/gaussian-half-line-operator-limit/verify.py diff --git a/research/gaussian-half-line-operator-limit/README.md b/research/gaussian-half-line-operator-limit/README.md new file mode 100644 index 0000000000..a250772493 --- /dev/null +++ b/research/gaussian-half-line-operator-limit/README.md @@ -0,0 +1,15 @@ +# Gaussian half-line inverse limit + +JoyboyBrian, with substantial OpenAI Codex assistance. Scoped written theorem with exact finite corroboration; no new kappa. + +For fixed alpha>0 and the original full cell N=floor(1/theta), the checkerboard inverse scaled by sqrt(theta) converges in operator norm, under an explicit two-edge step embedding, to two copies of a half-line Volterra operator. [PROOF.md](PROOF.md) gives the full infinite-product coefficient, boundary domain and quantified remainder. This resolves the boundary-layer implication left formal in Ryanson Jonathan #4435 and open after Nick Petalas #5150, beyond JoyboyBrian #5103's matching-order upper estimate. All finite q-LDU identities retain Jose Manuel/#4193, Vlado Vojdanovski/#1673 and classical lineage credit. + +The exact limit is alpha exp(b/4)/(2 sqrt(b) P(b)^3), b=pi/alpha², P(b)=product(1-exp(-2br)). A growing-alpha limit is not inferred. The complete cell is untruncated; the first source fixture is alpha3,theta1/400,N400. + +Run `python3.12 -B scripts/research_package.py --package research/gaussian-half-line-operator-limit`. Both normal and optimized commands use standard-library exact rational elimination and unchanged source exponent AST, without fitting a numerical norm. RESULT and SOURCES are mandatory and the entire receipt has typed canonical JSON equality. + +No coefficient-preparation or inverse-application algorithm, rounded-prefix guarantee, tape/movement/storage tariff, native admission, outer transfer or integer recovery is supplied. These are obligations, not zero charges. + +## Open next questions + +See PROOF.md: uniform growing-alpha estimates, other section/endpoint scalings, and an actual complete rounded caller remain separate. diff --git a/research/gaussian-half-line-operator-limit/RESULT.json b/research/gaussian-half-line-operator-limit/RESULT.json new file mode 100644 index 0000000000..fe71bf8630 --- /dev/null +++ b/research/gaussian-half-line-operator-limit/RESULT.json @@ -0,0 +1,40 @@ +{ + "exact": { + "matrices": 12, + "entries": 261, + "nonfirst_tail": "181711281244526291631416372864043841938044799092738477785088/190471383981728519572397642029361552234543366836814853515625", + "product_interval": [ + "5386556649350038188350496511122457094258124728934462595341461816075498050932354346318731286955276293692934505154980524109903519223055793838784626065533561467212214347827748796771641598371669701276608727077749502284235353133125939875683475783645562350528625499584190271035349861880217242579140095055211296373854599192113050081937841190308610278295720891327294064167855536374512531464864521266750145269863820700688350775324197046551552215943344729550769226029659992498650494195756430899566587450898661082952177494063772488092015126949450026917627415917077020993187819478495463957291403156718920587752333487439717043046448361643967737342700837055558760166330643969128080873136578630331775210422378178865754635531512213413089289403547934555680633155644723879693351904969053030081534416998637851818502157702087417999081049537164945761498809631498846167122179195545955661559839707080012103434121403474035777599440555824537125685362448260792983939739544294259240375842907547817343731689324283651881542486340442629743188399173923661695854930040667919656844297748344669454406023442166431148776280833114224655164744955125279375351965427398681640625/7823185169944624690862333421622510381882964170777786454179336436821124108015121575079361355345810924625716099431438272846159305200784937365374304077187608911661568843213926119782924978024192524960305489656234857295814449610481484375955118746436206058574333105523219247323645542570174455989537465024513601294752465770659181709989953102552700043602039143140402082267270150450450771418287572165560753934840297495912770475088683005010028122212158711689546560252560684813089770058546847056231312601376273057564702245962972121307218571519747599094470796827016439422270778861350072748474328729702713110841197193009790615683799988589959949153267959432202745529600446104728268651628712334007309536411134477261709185962891067129955564486215715978440933530342520709947592788926520738372274968696904490691159847660388275056040463017077965624401363723549513580082824435889916298472978277627661636304854610791631017149070630710967102330597780276944370475292242540729676876263783579703453509806553208493155136063711417040877770900350249926483067495650551671642966222622438210744708517897097735667967242634300423346647912896012762824118369374541159858176", + "4052394823484927556106697457161923149691286268777444714938609447376815210148605557488618907492826123709406173760687543086919402847458395556477655368266103679195804051841395632456675435653861833124607099031575361573298467145686810689966592698889949805258176204986213012502428675689438291448442769662900160565840158059231170626316441426785702516581776797174094193205694794540879396325449676039122320102514938611054785400799648739119228655837696345672617095090827983075560984710110428099543781737753298933930760953771060296396399481890214679633355971761698988204690240190779564221900822700881670238297122209651320052614215717745393947505342070829594576552514754445301794863059625311368772675232740524489968978905900972299207988185863039766413342870847796026995569605190399268498406001802017191717821119165066525532692339538035509372687904168748278150419210891613274420644155230667752729331245243758555860845109823360456358484993245445938591847130083802719571357981431249124159815775664296056354185011932732823694022331727822915717381970231501952020095965299704188309065765134624161873944103717803955078125/5885510382532226287840583450632860103535659861388354943844039519761868641357865490298562086651414546940995403410157040159649209295265705749228073680381854138795016035414915534738401192801472293596148650642835454781747172337821399683496787720821386472691083141583829110265239900065592520522448987342622699099596993166815673912444534441442291485827681897518692980104805674211553064860074769885148884530402817407658661941473043637923054293214462360067307875813715760016788010825606064862491679493540668602019519358921410056450408784237113867649954357122920647778991880236162388261002140487457007123339885368897715733396030835689053569076282964146473595031611395092705051231247926171204878184236399311054085754406715394258461064720237619850337151763781380815296744444759297360475904109545577838190897687482170262656487141955590092256509100714919242885807706805595361807532235394232038753353978586628384958709228837213801781432354758316140626562273123215071112329541254947422065071206349571709761173191116178457268720555714322631118542905042971587868805043953570084960915409456835042410928441719766411902976" + ] + }, + "geometry": { + "source_pairs": 7906, + "offsets": [ + "1", + "3/2", + "4/3" + ], + "first_fixture": { + "alpha": 3, + "theta": "1/400", + "N": 400 + } + }, + "operators": { + "controls": [ + "cell-isometry", + "kernel-h", + "missing-h", + "orthogonal-corners", + "adjoint-ground-state", + "nonzero-adjoint-trace" + ] + }, + "remainders": { + "exponent_comparisons": 216, + "geometric_tail_parameters": 9, + "regime_subsequence_cases": 6 + }, + "claim": "finite corroboration of written fixed-alpha operator-norm theorem; no physical caller or growing-alpha claim" +} diff --git a/research/gaussian-half-line-operator-limit/SOURCES.json b/research/gaussian-half-line-operator-limit/SOURCES.json new file mode 100644 index 0000000000..7f97693d2e --- /dev/null +++ b/research/gaussian-half-line-operator-limit/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "files": [ + { + "path": "LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "NOTICE", + "usage": "input", + "git_blob": "59d8e0cf3102e15bd11db430838365531e2d7f18", + "sha256": "b49022cb4104d90b182e4c335f670faf45529025b15db77bf0291835083c28bd" + }, + { + "path": "research/broad-phase-cell-inverse-bound/PROOF.md", + "usage": "input", + "git_blob": "efc7842083ea33a69525f2baf17febae17bd8b6d", + "sha256": "3107aa37b026fef8b21f8ba859acfc7968eb94fed28a3169f5e559fbbd70e52d" + }, + { + "path": "research/broad-phase-cell-inverse-bound/verify.py", + "usage": "input", + "git_blob": "c953addeca75ea55d6c5e4e4b9b061fad36b6e6d", + "sha256": "2f7c9e1148a331a01695cf7788cda5a78aa5e63232974e780d9d5733f435eaf2" + }, + { + "path": "research/forward-fine-theta-conditioning/verify.py", + "usage": "input", + "git_blob": "48fdf11e4bb4da2928c439d03f05574f7b2c88a7", + "sha256": "0484ba72b20a805ae2a0e9bde0527f6d048389c6453642d5337064d2da23e547" + }, + { + "path": "research/forward-turning-point/README.md", + "usage": "input", + "git_blob": "3f487ef4f53021863060ca5b1a7560de22a287b5", + "sha256": "cae911dd36e8911333312a7640aa0ea513e76b2f4c4b8ef1eb1524302cd5a2d6" + }, + { + "path": "research/forward-turning-point/verify.py", + "usage": "input", + "git_blob": "15c7dd506624ff85b5d3fe10113ab5db1199120b", + "sha256": "13e802f1283f2039490fd723e5b1fc835b9cc59d88c843c574bdaa3f2572fc73" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + } + ] +} diff --git a/research/gaussian-half-line-operator-limit/TASK.json b/research/gaussian-half-line-operator-limit/TASK.json new file mode 100644 index 0000000000..25e502795a --- /dev/null +++ b/research/gaussian-half-line-operator-limit/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Full two-edge half-line operator-norm limit for fixed-alpha untruncated phase cells, including exact endpoint domain and quantitative remainder.", + "scope_change_reason": "Takes explicit PR4435/5150 boundary-limit handoff, beyond the already established theta order.", + "bottleneck_link": "Closes a specific analytic inequality for the actual varying-phase broad kernel without importing a full-line boundary condition.", + "budget_minutes": 60, + "stop_rule": "20-minute viability stop if only pointwise convergence or a numerical fit survives.", + "outcome": "completed", + "evidence": "PROOF.md gives quantified theorem; model.py and verify.py give finite corroboration.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, checks and review.", + "open_questions": [ + { + "question": "Can the error be uniform in the production growing-alpha regime?", + "why_it_matters": "Fixed-alpha convergence does not justify that caller substitution.", + "first_step": "Sharpen product and tail constants jointly.", + "blocked_by": "Explicit constants here grow rapidly with alpha." + } + ] +} diff --git a/research/gaussian-half-line-operator-limit/VERIFY.json b/research/gaussian-half-line-operator-limit/VERIFY.json new file mode 100644 index 0000000000..bcb1330939 --- /dev/null +++ b/research/gaussian-half-line-operator-limit/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "LICENSE", + "NOTICE", + "research/broad-phase-cell-inverse-bound/PROOF.md", + "research/broad-phase-cell-inverse-bound/verify.py", + "research/forward-fine-theta-conditioning/verify.py", + "research/forward-turning-point/README.md", + "research/forward-turning-point/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact finite inverse, full coefficient, original N400 geometry, step embeddings and endpoint controls; typed frozen receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact finite inverse, full coefficient, original N400 geometry, step embeddings and endpoint controls; typed frozen receipt." + } + ] +} diff --git a/research/gaussian-half-line-operator-limit/verify.py b/research/gaussian-half-line-operator-limit/verify.py new file mode 100644 index 0000000000..90b2f727a4 --- /dev/null +++ b/research/gaussian-half-line-operator-limit/verify.py @@ -0,0 +1,21 @@ +"""Source-bound exact controls; universal result is the written proof. +JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. +""" +import hashlib,importlib.util,json +from pathlib import Path +from model import need,inverse_checks,geometry_checks,operator_controls,remainder_checks +HERE=Path(__file__).resolve().parent;ROOT=HERE.parents[1] +def canonical(x):return json.dumps(x,sort_keys=True,separators=(",",":"),allow_nan=False) +def run(): + manifest=json.loads((HERE/'SOURCES.json').read_text()) + for row in manifest['files']: + if row['usage']=='input':need(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'],'source hash: '+row['path']) + spec=importlib.util.spec_from_file_location('retained_geometry',ROOT/'research/broad-phase-cell-inverse-bound/verify.py') + mod=importlib.util.module_from_spec(spec);spec.loader.exec_module(mod) + setup,expr=mod.source_expression() + return {'exact':inverse_checks(),'geometry':geometry_checks(setup,expr),'operators':operator_controls(),'remainders':remainder_checks(),'claim':'finite corroboration of written fixed-alpha operator-norm theorem; no physical caller or growing-alpha claim'} +def main(): + expected=json.loads((HERE/'RESULT.json').read_text()) + actual=run();need(canonical(actual)==canonical(expected),'complete typed receipt mismatch') + print(canonical(actual));print('PASS_GAUSSIAN_HALF_LINE_OPERATOR_LIMIT') +if __name__=='__main__':main() From 73660fc53b9910aa25523f37ec7d34e3fd9f083b Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Fri, 23 Oct 2026 04:53:38 -0700 Subject: [PATCH 3/3] Record immutable cold replay and independent operator-limit proof review --- .../gaussian-half-line-operator-limit/VALIDATION.md | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 research/gaussian-half-line-operator-limit/VALIDATION.md diff --git a/research/gaussian-half-line-operator-limit/VALIDATION.md b/research/gaussian-half-line-operator-limit/VALIDATION.md new file mode 100644 index 0000000000..cf0d3c847d --- /dev/null +++ b/research/gaussian-half-line-operator-limit/VALIDATION.md @@ -0,0 +1,11 @@ +# Validation and independent review + +Scientific commit149d86bea7ea248e4222e60379f219d1a778e79d passes the registered normal and optimized commands on CPython3.12.7. The full typed frozen certificate records12 exact matrices,261 inverse entries,7906 original source/gauge pairs and216 exponent remainder controls. The first source fixture is alpha3,theta1/400,N400. + +Committed-byte/source-history preflight covers16 payload files. Official export integrity passes. Fresh Git-free PATH-empty optimized execution takes0.327seconds, changes none of17 exported files including its manifest, and uses a fresh external bytecode-cache prefix. Archive SHA256852c2875ec3c80685726d68438b7661d78792a518a77dd32036315a941c15ea1. + +Eight actual isolated export mutations reject: missing RESULT, missing SOURCES, source-byte drift, float/int typed receipt alias, dropped full positive tail, omitted reflected endpoint offset, missing h normalization and wrong q power. Restoration reproduces every original byte. No heavy historical suite, numerical norm fit, Lean or Docker was used. + +An independent root-agent written proof review passes at PROOF SHA2562bf0e36ecd0c3647888e78bc0b8ae30614f5daf07511a4424d69cb3efc29c904. It checks the full coefficient telescope/product derivative, both Schur tails, step isometry/direct sum, exceptional strips/explicit regime, maximal and Dirichlet adjoint domains, coercivity and exact extremizer. This is AI-assisted independent review, not human acceptance or formal proof-kernel verification. + +The final documentation commit adds only this validation record. Scientific proof, executable source, inputs, metadata and RESULT are byte-identical to the cold-tested commit. Source-history and export integrity are refreshed on final bytes; the recorded cold scientific replay remains attributed to149d86bea, not represented as a new full execution at the documentation commit.