From b942eb8bd0091937c681484382398f344195f995 Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Tue, 29 Sep 2026 16:13:38 -0500 Subject: [PATCH] Add explicit SIDE24 second-order remainder and fixed-d first-variation candidate OpenAI / GPT-6 Astra Pro. Derive full-covariance fixed-cone Taylor bound, include deep images and normalization products, enclose d=2,3 relative error below 1e-216 and determine its sign. First-variation polynomial derived for every fixed d>=2. Eleven standalone tests pass in both Python modes; six semantic mutants reject. Add source-bound hosted controls. Author-side analytic candidate only; non-OpenAI review required; no existing sources or scientific registers changed. --- .github/workflows/side24-remainder.yml | 40 +++ .../side24_remainder_20260929/PROOF.md | 307 ++++++++++++++++++ .../RECONNAISSANCE.md | 53 +++ .../side24_remainder_20260929/RESULTS.json | 36 ++ .../side24_remainder_20260929/SOURCES.json | 91 ++++++ .../side24_remainder_20260929/check.py | 242 ++++++++++++++ .../side24_remainder_20260929/test_check.py | 138 ++++++++ 7 files changed, 907 insertions(+) create mode 100644 .github/workflows/side24-remainder.yml create mode 100644 coefficients/side24_remainder_20260929/PROOF.md create mode 100644 coefficients/side24_remainder_20260929/RECONNAISSANCE.md create mode 100644 coefficients/side24_remainder_20260929/RESULTS.json create mode 100644 coefficients/side24_remainder_20260929/SOURCES.json create mode 100644 coefficients/side24_remainder_20260929/check.py create mode 100644 coefficients/side24_remainder_20260929/test_check.py diff --git a/.github/workflows/side24-remainder.yml b/.github/workflows/side24-remainder.yml new file mode 100644 index 000000000..bd8b8a3f3 --- /dev/null +++ b/.github/workflows/side24-remainder.yml @@ -0,0 +1,40 @@ +name: SIDE24 explicit remainder controls + +'on': + pull_request: + paths: + - 'coefficients/side24_remainder_20260929/**' + - '.github/workflows/side24-remainder.yml' + push: + branches: [main] + paths: + - 'coefficients/side24_remainder_20260929/**' + - '.github/workflows/side24-remainder.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-remainder: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Exact sources, both Python modes, semantic negative controls + run: | + set -euo pipefail + P=coefficients/side24_remainder_20260929 + python -B -S "$P/check.py" --verify-sources "$GITHUB_WORKSPACE" + python -B -S "$P/check.py" > "$RUNNER_TEMP/remainder-normal.json" + python -B -O -S "$P/check.py" > "$RUNNER_TEMP/remainder-optimized.json" + cmp "$P/RESULTS.json" "$RUNNER_TEMP/remainder-normal.json" + cmp "$RUNNER_TEMP/remainder-normal.json" "$RUNNER_TEMP/remainder-optimized.json" + python -B -S "$P/test_check.py" -v + python -B -O -S "$P/test_check.py" -v + git diff --exit-code diff --git a/coefficients/side24_remainder_20260929/PROOF.md b/coefficients/side24_remainder_20260929/PROOF.md new file mode 100644 index 000000000..0bcf0a6f5 --- /dev/null +++ b/coefficients/side24_remainder_20260929/PROOF.md @@ -0,0 +1,307 @@ +# SIDE24: a second-order remainder and the sign of the finite-size correction + +Object: **OA-SIDE24-REMAINDER-20260929-v1**. +Author: OpenAI / GPT-6 Astra Pro, foreground session, 29 September 2026. +Disposition: **AUTHOR-SIDE ANALYTIC CANDIDATE; non-OpenAI review required**. +Scientific effect: **NONE**. No existing proof bytes, review dispositions, registers, +claims, premises, prizes, or `lemma_closed` flags are changed. No self-merge. + +## 1. Exact object and results + +Let c_(d,L) mean exactly the coefficient expression (15.2) of the reconciled +UNIFORM-MATRIX-CAP-LIFETIME parent, with its exact variance-one covariance + + K_L(x) = [sum_(n in Z^d) exp(-|x+Ln|^2/2)] / + [sum_(n in Z^d) exp(-|Ln|^2/2)]. + +Let c_(d,ref) be the same expression evaluated on the Euclidean covariance +exp(-|x|^2/2). It is a local reference expression, not an infinite-volume +persistence theorem. All source identities and the parent's complete reading-rule +set are in SOURCES.json, bound to Math- main e1ca400b3414e5a7bec13b91bc4f1e5293df32be. +Interpreting this expression as the persistence asymptotic constant still consumes +that parent with its amendments; this note does not independently revalidate it. + +**Theorem R (candidate).** For d = 2 and d = 3, put z = exp(-288). Then + + |c_(d,24)/c_(d,ref) - 1 - P_d(24) z| < 10^(-216), (R1) + +where + + P_d(L) = -10 L^6/[3(d+2)(d+4)] + (d+4)L^4/(d+2) - d L^2, + P_2(24) = -26045568, + P_3(24) = -620813376/35. (R2) + +In particular c_(d,24) < c_(d,ref) for both dimensions. Section 7 supplies an +explicit rational bound, rather than an unspecified constant in a big-O term. +RESULTS.json encloses both full relative corrections by outward rational endpoints. +The existing coefficient intervals in coefficients/side24_v1 are left unchanged. +No finite-radius persistence error bound, RN/24-jet result, or theorem-status fold +follows from (R1). + +**Proposition V.** Formula P_d(L) in (R2) is the first normalized nearest-image +variation of the same coefficient expression for every fixed integer d >= 2. +Only d = 2,3 receive the numerical remainder (R1); no dimension-uniform estimate +is asserted. At d = 3 the polynomial agrees with Claude's reviewed first-variation +packet (Math-#144). We rederive it in Section 5, so that unmerged packet is a +comparison source, not an unverified runtime dependency. + +## 2. A fixed-subspace Gaussian integral removes moving cone boundaries + +For each axis u choose any orthonormal frame. Write m=d-1, G=grad f, +t=partial_u^3 f, H=Hess f, V=Hu, and A for the transverse m by m Hessian block. +Use the full covariance C of X=(G,t,svec H); svec uses sqrt(2) times off-diagonal +entries and diagonal entries unchanged. The ambient dimension and the free +subspace dimension after pinning G=0 and V=0 are + + n = d+1+d(d+1)/2, k = 1+m(m+1)/2. + +Denote that fixed linear subspace by E. On E use the nonnegative weight + + h(t,A) = |t|^(4/3) det(A)^2 1{A negative definite}, + p = degree(h) = 4/3 + 2m, nu = k+p. + +The function h is measurable, bounded on the unit sphere, and positively +homogeneous. It is not differentiated. Define + + F_u(C) = integral_E h(x) phi_C(x) dx_E. (R3) + +Because the stationary covariance is even, the odd block (G,t) is independent +of H. Disintegration on the pinned coordinates therefore shows + + F_u(C) = 2^(-m/2) M_(4/3) p_G(0) p_V(0) + tau_u^(4/3) D_u, (R4) + +where M_(4/3)=E|N(0,1)|^(4/3)>0 is independent of C, +tau_u^2=Var(t|G=0), and D_u=E[det(A)^2 1{A<0}|V=0]. +The factor 2^(-m/2) comes from pinning sqrt(2)H_(uj) rather than H_(uj). +It cancels in all ratios and derivatives of ratios. Thus the parent's (15.2) +is a positive constant times the angular integral of (R3). + +This representation uses the FULL covariance of the periodic jet. The periodic +field need not be rotationally invariant. In particular its coefficient is NOT +claimed to depend only on three isotropic moment scalars. Changing the transverse +frame is an orthogonal coordinate change preserving h, so no globally continuous +choice of transverse frame is required. + +## 3. Explicit second-order covariance bound + +Here is a general calculation for (R3). Let C_0 be positive definite, Delta +symmetric, C_s=C_0+s Delta for 0<=s<=1, and + + e = ||C_0^(-1/2) Delta C_0^(-1/2)|| <= 1/4. + +At a point x in E put B=C_s^(-1/2) Delta C_s^(-1/2), +y=C_s^(-1/2)x, and R^2=|y|^2. Differentiation of the ambient Gaussian density gives + + (log phi)' = -tr(B)/2 + y^T B y/2, + (log phi)'' = tr(B^2)/2 - y^T B^2 y. (R5) + +The negative sign in the second quadratic term matters. The covariance sandwich +implies ||B|| <= e/(1-e). Therefore + + |phi''| <= [e/(1-e)]^2 phi + [(n+R^2)^2/4+n/2+R^2]. (R6) + +All differentiations under the E integral are justified directly by a uniform +Gaussian majorant times a polynomial on this compact positive-definite path. +The cone indicator causes no difficulty because it is a fixed part of h. + +Under the probability measure proportional to h(x)phi_(C_s)(x)dx_E, R^2 has a +chi-square radial distribution with parameter nu=k+p (not necessarily an integer). +Indeed C_s^(-1/2) maps E linearly onto a k-dimensional subspace; its constant +Jacobian and the angular part of the homogeneous weight cancel on normalizing. +The radial density is proportional to R^(k+p-1)exp(-R^2/2). Integration by parts +then gives E R^2=nu and E R^4=nu(nu+2). Consequently + + |F_u''(C_s)| <= K(n,nu) [e/(1-e)]^2 F_u(C_s), + K(n,nu) = [n^2+2n nu+nu(nu+2)]/4+n/2+nu. (R7) + +For d=2: (n,k,p,nu)=(6,2,10/3,16/3). +For d=3: (n,k,p,nu)=(10,4,16/3,28/3), and K=1012/9. +The latter bounds the former term by term. Comparing the determinant and inverse +quadratic form in the density, followed by scaling on E, gives + + F_u(C_s)/F_u(C_0) + <= (1-e)^(-n/2)(1+e)^(nu/2) + <= (4/3)^5(5/4)^(14/3) <= (5/3)^5 = 3125/243. + +Taylor's integral remainder and (1-e)^(-2)<=16/9 now give, for d=2,3, + + |F_u(C_0+Delta)-F_u(C_0)-DF_u(C_0)[Delta]|/F_u(C_0) + <= (1/2)(1012/9)(16/9)(3125/243) e^2 <= 2000 e^2. (R8) + +The first derivative formula similarly implies, for ANY symmetric R_0, + + |DF_u(C_0)[R_0]|/F_u(C_0) + <= [(n+nu)/2] ||C_0^(-1/2) R_0 C_0^(-1/2)|| + <= (29/3) ||C_0^(-1/2) R_0 C_0^(-1/2)||. (R9) + +As an independent normalization check, F_u(a C_0)/F_u(C_0) +=a^((k+p-n)/2)=a^(-1/3). The score expectations in (R5) consequently give +first derivative -1/3 and second derivative 4/9 at a=1, exactly as the checker +verifies. Confusing the ambient dimension n with the free dimension k fails this +check. These estimates hold uniformly in u and hence pass to the positive angular +integral defining the coefficient. + +## 4. Uniform covariance comparison and reference floor + +We use the elementary derivative and reference-matrix bounds of side24_v1 +Sections 2-3, recording the constants here. For q<=6 mixed unit directional +derivatives of phi(x)=exp(-|x|^2/2), at |x|>=1, + + |D^q phi(x)| <= 76 |x|^6 exp(-|x|^2/2), + |D^q phi(0)| <= 15. + +The largest coefficient sum is 1+15+45+15=76 at q=6. Let + + B_0=76*24^6+15=14523826191, z=exp(-288). + +For d<=3, grouping lattice points by j=|n|_infinity gives at most 27j^3 points +and |n|^6<=27j^6. The successive ratio in sum j^9 z^(j^2) is at most +512 z^3<1/2. Thus + + sum_(n!=0) |n|^6 z^(|n|^2) <= 1458 z, + S-1 = sum_(n!=0) z^(|n|^2) <= 1458 z. + +A positive rational Taylor sum through degree 20 proves exp(288/125)>10, +so z<10^(-125). Including the exact variance normalization gives, for every +unit directional jet contraction through order six, + + |J_24-J_ref| <= 1458 B_0 z < E, + E=1458 B_0*10^(-125)=21175738586478*10^(-125). (R10) + +For the full svec covariance, each entry difference is <=2E, the dimension +is <=10, and therefore ||C_24-C_0||<=20E. The reference Hessian covariance +has eigenvalues d+2 on trace and 2 on traceless coordinates. The only nontrivial +odd block is [[1,-3],[-3,15]]; subtracting I/3 gives positive first principal +minor 2/3 and determinant 7/9. The remaining gradient variances are 1. Hence +C_0>=I/3, and uniformly in all frames + + e <= 60E =: e_0 < 1/4. (R11) + +## 5. First normalized image variation: every fixed dimension + +The angular coefficient functional is O(d)-invariant, and the reference jet is +isotropic. Its derivative at that jet is consequently an invariant LINEAR +functional and sees precisely the Haar projection of a perturbation. This is +only a first-derivative assertion; it is not a replacement of the anisotropic +coefficient by its isotropized value at second order. + +For a uniform v on S^(d-1), E v_i^2=1/d, E v_i^4=3/[d(d+2)], and +E v_i^6=15/[d(d+2)(d+4)]. These follow by factoring a standard Gaussian into +independent radius and uniform direction and using its second, fourth and sixth +moments. Apply the Hermite identities to the 2d nearest images +/-Le_i and +subtract their normalizer contribution 2d z times the reference jet. The +projected spectral variations, per unit z=exp(-L^2/2), are + + da = -2L^2, + dm4 = 6L^4/(d+2)-12L^2, + dchi = -30L^6/[(d+2)(d+4)]+90L^4/(d+2)-90L^2. (R12) + +The reference isotropic moments are (a,m4,chi)=(1,3,15). Along an isotropic +family, finite Gaussian conditioning gives + + p_G proportional to a^(-d/2), + p_V proportional to m4^(-d/2), + tau^2=chi-m4^2/a=(a chi-m4^2)/a, + D_u proportional to m4^(d-1). + +For completeness, Cov(V)=diag(m4,m4/3,...,m4/3). The transverse Hessian +conditional on V=0 has covariance m4/3 times its reference covariance: +conditioning on H_uu subtracts m4/9 from every diagonal-diagonal covariance, +leaving (m4/3)[(2/3)delta_ij delta_kl+delta_ik delta_jl+delta_il delta_jk]. +The cone determinant-square moment scales as m4^m. Therefore + + Phi proportional to a^(-d/2-2/3) m4^(d/2-1)(a chi-m4^2)^(2/3), + d log Phi = (1-d/2)da+(d/6-1)dm4+dchi/9 (R13) + +at the reference. Substitution of (R12) gives exactly (R2). The checker derives +the polynomial by both (R12)-(R13) and the closed expression, for d=2,...,20; +the displayed rational algebra itself proves it for every fixed integer d>=2. + +## 6. Deep images AND the normalization product + +Fix any directional contraction of order <=6 and write its unnormalized +numerator as a_0+a_1+a_2, where a_1 is the nearest-image contribution and a_2 +contains the remaining images. Write the denominator as 1+s_1+s_2, with +s_1=2d z<=6z. Its first normalized variation is b_1=a_1-s_1 a_0. Exactly, + + J_24-J_ref-b_1 + = [a_2-s_2 a_0-b_1(s_1+s_2)]/(1+s_1+s_2). (R14) + +The last product MUST be retained. Even in one dimension, division by +1+2z+O(z^4) produces a quadratic term. For example the second covariance +derivative is -1+2L^2 z-4L^2 z^2+O(z^3), not its linear part plus O(z^4). +This clarification does not change the first variation accepted in Math-#144. + +For the deep images define T_6=sum_(|n|^2>=2)|n|^6 z^(|n|^2). In dimension 3, +the j=1 shell has 20 non-nearest points, each with |n|^6<=27 and |n|^2>=2; +its contribution is <=540z^2. For j>=2 the successive ratio is bounded by +(3/2)^9 z^5<1/2, so the remaining contribution is at most + + 729 * 2 * 2^9 z^4 = 746496 z^4 < z^2. + +Thus T_6<541 z^2. The same bound holds in dimension 2 by embedding Z^2 in Z^3. +It follows that |a_2-s_2 a_0|<=B_0 T_6 and |b_1|<=6B_0 z. Combining (R14) +with S-1<=1458z gives the explicit contraction bound + + |J_24-J_ref-J_24^(1)| < (541+6*1458) B_0 z^2 + =9289 B_0 z^2. (R15) + +Here J_24^(1) includes the nearest-image normalizer subtraction; it is not just +the raw six-image numerator. By the same full-matrix and reference-floor +conversion as (R11), its covariance remainder R_0 satisfies + + ||C_0^(-1/2) R_0 C_0^(-1/2)|| + < 60*9289 B_0*10^(-250) =: rho_0. (R16) + +## 7. Combine the bounds and determine the sign + +Use Taylor's formula (R8) with the FULL exact Delta=C_24-C_0, then split its +linear term into the nearest normalized variation and R_0. Equations (R9), +(R11), (R16), and the first variation (R2) give + + |c_(d,24)/c_(d,ref)-1-P_d(24)z| + < 2000 e_0^2+(29/3)rho_0 = R_rat, + + R_rat = [2000(87480 B_0)^2+580*9289 B_0]10^(-250) + < 10^(-216). (R17) + +All constants in (R17) are explicit integers/rationals and checked without +floating point. This proves the candidate (R1). The weaker lower bound +z>10^(-126) follows from exp(16/7)<10, proved by a positive Taylor polynomial +through degree 40 plus its geometric tail. Both |P_2(24)|10^(-126) and +|P_3(24)|10^(-126) exceed R_rat, so both full relative corrections are negative. + +For tighter displayed rational intervals the checker encloses exp(9/32) by +its degree-100 positive Taylor sum and an exact geometric remainder, takes +reciprocals, and squares ten times, rounding outwards on a 10^(-260) rational +grid. Since 1024*(9/32)=288, this encloses z. Multiplication by the NEGATIVE +P_d reverses endpoints; subtraction/addition of R_rat then encloses the full +relative correction. No floating-point comparison supplies proof evidence. + +## 8. Verification, interpretation, and review request + +Local test-first evidence: all 11 tests failed at the intended missing- +implementation assertion before check.py existed. After implementation, the +11 tests pass. Replays in normal and optimized Python and six semantic +mutants are recorded separately; RESULTS.json is deterministic output. +Finite controls check the rational ledgers and analytic calibrations only. +They do not prove differentiation under the integral, radial disintegration, +angular invariance, or the infinite lattice estimate; those are the arguments +above and are the nonauthor review obligations. + +Primary external reconnaissance: Voigtlaender's generalized Price theorem +supports covariance smoothness for Gaussian pairings with tempered distributions, +which includes polynomially growing weights supported on a linear subspace. +The explicit constants here are derived directly and are not attributed to that +paper. Full bibliographic details and the unsuccessful Consensus request are in +RECONNAISSANCE.md. No novelty claim is made. + +Requested non-OpenAI review slices: +A. Fixed-subspace representation (R3)-(R4), radial moments and Taylor bound (R5)-(R9). +B. Haar first-variation projection versus the FULL anisotropic second-order bound. +C. Deep-shell and normalization ledger (R14)-(R17), outward intervals and sign. +The parent remains an imported source, not something this author has independently +re-reviewed. Same GitHub account as the other lanes; zero organizational- +independence credit. No status transition or merge is requested before review. diff --git a/coefficients/side24_remainder_20260929/RECONNAISSANCE.md b/coefficients/side24_remainder_20260929/RECONNAISSANCE.md new file mode 100644 index 000000000..932885907 --- /dev/null +++ b/coefficients/side24_remainder_20260929/RECONNAISSANCE.md @@ -0,0 +1,53 @@ +# External reconnaissance — covariance differentiation and SIDE24 remainder + +Object: OA-SIDE24-REMAINDER-RECON-20260929-v1. +Research performed 29 September 2026 by OpenAI / GPT-6 Astra Pro. +Scientific effect NONE. This is an attribution and search-limit record, not novelty certification. + +## Executed primary-source search + +Web query: `site.arxiv.org 1710.03576 general version Price theorem Voigtlaender`. +Primary records returned and inspected: + +- Felix Voigtlaender, *A General Version of Price's Theorem: A Tool for Bounding + the Expectation of Nonlinear Functions of Gaussian Random Vectors*, Journal of + Theoretical Probability 34 (2021), 1474-1485; published online 26 June 2020. + DOI: https://doi.org/10.1007/s10959-020-01017-w + Publisher full-text record: https://link.springer.com/article/10.1007/s10959-020-01017-w + Preprint: https://arxiv.org/abs/1710.03576 (first submitted 10 October 2017). + +Theorem 1 permits tempered-distribution pairings with centered Gaussian densities +and proves smooth covariance dependence. Our fixed-subspace weighted measure is +one such distribution. We instead differentiate the density explicitly to obtain +the particular norm constants and radial moments needed here. That theorem does +not supply our numerical SIDE24 error bound, the first-variation polynomial, +or an independent review of the project's persistence parent. + +No PDF figures, tables, or numerical plots are used; the publisher HTML theorem +statement and arXiv abstract establish this attribution. The paper is not invoked +as a replacement for the proof's direct dominated-differentiation argument. + +## Consensus attempt and limitation + +Consensus.search was invoked for Gaussian-field critical points, persistence +small lifetimes, near-diagonal asymptotics, factorial moments and Palm distributions. +It returned: "You've used all 30 searches this month. Resets October 1." +No Consensus paper was retrieved, so no completed Consensus literature review or +Consensus-derived novelty conclusion is claimed. The primary-source web search +above was the available fallback. + +## Adjacent bibliographic check shared with the literature lane + +Query: `site.cambridge.org "Wave-length and amplitude in Gaussian noise" Lindgren`. +The Cambridge publisher record and Lund University bibliography confirm: +Georg Lindgren, *Wave-length and amplitude in Gaussian noise*, Advances in Applied +Probability 4(1), April 1972, 81-108, DOI https://doi.org/10.2307/1425807. +Lund record: https://lup.lub.lu.se/record/1273129 +The publisher abstract concerns the following minimum after a randomly chosen +maximum and amplitude approximations for certain stationary Gaussian processes. +The 2016 online date is digitization, not the original publication year. +This is different from his 1972 high-maximum paper in volume 23, pages 293-326. + +Only the abstract and bibliography were checked, not that article's full proofs. +No claim is made that it contains or excludes a small-amplitude exponent -1/3. +The 1D prior-art question in Math-#147 therefore remains open. diff --git a/coefficients/side24_remainder_20260929/RESULTS.json b/coefficients/side24_remainder_20260929/RESULTS.json new file mode 100644 index 000000000..14fd5a394 --- /dev/null +++ b/coefficients/side24_remainder_20260929/RESULTS.json @@ -0,0 +1,36 @@ +{ + "correction_intervals": { + "2": { + "P_d_24": "-26045568", + "lower": "-21823431753268467426071399866208918278029905772768723599074002096620834711250642998010691932810095748094113421353305882126703204065182781296896e-260", + "upper": "-21823431753268467426071399866208918278029905772768723599074002096620834711250642998010691932810095683522799147022431207389568244956782755251328e-260" + }, + "3": { + "P_d_24": "-620813376/35", + "lower": "-14862170290658276072289278509316668032944472474170149096001945201177806734752060983236082834190337617567163232433420950347509773086903002385003e-260", + "upper": "-14862170290658276072289278509316668032944472474170149096001945201177806734752060983236082834190337552995848958102546275610374813978502984647477e-260" + } + }, + "groups": [ + "density-scores-and-homogeneity", + "nearest-image-first-variation", + "infinite-shells-and-normalization", + "remainder-and-negative-sign" + ], + "mutants": [ + "ambient-as-free", + "drop-cone-degree", + "hessian-sign", + "omit-normalizer", + "shell-q4", + "firstvar-sign" + ], + "object": "OA-SIDE24-REMAINDER-20260929-v1", + "passed": true, + "relative_remainder_bound": "< 1e-216 (d=2,3; L=24)", + "relative_remainder_rational": "161428285685827186686842837397771/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "scientific_acceptance": false, + "scientific_effect": "NONE", + "scope": "finite rational controls; continuum proof and nonauthor review separate", + "taylor_majorant": "25300000/19683" +} diff --git a/coefficients/side24_remainder_20260929/SOURCES.json b/coefficients/side24_remainder_20260929/SOURCES.json new file mode 100644 index 000000000..aa1246447 --- /dev/null +++ b/coefficients/side24_remainder_20260929/SOURCES.json @@ -0,0 +1,91 @@ +{ + "author": "OpenAI / GPT-6 Astra Pro", + "comparison_not_runtime_dependency": { + "commit": "6cfc8c7503c55d9e2b095fc1fd7cafcacac1305d", + "path": "frontiers/side24_periodization_20260929/PROOF.md", + "pr": 144, + "role": "reviewed d=3 first variation; independently rederived here", + "sha256": "745493e5e69fa794c44f07fce18c4fc3782ab31a5843184caff860254ffe33aa" + }, + "disposition": "AUTHOR_SIDE_ANALYTIC_CANDIDATE", + "execution_boundary": "Local standalone arithmetic/unit tests executed; upstream file readback through connector. Whole-repository execution must be provided by hosted checks, not presumed from local tests.", + "files": [ + { + "bytes": 14776, + "path": "PROOF.md", + "sha256": "f96dabac211d62ff9a6bd33eddeba63f04fe09a618d09994e0de2ee18e6c130b" + }, + { + "bytes": 3049, + "path": "RECONNAISSANCE.md", + "sha256": "86be2dd2542704241b4920c09ab9541ef770aef015ce91097e14ed21976fdef3" + }, + { + "bytes": 1749, + "path": "RESULTS.json", + "sha256": "67829b75cf5712bd78853d05e9a85d210b4ddca47d99a09f35af2c01fcf52611" + }, + { + "bytes": 9322, + "path": "check.py", + "sha256": "68e07112f4c7d85c7c071b52bc654abb6e83a988771a0fb8d345e77a5802452c" + }, + { + "bytes": 6107, + "path": "test_check.py", + "sha256": "a231822c2c94aeaa9ed3fe82e67cc127e80fc8e44ceb34d47b1a5b1f0073ee06" + } + ], + "object": "OA-SIDE24-REMAINDER-20260929-v1", + "organizational_independence_credit": 0, + "scientific_acceptance": false, + "scientific_effect": "NONE", + "upstream": [ + { + "commit": "e1ca400b3414e5a7bec13b91bc4f1e5293df32be", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "repository": "d6g8k5htny-coder/Math-", + "role": "coefficient expression (15.2)", + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7" + }, + { + "commit": "e1ca400b3414e5a7bec13b91bc4f1e5293df32be", + "git_blob": "0633aca3c2a2882b0de4399da0a75d64c2e6b2e1", + "path": "imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md", + "repository": "d6g8k5htny-coder/Math-", + "role": "retained parent reading-rule context, not re-proved", + "sha256": "0bf922b9203c29088b12388807aa0e2ecd020485eb0f6e919679841b5b2636fc" + }, + { + "commit": "e1ca400b3414e5a7bec13b91bc4f1e5293df32be", + "git_blob": "213594d6ca6a86fb938110f4d166d9ce275a02d0", + "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "repository": "d6g8k5htny-coder/Math-", + "role": "retained parent amendment E1", + "sha256": "bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028" + }, + { + "commit": "e1ca400b3414e5a7bec13b91bc4f1e5293df32be", + "git_blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", + "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "repository": "d6g8k5htny-coder/Math-", + "role": "retained parent amendment E2", + "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f" + }, + { + "commit": "e1ca400b3414e5a7bec13b91bc4f1e5293df32be", + "git_blob": "75da2597971510f843f8d90c743950cb8c177342", + "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "repository": "d6g8k5htny-coder/Math-", + "role": "reading rule, E3 and scoped source interpretation" + }, + { + "commit": "e1ca400b3414e5a7bec13b91bc4f1e5293df32be", + "git_blob": "44b66f04f89fcd87383b3603fa69f1feb64cdddd", + "path": "coefficients/side24_v1/PROOF.md", + "repository": "d6g8k5htny-coder/Math-", + "role": "reference covariance floor and all-direction image bound" + } + ] +} diff --git a/coefficients/side24_remainder_20260929/check.py b/coefficients/side24_remainder_20260929/check.py new file mode 100644 index 000000000..dbcd70b8d --- /dev/null +++ b/coefficients/side24_remainder_20260929/check.py @@ -0,0 +1,242 @@ +#!/usr/bin/env python3 +"""Exact finite controls for OA-SIDE24-REMAINDER-20260929-v1. + +These controls check the arithmetic of PROOF.md, not its continuum arguments. +No nonauthor acceptance or formal verification is asserted. Standard library only. +""" +import argparse +from fractions import Fraction as F +import hashlib +import json +from pathlib import Path +import sys + +MUTANTS = ('ambient-as-free', 'drop-cone-degree', 'hessian-sign', + 'omit-normalizer', 'shell-q4', 'firstvar-sign') + + +def exact(x): + if isinstance(x, bool) or not isinstance(x, (int, F)): + raise TypeError('exact integer or Fraction required') + return F(x) + + +def dimensions(d): + if isinstance(d, bool) or not isinstance(d, int) or d < 2: + raise ValueError('integer dimension d >= 2 required') + m = d-1 + n = d+1+d*(d+1)//2 + k = 1+m*(m+1)//2 + p = F(4, 3)+2*m + return n, k, p, k+p + + +def scalar_score_moments(d, curvature_sign=-1): + n, _, _, nu = dimensions(d) + first = (nu-n)/2 + second = (nu*(nu+2)-2*n*nu+n*n)/4+F(n,2)+curvature_sign*nu + return first, second + + +def score_majorant(d): + n, _, _, nu = dimensions(d) + return (n*n+2*n*nu+nu*(nu+2))/4+F(n,2)+nu + + +def taylor_constant(): + return F(1,2)*score_majorant(3)*F(16,9)*F(3125,243) + + +def projected_first_variation(d): + dimensions(d) + # Coefficients of L^2, L^4, L^6 in the projected nearest-image jets. + da = (F(-2), F(0), F(0)) + dm4 = (F(-12), F(6,d+2), F(0)) + dchi = (F(-90), F(90,d+2), F(-30,(d+2)*(d+4))) + return tuple((1-F(d,2))*a+(F(d,6)-1)*b+c/9 + for a,b,c in zip(da,dm4,dchi)) + + +def closed_first_variation(d): + dimensions(d) + return (F(-d), F(d+4,d+2), F(-10,3*(d+2)*(d+4))) + + +def first_variation_at(d, L): + L = exact(L) + return sum(c*L**(2*(j+1)) for j,c in enumerate(closed_first_variation(d))) + + +def normalize_linear(a0, a1, s1): + a0,a1,s1 = map(exact,(a0,a1,s1)) + return a0, a1-s1*a0, s1*s1*a0-s1*a1 + + +def exp_bounds(x, terms): + """Positive Taylor sum through terms, plus an exact geometric tail.""" + x = exact(x) + if isinstance(terms,bool) or not isinstance(terms,int) or terms < 0 or x < 0: + raise ValueError('nonnegative argument and integer truncation required') + ratio = x/(terms+2) + if ratio >= 1: + raise ValueError('tail ratio must be below one') + term = F(1) + total = term + for j in range(1,terms+1): + term *= x/j + total += term + following = term*x/(terms+1) + return total, total+following/(1-ratio) + + +def outward(x, places): + x = exact(x) + if isinstance(places,bool) or not isinstance(places,int) or places < 0: + raise ValueError('nonnegative integer precision required') + scale = 10**places + scaled = x*scale + a = scaled.numerator//scaled.denominator + b = -((-scaled.numerator)//scaled.denominator) + return F(a,scale),F(b,scale) + + +def q_interval(terms=100, places=260): + """Outward interval for exp(-288): exp(-9/32) raised to 1024.""" + elo,ehi = exp_bounds(F(9,32),terms) + lo = outward(1/ehi,places)[0] + hi = outward(1/elo,places)[1] + for _ in range(10): + lo = outward(lo*lo,places)[0] + hi = outward(hi*hi,places)[1] + return lo,hi + + +def image_bounds(include_normalizer=True, deep_power=2): + B = 76*24**6+15 + z = F(1,10**125) + E = 1458*B*z + normalizer = 6*1458 if include_normalizer else 0 + remainder = 541+normalizer + return {'B':B, 'E':E, 'epsilon':60*E, + 'deep_shell_coefficient':541, + 'normalization_coefficient':normalizer, + 'remainder_coefficient':remainder, + 'rho':60*remainder*B*z**deep_power} + + +def remainder_bound(): + data = image_bounds() + return 2000*data['epsilon']**2+F(29,3)*data['rho'] + + +def correction_interval(d): + if d not in (2,3) or isinstance(d,bool): + raise ValueError('certified remainder only for dimensions 2 and 3') + qlo,qhi = q_interval() + P = first_variation_at(d,24) + if P >= 0: + raise ValueError('negative first variation required for this interval order') + R = remainder_bound() + return outward(P*qhi-R,260)[0],outward(P*qlo+R,260)[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def verify(mutant=None): + if mutant not in (None,*MUTANTS): + raise ValueError('unknown mutant') + groups = [] + for d in (2,3): + n,k,p,nu = dimensions(d) + n = k if mutant == 'ambient-as-free' else n + nu = k+F(4,3) if mutant == 'drop-cone-degree' else nu + require((nu-n)/2 == F(-1,3), 'ambient/free/homogeneity scaling mismatch') + first,second = scalar_score_moments(d, 1 if mutant == 'hessian-sign' else -1) + require((first,second)==(F(-1,3),F(4,9)), 'density second derivative mismatch') + require(score_majorant(3)==F(1012,9), 'radial fourth moment / majorant mismatch') + require(taylor_constant()<2000, 'Taylor constant exceeds allowance') + groups.append('density-scores-and-homogeneity') + for d in range(2,21): + require(projected_first_variation(d)==closed_first_variation(d), 'projection/chain mismatch') + P3 = first_variation_at(3,24)*(-1 if mutant=='firstvar-sign' else 1) + require(P3==F(-620813376,35), 'first variation sign or coefficient mismatch') + require(first_variation_at(2,24)==-26045568, 'planar first variation mismatch') + groups.append('nearest-image-first-variation') + q_upper = F(1,10**125) + require(exp_bounds(F(288,125),20)[0]>10, 'q upper bracket unproved') + require(exp_bounds(F(16,7),40)[1]<10, 'q lower bracket unproved') + require(512*q_upper**3R, 'coarse sign margin fails') + corrections[str(d)]={'P_d_24':str(first_variation_at(d,24)), + 'lower':str(int(lo*10**260))+'e-260', + 'upper':str(int(hi*10**260))+'e-260'} + groups.append('remainder-and-negative-sign') + return {'object':'OA-SIDE24-REMAINDER-20260929-v1', + 'passed':True, 'groups':groups, 'mutants':list(MUTANTS), + 'scope':'finite rational controls; continuum proof and nonauthor review separate', + 'scientific_effect':'NONE', 'scientific_acceptance':False, + 'taylor_majorant':str(taylor_constant()), + 'relative_remainder_rational':str(R), + 'relative_remainder_bound':'< 1e-216 (d=2,3; L=24)', + 'correction_intervals':corrections} + + +def verify_sources(repo): + here = Path(__file__).resolve().parent + manifest = json.loads((here/'SOURCES.json').read_text(encoding='utf-8')) + expected = {row['path'] for row in manifest['files']}|{'SOURCES.json'} + require({p.name for p in here.iterdir()}==expected, 'packet file inventory mismatch') + for row in manifest['files']: + path = here/row['path'] + require(Path(row['path']).name==row['path'] and not path.is_symlink(), 'regular flat packet source required') + data = path.read_bytes() + require(len(data)==row['bytes'] and hashlib.sha256(data).hexdigest()==row['sha256'], + 'packet source identity mismatch: '+row['path']) + root = Path(repo).resolve() + for row in manifest['upstream']: + rel = Path(row['path']) + require(not rel.is_absolute() and '..' not in rel.parts, 'relative upstream path required') + path = root/rel + require(not path.is_symlink() and path.resolve().is_relative_to(root), 'upstream path escapes repository') + data = path.read_bytes() + blob = hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() + require(blob==row['git_blob'], 'upstream Git blob mismatch: '+row['path']) + if 'sha256' in row: + require(hashlib.sha256(data).hexdigest()==row['sha256'], 'upstream SHA256 mismatch') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--mutant',choices=MUTANTS) + parser.add_argument('--verify-sources',metavar='REPOSITORY_ROOT') + args = parser.parse_args() + try: + report = verify(args.mutant) + if args.verify_sources: + verify_sources(args.verify_sources) + report['source_manifest_verified'] = True + print(json.dumps(report,sort_keys=True,indent=2)) + return 0 + except (ValueError,TypeError,KeyError,OSError) as exc: + print('REJECTED: '+str(exc),file=sys.stderr) + return 1 + +if __name__=='__main__': + sys.exit(main()) diff --git a/coefficients/side24_remainder_20260929/test_check.py b/coefficients/side24_remainder_20260929/test_check.py new file mode 100644 index 000000000..6ba7f0afc --- /dev/null +++ b/coefficients/side24_remainder_20260929/test_check.py @@ -0,0 +1,138 @@ +"""Regression tests for the additive SIDE24 remainder candidate (stdlib only).""" +import importlib.util +import json +from pathlib import Path +import subprocess +import sys +import unittest +from fractions import Fraction as F + +HERE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location("side24_remainder_check", HERE / "check.py") +MOD = None +if SPEC is not None and (HERE / "check.py").is_file(): + MOD = importlib.util.module_from_spec(SPEC) + SPEC.loader.exec_module(MOD) + +class RemainderTests(unittest.TestCase): + def setUp(self): + self.assertIsNotNone(MOD, "Missing exact remainder implementation check.py") + + def test_dimensions_and_homogeneity(self): + self.assertEqual(MOD.dimensions(2), (6, 2, F(10, 3), F(16, 3))) + self.assertEqual(MOD.dimensions(3), (10, 4, F(16, 3), F(28, 3))) + for d in range(2, 13): + n, k, p, nu = MOD.dimensions(d) + self.assertEqual((nu-n)/2, F(-1, 3)) + self.assertEqual(n-k, 2*d) + + def test_density_score_scalar_covariance_calibration(self): + for d in (2, 3, 7): + first, second = MOD.scalar_score_moments(d) + self.assertEqual(first, F(-1, 3)) + self.assertEqual(second, F(4, 9)) + + def test_second_derivative_majorant(self): + self.assertEqual(MOD.score_majorant(3), F(1012, 9)) + self.assertLessEqual(MOD.score_majorant(2), MOD.score_majorant(3)) + expected = F(1, 2)*F(1012, 9)*F(16, 9)*F(3125, 243) + self.assertEqual(MOD.taylor_constant(), expected) + self.assertLess(expected, 2000) + + def test_first_variation_polynomial_all_fixed_dimensions(self): + for d in range(2, 21): + self.assertEqual(MOD.projected_first_variation(d), MOD.closed_first_variation(d)) + self.assertEqual(MOD.closed_first_variation(2), (F(-2), F(3,2), F(-5,36))) + self.assertEqual(MOD.closed_first_variation(3), (F(-3), F(7,5), F(-2,21))) + self.assertEqual(MOD.first_variation_at(3,24), F(-620813376,35)) + self.assertEqual(MOD.first_variation_at(2,24), F(-26045568)) + + def test_normalization_generates_second_order_term(self): + L=24 + self.assertEqual(MOD.normalize_linear(F(-1),2*(L*L-1),F(2)), + (F(-1),F(2*L*L),F(-4*L*L))) + # Formal-series multiplication, independent of any numerical q. + a0,a1,s=F(5,7),F(-3,2),F(4,3) + c0,c1,c2=MOD.normalize_linear(a0,a1,s) + self.assertEqual((c0,c1+s*c0,c2+s*c1),(a0,a1,F(0))) + + def test_image_bounds_include_normalizer(self): + z=F(1,10**125) + data=MOD.image_bounds() + self.assertEqual(data['B'],76*24**6+15) + self.assertEqual(data['E'],F(21175738586478,10**125)) + self.assertEqual(data['deep_shell_coefficient'],541) + self.assertEqual(data['normalization_coefficient'],6*1458) + self.assertEqual(data['remainder_coefficient'],541+6*1458) + self.assertLess(746496*z*z,1) + self.assertLess(F(3,2)**9*z**5,F(1,2)) + self.assertLess(512*z**3,F(1,2)) + + def test_exponential_bounds_prove_decimal_brackets(self): + lo,_=MOD.exp_bounds(F(288,125),20) + _,hi=MOD.exp_bounds(F(16,7),40) + self.assertGreater(lo,10) + self.assertLess(hi,10) + qlo,qhi=MOD.q_interval() + self.assertGreater(qlo,F(1,10**126)) + self.assertLess(qhi,F(1,10**125)) + self.assertLess(qhi-qlo,F(1,10**250)) + # Independent larger Taylor truncation must overlap the certified interval. + elo,ehi=MOD.exp_bounds(F(9,32),110) + exact_lo=(1/ehi)**1024 + exact_hi=(1/elo)**1024 + self.assertLessEqual(qlo,exact_hi) + self.assertGreaterEqual(qhi,exact_lo) + + def test_final_bound_and_sign(self): + data=MOD.image_bounds() + expected=2000*data['epsilon']**2+F(29,3)*data['rho'] + self.assertEqual(MOD.remainder_bound(),expected) + self.assertGreater(expected,0) + self.assertLess(expected,F(1,10**216)) + for d in (2,3): + lo,hi=MOD.correction_interval(d) + self.assertLess(lo,hi) + self.assertLess(hi,0) + self.assertGreater(lo,F(-1,10**117)) + self.assertLess(hi,F(-1,10**119)) + + def test_outward_grid_in_both_signs(self): + for x in (F(1,3), F(-1,3), F(0), F(17,5)): + lo,hi=MOD.outward(x,20) + self.assertLessEqual(lo,x) + self.assertGreaterEqual(hi,x) + self.assertLessEqual(hi-lo,F(1,10**20)) + + def test_invalid_inputs_fail_closed(self): + for value in (True,1.5,'1',None): + with self.assertRaises((TypeError,ValueError)): + MOD.exact(value) + for d in (True,1,0,-1,F(3,2)): + with self.assertRaises((TypeError,ValueError)): + MOD.dimensions(d) + with self.assertRaises(ValueError): + MOD.exp_bounds(F(-1),10) + with self.assertRaises(ValueError): + MOD.exp_bounds(F(20),2) + + def test_cli_both_modes_and_semantic_mutants(self): + outputs=[] + for flags in (['-B','-S'],['-B','-O','-S']): + proc=subprocess.run([sys.executable,*flags,str(HERE/'check.py')],capture_output=True,check=False,timeout=30) + self.assertEqual(proc.returncode,0,proc.stderr.decode()) + data=json.loads(proc.stdout) + self.assertTrue(data['passed']) + self.assertFalse(data['scientific_acceptance']) + outputs.append(proc.stdout) + for mutant in MOD.MUTANTS: + bad=subprocess.run([sys.executable,*flags,str(HERE/'check.py'),'--mutant',mutant],capture_output=True,timeout=30) + self.assertEqual(bad.returncode,1,(mutant,bad.stdout,bad.stderr)) + unknown=subprocess.run([sys.executable,*flags,str(HERE/'check.py'),'--mutant','UNKNOWN'],capture_output=True,timeout=30) + self.assertEqual(unknown.returncode,2) + self.assertEqual(outputs[0],outputs[1]) + if (HERE/'RESULTS.json').is_file(): + self.assertEqual(outputs[0],(HERE/'RESULTS.json').read_bytes()) + +if __name__=='__main__': + unittest.main()