From 8ab9498c3162db5f673607607582958e1468fae6 Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Mon, 28 Sep 2026 13:54:47 -0500 Subject: [PATCH] Add remote singleton configuration-law corollary for review Generic exact total-variation identity and source-bound use of fixed-remote mean/factorial estimates. Seven-file tree4cd9b9a784b056cf1b792a3f5d0758c255791cd0 plus read-only targeted controls. Fourteen tests per mode and six semantic mutants pass locally; finite controls are not continuum acceptance. No existing proof/status/graph edits, no global collision or Poisson-limit claim. --- .github/workflows/remote-singleton.yml | 33 +++ .../remote_singleton_law_20260928/PROOF.md | 272 ++++++++++++++++++ .../remote_singleton_law_20260928/README.md | 27 ++ .../RESULTS.json | 12 + .../SOURCE_FILES.json | 43 +++ .../finite_law.py | 70 +++++ .../run_validation.py | 80 ++++++ .../test_finite_law.py | 129 +++++++++ 8 files changed, 666 insertions(+) create mode 100644 .github/workflows/remote-singleton.yml create mode 100644 frontiers/remote_singleton_law_20260928/PROOF.md create mode 100644 frontiers/remote_singleton_law_20260928/README.md create mode 100644 frontiers/remote_singleton_law_20260928/RESULTS.json create mode 100644 frontiers/remote_singleton_law_20260928/SOURCE_FILES.json create mode 100644 frontiers/remote_singleton_law_20260928/finite_law.py create mode 100644 frontiers/remote_singleton_law_20260928/run_validation.py create mode 100644 frontiers/remote_singleton_law_20260928/test_finite_law.py diff --git a/.github/workflows/remote-singleton.yml b/.github/workflows/remote-singleton.yml new file mode 100644 index 000000000..3cdda862d --- /dev/null +++ b/.github/workflows/remote-singleton.yml @@ -0,0 +1,33 @@ +name: Remote single-point law finite controls + +'on': + pull_request: + paths: + - 'frontiers/remote_singleton_law_20260928/**' + - '.github/workflows/remote-singleton.yml' + push: + branches: [main] + paths: + - 'frontiers/remote_singleton_law_20260928/**' + - '.github/workflows/remote-singleton.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + finite-singleton-controls: + 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, two Python modes and semantic mutations + run: | + set -euo pipefail + python -B -S frontiers/remote_singleton_law_20260928/run_validation.py --output "${RUNNER_TEMP}/remote-singleton-${GITHUB_RUN_ID}-${GITHUB_RUN_ATTEMPT}" + git diff --exit-code diff --git a/frontiers/remote_singleton_law_20260928/PROOF.md b/frontiers/remote_singleton_law_20260928/PROOF.md new file mode 100644 index 000000000..2b0195697 --- /dev/null +++ b/frontiers/remote_singleton_law_20260928/PROOF.md @@ -0,0 +1,272 @@ +# Remote rare critical points: the single-point configuration law + +Object: OA-D5-REMOTE-SINGLETON-LAW-20260928-v1. +Author: OpenAI / ChatGPT, foreground continuation. +Disposition: AUTHOR-SIDE COROLLARY; NONAUTHOR REVIEW REQUIRED. +Scientific effect: NONE. No governing status, proof index, graph, prize or source body is changed. + +## 1. Intent and exact source dependencies + +The fixed-remote mean and second factorial moment say more than that a window +critical point is rare: when one appears, its complete remote configuration is +usually a singleton, and its location/index distribution can be identified. This +note makes that consumption explicit. It proves an elementary general probability +lemma and applies only already specified fixed-remote estimates. It introduces no +new Gaussian covariance argument and no global witness-collision assertion. + +Repository: `d6g8k5htny-coder/Math-`. + +1. `frontiers/remote_window_20260924/PROOF.md`, Theorem A, read at commit + `541d4e9daf3f2ca8b5a485d6e96ecf3dbf958f17`, blob + `b383bfcc88ec4ad497dff01fb6640e429ba24a84`. This gives the uniform fixed-remote + mean density expansion, not by itself a matching event-probability law. +2. `frontiers/remote_collision_20260928/PROOF.md`, Corollary D, v4 at commit + `66437d90f3b7222256b2b8aed62400c42a78a08a`, 26,002 bytes, SHA-256 + `b9b8b58fd8266db7ffe6537078003888ef138b445d3289ec5588f116af9050c2`, blob + `7b48a88e2af54e759e89a8c8219573bb450a65ea`. This gives the second factorial + moment with BOTH witnesses in the same fixed remote region. OpenAI's + source-exposed review 5343164624 of that source is not a review of this note. + +The application below is conditional on the mathematical validity of these +precise inputs. Publication or merger is not an additional proof premise. The +exact generic lemma in Sections 2-4 is proved here. No earlier verdict is +inherited for the new application. Math-#107's planar global first moment is +NOT an input: the present statement is remote in every fixed d>=2. + +## 2. A finite point-process lemma with an exact error identity + +Let S be a standard Borel space. Give the space of finite counting measures on S +its counting-map sigma algebra. A point is represented by its unit mass delta_x; +the singleton embedding and its inverse on singleton configurations are +measurable. Multiplicities are allowed in this lemma. + +Let Xi be a random finite counting measure, N=Xi(S), and + + mu(A)=E Xi(A), m=mu(S)<=1, + q=E[N(N-1)]=2]. (S1) + +Define Ber(mu) as a random counting measure: it is empty with probability 1-m, +and assigns singleton delta_x with subprobability measure mu(dx). When m>0 this +means sample a Bernoulli(m) indicator and, if nonempty, sample x from mu/m. For +m=0 it is the deterministic empty configuration. The condition m<=1 is necessary +for this definition; it is not silently replaced by min(m,1). + +Use probability total variation + + dTV(P,Q)=sup_A |P(A)-Q(A)|=(1/2)||P-Q||_var, + +where || ||_var is the full mass norm of a signed measure. + +**Lemma 1 (exact identity).** + + dTV(Law Xi, Ber(mu)) = h <= q. (S2) + +**Proof.** Define the singleton submeasure sigma on S by + + sigma(A)=P(N=1 and the unique point belongs to A), + +and the nonnegative multiple-point mean measure eta by + + eta(A)=E[Xi(A); N>=2]. + +Then mu=sigma+eta, sigma(S)=s:=P(N=1), and eta(S)=h. Put +alpha=P(N>=2) and p=P(N>=1)=s+alpha. Thus m=s+h and +m-p=h-alpha>=0. On the three disjoint parts of configuration space: + +- empty: Law Xi minus Ber(mu) has mass m-p=h-alpha; +- singletons: Ber(mu) minus Law Xi is the pushforward of eta, of mass h; +- configurations of size >=2: Law Xi minus Ber(mu) has mass alpha. + +The full variation is (h-alpha)+h+alpha=2h, proving equality in (S2). +Finally n<=n(n-1) for integers n>=2 gives h<=q. This also shows all relevant +measures are finite. No point independence, stationarity, Poisson hypothesis, +Gaussian conditioning or pair-density formula is used. QED. + +The constant one in h<=q is sharp: take Xi=delta_a+delta_b with probability +epsilon<=1/2, otherwise empty. Then m=h=q=2epsilon and dTV=2epsilon. +The points can coincide in the generic example; choosing distinct a,b gives a +simple-process example as well. + +**Why a first moment alone is insufficient.** The same example with +epsilon=r^3/2 has m=r^3 but dTV=r^3, not O(r^5). The factorial input is essential +to the stronger approximation asserted below. + +## 3. Conditional laws and single-witness location + +Suppose m>0. Necessarily p>0 since Xi is nonnegative. Denote by Delta(nu) the law +of a singleton at an S-valued point with probability distribution nu. + +**Lemma 2.** + + dTV(Law(Xi | N>=1), Delta(mu/m)) <= h/m <= q/m. (S3) + +If s=P(N=1)>0, then also + + dTV(Law(unique point | N=1), mu/m) <= h/m. (S4) + +**Proof.** The common submeasure Delta(sigma/m) is dominated by both laws in +(S3). In the first law the singleton part is Delta(sigma/p), and p<=m; in the +second it is Delta((sigma+eta)/m). Its total mass is s/m, so the probability-TV +distance is at most 1-s/m=h/m. This domination argument proves the claim for +arbitrary measurable configuration events, not just events determined by N. +For (S4), write mu/m=(s/m)(sigma/s)+eta/m; the usual mixture difference has +TV at most h/m. This argument identifies the unique point, not an arbitrary +selection rule from a configuration with several points. QED. + +The elementary count inequalities also give + + 0<=m-p=E[(N-1);N>=2]<=q/2, + P(N>=2 | N>=1)<=q/(2p), + s=m-h>=m-q. (S5) + +The factors 1/2 arise from 1<=n(n-1)/2 and n-1<=n(n-1)/2 for n>=2. Thus +q=o(m) ensures both a positive singleton event and conditional uniqueness with +probability tending to one. All these claims count multiplicity, not merely +distinct occupied sites. + +## 4. Replacing the exact mean measure by a leading approximation + +Let mu_0 be another nonnegative measure with 00, direct normalization gives + + dTV(mu/m,mu_0/m_0)<=D/m. (S7) + +Indeed mu/m-mu_0/m_0=(mu-mu_0)/m+mu_0(1/m-1/m_0), whose variation mass is at +most (D+|m-m_0|)/m<=2D/m. Combining with (S2)-(S4), + + dTV(Law Xi,Ber(mu_0)) <= q+D, + dTV(Law(Xi|N>=1),Delta(mu_0/m_0)) <= (q+D)/m. (S8) + +The unique-point version has the same upper bound when s>0. These bounds retain +the normalization denominator. An absolute O(r^4) mean error becomes O(r) +after conditioning on an event of order r^3; it does not remain O(r^4). + +## 5. Exact Gaussian application, keeping the remote scope + +Use exactly the normalized periodized field and original endpoint law in the +source Theorem A. In particular d>=2, L and 0=rho}. Define Xi_r on +S_E=E x {0,...,d} by placing one atom (x,j) at each nonsingular index-j critical +point with height in I_r=(b-k r^3,b). Thus N_r=Xi_r(S_E) is the TOTAL window count +on E. Positions and indices are joint marks; their independence is not assumed. +The height is restricted and then discarded as a mark. This note makes no claim +about the height's conditional distribution. + +The mean input and factorial input, summing finitely many indices where needed, +are + + mu_r(dx,{j}) = [k r^3 Lambda_j(x;b,k,u)+e_(r,j)(x)] dx, + |e_(r,j)(x)| <= C r^4 almost everywhere, + q_r:=E_(Q_r^W)[N_r(N_r-1)] <= C r^5 |E|. (S9) + +Theorem A already states the mean-density formulation. Alternatively its error +bound for every Borel set implies absolute continuity and the stated a.e. density +bound. Do not infer that statement from a single value of E. The factorial +estimate is Corollary D, including its uniform-in-E absorption of the separated +Cr^6|E|^2 term using finite torus volume and bounded small r. + +Put + + Lambda(x,j)=Lambda_j(x;b,k,u), + A_E=sum_j integral_E Lambda_j(x;b,k,u) dx, + mu_(0,r)(dx,{j})=k r^3 Lambda_j(x;b,k,u) dx. + +The fixed-remote Lambda_j are continuous, uniformly positive and bounded on the +source's compact parameter ranges. Consequently for |E|>0 and sufficiently small +r, uniformly over these deterministic E, + + c r^3 |E| <= m_r=mu_r(S_E) <= C r^3 |E| <=1, + D_r:=||mu_r-mu_(0,r)||_var <= C r^4 |E|, + q_r/m_r <= C r^2. (S10) + +The cutoff ensuring m_r<=1 uses |E|<=L^d and is uniform in E. Reducing it further +gives q_r0 define + + nu_E(dx,{j}) = Lambda_j(x;b,k,u) dx / A_E. + +Then + + Q_r^W(N_r=1 | N_r>=1) >= 1-C r^2, + dTV(Law(Xi_r | N_r>=1),Delta(mu_r/m_r)) <= C r^2, + dTV(Law(Xi_r | N_r>=1),Delta(nu_E)) <= C r. (S12) + +The distribution of the unique point conditional on N_r=1 obeys the same Cr +bound to nu_E. Equations (S11)-(S12) follow directly from (S2)-(S10), and their +constants have exactly the fixed d,L,rho and compact-mark dependencies of the +inputs. Conditional uniqueness uses p_r>=m_r-q_r/2 and q_r/m_r=O(r^2). + +These bounds hold uniformly even for positive-volume deterministic E=E_r shrinking +inside the SAME D_rho, since |E| cancels from (S10). They do not permit a random +region chosen from the realized field, or rho=rho(r) tending to zero. + +The joint density nu_E need not factor into an independent spatial law and index +law. Restricting to one chosen index gives its corresponding single-type version; +it is not necessary to pretend that several indices occur independently. + +## 6. What this contributes and what remains open + +The new output is a usable rare-event configuration and conditional spatial/index +law, obtained from source-bound mean and pair estimates. It can compare a sampled +remote witness distribution with the normalized contact profile; it cannot certify +an elder-pairing law or the location of a globally selected persistence partner. + +It does not prove a torus-wide second factorial moment, control pairs with either +witness near the pins or at intermediate distances, remove the height window, +produce numerical constants, change any governing status, or prove a nondegenerate +Poisson limit. Ber(mu_r) itself tends to the empty configuration; (S12), obtained +after conditioning on a rare occurrence, is the nontrivial spatial statement. +No Poisson approximation theorem is imported or needed here. + +No mathematical proof is inferred from test counts. Sections 2-4 provide complete +measure-theoretic proofs of the probability statements; Section 5 spells out +exactly which analytic inputs are still required from the Gaussian sources. +Nonauthor review should check the TV convention, empty/single/multiple signed +measure split, normalization factors, arbitrary-Borel mean-error implication, +index marking, and fixed-remote versus global boundaries. + +## 7. Finite controls and limited reconnaissance + +The standard-library test suite computes exact rational probability laws on two +atoms with up to three-point configurations, retaining multiplicities. It checks +(S2)-(S8), sharpness, invalid mean>1 and zero conditioning events, the failure of +first-moment-only inference, and an explicit r-dependent family with r^3 mean, +r^5 factorial moment and r-sized leading conditional correction. Deliberate +mutations distinguish h from P(N>=2), mean from event probability, and TV from +the full variation norm. None of this tests Gaussian field simulation or infinite +configuration spaces. + +Consensus discovery query in this session concerned total variation, factorial +moments and rare single-point processes. A fetched record was Breton--Privault, +*Factorial moments of point processes*, Stochastic Processes and their Applications +124, 3412-3428 (record lists 2013). The fetch supplied metadata only, not an abstract +or theorem. No result from it is consumed. This note's generic probability proof +is elementary, and no novelty or priority claim is made for it. The contribution +claimed here is the explicit, correctly scoped application to the project's remote +critical-point inputs, not invention of Bernoulli approximations. diff --git a/frontiers/remote_singleton_law_20260928/README.md b/frontiers/remote_singleton_law_20260928/README.md new file mode 100644 index 000000000..63d9608f8 --- /dev/null +++ b/frontiers/remote_singleton_law_20260928/README.md @@ -0,0 +1,27 @@ +# Remote single-point law — bounded distributional corollary + +Scientific effect: NONE. AUTHOR_SIDE_REVIEW_REQUIRED. + +Read PROOF.md. It proves the exact generic identity + + dTV(Law Xi, Ber(E Xi)) = E[N;N>=2] <= E[N(N-1)], + +when E N<=1, with probability-TV convention. It then consumes exactly the +fixed-remote mean theorem and remote factorial bound to obtain complete- +configuration error O(r^5), conditional singleton error O(r^2) to the exact mean +profile, and O(r) to the leading location/index density. The region must remain +inside fixed D_rho, and the original between-pin height window is retained. + +This is not a new Gaussian covariance proof, global collision bound, elder-rule +claim, numerical certificate, or nondegenerate Poisson limit. Prior reviews are +not inherited as reviews of this corollary. The full generic proof is separate +from finite control fixtures and from the Gaussian application premises. + +Run (new output directory outside this folder): + + python3 -B -S run_validation.py --output /tmp/new-singleton-validation + +The runner checks SOURCE_FILES membership and hashes, runs 14 named tests in each +normal/optimized Python mode and six semantic mutants, and compares its stored +summary. Its fixtures are finite rational laws, not a continuum proof checker. +No archived research script, network request or status mutation is performed. diff --git a/frontiers/remote_singleton_law_20260928/RESULTS.json b/frontiers/remote_singleton_law_20260928/RESULTS.json new file mode 100644 index 000000000..ddb924e8a --- /dev/null +++ b/frontiers/remote_singleton_law_20260928/RESULTS.json @@ -0,0 +1,12 @@ +{ + "all_mutants_assertion_rejected": true, + "baseline_passed": true, + "continuum_verified": false, + "distinct_mutants": 6, + "modes": [ + "normal", + "optimized" + ], + "named_tests_per_mode": 14, + "scientific_effect": "NONE" +} diff --git a/frontiers/remote_singleton_law_20260928/SOURCE_FILES.json b/frontiers/remote_singleton_law_20260928/SOURCE_FILES.json new file mode 100644 index 000000000..c31b0597c --- /dev/null +++ b/frontiers/remote_singleton_law_20260928/SOURCE_FILES.json @@ -0,0 +1,43 @@ +{ + "files": [ + { + "bytes": 13112, + "git_blob": "2b01956978d7f1d917e929a955f2588263a87426", + "path": "PROOF.md", + "sha256": "f5bbdb0923f5dcdeeb21de7c624a08afe71ebd8c0b8c09e67152359ff544615a" + }, + { + "bytes": 1367, + "git_blob": "63d9608f85f4c0f2146978154824a5591677429e", + "path": "README.md", + "sha256": "eb00fc3c5faa55f92df599b4c7db98d26cef1e4424d2e50ecbee402e0e6fbb2c" + }, + { + "bytes": 237, + "git_blob": "ddb924e8ab8e1e05ee809474346b41dfcb6960a0", + "path": "RESULTS.json", + "sha256": "dd03dd87754fce5b27950a0f3a1eb5b2131659d96e5b69fc2891d3e7a34e1fae" + }, + { + "bytes": 2324, + "git_blob": "d33187b5b53842082fdf12e51fdfbff861b4fd44", + "path": "finite_law.py", + "sha256": "6da15ef3fe1d76af68b4df0630c7dc347868a9369d95eae61d46e833b3aae74c" + }, + { + "bytes": 4336, + "git_blob": "311503783d88e55aa742c76027983fd0692c1f41", + "path": "run_validation.py", + "sha256": "744cc6ebee673f8562311df43d8209f55f0b34700a9b56989d8e0ca6827412af" + }, + { + "bytes": 5826, + "git_blob": "45244c3cf659c62e2f237de20bfa36f76b4abf50", + "path": "test_finite_law.py", + "sha256": "23823e6ff8f67d0d2a0ac636a8f68365f269d3638924a020c7b58b92fe36189d" + } + ], + "review_status": "AUTHOR_SIDE_REVIEW_REQUIRED", + "schema": 1, + "scientific_effect": "NONE" +} diff --git a/frontiers/remote_singleton_law_20260928/finite_law.py b/frontiers/remote_singleton_law_20260928/finite_law.py new file mode 100644 index 000000000..d33187b5b --- /dev/null +++ b/frontiers/remote_singleton_law_20260928/finite_law.py @@ -0,0 +1,70 @@ +"""Exact finite probability algebra. Not a Gaussian or continuum verifier.""" +from fractions import Fraction as F + + +def exact(x): + if isinstance(x,bool) or not isinstance(x,(int,F)): + raise TypeError('int or Fraction required') + return F(x) + + +def validate(p): + if not isinstance(p,dict):raise TypeError('finite law must be a dictionary') + if any(not isinstance(c,tuple) or any(type(x) is not int or x<0 for x in c) + or tuple(sorted(c))!=c for c in p): + raise ValueError('sorted tuples of nonnegative integer atoms required') + vals=[exact(v) for v in p.values()] + if any(v<0 for v in vals) or sum(vals)!=1: + raise ValueError('probabilities must be nonnegative and sum to one') + + +def mean_measure(p): + validate(p); mu={} + for c,w in p.items(): + for x in c: + mu[x]=mu.get(x,F(0))+w + return mu + + +def multiple_point_mass(p): + validate(p) + return sum((len(c)*w for c,w in p.items() if len(c)>=2),F(0)) + + +def factorial(p): + validate(p) + return sum((len(c)*(len(c)-1)*w for c,w in p.items()),F(0)) + + +def bernoulli(mu): + if not isinstance(mu,dict):raise TypeError('measure must be a dictionary') + vals={x:exact(v) for x,v in mu.items()} + if any(type(x) is not int or x<0 for x in vals) or any(v<0 for v in vals.values()): + raise ValueError('nonnegative measure on integer atoms required') + m=sum(vals.values(),F(0)) + if m>1:raise ValueError('Bernoulli mean cannot exceed one') + return {():1-m,**{(x,):v for x,v in vals.items()}} + + +def tv(p,q): + """Half total mass norm; inputs used as probabilities in the tests.""" + return sum((abs(exact(p.get(c,0))-exact(q.get(c,0))) for c in set(p)|set(q)),F(0))/2 + + +def nonempty(p): + validate(p) + mass=sum((w for c,w in p.items() if c),F(0)) + if mass==0:raise ValueError('nonempty event has zero probability') + return {c:w/mass for c,w in p.items() if c} + + +def unique(p): + validate(p); mass=sum((w for c,w in p.items() if len(c)==1),F(0)) + if mass==0:raise ValueError('singleton event has zero probability') + return {c:w/mass for c,w in p.items() if len(c)==1} + + +def conditional_multiple_bound(q,p): + q,p=map(exact,(q,p)) + if q<0 or not 0=2','w for c,w in p.items() if len(c)>=2'), + 'erase_multiplicity':('for x in c:','for x in set(c):'), + 'wrong_nonempty_normalizer':('mass=sum((w for c,w in p.items() if c),F(0))','mass=sum((len(c)*w for c,w in p.items()),F(0))'), + 'wrong_empty_mass':('return {():1-m,','return {():m,'), + 'square_instead_of_factorial':('len(c)*(len(c)-1)*w','len(c)*len(c)*w'), +} + + +def require(ok,msg): + if not ok:raise RuntimeError(msg) + + +def identity(p): + require(p.is_file() and not p.is_symlink(),'not a regular file: '+p.name) + b=p.read_bytes() + return {'bytes':len(b),'sha256':hashlib.sha256(b).hexdigest(), + 'git_blob':hashlib.sha1(('blob '+str(len(b))+'\0').encode()+b).hexdigest()} + + +def sources(): + rows=json.loads((ROOT/'SOURCE_FILES.json').read_text())['files']; seen=set() + for row in rows: + name=row['path'] + require(name not in seen and Path(name).name==name and name!='SOURCE_FILES.json','invalid source path') + seen.add(name) + require(identity(ROOT/name)=={k:row[k] for k in ['bytes','sha256','git_blob']},'source mismatch: '+name) + require({p.name for p in ROOT.iterdir()}==seen|{'SOURCE_FILES.json'},'extra/missing source member') + return {p.name:identity(p) for p in sorted(ROOT.iterdir())} + + +def main(): + ap=argparse.ArgumentParser(description=__doc__); ap.add_argument('--output',type=Path,required=True) + out=ap.parse_args().output.resolve() + require(not out.exists() and not out.is_relative_to(ROOT),'new output path outside source required') + before=sources(); out.mkdir(parents=True); code=(ROOT/'finite_law.py').read_text() + report={'passed':False,'scientific_effect':'NONE','continuum_verified':False,'source_files':before,'modes':{}} + try: + for mode,flags in [('normal',[]),('optimized',['-O'])]: + results={} + for name,pair in [('baseline',None),*MUTANTS.items()]: + cwd=ROOT + if pair: + old,new=pair; require(code.count(old)==1,'mutation not unique: '+name) + cwd=out/'mutants'/mode/name; cwd.mkdir(parents=True) + (cwd/'finite_law.py').write_text(code.replace(old,new)) + (cwd/'test_finite_law.py').write_bytes((ROOT/'test_finite_law.py').read_bytes()) + r=subprocess.run([sys.executable,'-B',*flags,'-S','-m','unittest','-v','test_finite_law'], + cwd=cwd,capture_output=True,timeout=30) + (out/(name+'_'+mode+'.stdout')).write_bytes(r.stdout) + (out/(name+'_'+mode+'.stderr')).write_bytes(r.stderr) + t=r.stderr.decode('utf8','replace') + require('Ran 14 tests' in t and 'skipped=' not in t,'test count: '+name) + if pair: + require(r.returncode==1 and 'AssertionError' in t and 'FAILED (failures=' in t and 'errors=' not in t, + 'mutant did not assertion-reject: '+name) + else:require(r.returncode==0 and t.rstrip().endswith('OK'),'baseline failed') + results[name]={'exit_code':r.returncode,'assertion_rejected':bool(pair)} + report['modes'][mode]=results + summary={'named_tests_per_mode':14,'distinct_mutants':6,'modes':['normal','optimized'], + 'baseline_passed':True,'all_mutants_assertion_rejected':True, + 'scientific_effect':'NONE','continuum_verified':False} + raw=(json.dumps(summary,sort_keys=True,indent=2)+'\n').encode() + require((ROOT/'RESULTS.json').read_bytes()==raw,'stored summary mismatch') + for mode in ['normal','optimized']:(out/('summary_'+mode+'.json')).write_bytes(raw) + require(sources()==before,'source mutation detected') + report.update(passed=True,sources_unchanged=True,deterministic_summaries_equal=True) + print(raw.decode(),end='') + finally:(out/'REPORT.json').write_text(json.dumps(report,sort_keys=True,indent=2)+'\n') +if __name__=='__main__':main() diff --git a/frontiers/remote_singleton_law_20260928/test_finite_law.py b/frontiers/remote_singleton_law_20260928/test_finite_law.py new file mode 100644 index 000000000..45244c3cf --- /dev/null +++ b/frontiers/remote_singleton_law_20260928/test_finite_law.py @@ -0,0 +1,129 @@ +"""Finite rational laws test the probability algebra, not a Gaussian theorem.""" +from fractions import Fraction as F +from itertools import product +import unittest +import finite_law as a + + +def laws(): + for aa,bb,cc,dd in product(range(3), repeat=4): + p={():1-F(aa+bb+cc+dd,12),(0,):F(aa,12),(1,):F(bb,12), + (0,1):F(cc,12),(0,0,1):F(dd,12)} + if sum(F(len(c))*w for c,w in p.items())<=1: + yield p + + +def brute_tv(p,q): + return sum(abs(p.get(k,F(0))-q.get(k,F(0))) for k in set(p)|set(q))/2 + + +def brute_mean(p): + return {x:sum(w*c.count(x) for c,w in p.items()) for x in {x for c in p for x in c}} + + +class FiniteLawTests(unittest.TestCase): + def test_two_point_sharp_identity(self): + p={():F(3,4),(0,1):F(1,4)} + b=a.bernoulli(a.mean_measure(p)) + self.assertEqual(b,{():F(1,2),(0,):F(1,4),(1,):F(1,4)}) + self.assertEqual(a.tv(p,b),F(1,2)) + self.assertEqual(a.multiple_point_mass(p),F(1,2)) + self.assertEqual(a.factorial(p),F(1,2)) + + def test_grid_exact_identity_and_factorial_bound(self): + for p in laws(): + mu=a.mean_measure(p); b=a.bernoulli(mu) + self.assertEqual(mu,brute_mean(p)) + self.assertEqual(sum(b.values()),1) + self.assertEqual(a.tv(p,b),brute_tv(p,b)) + h=sum(len(c)*w for c,w in p.items() if len(c)>=2) + self.assertEqual(a.multiple_point_mass(p),h) + self.assertEqual(a.tv(p,b),h) + self.assertLessEqual(h,a.factorial(p)) + + def test_conditional_nonempty_configuration_law(self): + for p in laws(): + mu=a.mean_measure(p); m=sum(mu.values()) + if not m: continue + one={(x,):w/m for x,w in mu.items()} + q=a.nonempty(p) + self.assertEqual(q,{c:w/sum(v for d,v in p.items() if d) for c,w in p.items() if c}) + self.assertEqual(sum(q.values()),1) + self.assertLessEqual(a.tv(q,one),a.multiple_point_mass(p)/m) + + def test_conditional_unique_location_law(self): + for p in laws(): + mass=sum(w for c,w in p.items() if len(c)==1) + if not mass: continue + mu=a.mean_measure(p); m=sum(mu.values()) + target={(x,):v/m for x,v in mu.items()} + q=a.unique(p) + self.assertEqual(sum(q.values()),1) + self.assertLessEqual(a.tv(q,target),a.multiple_point_mass(p)/m) + + def test_count_tail_and_mean_minus_event(self): + for p in laws(): + m=sum(a.mean_measure(p).values()); event=sum(v for c,v in p.items() if c) + tail=sum(v for c,v in p.items() if len(c)>=2); q=a.factorial(p) + self.assertGreaterEqual(m-event,0) + self.assertLessEqual(m-event,q/2) + if event: + self.assertLessEqual(tail/event,a.conditional_multiple_bound(q,event)) + p={():F(3,4),(0,1):F(1,4)} + self.assertEqual(a.conditional_multiple_bound(a.factorial(p),F(1,4)),1) + + def test_multiplicity_not_distinct_site_count(self): + p={():F(7,8),(0,0,1):F(1,8)} + self.assertEqual(a.mean_measure(p),{0:F(1,4),1:F(1,8)}) + self.assertEqual(a.factorial(p),F(3,4)) + self.assertEqual(a.multiple_point_mass(p),F(3,8)) + + def test_mean_one_boundary(self): + self.assertEqual(a.bernoulli({0:F(2,3),1:F(1,3)}),{():F(0),(0,):F(2,3),(1,):F(1,3)}) + + def test_mean_above_one_rejected(self): + with self.assertRaises(ValueError): a.bernoulli({0:F(5,4)}) + with self.assertRaises(ValueError): a.bernoulli({0:F(-1,4)}) + + def test_empty_conditioning_rejected(self): + self.assertEqual(a.bernoulli({}),{():F(1)}) + with self.assertRaises(ValueError): a.nonempty({():F(1)}) + with self.assertRaises(ValueError): a.unique({():F(3,4),(0,1):F(1,4)}) + + def test_bad_law_inputs_rejected(self): + for p in [{():F(1,2)}, {():F(3,2),(0,):F(-1,2)}, {(1,0):F(1)}, {(True,):F(1)}]: + with self.assertRaises((TypeError,ValueError)): a.mean_measure(p) + with self.assertRaises(TypeError): a.mean_measure({():1.0}) + + def test_first_moment_does_not_imply_fifth_order_error(self): + for n in [2,4,16,64]: + r=F(1,n); p={():1-r**3/2,(0,1):r**3/2} + self.assertEqual(sum(a.mean_measure(p).values()),r**3) + self.assertEqual(a.tv(p,a.bernoulli(a.mean_measure(p))),r**3) + self.assertEqual(a.tv(p,a.bernoulli(a.mean_measure(p)))/r**5,1/r**2) + + def test_mark_dependence_not_independence(self): + # At site0 only mark0; at site1 only mark1. Encoded marks remain atoms. + p={():F(3,4),(0,):F(1,8),(3,):F(1,8)} + self.assertEqual(a.nonempty(p),{(0,):F(1,2),(3,):F(1,2)}) + independent={(0,):F(1,4),(1,):F(1,4),(2,):F(1,4),(3,):F(1,4)} + self.assertEqual(a.tv(a.nonempty(p),independent),F(1,2)) + + def test_normalized_mean_perturbation_bound(self): + for aa,bb,cc,dd in product(range(1,4),repeat=4): + mu={0:F(aa,12),1:F(bb,12)}; nu={0:F(cc,12),1:F(dd,12)} + m=sum(mu.values()); n=sum(nu.values()) + delta=sum(abs(mu[x]-nu[x]) for x in mu) + self.assertLessEqual(a.tv({x:v/m for x,v in mu.items()},{x:v/n for x,v in nu.items()}),delta/m) + self.assertLessEqual(a.tv(a.bernoulli(mu),a.bernoulli(nu)),delta) + + def test_explicit_remote_rate_model(self): + for n in [4,8,16,32,64]: + r=F(1,n); c=r**5/4 + p={(0,):r**3/3+r**4/4,(1,):2*r**3/3-r**4/4,(0,1):c} + p[()]=1-sum(p.values()); mu=a.mean_measure(p); m=sum(mu.values()) + self.assertEqual(a.tv(p,a.bernoulli(mu)),r**5/2) + self.assertLessEqual(a.tv(a.nonempty(p),{(x,):v/m for x,v in mu.items()}),r**2/2) + self.assertLessEqual(a.tv(a.nonempty(p),{(0,):F(1,3),(1,):F(2,3)}),r) + +if __name__=='__main__':unittest.main(verbosity=2)