From 771913a7dffdc1283e491166d0faa9ec53e1f06a Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 20:54:30 -0700 Subject: [PATCH] LM006: conditional sign-band integration and cubic saddle-sign bound Four additive analytic and exact-test files only. Preserve all existing proofs, Lean sources, gates, workflows and scientific registers. Dylan Roy delegated work; actual author OpenAI / GPT-6 Astra Pro, round18-cubic-sign-band-audit-20261006. Scientific effect NONE; new nonauthor review pending. --- .../lm006_cubic_sign_band_20261006/NOTE.md | 314 ++++++++++++++++++ .../SOURCES.json | 74 +++++ .../cubic_band.py | 218 ++++++++++++ .../test_cubic_band.py | 103 ++++++ 4 files changed, 709 insertions(+) create mode 100644 reviews/lm006_cubic_sign_band_20261006/NOTE.md create mode 100644 reviews/lm006_cubic_sign_band_20261006/SOURCES.json create mode 100644 reviews/lm006_cubic_sign_band_20261006/cubic_band.py create mode 100644 reviews/lm006_cubic_sign_band_20261006/test_cubic_band.py diff --git a/reviews/lm006_cubic_sign_band_20261006/NOTE.md b/reviews/lm006_cubic_sign_band_20261006/NOTE.md new file mode 100644 index 000000000..88dae06c5 --- /dev/null +++ b/reviews/lm006_cubic_sign_band_20261006/NOTE.md @@ -0,0 +1,314 @@ +# LM006: conditional sign-band integration and a cubic saddle-sign bound + +Dylan Roy — delegated AI mathematical work. Actual author OpenAI / GPT-6 +Astra Pro, session `round18-cubic-sign-band-audit-20261006`. +Scientific effect NONE. This is an additive analytic companion, not a Lean +formalization, a replacement of a historical proof, or program acceptance. + +## 1. Scope, exact predecessors, and what is additional + +Use the six adjusted endpoint coordinates from #301 and the exact typed +weight from #315, with the conventions of #318/#325: + + v=(a_minus,a_plus,b_minus,b_plus,c_minus,c_plus), + T_r(v)=[(a_minus)_- (c_minus)_- - r b_minus^2]_+ + [r b_plus^2-a_plus c_plus]_+, 0<=r<=1. (1) + +Here x_+=max(x,0), x_-=max(-x,0). For physical r>0, T_r=W_r/r^2. +Let E={c_plus>=0}; this is the SADDLE transverse sign, not the sign already +forced at the maximum. Write z_r=E_Qr T_r and nu_r(E)=E_Qr[T_r 1_E]/z_r. +Qr is the original Gaussian pin law; it has no additional good-event +conditioning. No pin density or coordinate Jacobian is inserted into z_r. + +The #325 moment-only estimate is of order r e+e^4, hence O(r^2) when a +valid coupling error satisfies e=O(r). We add a CONDITIONAL density bound +for the scalar c_plus after all other endpoint coordinates are specified. +Integrating the actual sign interval yields order r e^2+e^5 and hence O(r^3). +Marginal density, full density at each positive r, and bounded covariance +alone do not imply the uniform conditional-density premise. + +Prior-work credit is essential: P, `UNIFORM_MATRIX_CAP_AND_LIFETIME.md`, +sections 6–7, already uses two soft determinant factors and a boundary-layer +width to produce the cubic power, including its separate scalar case. This +note is not the first cubic soft-layer argument or a new generic Gaussian +regression method. It supplies the explicit one-dimensional endpoint-band +formula, a sufficient 11-observation confluent Gram proof using a finite tenth +spectral moment, and the source-matched consequence for this particular sign +event. P's global selection and lifetime theorems are NOT premises here. +Neither #329's weaker-regularity rate nor #333's application is rewritten. + +## 2. Exact deterministic band and its Lebesgue integral + +Put t=c_plus, g=c_plus-c_minus, so c_minus=t-g. Hold +h=(a_minus,a_plus,b_minus,b_plus,g) fixed. On E and positive typed weight, +necessarily a_minus<0 and 0<=t=0} + <= |a_minus| (g_+-t)(r b_plus^2+(a_plus)_- t) + 1_{0<=t<=g_+}. (2) + +Indeed the first positive part in (1) is at most +|a_minus|(g-t) on its support; the second is at most +r b_plus^2+(a_plus)_-t for t>=0. At either type boundary the determinant +weight is zero, so no boundary mass is removed in (2). + +Integrating the nonnegative quadratic polynomial gives + + int_0^infty T_r(h,t) dt + <= |a_minus| [r b_plus^2 g_+^2/2 + +(a_plus)_- g_+^3/6]. (3) + +The two coefficients are individually sharp for this envelope: with +b_minus=0 and a_plus=0 the first integral is exactly the first term; with +b_minus=b_plus=0 and a_plus<0 it is exactly the second term. These witnesses +work at positive r as well. This does not assert simultaneous sharpness of +all later Gaussian constants or sharpness for a particular field. + +## 3. Conditional density is the load-bearing new hypothesis + +Let X be any measurable R6-valued random vector and +H=(X_a_minus,X_a_plus,X_b_minus,X_b_plus,G), G=X_c_plus-X_c_minus. +Assume the conditional law of X_c_plus given H has a Lebesgue density +f(t|H)<=L almost everywhere for a fixed finite L. All expectations in this +section are under the SAME law of X. Disintegration and Tonelli, followed +by (3), give + + N_r:=E[T_r(X)1_E] + <= L { (r/2) E[|X_a_minus| X_b_plus^2 G_+^2] + +(1/6) E[|X_a_minus| (X_a_plus)_- G_+^3] }. (4) + +This holds as an extended nonnegative inequality; the following moment +assumptions make its right-hand side finite. No independence is assumed. + +One cannot substitute a bound on the marginal density of X_c_plus. For a +rational counterexample, take t uniform on [0,1], g=3t/2, a_minus=a_plus=-1, +and b_minus=b_plus=0. Then T=t^2/2, so N=1/6. Inserting the marginal density +cap L=1 into the proposed right-hand side gives E[g^3]/6=9/64<1/6. +H determines t; its conditional law has no density. This example is not a +Gaussian field. Even for Gaussian variables, a nonsingular marginal can +become deterministic after conditioning on a correlated coordinate. + +## 4. Explicit Gaussian-error consequence + +Define U=X_a_plus-1, u2=E U^2, g2=E G^2, +K2=E X_a_minus^2, K6=E[X_a_minus^2 X_b_plus^4]. Assume K2,K6 finite and +U,G individually Gaussian, possibly noncentered, degenerate and dependent. +The elementary inequality (x)_- <= (x-1)^2/4 gives + + N_r <= L [ (sqrt(3 K6)/2) r g2 + +(105*10395)^(1/4) sqrt(K2) u2 g2^(3/2)/24 ]. (5) + +Details of the moment step, without independence: + + E[|X_a_minus| X_b_plus^2 G_+^2] + <= sqrt(K6) sqrt(E G^4) <= sqrt(3 K6) g2, + E[|X_a_minus| U^2 |G|^3] + <= sqrt(K2) (E U^4 G^6)^(1/2) + <= sqrt(K2) (E U^8 E G^12)^(1/4) + <= (105*10395)^(1/4) sqrt(K2) u2 g2^(3/2). + +For any real Gaussian Z=m+sZ0, its binomial even-moment expansion implies +E Z^(2k) <= (2k-1)!! (E Z^2)^k. Coefficientwise, the ratio of the j-th +variance coefficient to the corresponding upper coefficient is +1/(2(k-j)-1)!!<=1, with (-1)!!=1. The needed constants are 3,105,10395 +for orders 4,8,12. Thus (5) also covers zero variances and nonzero means. + +Now assume a specified coupling to Y with Y_a_plus=1 and Y_c_plus=Y_c_minus +almost surely, and e^2=E||X-Y||^2. Then u2<=e^2 and g2<=2e^2, so + + N_r <= L [sqrt(3 K6) r e^2 + +(105*10395)^(1/4) sqrt(2 K2) e^5/12]. (6) + +If 00. + +This is the eleven-observation residual variance, not the variance of Q_L +conditioned only on the six contact pins used to define z0 below. + +For h=r/2>0 consider the 11 observations + + O_r=(F(-h),F'(-h),F''(-h), F(h),F'(h),F''(h), + H_y(-h),H_y'(-h),H_y(h),H_y'(h), Q(h)-Q(-h)). (8) + +These are exactly the six raw pins together with the four axial/mixed +Hessian entries and the transverse difference, up to permutation and +nonzero scaling/subtraction of known pin rows. They do NOT include Q(h) +as an extra conditioned observation. Conditioning first on the six pins +and then on H in section 3 is equivalent to conditioning on (8). + +Here is an explicit invertible transformation removing the coalescing +singularity. For m=3 or 2 define the fixed 2m by 2m real matrix + + V_m[(s,ell),j] = (d^ell/dt^ell t^j)|_{t=s}, + s=-1,+1; ell=0,...,m-1; j=0,...,2m-1. (9) + +It is invertible: a polynomial of degree <2m with all m derivatives +vanishing at both nodes would be divisible by (t-1)^m(t+1)^m, so is zero. +Use V_3 on the six F rows in (8), multiplying the ell-th observed derivative +by h^ell first. If c_j is the resulting coefficient after V_3^-1, set +R_j=j! h^-j c_j. Hilbert-space Taylor expansion gives, for ell<=2, + + h^ell F^(ell)(s h) + = sum_{j=ell}^5 [F^(j)(0) h^j/j!] V_3[(s,ell),j]+o(h^5). + +Thus R_j=F^(j)(0)+o(h^(5-j)) and all six rows converge in L2. +Apply the identical construction with m=2 to H_y and its first derivative; +the four rows converge to H_y^(j)(0), j=0,...,3. Divide the last row in (8) +by 2h to obtain convergence to Q'(0). The combined change of rows is +invertible for every h>0. Call the transformed vector R_r; then + + (R_r,Q(h)) -> (J11,Q(0)) in L2. (10) + +The 12 by 12 covariance matrices converge. Since the limiting one is +positive definite, its 11 by 11 observation block is invertible for small r, +and the scalar Schur complement is continuous and tends to sigma0^2. +Consequently + + Var(Q(h) | O_r) >= sigma0^2/2 (11) + +on a sufficiently small fixed interval. In a jointly Gaussian family this +conditional variance does not depend on the prescribed values. The canonical +conditional density of Q(h) is therefore bounded by + + L=(pi sigma0^2)^(-1/2). (12) + +The actual successive pin/endpoint conditionings in section 3 have precisely +this variance: their raw observations are related to O_r by the invertible +maps just described. Their means may depend on all prescribed values, but +a Gaussian density's supremum does not depend on its mean. The raw or scaled +six-endpoint covariance is not assumed uniformly invertible; several of its +eigenvalues may tend to zero. Equation (11) is a scalar residual statement +proved through the DIFFERENT rescaled observation frame R_r. + +## 6. Spectral-class and source-matched fixed-field corollaries + +Suppose the actual stationary covariance is + + C(z)=sum_{k in Z2} p_k exp(i nu k.z), + p_k>0, p_-k=p_k, nu>0, sum_k p_k(1+|nu k|^10)0 but make it vanish at contact; +the checker retains that countercontrol. + +Use the same axial pins as #301: F(-h)=b, F(h)=b-r^3/6 and both gradient +pins zero, with b=6/5. This is k=1/6 in P's convention. The #301 pin frame +has d_r=(b-r^3/12,0,0,0,0,2); after pinning, the adjusted axial/mixed Hessian +entries are precisely the physical entries divided by r. There is no switch +of endpoint coordinates or height-gap coefficient in applying (8). + +Under (13), the stronger derivative assumptions of #329 hold, so its +explicit common regression coupling gives e<=K_e r, bounded Gaussian means +and covariances, and z_r>=z0/2>0 on a sufficiently small interval. The same +marginals and coupling are used in (5)--(7). For example its moment bounds +supply C2=M^2+6Lambda and C6=32(M^6+480Lambda^3). The limiting contact +transverse Gaussian has positive variance by the 12-jet Gram, hence +z0=E(Q_L)_-^2>0. Intersect that interval with the one in (11) and r<=1. +Equation (7) proves the cubic sign bound for this spectral class. + +For P's actual periodized Gaussian field, specialize d=2, L=24 and nu=2pi/24. +P sections 1--2 specify exactly + + p_k=exp(-2pi^2|k|^2/24^2) / sum_j exp(-2pi^2|j|^2/24^2). + +These weights are strictly positive and have finite moments of every order; +thus (13) holds. This is a check of the actual model and pins, not an import +of P's global theorems. We obtain constants C0 such that + + nu_r{ f_yy(S)>=0 } <= C r^3, 00} nu_r(E)/r^3=5 phi(0)/3>0. (15) + +Thus an exponent strictly larger than 3 cannot hold for the entire abstract +Gaussian/density/coupling class. This rank-one Gaussian family is NOT claimed +to be an actual six-pin periodic field, or an actual-field lower asymptotic. +It establishes sharp order for the assumptions, not equality of any coarse +constant in (7). + +## 8. Reproduction, controls, and boundaries + +`python -B -S test_cubic_band.py` and its `-O` version run 12 methods. +`cubic_band.py` runs 2214 exact controls: 2160 band integrations, 40 Hermite +monomial recoveries, four conditional variances, four sharp cubic integrals +and six isolated witnesses. Its outputs are deterministic. The finite +Gaussian model uses independent coefficients of 15 explicitly defined +monomials. Exact Schur computation gives 1+h^4/4; deleting its constant Q +mode gives h^4/4, so positive-radius density alone does not supply a uniform +floor. It is not an evaluation of the infinite periodic covariance. + +M1--M6 must exit1 with the respective reasons BAND_R_COEFFICIENT, +BAND_CUBIC_COEFFICIENT, HERMITE_DERIVATIVE_SCALE, GAUSSIAN_TWELFTH, +CONDITIONAL_NOT_MARGINAL, MARGINAL_DENSITY_NOT_SUFFICIENT. Unknown arguments +exit2. Numerical checks are not proofs of the continuum claims. No existing +workflow automatically runs this new checker; no Lean target is added. + +General linear Gaussian conditioning is prior methodology. The primary +abstract record Majumdar--Majumdar, arXiv:1710.09285, was consulted as context, +not imported as an unread proof of (10)--(14). The finite covariance/Schur and +polynomial arguments above give the assumptions and derivation explicitly. +A fresh nonauthor review must inspect the new conditional-density step, +constants, exact pin correspondence, Gaussian moment use and exclusions. +All historical proof bytes, review dispositions and scientific flags remain +unchanged. In particular this does not repair the separate source-admission +gate or resolve missing independent formal alignment/provenance. diff --git a/reviews/lm006_cubic_sign_band_20261006/SOURCES.json b/reviews/lm006_cubic_sign_band_20261006/SOURCES.json new file mode 100644 index 000000000..eeceaceaa --- /dev/null +++ b/reviews/lm006_cubic_sign_band_20261006/SOURCES.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "scientific_effect": "NONE", + "author": { + "provider": "OpenAI", + "model": "GPT-6 Astra Pro", + "session": "round18-cubic-sign-band-audit-20261006" + }, + "files": { + "NOTE.md": { + "bytes": 15359, + "sha256": "21284fa5945752736483437a59e5c98477b9ded3e90c6107d1454bf5f3d8ce9c", + "git_blob": "88dae06c5eefd102239f976513eb5e97c4ac7580" + }, + "cubic_band.py": { + "bytes": 7865, + "sha256": "932a9ec1f038dce87e27007c917efa40cc07702e77e789a055ccacf5aa1e67cb", + "git_blob": "ea3225adc01311f6bd50e80c9d629c3c04b42345" + }, + "test_cubic_band.py": { + "bytes": 4983, + "sha256": "ab92fbd9d36a0342f0bd277e705b85286645c574afb6061b4e7814b30d66ff27", + "git_blob": "bd565daa715a3532f7b7d1e0e0a432ef2acef2f7" + } + }, + "sources": [ + { + "id": "P", + "repository": "d6g8k5htny-coder/Math-", + "commit": "b25cac0bcbb4032d624f14795257d9578c90d105", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "consumed": "sections1-2 model, pin convention, positive spectrum; sections6-7 prior-methodology credit only, no global theorem imported" + }, + { + "id": "E", + "repository": "d6g8k5htny-coder/Math-", + "commit": "e31b6ad8356e0760c8a7fb6e816ff640c45176c9", + "path": "reviews/lm006_endpoint_extension_20261005/NOTE.md", + "git_blob": "551aa563562bc88a19e33d146259c03aa2d318f6", + "consumed": "sections2-3 exact pin frame and adjusted coordinates" + }, + { + "id": "N", + "repository": "d6g8k5htny-coder/Math-", + "commit": "5e027afcae8c7bd42a6df8ae2025f82105b3e586", + "path": "reviews/lm006_normalizer_stability_20261005/NOTE.md", + "git_blob": "5790aaa0332bd8e79b276be1577e4c5f3502eed6", + "consumed": "exact normalized physical weight; new deterministic bound rederived" + }, + { + "id": "R", + "repository": "d6g8k5htny-coder/Math-", + "commit": "5b22d6f8d3335e2d863702fb7bbd75b5a891178e", + "path": "reviews/lm006_quantified_regression_20261005/NOTE.md", + "git_blob": "a58948d251abdb34b334e1a1da83ec8982de29dc", + "sha256": "b68e077adbfdc551e6211cf8e61aa2d98719f1de4f653abcdbd5d90c613a11b1", + "consumed": "sections2-5 specified RMS coupling and uniform Gaussian moments/normalized lower floor; published immutable source, not a claim of merge" + }, + { + "id": "S", + "repository": "d6g8k5htny-coder/Math-", + "commit": "1dfe801eb61a8335a2e42b886fca9b000fb3598c", + "path": "reviews/lm006_typed_sign_suppression_20261005/NOTE.md", + "git_blob": "9015971fa03f44ae99d410facc6f3d8c26cdc945", + "consumed": "prior r e+e^4 comparison only; not used to prove new band estimate" + } + ], + "external_context": { + "arxiv": "1710.09285", + "read": "abstract record only", + "role": "prior linear Gaussian conditioning; not proof premise" + } +} diff --git a/reviews/lm006_cubic_sign_band_20261006/cubic_band.py b/reviews/lm006_cubic_sign_band_20261006/cubic_band.py new file mode 100644 index 000000000..ea3225adc --- /dev/null +++ b/reviews/lm006_cubic_sign_band_20261006/cubic_band.py @@ -0,0 +1,218 @@ +#!/usr/bin/env python3 +"""Exact finite controls for the conditional cubic saddle-sign bound. + +Standard library only. These controls are not a continuum proof or Lean run. +""" +import argparse +from fractions import Fraction as F +import itertools +import json +from math import factorial, comb +import sys + + +def exact(value): + if type(value) not in (int,F): + raise TypeError('exact int or Fraction required') + return F(value) + + +def radius(value): + value=exact(value) + if not 0<=value<=1: + raise ValueError('radius must lie in [0,1]') + return value + + +def positive(value): + return max(F(0),value) + + +def weight(v,r): + v=tuple(map(exact,v)); r=radius(r) + if len(v)!=6: + raise ValueError('six endpoint coordinates required') + am,ap,bm,bp,cm,cp=v + return positive(positive(-am)*positive(-cm)-r*bm*bm)*positive(r*bp*bp-ap*cp) + + +def band_integral(am,ap,bm,bp,g,r): + """Exact Lebesgue integral of T_r over c_plus>=0 at fixed other coordinates.""" + am,ap,bm,bp,g=map(exact,(am,ap,bm,bp,g)); r=radius(r) + a=positive(-am) + if a==0 or g<=0: + return F(0) + f0=a*g-r*bm*bm + upper=positive(f0/a) + if ap>0: + upper=min(upper,r*bp*bp/ap) + # (f0-a*t)*(r*bp^2-ap*t) integrated to the first positive-part zero. + return f0*r*bp*bp*upper-(a*r*bp*bp+f0*ap)*upper**2/2+a*ap*upper**3/3 + + +def band_bound(am,ap,bp,g,r,mutant=None): + am,ap,bp,g=map(exact,(am,ap,bp,g)); r=radius(r) + a=abs(am); g=positive(g) + c2=4 if mutant=='M1' else 2 + c3=12 if mutant=='M2' else 6 + return a*(r*bp*bp*g*g/c2+positive(-ap)*g**3/c3) + + +def identity(n): + return [[F(int(i==j)) for j in range(n)] for i in range(n)] + + +def matrix(a): + a=[list(map(exact,row)) for row in a] + if not a or not a[0] or any(len(row)!=len(a[0]) for row in a): + raise ValueError('nonempty rectangular matrix required') + return a + + +def matmul(a,b): + a,b=matrix(a),matrix(b) + if len(a[0])!=len(b): + raise ValueError('matrix shapes do not compose') + return [[sum((x*y for x,y in zip(row,col)),F(0)) for col in zip(*b)] for row in a] + + +def inverse(a): + a=matrix(a); n=len(a) + if len(a[0])!=n: + raise ValueError('square matrix required') + a=[row+unit for row,unit in zip(a,identity(n))] + for j in range(n): + pivot=next((i for i in range(j,n) if a[i][j]),None) + if pivot is None: raise ValueError('singular matrix') + a[j],a[pivot]=a[pivot],a[j] + t=a[j][j]; a[j]=[x/t for x in a[j]] + for i in range(n): + if i!=j: + t=a[i][j]; a[i]=[x-t*y for x,y in zip(a[i],a[j])] + return [row[n:] for row in a] + + +def determinant(a): + a=matrix(a); n=len(a); ans=F(1) + if len(a[0])!=n: raise ValueError('square matrix required') + for j in range(n): + pivot=next((i for i in range(j,n) if a[i][j]),None) + if pivot is None: return F(0) + if pivot!=j: a[j],a[pivot]=a[pivot],a[j]; ans=-ans + t=a[j][j]; ans*=t + for i in range(j+1,n): + s=a[i][j]/t + a[i]=[x-s*y for x,y in zip(a[i],a[j])] + return ans + + +def hermite(m,mutant=None): + if type(m) is not int or m not in (2,3): raise ValueError('m must be 2 or 3') + return [[F(0) if j=ell),F(0))) + scaled=matmul(inverse(hermite(m)),[[x] for x in values]) + return [F(factorial(j))*row[0]/h**j for j,row in enumerate(scaled)] + + +def gram(rows): + return matmul(rows,list(map(list,zip(*rows)))) + + +def observation_rows(h,drop_q=False): + """A finite independent-coefficient polynomial Gaussian, not a periodic field.""" + h=exact(h) + if h<=0: raise ValueError('positive half-separation required') + powers=[(j,0) for j in range(6)]+[(j,1) for j in range(4)]+[(1,2),(0,2),(6,0),(4,1),(2,2)] + if drop_q: powers.remove((0,2)) + def row(x,dx,dy): + return [x**(p-dx)/factorial(p-dx) if q==dy and p>=dx else F(0) for p,q in powers] + rows=[row(sign*h,ell,0) for sign in (-1,1) for ell in range(3)] + rows += [row(sign*h,ell,1) for sign in (-1,1) for ell in range(2)] + plus,minus=row(h,0,2),row(-h,0,2) + rows.append([(x-y)/(2*h) for x,y in zip(plus,minus)]) + return rows,plus + + +def residual_variance(rows,target,mutant=None): + target=list(map(exact,target)); raw=sum((x*x for x in target),F(0)) + if mutant=='M5': return raw + k=matmul(rows,[[x] for x in target]) + return raw-matmul(list(map(list,zip(*k))),matmul(inverse(gram(rows)),k))[0][0] + + +def centered_even(k,mutant=None): + if type(k) is not int or k<0: raise ValueError('nonnegative integer moment index required') + if mutant=='M4' and k==6: return 945 + value=1 + for j in range(1,2*k,2): value*=j + return value + + +def noncentral_even(m,s,k): + m,s=exact(m),exact(s) + if s<0: raise ValueError('standard deviation must be nonnegative') + return sum((F(comb(2*k,2*j))*m**(2*k-2*j)*s**(2*j)*centered_even(j) for j in range(k+1)),F(0)) + + +def marginal_counterexample(): + # Q uniform[0,1], G=3Q/2, a_minus=a_plus=-1, b_minus=b_plus=0. + # T=Q^2/2; the invalid use of marginal density cap1 gives E[G^3]/6. + return F(1,2)*F(1,3),F(3,2)**3*F(1,4)/6 + + +def require(ok,label): + if not ok: raise ValueError(label) + + +def controls(mutant=None): + require(band_integral(-1,0,0,1,2,F(1,2))<=band_bound(-1,0,1,2,F(1,2),mutant),'BAND_R_COEFFICIENT') + require(band_integral(-1,-1,0,0,1,0)<=band_bound(-1,-1,0,1,0,mutant),'BAND_CUBIC_COEFFICIENT') + require(hermite(3,mutant)[2][2]==2,'HERMITE_DERIVATIVE_SCALE') + require(centered_even(6,mutant)==10395,'GAUSSIAN_TWELFTH') + rows,q=observation_rows(F(1,2)) + require(residual_variance(rows,q,mutant)==F(65,64),'CONDITIONAL_NOT_MARGINAL') + actual,bad=marginal_counterexample() + require(actual<=bad if mutant=='M6' else actual>bad,'MARGINAL_DENSITY_NOT_SUFFICIENT') + counts={'isolated_witnesses':6,'band':0,'hermite_monomials':0,'variance':0,'sharp_cubic':0} + for am,ap,bm,bp,g,r in itertools.product((-2,-1,0,1),(-2,-1,0,1,2),(0,1,2),(0,1,2),(-1,0,1,2),(F(0),F(1,4),F(1))): + value=band_integral(am,ap,bm,bp,g,r) + require(0<=value<=band_bound(am,ap,bp,g,r),'BAND_GRID') + counts['band']+=1 + for m in (2,3): + for h in (F(1,2),F(1,4),F(1,8),F(1,16)): + for j in range(2*m): + require(recover([int(i==j) for i in range(2*m)],m,h)==[F(factorial(i) if i==j else 0) for i in range(2*m)],'HERMITE_RECOVERY') + counts['hermite_monomials']+=1 + for h in (F(1,2),F(1,4),F(1,8),F(1,16)): + rows,q=observation_rows(h) + require(residual_variance(rows,q)==1+h**4/4,'CONDITIONAL_VARIANCE') + counts['variance']+=1 + r=2*h + require(band_integral(-1,1,-1,1,3*r,r)==F(5,6)*r**3,'CUBIC_SHARPNESS') + counts['sharp_cubic']+=1 + return {'scientific_effect':'NONE','controls':counts,'total':sum(counts.values()),'scope':'finite rational diagnostics; no continuum or Lean execution'} + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--mutant',choices=['M'+str(i) for i in range(1,7)]) + args=parser.parse_args() + try: result=controls(args.mutant) + except (ValueError,TypeError) as exc: + print('CUBIC_BAND_FAIL: '+str(exc),file=sys.stderr) + return 1 + print(json.dumps(result,sort_keys=True)) + return 0 + +if __name__=='__main__': sys.exit(main()) diff --git a/reviews/lm006_cubic_sign_band_20261006/test_cubic_band.py b/reviews/lm006_cubic_sign_band_20261006/test_cubic_band.py new file mode 100644 index 000000000..bd565daa7 --- /dev/null +++ b/reviews/lm006_cubic_sign_band_20261006/test_cubic_band.py @@ -0,0 +1,103 @@ +"""Exact controls for a conditional cubic sign-band bound, not Lean evidence.""" +import importlib.util +import itertools +from fractions import Fraction as F +from pathlib import Path +import subprocess +import sys +import unittest + +PATH = Path(__file__).with_name('cubic_band.py') + +class CubicBandTests(unittest.TestCase): + def setUp(self): + self.assertTrue(PATH.is_file(), 'cubic-band implementation missing') + spec = importlib.util.spec_from_file_location('cubic_band', PATH) + self.m = importlib.util.module_from_spec(spec) + spec.loader.exec_module(self.m) + + def test_exact_sign_band(self): + for am,ap,bm,bp,g,r in itertools.product((-2,-1,0,1),(-2,-1,0,1,2),(0,1,2),(0,1,2),(-1,0,1,2),(F(0),F(1,4),F(1))): + value = self.m.band_integral(am,ap,bm,bp,g,r) + self.assertGreaterEqual(value,0) + self.assertLessEqual(value,self.m.band_bound(am,ap,bp,g,r)) + + def test_both_constants_are_exact(self): + self.assertEqual(self.m.band_integral(-1,0,0,1,2,F(1,2)),1) + self.assertEqual(self.m.band_bound(-1,0,1,2,F(1,2)),1) + self.assertEqual(self.m.band_integral(-1,-1,0,0,1,0),F(1,6)) + self.assertEqual(self.m.band_bound(-1,-1,0,1,0),F(1,6)) + + def test_sign_support_and_singular_edges(self): + for t,g in itertools.product((F(-1),F(0),F(1,2),F(1),F(2)),(-1,0,1)): + value = self.m.weight((-1,1,1,1,t-g,t),F(1,4)) + if t>=0 and value>0: + self.assertLess(t,g) + self.assertEqual(self.m.band_integral(0,-1,0,1,1,1),0) + self.assertEqual(self.m.band_integral(-1,1,0,0,1,0),0) + + def test_hermite_inverses(self): + for m,want in ((2,16),(3,2048)): + v=self.m.hermite(m) + self.assertEqual(self.m.determinant(v),want) + self.assertEqual(self.m.matmul(v,self.m.inverse(v)),self.m.identity(2*m)) + + def test_all_monomial_recoveries(self): + for m in (2,3): + for h in (F(1,2),F(1,4),F(1,8),F(1,16)): + for degree in range(2*m): + p=[F(int(i==degree)) for i in range(2*m)] + self.assertEqual(self.m.recover(p,m,h),[F(self.m.factorial(j) if j==degree else 0) for j in range(2*m)]) + + def test_gaussian_schur_and_confluent_limit(self): + for h in (F(1,2),F(1,4),F(1,8),F(1,16)): + rows,target=self.m.observation_rows(h) + self.assertEqual(self.m.residual_variance(rows,target),1+h**4/4) + self.assertEqual(len(rows),11) + self.assertGreater(self.m.determinant(self.m.gram(rows)),0) + + def test_missing_contact_mode_is_not_uniform(self): + for h in (F(1,2),F(1,4),F(1,8)): + rows,target=self.m.observation_rows(h,drop_q=True) + self.assertEqual(self.m.residual_variance(rows,target),h**4/4) + + def test_gaussian_moment_constants(self): + for k,want in ((2,3),(4,105),(6,10395)): + self.assertEqual(self.m.centered_even(k),want) + for m,s in itertools.product((0,1,2),(0,1,2)): + self.assertLessEqual(self.m.noncentral_even(m,s,k),want*(m*m+s*s)**k) + + def test_cubic_example_integral(self): + for r in (F(1),F(1,2),F(1,4),F(1,8),F(1,16)): + self.assertEqual(self.m.band_integral(-1,1,-1,1,3*r,r),F(5,6)*r**3) + self.assertEqual(F(5,6)/F(1,2),F(5,3)) + + def test_marginal_density_counterexample(self): + actual,false_bound=self.m.marginal_counterexample() + self.assertEqual(actual,F(1,6)) + self.assertEqual(false_bound,F(9,64)) + self.assertGreater(actual,false_bound) + + def test_invalid_inputs(self): + for r in (-1,2,True,0.5): + with self.assertRaises((ValueError,TypeError)): + self.m.band_integral(-1,1,0,1,1,r) + with self.assertRaises(ValueError): self.m.recover([1],3,0) + with self.assertRaises(ValueError): self.m.inverse([[1,1],[1,1]]) + + def test_cli_and_intended_rejections(self): + reasons=['BAND_R_COEFFICIENT','BAND_CUBIC_COEFFICIENT','HERMITE_DERIVATIVE_SCALE','GAUSSIAN_TWELFTH','CONDITIONAL_NOT_MARGINAL','MARGINAL_DENSITY_NOT_SUFFICIENT'] + for flags in (['-B','-S'],['-B','-O','-S']): + p=subprocess.run([sys.executable,*flags,str(PATH)],capture_output=True,timeout=30) + self.assertEqual(p.returncode,0,p.stderr) + self.assertEqual(p.stderr,b'') + for j,reason in enumerate(reasons,1): + p=subprocess.run([sys.executable,*flags,str(PATH),'--mutant','M'+str(j)],capture_output=True,timeout=30) + self.assertEqual(p.returncode,1) + self.assertEqual(p.stderr,('CUBIC_BAND_FAIL: '+reason+'\n').encode()) + self.assertEqual(p.stdout,b'') + for args in (['--mutant','M9'],['--bogus'],['--mutant']): + p=subprocess.run([sys.executable,*flags,str(PATH),*args],capture_output=True,timeout=30) + self.assertEqual(p.returncode,2) + +if __name__=='__main__': unittest.main()