From 544499292f1cf09fe1bd030ce25d7cd0d80fc38c Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 19:44:15 -0700 Subject: [PATCH] Add quantitative two-mass moment floors and exact controls MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Dylan Roy — delegated AI work. Actual author OpenAI / GPT-6 Astra Pro, continuation-d2-proof-execution-audit-20261006. Complete square proof, individual sharpness, C7 comparison, and conditional all-angle scalar floors. Six additive files only; zero Lean declarations, no existing proof/gate/dependency/status change. Tests first failed on absent implementation, then10 methods passed in each mode with exact named mutant protocols. Scientific effect NONE; separate nonauthor review required. --- .github/workflows/d2-two-mass-floors.yml | 86 ++++++++ reviews/d2_two_mass_floors_20261006/NOTE.md | 200 ++++++++++++++++++ .../d2_two_mass_floors_20261006/RESULTS.json | 1 + .../d2_two_mass_floors_20261006/SOURCES.json | 38 ++++ .../test_two_mass.py | 108 ++++++++++ .../d2_two_mass_floors_20261006/two_mass.py | 123 +++++++++++ 6 files changed, 556 insertions(+) create mode 100644 .github/workflows/d2-two-mass-floors.yml create mode 100644 reviews/d2_two_mass_floors_20261006/NOTE.md create mode 100644 reviews/d2_two_mass_floors_20261006/RESULTS.json create mode 100644 reviews/d2_two_mass_floors_20261006/SOURCES.json create mode 100644 reviews/d2_two_mass_floors_20261006/test_two_mass.py create mode 100644 reviews/d2_two_mass_floors_20261006/two_mass.py diff --git a/.github/workflows/d2-two-mass-floors.yml b/.github/workflows/d2-two-mass-floors.yml new file mode 100644 index 000000000..cb27256ab --- /dev/null +++ b/.github/workflows/d2-two-mass-floors.yml @@ -0,0 +1,86 @@ +name: D2 two-mass floors exact controls + +'on': + pull_request: + paths: + - 'reviews/d2_two_mass_floors_20261006/**' + - '.github/workflows/d2-two-mass-floors.yml' + - 'formal/ResearchFormalCoreR1/D2Schur.lean' + - 'reviews/side24_d2_certified_small_L_claude_20261005/NOTE.md' + push: + branches: [main] + paths: + - 'reviews/d2_two_mass_floors_20261006/**' + - '.github/workflows/d2-two-mass-floors.yml' + - 'formal/ResearchFormalCoreR1/D2Schur.lean' + - 'reviews/side24_d2_certified_small_L_claude_20261005/NOTE.md' + workflow_dispatch: + +permissions: + contents: read + +jobs: + two-mass-controls: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + fetch-depth: 0 + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.13.5' + - name: Authenticate sources and run exact controls in both modes + shell: bash + run: | + set -euo pipefail + P=reviews/d2_two_mass_floors_20261006 + python -B -S - <<'PY' + import hashlib, json, os, pathlib, subprocess + def need(ok, message): + if not ok: raise ValueError(message) + def pairs(items): + result={} + for key,value in items: + need(key not in result, 'duplicate JSON key') + result[key]=value + return result + def git(*args): + return subprocess.run(['git',*args],check=True,capture_output=True).stdout + def identity(raw): + return {'bytes':len(raw),'sha256':hashlib.sha256(raw).hexdigest(), + 'git_blob':hashlib.sha1(b'blob %d\0'%len(raw)+raw).hexdigest()} + prefix='reviews/d2_two_mass_floors_20261006' + workflow='.github/workflows/d2-two-mass-floors.yml' + meta=json.loads(pathlib.Path(prefix,'SOURCES.json').read_bytes(),object_pairs_hook=pairs) + need(set(meta)=={'object','scientific_effect','files','upstream'},'manifest shape') + need(meta['object']=='D2-TWO-MASS-FLOORS-20261006-v1' and meta['scientific_effect']=='NONE','scope') + expected={prefix+'/'+n for n in ('NOTE.md','two_mass.py','test_two_mass.py','RESULTS.json')} + expected.add(workflow) + need(set(meta['files'])==expected,'manifest inventory') + actual=set(git('ls-tree','-r','--name-only','HEAD','--',prefix).decode().splitlines())|{workflow} + need(actual==expected|{prefix+'/SOURCES.json'},'tracked packet membership') + for path in expected|{prefix+'/SOURCES.json'}: + p=pathlib.Path(path) + need(not any(q.is_symlink() for q in [p,*p.parents]),'symlink source') + raw=p.read_bytes() + need(raw==git('show','HEAD:'+path),'dirty source: '+path) + if path in expected: need(identity(raw)==meta['files'][path],'source identity: '+path) + pins={ + 'formal/ResearchFormalCoreR1/D2Schur.lean':'b95460c0d263a32ea274b347079cca6aaab3d2e9', + 'reviews/side24_d2_certified_small_L_claude_20261005/NOTE.md':'852f7403a8a06a1ef061e363df9502ae16f7a341'} + need(meta['upstream']=={'commit':'2f8b6f372be383d752e9dd30d38234faa977243c','files':pins},'upstream contract') + for path,bid in pins.items(): + need(git('rev-parse','HEAD:'+path).decode().strip()==bid,'changed consumed slice') + need(identity(git('show',meta['upstream']['commit']+':'+path))['git_blob']==bid,'historical source') + need(git('rev-parse','HEAD').decode().strip()==os.environ['GITHUB_SHA'],'tested commit') + print('source membership, Git HEAD and upstream pins PASS; scientific effect NONE') + PY + python -B -S "$P/test_two_mass.py" + python -B -O -S "$P/test_two_mass.py" + python -B -S "$P/two_mass.py" > /tmp/two-mass-normal.json + python -B -O -S "$P/two_mass.py" > /tmp/two-mass-optimized.json + cmp "$P/RESULTS.json" /tmp/two-mass-normal.json + cmp /tmp/two-mass-normal.json /tmp/two-mass-optimized.json + echo 'PASS: finite rational controls only; no new Lean or scientific acceptance' diff --git a/reviews/d2_two_mass_floors_20261006/NOTE.md b/reviews/d2_two_mass_floors_20261006/NOTE.md new file mode 100644 index 000000000..b3e3b3376 --- /dev/null +++ b/reviews/d2_two_mass_floors_20261006/NOTE.md @@ -0,0 +1,200 @@ +# Quantitative two-mass floors for the d2 moment interface + +Object: D2-TWO-MASS-FLOORS-20261006-v1. +Dylan Roy — delegated AI work. Author: OpenAI / GPT-6 Astra Pro, +`continuation-d2-proof-execution-audit-20261006`; author exposure to D2Schur and +AUD-309-REVIEW-STRICTNESS-01. Scientific effect NONE; organizational-independence +credit 0. This is an additive analytical candidate, not an accepted scientific +status or a Lean theorem. Claim: main#229/6008048138. + +## 1. Scope and predecessor distinction + +The existing #302 NOTE section 4/C7 already gives two-radius Gram floors. The +qualitative #317 companion proves actual-integral residual identities and strict +positivity from suitable atoms. This note does not rebrand either as new. Its +additional result is a locally normalized, sharp two-mass lower bound, compared +explicitly with the older pair bounds, and its propagation through the existing +d2 scalar formulas. No reviewed packet, gate, manifest, dependency or verdict is +modified. The elementary completion-of-squares argument is included in full. + +Let X be a measurable real random variable on a probability space, with finite +second, fourth and sixth moments. Write + + m2 = E[X^2], m4 = E[X^4], m6 = E[X^6], + G = m4 - m2^2, Delta = m6 - m4^2/m2. + +Take distinct squared radii s,t > 0 and lower masses p,r > 0 such that + + P(X^2=s) >= p, P(X^2=t) >= r. + +Thus p+r <= 1. The masses aggregate both signs; no symmetry or independence is +assumed. Put H(u,v)=uv/(u+v) for nonnegative u,v with positive sum, and + + ell = p*s + r*t, + g = H(p,r)*(s-t)^2, + d = H(p*s,r*t)*(s-t)^2. + +All three numbers are strictly positive. The conclusion is + + m2 >= ell, G >= g, Delta >= d. (1) + +A zero radius is allowed for the G bound, but then d=0 and strict Delta does NOT +follow. Merely having nonconstant |X| does not imply Delta>0. The zero/+-1 example +from AUD-309-REVIEW-STRICTNESS-01 has G=1/4 and Delta=0. + +## 2. Complete proof and exact hypotheses + +For u,v>0 and real A,B,c, expansion gives + + u(A-c)^2 + v(B-c)^2 + = H(u,v)(A-B)^2 + (u+v)(c-(u*A+v*B)/(u+v))^2. (2) + +Hence the left side is at least its first term, for EVERY c; equality occurs at +the displayed weighted mean. This is an exact algebraic identity, not a numerical +interpolation or a reliance on a finite test grid. + +The two disjoint level sets yield m2 >= p*s+r*t. Probability normalization and +integrability give G=E[(X^2-m2)^2]. Retaining only those two nonnegative level-set +contributions, and then applying (2) with (u,v,A,B,c)=(p,r,s,t,m2), proves G>=g. + +For m2>0, expansion and linearity of the integrals give + + Delta = E[(X^3-(m4/m2)X)^2] + = E[X^2 (X^2-m4/m2)^2]. (3) + +All terms are integrable by the stated moment assumptions. Retaining the same +level sets gives p*s*(s-m4/m2)^2+r*t*(t-m4/m2)^2. Apply (2) with u=p*s,v=r*t to +obtain Delta>=d. Lower masses can replace actual masses because every retained +squared contribution is nonnegative. No distributional independence was used. + +The Delta part of the argument also holds for a nonnegative measure not +normalized to probability, provided the moments are integrable and m2>0. The +unscaled G identity requires probability normalization: for a finite measure of +total mass M, the centered integral is m4-2*m2^2+M*m2^2, not generally m4-m2^2. +For example, 2*delta_1 gives centered integral 2 but m4-m2^2=-2. The executable +`floors` helper deliberately accepts probability-mass inputs only. + +## 3. Individual sharpness, not simultaneous optimizer claims + +Fix exact p,r,s,t with s,t>0, s!=t and p+r<=1. These are squared-radius laws; each +is realized by X=sqrt(Y), or by any split of each mass between the two signs. + +For Delta, the law of Y=X^2 assigning p to s, r to t and 1-p-r to 0 attains d. +Indeed, c=m4/m2=(p*s^2+r*t^2)/(p*s+r*t), the weighted mean in (2) with u=p*s,v=r*t; +the remaining zero atom contributes nothing to the residual (3). + +For G, put c0=(p*s+r*t)/(p+r). Assign p to s, r to t and 1-p-r to c0. This law +has m2=c0 and attains g. Thus neither constant in (1) can be increased uniformly +using just these two exact masses/radii. + +For p+r<1, these are different extremizers. The residual-optimal nonzero squared +radius is (p*s^2+r*t^2)/(p*s+r*t), strictly larger than c0 by +p*r*(s-t)^2/((p*s+r*t)*(p+r)). We do NOT claim simultaneous attainment of both +floors by a common law when unassigned mass remains. The later combined scalar +bounds are valid conservative consequences, not asserted optimal joint bounds. + +## 4. Comparison with the existing lattice Gram floors + +For s=h^2,t=4h^2, p=P(|X|=h), r=P(|X|=2h), (1) reads + + G >= 9*h^4*p*r/(p+r), + Delta >= 36*h^6*p*r/(p+4*r). (4) + +The older #302/C7 floors are 9*h^4*p*r and 36*h^8*p*r/m2. The first new bound is +at least the old because p+r<=1. The second is at least the old because +m2>=h^2*(p+4*r). This is only a symbolic comparison; it does not replace the +existing outward enclosures or supply new numerical values for any period. +The comparison is not a claim that the old, correct bounds were defective. + +## 5. Explicit all-direction scalar bounds + +This section uses the exact algebraic formulas of the existing D2Schur source. +It does not identify a Gaussian/Palm covariance with those scalar expressions. +For q in the CLOSED interval [0,1/4], set + + D(q) = m2^2*m4 + (m4-3*m2^2)*(m4+m2^2)*q, + N = m2^2*(m4^2-m2^4), S(q)=N/D(q), + T(q) = Delta*(1-3*q) + 9*q*m2*G. + +The endpoint identities are + + D(0)=m2^2*m4, D(1/4)=G*(m4+3*m2^2)/4, + T(0)=Delta, T(1/4)=(Delta+9*m2*G)/4. + +Both D and T are affine. Given ACTUAL upper bounds m2<=U2 and m4<=U4, define + + D_lower = min{ell^2*(ell^2+g), g*(4*ell^2+g)/4}, + D_upper = max{U2^2*U4, (U4-ell^2)*(U4+3*U2^2)/4}, + N_lower = ell^2*g*(2*ell^2+g), + T_lower = min{d, (d+9*ell*g)/4}. + +Then + + 0 < D_lower <= D(q) <= D_upper, + 0 < N_lower/D_upper <= S(q), + 0 < T_lower <= T(q). (5) + +Proof: m4=m2^2+G, m2>=ell and G>=g give each determinant endpoint lower bound +and N>=N_lower. For the upper bound, m2^2*m4<=U2^2*U4, and +G<=U4-ell^2 while m4+3*m2^2<=U4+3*U2^2. All factors are nonnegative; +U4-ell^2>=g>0 follows from the actual assumptions. Affine interpolation now +bounds D at every q. Divide the positive N lower bound by the D upper bound; +using the LOWER determinant in this division would give the wrong direction. +Similarly both T endpoints dominate their indicated expressions, so affine +interpolation proves the final bound. Formula S=N/D uses D>0 just established, +not Lean's totalized division at zero. The determinant lower bound and T bound +do not require U2,U4; only the explicit Schur bound above uses them. + +## 6. Uniform-input interface and its limits + +H is nondecreasing in each nonnegative argument: for u'>=u and v>0, + + H(u',v)-H(u,v)=v^2*(u'-u)/((u'+v)*(u+v)) >= 0. + +Suppose a family has certified lower masses p_-,r_->0, lower squared radii +s_-,t_->0, and a certified separation |s-t|>=eta>0. Then uniform substitutes are + + ell_- = p_-*s_-+r_-*t_-, + g_- = H(p_-,r_-)*eta^2, + d_- = H(p_-*s_-,r_-*t_-)*eta^2. + +Together with actual uniform U2,U4 these may be used in (5). They are inputs, +NOT certificates supplied here. Overlapping radius intervals do not establish a +positive eta. Two merely positive masses need not be bounded away from zero. +In particular X -> epsilon*X scales G by epsilon^4 and Delta by epsilon^6; +strict positivity alone cannot give a uniform positive floor. No claim is made +uniformly over all L, all marks, or the actual periodic spectral family. + +A follow-on Lean development may first formalize (2) and its inequalities, then +use the actual-integral identities from #317 and measurable level-set bounds. +This packet adds ZERO Lean declarations and does not alter the primary 63-target +manifest. The existing qualitative companion's review is not a review of (1)-(6). + +## 7. Reproduction, controls and source map + +Run, from this directory: + + python -B -S test_two_mass.py + python -B -O -S test_two_mass.py + python -B -S two_mass.py + python -B -O -S two_mass.py + +The checker uses Fraction only. Its seven mutations must exit1 with exactly the +named failing check and empty stderr: M1 square completion; M2 fourth floor; +M3 Delta floor; M4 wrong tau endpoint; M5 omitted probability normalization; +M6 wrong Schur denominator endpoint; M7 zero-atom strictness. M9 exits2 with +exactly `unknown mutant\n`. These are finite controls, not a continuum proof. +The dedicated workflow validates source membership/hashes and pinned upstream +blobs, then runs both test modes and authentic baseline/mutation protocols. +Configured CI is not successful execution; actual run identity is recorded in +the PR, separately from the theorem's ordinary mathematical review. + +SOURCES.json records exact immutable upstream files. The consumed algebraic +source is Math- commit 2f8b6f372be383d752e9dd30d38234faa977243c: +- formal/ResearchFormalCoreR1/D2Schur.lean (scalar definitions and endpoint facts); +- reviews/side24_d2_certified_small_L_claude_20261005/NOTE.md, sections2/4 (original + reduction and C7 comparison only; its numerical outputs are not recertified). +The #317 actual-integral source at b122462634460a8bb9e88406072cb7a356957407 is +motivating correspondence, not needed as an accepted premise: (2)-(3) are proved +above. Its existing review and kernel evidence do not transfer to this note. +No private cloud source is an input to this packet. diff --git a/reviews/d2_two_mass_floors_20261006/RESULTS.json b/reviews/d2_two_mass_floors_20261006/RESULTS.json new file mode 100644 index 000000000..f5cb50038 --- /dev/null +++ b/reviews/d2_two_mass_floors_20261006/RESULTS.json @@ -0,0 +1 @@ +{"checks":{"delta_floor":true,"fourth_floor":true,"probability_boundary":true,"schur_endpoint":true,"square_completion":true,"tau_endpoint":true,"zero_atom_boundary":true},"controls":{"boundary_cases":2,"completion":27,"directional_cases":480,"finite_laws":60},"failed":[],"method":"exact finite diagnostics; not continuum or Lean proof","ok":true,"scientific_effect":"NONE"} diff --git a/reviews/d2_two_mass_floors_20261006/SOURCES.json b/reviews/d2_two_mass_floors_20261006/SOURCES.json new file mode 100644 index 000000000..726286d35 --- /dev/null +++ b/reviews/d2_two_mass_floors_20261006/SOURCES.json @@ -0,0 +1,38 @@ +{ + "files": { + ".github/workflows/d2-two-mass-floors.yml": { + "bytes": 4326, + "git_blob": "cb27256abc00337b6b6625ab03d5a76cb69c1817", + "sha256": "799a3b99a3c6972cac2c2a5916ffc6cc1517e2fc9f1569ff734d81b34c89ec71" + }, + "reviews/d2_two_mass_floors_20261006/NOTE.md": { + "bytes": 9509, + "git_blob": "b3e3b337697e4bf8c15bdab3666e49dc8833ca80", + "sha256": "6d8a41ada3dc7a104765c33f85aa58938d3572786b6ec7e7963f3e5b9f9c04c9" + }, + "reviews/d2_two_mass_floors_20261006/RESULTS.json": { + "bytes": 376, + "git_blob": "f5cb50038b22340692acd89ab684a0282e17a847", + "sha256": "aeedeab1a1e387a902f6a8c0593ceda81510c76d50e9731dd7d962314dcf4e4b" + }, + "reviews/d2_two_mass_floors_20261006/test_two_mass.py": { + "bytes": 4929, + "git_blob": "88041eaf70e720f1a10e0dcda643e42a7e9cbf47", + "sha256": "b055156564b0ae768825adaac64bdbc87041b967aad095d0020dea9714e7e44c" + }, + "reviews/d2_two_mass_floors_20261006/two_mass.py": { + "bytes": 5667, + "git_blob": "c56170026bc4e9328c0a8eddf4100dc094d808f6", + "sha256": "344c070966d2836fc12712b60f805c4b62d858789414f9ebe309d689e65afb9b" + } + }, + "object": "D2-TWO-MASS-FLOORS-20261006-v1", + "scientific_effect": "NONE", + "upstream": { + "commit": "2f8b6f372be383d752e9dd30d38234faa977243c", + "files": { + "formal/ResearchFormalCoreR1/D2Schur.lean": "b95460c0d263a32ea274b347079cca6aaab3d2e9", + "reviews/side24_d2_certified_small_L_claude_20261005/NOTE.md": "852f7403a8a06a1ef061e363df9502ae16f7a341" + } + } +} diff --git a/reviews/d2_two_mass_floors_20261006/test_two_mass.py b/reviews/d2_two_mass_floors_20261006/test_two_mass.py new file mode 100644 index 000000000..88041eaf7 --- /dev/null +++ b/reviews/d2_two_mass_floors_20261006/test_two_mass.py @@ -0,0 +1,108 @@ +#!/usr/bin/env python3 +"""Exact finite controls; not continuum proof or a Lean execution.""" +from fractions import Fraction as F +import importlib.util +import json +from pathlib import Path +import subprocess +import sys +import unittest + +SIDE = Path(__file__).resolve().parent + +class TwoMassTests(unittest.TestCase): + def module(self): + path = SIDE / 'two_mass.py' + self.assertTrue(path.is_file(), 'two_mass.py implementation is missing') + spec = importlib.util.spec_from_file_location('two_mass_control', path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + def test_weighted_completion(self): + m = self.module() + for u in (F(1,7), F(1), F(4)): + for v in (F(1,9), F(2), F(7)): + for a,b,c in ((F(-3),F(2),F(1)),(F(1),F(4),F(0)),(F(1),F(4),(u+4*v)/(u+v))): + self.assertEqual(u*(a-c)**2+v*(b-c)**2, + m.harmonic(u,v)*(a-b)**2+(u+v)*(c-(u*a+v*b)/(u+v))**2) + + def test_probability_mass_domain(self): + m = self.module() + for args in ((F(0),F(1,2),F(1),F(4)),(F(1),F(1),F(1),F(4)), + (F(1,4),F(1,4),F(-1),F(4)),(F(1,4),F(1,4),F(1),F(1))): + with self.assertRaises(ValueError): m.floors(*args) + with self.assertRaises(TypeError): m.floors(0.25,F(1,4),F(1),F(4)) + + def test_distinct_sharp_extremizers(self): + m = self.module(); p,r,s,t = F(1,5),F(2,5),F(1),F(9) + f = m.floors(p,r,s,t); d = (p*s+r*t)/(p+r) + a2,a4,a6 = m.moments([(s,p),(t,r),(F(0),1-p-r)]) + self.assertEqual(a6-a4*a4/a2, f['delta']) + self.assertGreater(a4-a2*a2, f['gap']) + b2,b4,b6 = m.moments([(s,p),(t,r),(d,1-p-r)]) + self.assertEqual(b4-b2*b2, f['gap']) + self.assertGreater(b6-b4*b4/b2, f['delta']) + + def test_zero_radius_is_not_strict_delta(self): + m = self.module(); f=m.floors(F(1,2),F(1,2),F(0),F(1)) + self.assertEqual(f['gap'],F(1,4)); self.assertEqual(f['delta'],0) + self.assertEqual(m.moments([(F(0),F(1,2)),(F(1),F(1,2))]),(F(1,2),)*3) + + def test_mass_and_radius_lower_bounds(self): + m = self.module() + for u,v in ((F(1,10),F(2,5)),(F(2),F(3))): + self.assertLessEqual(m.harmonic(u,v),m.harmonic(2*u,3*v)) + p,r,s,t=F(1,5),F(1,3),F(1,4),F(4) + lower=m.floors(p/2,r/3,s,t); actual=m.floors(p,r,s,t) + for key in lower: self.assertLessEqual(lower[key],actual[key]) + + def test_lattice_floor_dominates_old_pair_floor(self): + m=self.module(); p,r,h=F(1,6),F(1,9),F(1,3) + s,t=h*h,4*h*h + m2,m4,m6=m.moments([(s,p),(t,r),(9*h*h,1-p-r)]) + f=m.floors(p,r,s,t) + self.assertGreater(f['gap'],9*h**4*p*r) + self.assertGreater(f['delta'],36*h**8*p*r/m2) + self.assertLessEqual(f['delta'],m6-m4*m4/m2) + + def test_directional_endpoint_floors(self): + m=self.module() + for p,r,s,t,law in m.laws(): + m2,m4,m6=m.moments(law) + for u2,u4 in ((m2,m4),(2*m2,2*m4)): + f=m.directional(p,r,s,t,u2,u4) + for q in (F(0),F(1,64),F(1,8),F(1,4)): + d,schur,tau=m.direct(m2,m4,m6,q) + self.assertLessEqual(f['det'],d) + self.assertLessEqual(f['schur'],schur) + self.assertLessEqual(f['tau'],tau) + + def test_no_probability_normalization_for_general_measure(self): + m=self.module(); a2,a4,_=m.moments([(F(1),F(2))]) + residual=2*(1-a2)**2 + self.assertNotEqual(residual,a4-a2*a2) + self.assertEqual(residual,a4-2*a2*a2+2*a2*a2) + + def test_homogeneous_scaling(self): + m=self.module(); p,r,s,t=F(1,5),F(1,3),F(1),F(4) + f=m.floors(p,r,s,t) + for scale in (F(1,9),F(4),F(16)): + g=m.floors(p,r,scale*s,scale*t) + for key,power in (('m2',1),('gap',2),('delta',3)): + self.assertEqual(g[key],f[key]*scale**power) + + def test_cli_baseline_and_each_exact_mutant(self): + m=self.module() + def run(*args): + flags=['-B','-S'] if not sys.flags.optimize else ['-B','-O','-S'] + return subprocess.run([sys.executable,*flags,str(SIDE/'two_mass.py'),*args],capture_output=True,text=True,timeout=15) + good=run(); self.assertEqual(good.returncode,0,good.stderr); self.assertEqual(good.stderr,'') + j=json.loads(good.stdout);self.assertTrue(j['ok']);self.assertEqual(j['scientific_effect'],'NONE') + for label,reason in m.MUTANTS.items(): + bad=run('--mutant',label) + self.assertEqual(bad.returncode,1,(label,bad.stdout,bad.stderr));self.assertEqual(bad.stderr,'') + self.assertEqual(json.loads(bad.stdout)['failed'],[reason]) + bad=run('--mutant','M9');self.assertEqual((bad.returncode,bad.stdout,bad.stderr),(2,'unknown mutant\n','')) + +if __name__=='__main__': unittest.main(verbosity=2) diff --git a/reviews/d2_two_mass_floors_20261006/two_mass.py b/reviews/d2_two_mass_floors_20261006/two_mass.py new file mode 100644 index 000000000..c56170026 --- /dev/null +++ b/reviews/d2_two_mass_floors_20261006/two_mass.py @@ -0,0 +1,123 @@ +#!/usr/bin/env python3 +"""Exact-rational diagnostics for NOTE.md; no statistical or Lean certificate. + +Radii s,t below are SQUARED radii. Masses aggregate either sign. The measure +argument in the note is not replaced by this finite enumeration. +""" +import argparse +from fractions import Fraction as F +import json + +MUTANTS = {'M1':'square_completion','M2':'fourth_floor','M3':'delta_floor', + 'M4':'tau_endpoint','M5':'probability_boundary','M6':'schur_endpoint', + 'M7':'zero_atom_boundary'} + +def require(ok, message): + if not ok: + raise ValueError(message) + +def rational(*values): + if any(type(x) is not F for x in values): + raise TypeError('exact Fraction inputs required') + +def harmonic(u, v): + rational(u, v) + require(u >= 0 and v >= 0 and u + v > 0, 'nonnegative weights, positive sum required') + return u*v/(u+v) + +def floors(p, r, s, t): + """Probability-law floors from lower masses at distinct squared radii.""" + rational(p, r, s, t) + require(p > 0 and r > 0 and p+r <= 1, 'positive probability masses required') + require(s >= 0 and t >= 0 and s != t, 'distinct nonnegative squared radii required') + return {'m2':p*s+r*t, 'gap':harmonic(p,r)*(s-t)**2, + 'delta':harmonic(p*s,r*t)*(s-t)**2} + +def moments(law): + """Raw even moments of a finite NONNEGATIVE measure, not necessarily mass1.""" + for squared_radius, mass in law: + rational(squared_radius, mass) + require(squared_radius >= 0 and mass >= 0, 'nonnegative measure required') + return tuple(sum((mass*squared_radius**n for squared_radius,mass in law),F(0)) + for n in (1,2,3)) + +def direct(m2, m4, m6, q): + """Subtractive Schur/cumulant expressions, independent of floor formulas.""" + rational(m2,m4,m6,q) + require(m2 > 0 and F(0) <= q <= F(1,4), 'positive second moment and physical q required') + k4=m4-3*m2*m2; k6=m6-15*m4*m2+30*m2**3 + alpha=m4-2*k4*q; gamma=m2*m2+2*k4*q + det=alpha*gamma-k4*k4*q*(1-4*q) + require(det > 0, 'positive pin determinant required') + schur=alpha-(gamma**3+(2*gamma+alpha)*k4*k4*q*(1-4*q))/det + tau=6*m2**3+9*m2*k4*(1-2*q)+(k6-k4*k4/m2)*(1-3*q) + return det,schur,tau + +def directional(p,r,s,t,m2_upper,m4_upper): + """Requires ACTUAL moment upper bounds; consistency checks do not certify them.""" + rational(m2_upper,m4_upper) + f=floors(p,r,s,t); ell,g,d=f['m2'],f['gap'],f['delta'] + require(s > 0 and t > 0, 'strict Delta requires two nonzero radii') + require(m2_upper >= ell and m4_upper >= ell*ell+g, 'inconsistent upper bounds') + dmin=min(ell*ell*(ell*ell+g),g*(4*ell*ell+g)/4) + dmax=max(m2_upper*m2_upper*m4_upper, + (m4_upper-ell*ell)*(m4_upper+3*m2_upper*m2_upper)/4) + return {'det':dmin,'schur':ell*ell*g*(2*ell*ell+g)/dmax, + 'tau':min(d,(d+9*ell*g)/4)} + +def laws(): + masses=((F(1,5),F(1,3)),(F(1,2),F(1,2)),(F(1,9),F(2,9)),(F(1,8),F(3,4))) + radii=((F(1,9),F(4,9)),(F(1),F(4)),(F(1),F(9)),(F(4),F(25)),(F(1,4),F(25,4))) + for p,r in masses: + for s,t in radii: + for other in (F(0),(s+t)/2,2*t): + yield p,r,s,t,[(s,p),(t,r),(other,1-p-r)] + +def check(mutant=None): + checks={name:True for name in MUTANTS.values()} + count={'completion':0,'finite_laws':0,'directional_cases':0,'boundary_cases':2} + for u in (F(1,7),F(1),F(4)): + for v in (F(1,9),F(2),F(7)): + for a,b,c in ((F(-3),F(2),F(1)),(F(1),F(4),F(0)),(F(1),F(4),(u+4*v)/(u+v))): + lower=harmonic(u,v)*(a-b)**2*(2 if mutant=='M1' else 1) + rhs=lower+(u+v)*(c-(u*a+v*b)/(u+v))**2 + checks['square_completion'] &= u*(a-c)**2+v*(b-c)**2==rhs + count['completion']+=1 + for p,r,s,t,law in laws(): + m2,m4,m6=moments(law); f=floors(p,r,s,t) + gap=f['gap']*(2 if mutant=='M2' else 1) + delta=f['delta']/(s*t) if mutant=='M3' else f['delta'] + checks['fourth_floor'] &= gap <= m4-m2*m2 + checks['delta_floor'] &= delta <= m6-m4*m4/m2 + count['finite_laws']+=1 + for u2,u4 in ((m2,m4),(2*m2,2*m4)): + df=directional(p,r,s,t,u2,u4) + if mutant=='M4': df['tau']=max(f['delta'],(f['delta']+9*f['m2']*f['gap'])/4) + if mutant=='M6': + ell,g=f['m2'],f['gap'] + wrong=min(u2*u2*u4,(u4-ell*ell)*(u4+3*u2*u2)/4) + df['schur']=ell*ell*g*(2*ell*ell+g)/wrong + for q in (F(0),F(1,64),F(1,8),F(1,4)): + det,schur,tau=direct(m2,m4,m6,q) + checks['tau_endpoint'] &= df['tau']<=tau + checks['schur_endpoint'] &= df['schur']<=schur and df['det']<=det + count['directional_cases']+=1 + m2,m4,_=moments([(F(1),F(2))]); residual=2*(1-m2)**2 + checks['probability_boundary']=(residual==m4-m2*m2) if mutant=='M5' else (residual!=m4-m2*m2) + m2,m4,m6=moments([(F(0),F(1,2)),(F(1),F(1,2))]) + checks['zero_atom_boundary']=(m4>m2*m2 and ((m6-m4*m4/m2>0) if mutant=='M7' else (m6-m4*m4/m2==0))) + failed=[name for name,ok in checks.items() if not ok] + return {'ok':not failed,'checks':checks,'failed':failed,'controls':count, + 'method':'exact finite diagnostics; not continuum or Lean proof','scientific_effect':'NONE'} + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--mutant') + args=parser.parse_args() + if args.mutant is not None and args.mutant not in MUTANTS: + print('unknown mutant');return 2 + result=check(args.mutant) + print(json.dumps(result,sort_keys=True,separators=(',',':'))) + return 0 if result['ok'] else 1 + +if __name__=='__main__':raise SystemExit(main())