From 1dfe801eb61a8335a2e42b886fca9b000fb3598c Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 19:37:30 -0700 Subject: [PATCH] LM006: direct typed saddle-sign bound with quartic Gaussian error MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Four additive analytic/diagnostic files only. Existing proof, Lean, gate, workflow and scientific-register bytes unchanged. Dylan Roy — delegated AI work; actual author OpenAI / GPT-6 Astra Pro, round16-typed-sign-and-final-evidence-20261005. Scientific effect NONE; fresh nonauthor review pending. --- .../NOTE.md | 257 ++++++++++++++++++ .../SOURCES.json | 43 +++ .../test_typed_sign.py | 108 ++++++++ .../typed_sign_check.py | 96 +++++++ 4 files changed, 504 insertions(+) create mode 100644 reviews/lm006_typed_sign_suppression_20261005/NOTE.md create mode 100644 reviews/lm006_typed_sign_suppression_20261005/SOURCES.json create mode 100644 reviews/lm006_typed_sign_suppression_20261005/test_typed_sign.py create mode 100644 reviews/lm006_typed_sign_suppression_20261005/typed_sign_check.py diff --git a/reviews/lm006_typed_sign_suppression_20261005/NOTE.md b/reviews/lm006_typed_sign_suppression_20261005/NOTE.md new file mode 100644 index 000000000..9015971fa --- /dev/null +++ b/reviews/lm006_typed_sign_suppression_20261005/NOTE.md @@ -0,0 +1,257 @@ +# LM006: direct typed-weight suppression of the saddle-transverse sign event + +Dylan Roy — delegated AI mathematical work. Actual author OpenAI / GPT-6 +Astra Pro, session `round16-typed-sign-and-final-evidence-20261005`. +Scientific effect NONE. This is a new conditional analytic companion with +finite supporting diagnostics, not a Lean formalization or a status change. + +## 1. Source and purpose + +The endpoint definitions are those of Math-#315, now landed at +`99ba2dfe33ef0052694510355b0c4d811fd66441`, path +`reviews/lm006_normalizer_stability_20261005/NOTE.md`, blob +`5790aaa0332bd8e79b276be1577e4c5f3502eed6`, SHA256 +`2e63518026cef54bb91757ccbdba986a0765f8a8b640240417ba30c59e2f5fd4`. +Its physical type identity and Gaussian norm moments are restated below. + +The generic tilted-law packet is Math-#318, original head +`ecafa5206c528b0c662ea0bcbb26938681251aa5`, NOTE blob +`6633cdf0bfee55e2fc2046176effbf44634454b3`. Its later author comment6007838056 +bounds a particular sign event by a density error plus a squared coupling +error; its separate review6008028956 does not review this new argument. +The new result uses the actual typed weight instead of comparing arbitrary +weights. It removes the density-error term from the NUMERATOR estimate. +A positive lower normalizer remains indispensable. + +This is not a claim of general Gaussian-inequality novelty. It is a +source-specific improvement for one endpoint event. No concrete coupling +rate, uniform radius, field identification, or full-field event is supplied. + +For v=(a_-,a_+,b_-,b_+,c_-,c_+) in R^6, define x_+=max(x,0), +x_-=max(-x,0), and, for 0<=r<=1, + + F_r(v)=[(a_-)_-(c_-)_- - r b_-^2]_+, + G_r(v)=[r b_+^2-a_+c_+]_+, + T_r(v)=F_r(v)G_r(v). (1) + +For r>0, T_r is the physical maximum/saddle-filtered Hessian determinant +product divided by r^2. Explicitly, the two Hessians are + + [[r a_-,r b_-],[r b_-,c_-]], [[r a_+,r b_+],[r b_+,c_+]]. + +The first is selected to be negative definite; the second has negative +determinant. Singular boundaries have zero determinant weight. At r=0, +(1) is a continuous extension, not division by zero. The event considered +throughout is E={c_+>=0}, including its boundary. This is not a trivial +maximum-type condition: a 2x2 saddle can have c_+=0 or c_+>0. + +## 2. Pointwise estimate with sharp algebraic coefficients + +Put u=a_+-1 and g=c_+-c_-. Then for every v and 0<=r<=1, + + T_r(v) 1_E <= r |a_-| b_+^2 |g| + + (1/16)|a_-| u^2 g^2. (2) + +Proof. Off E the left side is zero and both right terms are nonnegative. +On E, if F_r=0 there is again nothing to show. Otherwise a_-<0 and c_-<0. +Write A=-a_->0, C=-c_->0 and d=c_+>=0. Then g=C+d>=0, and + + F_r<=A C, G_r<=(r b_+^2)+ (a_+)_- d. + +The latter follows from [s+t]_+<=s+t_+ when s>=0. Thus + + T_r <= r A b_+^2 C + A (a_+)_- C d. + +Two elementary inequalities finish the proof: + + C<=C+d=|g|, C d <= (C+d)^2/4, + (a_+)_- <= (a_+-1)^2/4. (3) + +For the last inequality, a_+>=0 gives zero on the left. If a_+<0, multiply +by4 and subtract: (a_+-1)^2+4a_+=(a_++1)^2>=0. +Combining both factors1/4 produces1/16 in (2). No eigenvalue inverse, +density assumption, type-boundary probability or independence is used. + +The two coefficients in this PARTICULAR pointwise form cannot separately +be decreased while the other term is fixed: +- v=(-A,1,0,1,-q,0), A,q>0, gives T_r=r A q, with equality in the + first term and zero second term for r>0. +- v=(-A,-1,0,0,-q,q), A,q>0, gives T_r=A q^2, with zero first term + and equality in the second term, for every r>=0 in the domain. + +These are algebraic Hessian witnesses, not realizations of the specified +six-pin random field. Sharpness of (2) does not assert sharpness of the +subsequent expectation constants. + +The shared transverse difference g is essential. The event E and maximum +type force c_- and c_+ to lie on opposite sides of zero; their product is +therefore controlled by g^2. When c_-=c_+ exactly, T_r 1_E=0 for every r. + +## 3. Expectation bound before any Gaussian assumption + +Let X be a measurable R^6-valued random vector on a probability space. +Use its coordinates in (1), U=X_{a_+}-1 and G=X_{c_+}-X_{c_-}. Define + + K2=E[X_{a_-}^2], K6=E[X_{a_-}^2 X_{b_+}^4], + g2=E[G^2], R44=E[U^4 G^4]. + +Assume these four nonnegative moments are finite. Integrating (2) and +applying Cauchy--Schwarz to each term separately gives + + N_r:=E[T_r(X) 1_E] + <= r sqrt(K6 g2) + (1/16) sqrt(K2 R44). (4) + +This step is valid for non-Gaussian variables with arbitrary dependence. +It establishes integrability of the event-restricted weight. For a +normalized endpoint probability also assume + + 0=0, with Z standard normal, + + E H^8 = m^8+28m^6s^2+210m^4s^4+420m^2s^6+105s^8 + <=105(m^2+s^2)^4. (6) + +The coefficients follow by the binomial expansion, vanishing odd centered +moments and the integration-by-parts recursion E Z^(2k)=(2k-1)E Z^(2k-2). +The inequality is coefficientwise: the difference is +104m^8+392m^6s^2+420m^4s^4. Thus it includes s=0 and nonzero means. +Applying Cauchy--Schwarz once more, without assuming independence, + + R44 <= sqrt(E U^8 E G^8) <=105 u2^2 g2^2. + +Consequently (4) becomes + + N_r <= r sqrt(K6 g2) + [sqrt(105 K2)/16] u2 g2. (7) + +This is the useful moment-specific form. It does not require a lower +variance bound or invertible covariance matrix. K2 and K6 may be retained +as actual mixed moments rather than replaced by coarse norm bounds. + +## 5. A coupling to the contact plane and the r e + e^4 estimate + +On one probability space, let Y be a measurable vector with + + Y_{a_+}=1, Y_{c_+}=Y_{c_-} almost surely, + +and suppose e^2=E||X-Y||^2 v_{c_+}-v_{c_-}, not an omitted independence assumption. Hence, under +the Gaussian-error-coordinate assumptions of §4, + + N_r <= sqrt(2 K6) r e + [sqrt(105 K2)/8] e^4. (8) + +Let z_r>=z_*>0 be a genuinely supplied bound. Then + + nu_r(E) <= min(1, [sqrt(2 K6) r e + +sqrt(105 K2)e^4/8]/z_*). (9) + +Unlike an arbitrary-weight TV transfer, (9) has no Delta=E|a-b| term. +That term was not silently set to zero: the exact numerator was bounded +directly using (1)--(3). A normalizer estimate is still required, and this +result does not control a different arbitrary weight. + +For Gaussian X in R^6 with ||E X||<=M and ||Cov X||_op<=Lambda, the +predecessor's norm moment argument supplies + + K2<=M^2+6Lambda=:C2, + K6<=E||X||^6<=32(M^6+480Lambda^3)=:C6. + +The number480 is 6*8*10, the sixth radial moment of a standard6 Gaussian. +If both X,Y have the specified affine Gaussian coupling and bounds in +#315, and its independently supplied condition guarantees z_r>=z0/2>0, +one may set z_*=z0/2, K2<=C2, K6<=C6 in (9). The z_r here is the normalized +physical quantity Z_r/r^2, not Z_r itself; no extra power of r is lost. + +If, in addition, e<=K r^alpha with alpha>0, one common K, and uniform C2,C6 +and z_*, then + + nu_r(E) <= [sqrt(2 C6) K/z_*] r^(1+alpha) + +[sqrt(105 C2) K^4/(8z_*)] r^(4alpha). (10) + +In particular a PROVED e=O(r) input yields O(r^2), with a smaller O(r^4) +term. This note does not prove that input for the concrete field, evaluate +a numerical radius, or infer uniformity from pointwise constants. +At e=0 the event mass is zero by (8), provided normalization is defined. + +The earlier generic sign-comment bound (Delta+e^2)/z0 remains correct +at its broader arbitrary-weight scope. It is not being retracted or +relabeled. The improvement here is specific to the exact typed T_r. + +## 6. Why the Gaussian moment condition must not disappear + +The pointwise estimate and (4) do not require Gaussianity; the replacement +of R44 by105u2^2g2^2 does. A rare-atom example exposes the distinction. + +Take fixed Y=(-1,1,0,0,-1,-1). With probability1-p let X=Y; with +probability p let X=(-1,-1,0,0,-1,1). Both atoms have T_r=1 for every +r in[0,1], so z_r=1 and nu_r(E)=p. Here K2=1, K6=0 and e^2=8p. +The purported non-Gaussian version of (8) would assert + + p <= (sqrt(105)/8)(8p)^2 = 8sqrt(105)p^2, + +which fails, for example at p=1/1000. U and G are not Gaussian in this +example. It is a counterexample to removing a hypothesis, not a +counterexample to this theorem or a six-pin Gaussian-field realization. +The exact general bound (4) still holds; its second term is sqrt(p), +which is at least p. The pointwise bound (2), before Cauchy--Schwarz, +is exact on both atoms. + +## 7. Reproduction, controls, and exclusions + +From this directory run + + python -B -S test_typed_sign.py + python -B -O -S test_typed_sign.py + python -B -S typed_sign_check.py + python -B -O -S typed_sign_check.py + +The12-method test suite checks the physical identity, full pointwise +majorant, both sharpness witnesses, the two scalar inequalities, Gaussian +eighth moments, correlated/degenerate Gaussian polynomial moments,180 +finite-law Cauchy bounds, a non-Gaussian counterexample, normalization, +input validation, exact failure reasons and CLI rejection. + +The standalone checker reports3753 exact controls:1458 physical identities, +2187 pointwise inequalities,20 eighth-moment comparisons,81 mixed Gaussian +polynomial comparisons, and7 isolated witnesses. The mixed diagnostic uses +two affine functions of one standard normal, so it explicitly includes +perfect correlation and degeneracy. General covariance is covered by the +analytic Cauchy--Schwarz proof, not extrapolated from this finite screen. + +M1 uses r^2 instead of r in the main term; M2 weakens1/16 to1/32; M3 drops +the event restriction; M4 uses15 instead of105 for the eighth moment; +M5 discards the Gaussian mean; M6 falsely applies the Gaussian conclusion +to the rare-atom law; M7 omits normalization. Each must exit1 with its +specified SIGN_FAIL reason. Unknown labels or arguments exit2. Generic +crashes are not intended mathematical rejections. These are finite +supporting diagnostics, not Lean execution or continuum certification. + +Excluded: an actual-field Gaussian/conditioning/Gram construction; a new +numerical normalizer or error rate; a full-field capture/persistence event; +arbitrary endpoint event bounds; total-variation convergence; higher-d +matrix generalization; proof-library alignment; historical verdict changes. +A fresh nonauthor read must inspect (2)--(10), especially the two1/4 factors, +mean-sensitive eighth moment, dependence allowance, and the normalized +z_r. Prior #315/#318 or comment6007838056 reviews do not cover this proof. diff --git a/reviews/lm006_typed_sign_suppression_20261005/SOURCES.json b/reviews/lm006_typed_sign_suppression_20261005/SOURCES.json new file mode 100644 index 000000000..b8b368503 --- /dev/null +++ b/reviews/lm006_typed_sign_suppression_20261005/SOURCES.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "scientific_effect": "NONE", + "author": { + "provider": "OpenAI", + "model": "GPT-6 Astra Pro", + "session": "round16-typed-sign-and-final-evidence-20261005" + }, + "files": { + "NOTE.md": { + "bytes": 11399, + "sha256": "bd9e15faff1c38d935a9761c36b9af32bfd4006fc900382e2e2430f481749a35", + "git_blob": "9015971fa03f44ae99d410facc6f3d8c26cdc945" + }, + "typed_sign_check.py": { + "bytes": 4040, + "sha256": "972e62c46a7e738835fa3dcfdfffafb280740da43b33bdd4306e0fa34a4a35b7", + "git_blob": "58f93a254a0b267210ec70bb190b9f4d7ba0d8ea" + }, + "test_typed_sign.py": { + "bytes": 5350, + "sha256": "e26e9e57d3d20b6361f6fc8ede4981e7aeee60640ded3abdf9bbfa7b7d6c2c1e", + "git_blob": "de4c34aecf0a62772f8b8918ad2bccbc9904a059" + } + }, + "inputs": [ + { + "repository": "d6g8k5htny-coder/Math-", + "commit": "99ba2dfe33ef0052694510355b0c4d811fd66441", + "path": "reviews/lm006_normalizer_stability_20261005/NOTE.md", + "git_blob": "5790aaa0332bd8e79b276be1577e4c5f3502eed6", + "sha256": "2e63518026cef54bb91757ccbdba986a0765f8a8b640240417ba30c59e2f5fd4", + "scope": "physical typed endpoint definition and Gaussian norm moments; assumptions retained" + }, + { + "repository": "d6g8k5htny-coder/Math-", + "commit": "ecafa5206c528b0c662ea0bcbb26938681251aa5", + "path": "reviews/lm006_tilted_endpoint_law_20261005/NOTE.md", + "git_blob": "6633cdf0bfee55e2fc2046176effbf44634454b3", + "scope": "comparison context only; no previous verdict transferred" + } + ] +} diff --git a/reviews/lm006_typed_sign_suppression_20261005/test_typed_sign.py b/reviews/lm006_typed_sign_suppression_20261005/test_typed_sign.py new file mode 100644 index 000000000..de4c34aec --- /dev/null +++ b/reviews/lm006_typed_sign_suppression_20261005/test_typed_sign.py @@ -0,0 +1,108 @@ +"""Exact finite diagnostics; not a Lean or continuum-Gaussian proof.""" +from fractions import Fraction as F +from pathlib import Path +import importlib.util,itertools,random,subprocess,sys,unittest + +P=Path(__file__).with_name("typed_sign_check.py") +def le_sqrt_sum(x,A,B): + return x*x<=A+B or (x*x-A-B)**2<=4*A*B + +class TypedSignTests(unittest.TestCase): + def setUp(self): + self.assertTrue(P.is_file(),"typed-sign implementation not supplied") + s=importlib.util.spec_from_file_location("typed_sign",P) + self.m=importlib.util.module_from_spec(s);s.loader.exec_module(self.m) + + def test_physical_identity(self): + for v in itertools.product((-1,0,1),repeat=6): + for r in (F(1,4),F(1)): + self.assertEqual(self.m.weight(v,r),self.m.physical(v,r)) + + def test_pointwise_majorant(self): + for v in itertools.product((-1,0,1),repeat=6): + for r in (F(0),F(1,4),F(1)): + q=self.m.weight(v,r) if v[5]>=0 else F(0) + terms=self.m.terms(v,r) + self.assertLessEqual(q,sum(terms)) + + def test_first_constant_is_sharp(self): + for r,g in itertools.product((F(1,8),F(1,2),F(1)),(F(1,4),F(1),F(3))): + v=(-1,1,0,1,-g,0) + n=self.m.weight(v,r); first,second=self.m.terms(v,r) + self.assertEqual(n,r*g);self.assertEqual((first,second),(n,0)) + + def test_quartic_constant_is_sharp(self): + for A,g in itertools.product((F(1,4),F(1),F(3)),repeat=2): + v=(-A,-1,0,0,-g,g) + n=self.m.weight(v,0); first,second=self.m.terms(v,0) + self.assertEqual(n,A*g*g);self.assertEqual((first,second),(0,n)) + + def test_scalar_product_inequalities(self): + vals=[F(n,4) for n in range(-12,13)] + for a in vals: + self.assertLessEqual(max(-a,F(0)),(a-1)**2/4) + for c,d in itertools.product(vals,repeat=2): + if c<=0<=d:self.assertLessEqual((-c)*d,(d-c)**2/4) + + def test_gaussian_eighth(self): + for m,s2 in itertools.product((F(-2),F(-1),F(0),F(1),F(2)),(F(0),F(1,4),F(1),F(4))): + exact=self.m.normal_even(m,s2,4) + self.assertLessEqual(exact,105*(m*m+s2)**4) + self.assertEqual(self.m.normal_even(0,1,4),105) + self.assertEqual(self.m.normal_even(2,0,4),256) + + def test_correlated_gaussian_product(self): + for m,n,s,t in itertools.product((-1,0,1),repeat=4): + val=self.m.mixed_fourth(m,s,n,t) + self.assertGreaterEqual(val,0) + self.assertLessEqual(val,105*(m*m+s*s)**2*(n*n+t*t)**2) + self.assertEqual(self.m.mixed_fourth(0,1,0,1),105) + + def test_finite_coupling_cauchy_step(self): + rng=random.Random(2026100516); probs=(F(1,4),F(1,4),F(1,2)) + for _ in range(180): + vs=[tuple(F(rng.randrange(-6,7),3) for _ in range(6)) for _ in probs] + r=F(rng.randrange(5),4) + n=sum(p*self.m.weight(v,r) for p,v in zip(probs,vs) if v[5]>=0) + k2=sum(p*v[0]**2 for p,v in zip(probs,vs)) + k6=sum(p*v[0]**2*v[3]**4 for p,v in zip(probs,vs)) + g2=sum(p*(v[5]-v[4])**2 for p,v in zip(probs,vs)) + r44=sum(p*(v[1]-1)**4*(v[5]-v[4])**4 for p,v in zip(probs,vs)) + self.assertTrue(le_sqrt_sum(n,r*r*k6*g2,k2*r44/256)) + + def test_nongaussian_exception_and_normalization(self): + p=F(1,1000);e2=8*p + # Bad and good atoms both have T_r=1, but the error coordinates are not Gaussian. + self.assertGreater(p*p,F(105,64)*e2**4) + self.assertEqual(self.m.weight((-1,-1,0,0,-1,1),F(1,2)),1) + self.assertEqual(self.m.weight((-1,1,0,0,-1,-1),F(1,2)),1) + n=self.m.weight((-1,-1,0,0,F(-1,2),F(1,2)),0) + self.assertEqual(n,F(1,4));self.assertEqual(n/n,1) + + def test_invalid_inputs(self): + for v,r in [((0,)*5,0),((True,)*6,0),((0.0,)*6,0),((0,)*6,-1),((0,)*6,2)]: + with self.assertRaises((ValueError,TypeError)): self.m.weight(v,r) + for args in ((0,-1,4),(0,1,-1),(0,1,True)): + with self.assertRaises((ValueError,TypeError)):self.m.normal_even(*args) + with self.assertRaises(ValueError):self.m.physical((0,)*6,0) + + def test_cli_baseline_and_mutants(self): + reasons=["RADIAL_SCALE","QUARTIC_CONSTANT","EVENT_RESTRICTION","GAUSSIAN_EIGHTH", + "GAUSSIAN_MEAN","GAUSSIAN_PREMISE_ESSENTIAL","NORMALIZER"] + previous=None + for flags in (["-B","-S"],["-B","-O","-S"]): + b=subprocess.run([sys.executable,*flags,str(P)],capture_output=True,text=True,timeout=20) + self.assertEqual((b.returncode,b.stderr),(0,"")) + if previous is not None:self.assertEqual(previous,b.stdout) + previous=b.stdout + for i,reason in enumerate(reasons,1): + q=subprocess.run([sys.executable,*flags,str(P),"--mutant",f"M{i}"],capture_output=True,text=True,timeout=20) + self.assertEqual((q.returncode,q.stdout,q.stderr),(1,"",f"SIGN_FAIL: {reason}\n")) + + def test_cli_invalid(self): + for flags in (["-B","-S"],["-B","-O","-S"]): + for args in (["--mutant","M8"],["--bogus"],["--mutant"]): + p=subprocess.run([sys.executable,*flags,str(P),*args],capture_output=True,text=True,timeout=10) + self.assertEqual(p.returncode,2) + +if __name__=="__main__": unittest.main() diff --git a/reviews/lm006_typed_sign_suppression_20261005/typed_sign_check.py b/reviews/lm006_typed_sign_suppression_20261005/typed_sign_check.py new file mode 100644 index 000000000..58f93a254 --- /dev/null +++ b/reviews/lm006_typed_sign_suppression_20261005/typed_sign_check.py @@ -0,0 +1,96 @@ +#!/usr/bin/env python3 +"""Rational controls for a typed saddle-sign estimate; no Lean execution.""" +from fractions import Fraction as F +from math import comb +import argparse,itertools,json,sys + +def exact(x): + if type(x) not in (int,F):raise TypeError("exact int/Fraction required") + return F(x) + +def vector(v): + v=tuple(map(exact,v)) + if len(v)!=6:raise ValueError("six endpoint coordinates required") + return v + +def radius(r): + r=exact(r) + if not 0<=r<=1:raise ValueError("r must be in [0,1]") + return r + +def weight(v,r): + am,ap,bm,bp,cm,cp=vector(v);r=radius(r) + return max(max(-am,F(0))*max(-cm,F(0))-r*bm*bm,F(0))*max(r*bp*bp-ap*cp,F(0)) + +def physical(v,r): + am,ap,bm,bp,cm,cp=vector(v);r=radius(r) + if not r:raise ValueError("physical normalization needs r>0") + dm=r*am*cm-r*r*bm*bm;ds=r*ap*cp-r*r*bp*bp + return abs(dm*ds)/(r*r) if r*am<0 and dm>0 and ds<0 else F(0) + +def terms(v,r,mutant=None): + am,ap,bm,bp,cm,cp=vector(v);r=radius(r);g=cp-cm + rr=r*r if mutant=="M1" else r + den=32 if mutant=="M2" else 16 + return rr*abs(am)*bp*bp*abs(g),abs(am)*(ap-1)**2*g*g/den + +def centered_even(k): + value=1 + for n in range(1,2*k,2):value*=n + return value + +def normal_even(m,s2,k,mutant=None): + m,s2=exact(m),exact(s2) + if type(k) is not int or k<0 or s2<0:raise ValueError("invalid normal moment parameters") + if mutant=="M5":m=F(0) + return sum((F(comb(2*k,2*j)*centered_even(j))*m**(2*k-2*j)*s2**j + for j in range(k+1)),F(0)) + +def mixed_fourth(m,s,n,t): + m,s,n,t=map(exact,(m,s,n,t));value=F(0) + for i,j in itertools.product(range(5),repeat=2): + if (i+j)%2:continue + value+=comb(4,i)*comb(4,j)*m**(4-i)*s**i*n**(4-j)*t**j*centered_even((i+j)//2) + return value + +def need(ok,reason): + if not ok:raise ValueError(reason) + +def controls(mutant=None): + counts={"isolated_witnesses":0,"physical":0,"pointwise":0,"eighth":0,"mixed":0} + v=(-1,1,0,1,-1,0);r=F(1,4) + need(weight(v,r)<=sum(terms(v,r,mutant)),"RADIAL_SCALE");counts["isolated_witnesses"]+=1 + v=(-1,-1,0,0,-1,1) + need(weight(v,0)<=sum(terms(v,0,mutant)),"QUARTIC_CONSTANT");counts["isolated_witnesses"]+=1 + v=(-1,1,0,0,-1,-1) + lhs=weight(v,0) if mutant=="M3" else F(0) + need(lhs<=sum(terms(v,0)),"EVENT_RESTRICTION");counts["isolated_witnesses"]+=1 + need(normal_even(0,1,4)<=(15 if mutant=="M4" else 105),"GAUSSIAN_EIGHTH");counts["isolated_witnesses"]+=1 + need(normal_even(2,0,4,mutant)==256,"GAUSSIAN_MEAN");counts["isolated_witnesses"]+=1 + p=F(1,1000);e2=8*p;false_bound=p*p<=F(105,64)*e2**4 + need(false_bound if mutant=="M6" else not false_bound,"GAUSSIAN_PREMISE_ESSENTIAL");counts["isolated_witnesses"]+=1 + n=weight((-1,-1,0,0,F(-1,2),F(1,2)),0) + need((n if mutant=="M7" else n/n)==1,"NORMALIZER");counts["isolated_witnesses"]+=1 + + for v in itertools.product((-1,0,1),repeat=6): + for r in (F(1,4),F(1)): + need(weight(v,r)==physical(v,r),"BASE_PHYSICAL");counts["physical"]+=1 + for r in (F(0),F(1,4),F(1)): + lhs=weight(v,r) if v[5]>=0 else F(0) + need(lhs<=sum(terms(v,r)),"BASE_MAJORANT");counts["pointwise"]+=1 + for m,s2 in itertools.product((-2,-1,0,1,2),(F(0),F(1,4),F(1),F(4))): + need(normal_even(m,s2,4)<=105*(m*m+s2)**4,"BASE_EIGHTH");counts["eighth"]+=1 + for m,s,n,t in itertools.product((-1,0,1),repeat=4): + need(mixed_fourth(m,s,n,t)<=105*(m*m+s*s)**2*(n*n+t*t)**2,"BASE_MIXED");counts["mixed"]+=1 + return {"scientific_effect":"NONE","counts":counts,"total":sum(counts.values()), + "scope":"exact finite diagnostics; not continuum proof or Lean"} + +def main(): + p=argparse.ArgumentParser(description=__doc__) + p.add_argument("--mutant",choices=[f"M{i}" for i in range(1,8)]) + a=p.parse_args() + try:result=controls(a.mutant) + except (ValueError,TypeError) as exc: + print("SIGN_FAIL: "+str(exc),file=sys.stderr);return 1 + print(json.dumps(result,sort_keys=True));return 0 +if __name__=="__main__":sys.exit(main())