From ecafa5206c528b0c662ea0bcbb26938681251aa5 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 18:33:05 -0700 Subject: [PATCH] LM006: tilted endpoint-law bounds and singular-support obstruction MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Four additive analytic/test files; no existing proof, Lean, gate or workflow changes. Actual author OpenAI / GPT-6 Astra Pro, round13-endpoint-law-audit-20261005. Dylan Roy — delegated AI work. Scientific effect NONE; new review pending. --- .../NOTE.md | 226 ++++++++++++++++++ .../SOURCES.json | 48 ++++ .../test_tilt.py | 89 +++++++ .../tilt_check.py | 117 +++++++++ 4 files changed, 480 insertions(+) create mode 100644 reviews/lm006_tilted_endpoint_law_20261005/NOTE.md create mode 100644 reviews/lm006_tilted_endpoint_law_20261005/SOURCES.json create mode 100644 reviews/lm006_tilted_endpoint_law_20261005/test_tilt.py create mode 100644 reviews/lm006_tilted_endpoint_law_20261005/tilt_check.py diff --git a/reviews/lm006_tilted_endpoint_law_20261005/NOTE.md b/reviews/lm006_tilted_endpoint_law_20261005/NOTE.md new file mode 100644 index 000000000..6633cdf0b --- /dev/null +++ b/reviews/lm006_tilted_endpoint_law_20261005/NOTE.md @@ -0,0 +1,226 @@ +# LM006: tilted endpoint laws, event margins, and the singular-support obstruction + +Dylan Roy — delegated AI mathematical work. Actual author OpenAI / GPT-6 +Astra Pro, session `round13-endpoint-law-audit-20261005`. Scientific effect NONE. +This is an additive analytic companion, not a Lean formalization or a change +of any historical theorem, review, or scientific register. + +## 1. Exact source and scope + +The predecessor is Math-#315 at `5e027afcae8c7bd42a6df8ae2025f82105b3e586`, +`reviews/lm006_normalizer_stability_20261005/NOTE.md`, Git blob +`5790aaa0332bd8e79b276be1577e4c5f3502eed6`, SHA256 +`2e63518026cef54bb91757ccbdba986a0765f8a8b640240417ba30c59e2f5fd4`. +It is a separately reviewed analytic source, not a new Lean theorem or a +statement that its PR is already merged. It explicitly excludes arbitrary +full-field event transfer. This companion proves conditional statements about +endpoint laws on R^6 and records exactly why total variation can fail there. + +Use its endpoint function, with x_+=max(x,0) and x_-=max(-x,0): + + T_r(v)=[(a_-)_-(c_-)_- - r b_-^2]_+ [r b_+^2-a_+c_+]_+, + v=(a_-,a_+,b_-,b_+,c_-,c_+), 0<=r<=1. (1) + +For r>0 this is the normalized physical typed weight W_r/r^2. At +v0(u,q)=(-1,1,-u/2,u/2,q,q), T_0(v0)=(q_-)^2, including q=0. +The input inequality, predecessor (5), is + + |T_r(v)-T_s(w)| <= (||v||+||w||)^3 ||v-w||+|r-s| ||w||^4. (2) + +General posterior/reweighted-measure stability and the distinction between +probability metrics have extensive prior literature; this note claims no new +general stability principle. Repository `formal/WeightPerturbation` (under +`formal/ResearchFormalCoreR1/`) already handles two weights under one law. +The present addition distinguishes a common latent law from TWO different +pushforward maps, provides explicit endpoint/margin constants, and exhibits +the singular-support obstruction for (1). The prior remote-window result also +already uses common regression couplings and filtered determinants. + +## 2. A normalized-density lemma on the common probability space + +Let (Omega,gamma) be a probability space. Let a,b be measurable, nonnegative, +integrable random variables, z=E_gamma a>0 and z0=E_gamma b>0. Write +Delta=E_gamma|a-b|. The tilted probability laws on Omega are gamma_a with +density a/z and gamma_b with density b/z0. Then + + E_gamma|a/z-b/z0| <= 2 Delta/z0. (3) + +Indeed split a/z-b/z0=(a-b)/z0+a(1/z-1/z0), integrate absolute values, and +use |z-z0|<=Delta. No smallness assumption is needed once both normalizers +are positive. Delta<=z0/2 is a useful sufficient condition for z>=z0/2>0. + +We use TV(mu,nu)=sup_A|mu(A)-nu(A)|, with range [0,1]. For probability +densities the signed difference integrates to zero; its positive and negative +parts have equal integral, each half the L1 norm. Thus + + TV(gamma_a,gamma_b) <= min(1,Delta/z0)=:theta, (4) + |E_gamma_a h-E_gamma_b h| <= theta for 0<=h<=1, + |E_gamma_a h-E_gamma_b h| <= 2 theta for |h|<=1. + +These are bounds for the SAME measurable function h on Omega. Replacing h +by two unrelated functions is not justified by (3) or (4). + +## 3. Moving endpoint maps: bounded-Lipschitz and padded-event bounds + +Let X,Y:Omega->R^6 be measurable maps. Set + + nu=X_#gamma_a, nu0=Y_#gamma_b, nu_tilde=X_#gamma_b, + D=||X-Y||, H=(E_gamma b^2)^(1/2), e=(E_gamma D^2)^(1/2), + +and assume H,e are finite. All three measures are well-defined probabilities; +countable additivity follows from that of integrals of nonnegative densities. +No independence between a,b,X,Y is required. + +For real phi with |phi|<=1 and Lipschitz constant at most1, + + |nu(phi)-nu0(phi)| <= 2 theta + E_gamma[b D]/z0 + <= 2 theta+H e/z0. (5) + +Proof: compare nu with nu_tilde using (4) on phi(X), then compare nu_tilde +with nu0 using the actual coupling (X,Y) under gamma_b. Cauchy--Schwarz under +gamma proves the last inequality. Taking the supremum defines the bounded- +Lipschitz metric d_BL used here, which is also at most2. The density comparison +alone is insufficient: the movement term must remain. We make no W1 claim +for unbounded test functions by merely substituting TV into this proof. + +For a Borel set A and t>0, let A^t={y:dist(y,A)<=t}; distance to an arbitrary +set means distance to its closure, and distance to the empty set is infinity. +These neighborhoods are Borel. Put kappa(t)=E_gamma[b 1_{D>t}]/z0. Then + + nu(A) <= nu0(A^t)+theta+kappa(t), + nu0(A) <= nu(A^t)+theta+kappa(t). (6) + +Proof: on {D<=t}, X in A implies Y in A^t, and conversely with X,Y reversed. +Take expectations under gamma_b and use (4) for the appropriate event of X. +Consequently kappa(t)<=H e/(z0 t), by Cauchy--Schwarz and Markov's inequality. +The probability in this tail is reweighted by b; substituting gamma(D>t) +without a bound on b would be an error. + +In Euclidean space a line segment between points with different membership +in A meets the topological boundary of A. Hence if indicators differ and +D<=t, dist(Y,boundary A)<=t. This covers arbitrary Borel A, including points +on the boundary; for A empty or full the assertion is trivial. Therefore + + |nu(A)-nu0(A)| <= theta+beta_A(t)+kappa(t), (7) + beta_A(t)=nu0({y:dist(y,boundary A)<=t}). + +A small marginal approximation error does NOT supply beta_A(t). For an event +whose boundary contains the limiting support, beta_A(t)=1 and (7) does not +assert convergence. This is the required safeguard for moving-band events. + +## 4. Gaussian specialization and conditional event rates + +Assume X=m_r+A_r Z and Y=m_0+A_0 Z with one standard Gaussian Z and finite +factors having the same number of columns. Singular covariances are allowed. +Then X-Y is Gaussian and + + e^2=||m_r-m_0||^2+||A_r-A_0||_F^2. + +For a Gaussian vector U with mean m and covariance C, direct expansion gives + + E||U||^4=(||m||^2+tr C)^2+2 tr(C^2)+4 m^T C m + <=3(||m||^2+tr C)^2. (8) + +To verify the expansion, diagonalize C; centered coordinates are independent, +with E Z_i^2=1, E Z_i^4=3 and odd moments zero. Use tr(C^2)<=(tr C)^2 and +m^T C m<=||m||^2 tr C for the bound. No invertibility is needed. Applied to +U=X-Y, Cauchy--Schwarz plus fourth-moment Markov yields the alternative + + kappa(t) <= min(H e/(z0 t), sqrt(3) H e^2/(z0 t^2)). (9) + +For a=T_r(X), b=T_0(Y), Y=v0(u,Q), the predecessor's bound (2) gives the +STRONGER L1 estimate, not only cancellation of signed expectations: + + Delta=E|T_r(X)-T_0(Y)| <= B e+D0 r, (10) + B=sqrt(2048(M^6+480 Lambda^3)), + D0=8(M^4+48 Lambda^2), + +provided the means have norm<=M and covariance operator norms<=Lambda as in +that predecessor. This follows by integrating the absolute pointwise bound; +it is not inferred from |E T_r-E T_0| alone. Here z0=E(Q_-)^2, and +H^2=E(Q_-)^4. A convenient coarse bound is + + H^2<=E||Y||^8<=128(M^8+5760 Lambda^4). + +Suppose z0>0 and B e+D0 r<=z0/2. Equations (5)--(10) then control actual +tilted endpoint laws with all constants explicit in the supplied inputs. +For example + + d_BL(nu_r,nu0) <= min(2, [2(B e+D0 r)+H e]/z0). (11) + +If additionally beta_A(t)<=C_A t^alpha for 00, then for +00 for every epsilon>0; +quartic growth gives integrability. X_epsilon and its tilt have a density, +while nu0 is the point mass at y. Therefore (13) holds for every epsilon, +although (11) tends to zero. This example is NOT a claimed six-pin Gaussian +field realization. In the actual LM006 application, (13) holds whenever the +finite-r endpoint vector has a density; establishing that property is the +separate positive pin/Hessian Gram argument, not a consequence of (11). + +This is a scope obstruction, not an error finding against #315, whose text +already excludes full-field event transfer. It prohibits strengthening the +new endpoint conclusion to convergence in TV without a different coordinate +representation or additional argument. + +## 6. Exact finite controls and review boundary + +Run `python -B -S test_tilt.py` and the same with `-O`. The 12 methods verify +676 weight-pair TV comparisons,64 latent events,300 clipped-Lipschitz cases, +400 directed padded inequalities,150 threshold/margin inequalities,81 exact +Gaussian fourth-moment parameter cases, normalization/null-mass/input edges, +and the movement-vs-TV counterexample. These are one-dimensional finite +analogues of the inequalities, not a proof of the R^6 or Gaussian claims. +`tilt_check.py` has687 exact baseline controls. M1--M7 independently test: +omitted normalization, signed instead of absolute weight error, omitted map +movement, unweighted tail substitution, omitted event margin, wrong Gaussian +fourth-moment coefficient, and substituting BL for TV. Each must exit1 with +its exact named TILT_FAIL diagnostic; invalid arguments exit2. A crash is not +an accepted rejection. The predecessor's existing workflow is not represented +as an execution of these new tests, and no new Lean target is claimed. + +## 7. Attribution and external context + +The original normalizer and endpoint definitions remain unchanged. The +predecessor's source review is reused only for (1),(2),(10)'s stated inputs; +this new density/map argument needs its own nonauthor read. Other ongoing +moment-law, Cap I4, spectral and gate-hardening work is not a premise here. + +As related context only, Latz, *On the well-posedness of Bayesian inverse +problems*, arXiv:1902.10257, and Sprungk, *On the local Lipschitz stability of +Bayesian inverse problems*, arXiv:1906.07120, distinguish stability metrics +and normalization-sensitive posterior bounds. Their abstract records were +consulted, not imported as proofs of (1)--(13); the elementary argument above +is complete on its explicit assumptions. No claim of literature novelty or +complete literature coverage is made. A requested Consensus search hit its +monthly limit, so no Consensus result supplies any premise. diff --git a/reviews/lm006_tilted_endpoint_law_20261005/SOURCES.json b/reviews/lm006_tilted_endpoint_law_20261005/SOURCES.json new file mode 100644 index 000000000..abbfce6eb --- /dev/null +++ b/reviews/lm006_tilted_endpoint_law_20261005/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "scientific_effect": "NONE", + "author": { + "provider": "OpenAI", + "model": "GPT-6 Astra Pro", + "session": "round13-endpoint-law-audit-20261005" + }, + "files": { + "NOTE.md": { + "bytes": 11397, + "sha256": "ebff808093e4fcc9959ff8690c9cf049d91ac3306297853e559d70739747f113", + "git_blob": "6633cdf0bfee55e2fc2046176effbf44634454b3" + }, + "tilt_check.py": { + "bytes": 4312, + "sha256": "aac9b23deb8f8ffd5e5abefd9d33caec6d327ac2fc4bd079047c0c20041c3ada", + "git_blob": "5f66506eb38325b0594200acf4c4d2d50a698c89" + }, + "test_tilt.py": { + "bytes": 5194, + "sha256": "6badbbcd1037d9c397c258d5c356a39c396b189e39b919e500df30b85baff4a0", + "git_blob": "0bda8438ba1e06d03e134ff4cd17c6a1786b023c" + } + }, + "dependencies": [ + { + "repository": "d6g8k5htny-coder/Math-", + "commit": "5e027afcae8c7bd42a6df8ae2025f82105b3e586", + "path": "reviews/lm006_normalizer_stability_20261005/NOTE.md", + "git_blob": "5790aaa0332bd8e79b276be1577e4c5f3502eed6", + "sha256": "2e63518026cef54bb91757ccbdba986a0765f8a8b640240417ba30c59e2f5fd4", + "slice": "endpoint definition (1), pointwise bound (5), Gaussian moment bounds; no prior review transferred to this new proof" + } + ], + "external_context": [ + { + "arxiv": "1902.10257v4", + "read": "abstract only", + "role": "metric distinction; not proof premise" + }, + { + "arxiv": "1906.07120v3", + "read": "abstract only", + "role": "normalization-sensitive reweighting stability; not proof premise" + } + ] +} diff --git a/reviews/lm006_tilted_endpoint_law_20261005/test_tilt.py b/reviews/lm006_tilted_endpoint_law_20261005/test_tilt.py new file mode 100644 index 000000000..0bda8438b --- /dev/null +++ b/reviews/lm006_tilted_endpoint_law_20261005/test_tilt.py @@ -0,0 +1,89 @@ +"""Exact finite probability controls; neither Lean nor continuum proof.""" +from fractions import Fraction as F +import importlib.util, itertools, json +from pathlib import Path +import random, subprocess, sys, unittest +P=Path(__file__).with_name('tilt_check.py') +class TiltTests(unittest.TestCase): + def setUp(self): + self.assertTrue(P.is_file(),'tilted-law implementation not supplied') + s=importlib.util.spec_from_file_location('tilt',P); self.m=importlib.util.module_from_spec(s); s.loader.exec_module(self.m) + def test_density_normalization(self): + p=(F(1,4),F(1,4),F(1,2)) + for a in itertools.product((0,1,2),repeat=3): + if not any(a): continue + w=self.m.tilt(p,a) + self.assertEqual(sum(w),1); self.assertTrue(all(v>=0 for v in w)) + def test_reference_tv_bound(self): + p=(F(1,4),F(1,4),F(1,2)) + ws=[a for a in itertools.product((0,1,2),repeat=3) if any(a)] + for a,b in itertools.product(ws,repeat=2): + d=self.m.density_data(p,a,b) + self.assertLessEqual(d['tv'],d['delta']/d['z0']) + def test_all_latent_events(self): + p=(F(1,3),F(2,3)); events=list(itertools.product((False,True),repeat=2)) + for a,b in itertools.product(((1,0),(0,1),(1,3),(2,2)),repeat=2): + d=self.m.density_data(p,a,b) + for event in events: + gap=abs(sum(v for v,c in zip(d['alpha'],event) if c)-sum(v for v,c in zip(d['beta'],event) if c)) + self.assertLessEqual(gap,d['delta']/d['z0']) + def test_clipped_lipschitz_observables(self): + p=(F(1,4),F(1,4),F(1,2)); rng=random.Random(913) + for _ in range(300): + a=tuple(F(rng.randrange(1,5)) for _ in p); b=tuple(F(rng.randrange(1,5)) for _ in p) + x=tuple(F(rng.randrange(-8,9),4) for _ in p); y=tuple(F(rng.randrange(-8,9),4) for _ in p) + d=self.m.density_data(p,a,b) + fun=lambda t:max(F(-1),min(F(1),t)) + gap=abs(sum(v*fun(t) for v,t in zip(d['alpha'],x))-sum(v*fun(t) for v,t in zip(d['beta'],y))) + self.assertLessEqual(gap,self.m.bl_bound(p,a,b,x,y)) + def test_padded_event_both_directions(self): + p=(F(1,4),F(3,4)); rng=random.Random(914) + for _ in range(200): + a=tuple(F(rng.randrange(1,4)) for _ in p); b=tuple(F(rng.randrange(1,4)) for _ in p) + x=tuple(F(rng.randrange(-4,5),2) for _ in p); y=tuple(F(rng.randrange(-4,5),2) for _ in p) + A={F(rng.randrange(-4,5),2)}; t=F(1,2) + d=self.m.density_data(p,a,b); budget=self.m.padded_budget(p,a,b,x,y,t) + for z,w,az,aw in ((x,y,d['alpha'],d['beta']),(y,x,d['beta'],d['alpha'])): + lhs=sum(v for v,q in zip(az,z) if q in A) + rhs=sum(v for v,q in zip(aw,w) if min(abs(q-u) for u in A)<=t) + self.assertLessEqual(lhs,rhs+budget) + def test_threshold_margin(self): + p=(F(1,2),F(1,2)); rng=random.Random(915) + for _ in range(150): + a=(F(1),F(rng.randrange(1,4))); b=(F(rng.randrange(1,4)),F(1)) + x=tuple(F(rng.randrange(-8,9),4) for _ in p); y=tuple(F(rng.randrange(-8,9),4) for _ in p) + d=self.m.density_data(p,a,b); t=F(1,2) + gap=abs(sum(v for v,q in zip(d['alpha'],x) if q<=0)-sum(v for v,q in zip(d['beta'],y) if q<=0)) + margin=sum(v for v,q in zip(d['beta'],y) if abs(q)<=t) + self.assertLessEqual(gap,margin+self.m.padded_budget(p,a,b,x,y,t)) + def test_movement_not_weight_error(self): + p=(F(1),); a=b=(F(1),); x=(F(1,8),); y=(F(0),) + d=self.m.density_data(p,a,b) + self.assertEqual(d['delta'],0); self.assertEqual(self.m.bl_bound(p,a,b,x,y),F(1,8)) + self.assertEqual(self.m.discrete_tv(self.m.pushforward(p,a,x),self.m.pushforward(p,b,y)),1) + def test_tilted_motion_not_original_probability(self): + p=(F(1,16),F(15,16)); a=b=(F(16),F(0)); x=(F(1),F(0)); y=(F(0),F(0)) + self.assertEqual(self.m.padded_budget(p,a,b,x,y,F(1,2)),1) + def test_gaussian_fourth_moment_bound(self): + for mu in itertools.product((F(-1),F(0),F(2)),repeat=2): + for lam in itertools.product((F(0),F(1,2),F(2)),repeat=2): + m4,e2=self.m.gaussian_diagonal_fourth(mu,lam) + self.assertLessEqual(m4,3*e2*e2) + self.assertEqual(self.m.gaussian_diagonal_fourth((0,),(1,)),(F(3),F(1))) + def test_zero_normalizers_and_invalid_inputs(self): + for p,a in [((F(1),),(0,)),((F(1),),(-1,)),((F(1,2),),(1,)),((1,),(True,)),((1,),(1.0,))]: + with self.assertRaises((ValueError,TypeError)): self.m.tilt(p,a) + self.assertEqual(self.m.tilt((F(0),F(1)),(-2,1)),(F(0),F(1))) + def test_cli_named_failures(self): + expected={'M1':'NORMALIZED_MASS','M2':'ABSOLUTE_NOT_SIGNED_ERROR','M3':'MOVEMENT_TERM','M4':'TILTED_TAIL','M5':'BOUNDARY_MARGIN','M6':'GAUSSIAN_FOURTH','M7':'TV_NOT_BL'} + for flags in (['-B','-S'],['-B','-O','-S']): + r=subprocess.run([sys.executable,*flags,str(P)],capture_output=True,text=True,timeout=15) + self.assertEqual(r.returncode,0,r.stderr); self.assertEqual(r.stderr,''); self.assertGreater(json.loads(r.stdout)['controls'],0) + for m,want in expected.items(): + r=subprocess.run([sys.executable,*flags,str(P),'--mutant',m],capture_output=True,text=True,timeout=15) + self.assertEqual(r.returncode,1); self.assertEqual(r.stdout,''); self.assertEqual(r.stderr,'TILT_FAIL: '+want+'\n') + def test_cli_invalid(self): + for args in (['--mutant','M9'],['--invalid'],['--mutant']): + r=subprocess.run([sys.executable,'-B','-S',str(P),*args],capture_output=True,text=True,timeout=15) + self.assertEqual(r.returncode,2) +if __name__=='__main__': unittest.main() diff --git a/reviews/lm006_tilted_endpoint_law_20261005/tilt_check.py b/reviews/lm006_tilted_endpoint_law_20261005/tilt_check.py new file mode 100644 index 000000000..5f66506eb --- /dev/null +++ b/reviews/lm006_tilted_endpoint_law_20261005/tilt_check.py @@ -0,0 +1,117 @@ +#!/usr/bin/env python3 +"""Exact finite controls for tilted endpoint-law transfer; stdlib only. + +This is finite arithmetic, not Lean execution or a continuum Gaussian proof. +""" +from fractions import Fraction as F +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 inputs(p,a): + p=tuple(map(exact,p)); a=tuple(map(exact,a)) + if not p or len(p)!=len(a) or sum(p)!=1 or any(x<0 for x in p): + raise ValueError('probability vector/weight shape invalid') + if any(q>0 and w<0 for q,w in zip(p,a)): raise ValueError('negative weight on positive mass') + z=sum(q*w for q,w in zip(p,a)) + if z<=0: raise ValueError('normalizer must be positive') + return p,a,z + + +def tilt(p,a): + p,a,z=inputs(p,a) + return tuple(q*w/z for q,w in zip(p,a)) + + +def density_data(p,a,b): + p,a,z=inputs(p,a); _,b,z0=inputs(p,b) + alpha=tilt(p,a); beta=tilt(p,b) + delta=sum(q*abs(v-w) for q,v,w in zip(p,a,b)) + tv=sum(abs(v-w) for v,w in zip(alpha,beta))/2 + return dict(z=z,z0=z0,delta=delta,alpha=alpha,beta=beta,tv=tv) + + +def locations(x,y,n): + x=tuple(map(exact,x)); y=tuple(map(exact,y)) + if len(x)!=n or len(y)!=n: raise ValueError('location shape invalid') + return x,y + + +def bl_bound(p,a,b,x,y): + d=density_data(p,a,b); x,y=locations(x,y,len(d['beta'])) + return 2*d['delta']/d['z0']+sum(q*abs(v-w) for q,v,w in zip(d['beta'],x,y)) + + +def padded_budget(p,a,b,x,y,t): + t=exact(t) + if t<=0: raise ValueError('positive padding required') + d=density_data(p,a,b); x,y=locations(x,y,len(d['beta'])) + return d['delta']/d['z0']+sum(q for q,v,w in zip(d['beta'],x,y) if abs(v-w)>t) + + +def pushforward(p,a,x): + alpha=tilt(p,a); x,_=locations(x,x,len(alpha)); out={} + for q,v in zip(alpha,x): out[v]=out.get(v,F(0))+q + return out + + +def discrete_tv(p,q): + return sum(abs(p.get(k,F(0))-q.get(k,F(0))) for k in p.keys()|q.keys())/2 + + +def gaussian_diagonal_fourth(mu,lam): + mu=tuple(map(exact,mu)); lam=tuple(map(exact,lam)) + if not mu or len(mu)!=len(lam) or any(x<0 for x in lam): raise ValueError('invalid Gaussian parameters') + m2=sum(x*x for x in mu); tr=sum(lam); e2=m2+tr + fourth=m2*m2+2*m2*tr+4*sum(x*x*t for x,t in zip(mu,lam))+tr*tr+2*sum(t*t for t in lam) + return fourth,e2 + + +def need(ok,reason): + if not ok: raise ValueError(reason) + + +def controls(mutant=None): + count=0 + p=(F(1,4),F(1,4),F(1,2)); ws=[a for a in itertools.product((0,1,2),repeat=3) if any(a)] + for a,b in itertools.product(ws,repeat=2): + d=density_data(p,a,b); need(d['tv']<=d['delta']/d['z0'],'REFERENCE_TV_BOUND'); count+=1 + # Minimal exact witnesses, each isolates one omitted/incorrect operation. + p=(F(1,2),F(1,2)); a=(F(2),F(2)) + masses=tuple(q*w for q,w in zip(p,a)) if mutant=='M1' else tilt(p,a) + need(sum(masses)==1,'NORMALIZED_MASS'); count+=1 + a,b=(F(2),F(0)),(F(0),F(2)); d=density_data(p,a,b) + delta=abs(sum(q*(v-w) for q,v,w in zip(p,a,b))) if mutant=='M2' else d['delta'] + need(d['tv']<=delta/d['z0'],'ABSOLUTE_NOT_SIGNED_ERROR'); count+=1 + p=(F(1),); a=b=(F(1),); x=(F(1,8),); y=(F(0),) + bd=0 if mutant=='M3' else bl_bound(p,a,b,x,y) + need(F(1,8)<=bd,'MOVEMENT_TERM'); count+=1 + p=(F(1,16),F(15,16)); a=b=(F(16),F(0)); x=(F(1),F(0)); y=(F(0),F(0)) + bd=F(1,16) if mutant=='M4' else padded_budget(p,a,b,x,y,F(1,2)) + need(1<=bd,'TILTED_TAIL'); count+=1 + # A={x<=0}; both deterministic points are within t of each other and straddle 0. + x,y=(F(1,8),),(F(-1,8),); p=a=b=(F(1),) + bd=padded_budget(p,a,b,x,y,F(1,2))+(0 if mutant=='M5' else 1) + need(1<=bd,'BOUNDARY_MARGIN'); count+=1 + m4,e2=gaussian_diagonal_fourth((0,),(1,)) + need(m4<=(1 if mutant=='M6' else 3)*e2*e2,'GAUSSIAN_FOURTH'); count+=1 + for n in (2,4,8,16,32): + x=(F(1,n),); y=(F(0),) + tv=discrete_tv(pushforward(p,a,x),pushforward(p,b,y)) + need(tv<=(F(1,n) if mutant=='M7' else 1),'TV_NOT_BL'); count+=1 + return {'controls':count,'scope':'finite exact controls, not continuum proof or Lean','scientific_effect':'NONE'} + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--mutant',choices=['M'+str(n) for n in range(1,8)]) + args=parser.parse_args() + try: result=controls(args.mutant) + except (ValueError,TypeError) as exc: + print('TILT_FAIL: '+str(exc),file=sys.stderr); return 1 + print(json.dumps(result,sort_keys=True)); return 0 +if __name__=='__main__': sys.exit(main())