From 31f7a6b5a36045be7795a6461da067a8ada96343 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 20:04:41 -0700 Subject: [PATCH] D2: quantitative two-atom moment and all-direction scalar floors 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; pickup main#229/6008048138. Six additive files only: a self-contained weighted-square derivation, exact-rational helpers and twelve finite-model tests, a six-method source/mutation wrapper and a read-only evidence workflow. Normal and optimized local suites pass; all four named wrong-formula mutations are rejected. Existing D2Schur blob and all formal/gate/companion sources unchanged. Ordinary author-side mathematics, not Lean verification, concrete periodic-law certification, independent review or scientific acceptance. Scientific effect NONE. --- .github/workflows/d2-two-atom-floors.yml | 72 ++++++ reviews/d2_two_atom_floors_20261006/NOTE.md | 216 ++++++++++++++++++ .../SOURCE_FILES.json | 52 +++++ .../test_two_atom_bounds.py | 190 +++++++++++++++ .../two_atom_bounds.py | 70 ++++++ tests/test_d2_two_atom_floors.py | 124 ++++++++++ 6 files changed, 724 insertions(+) create mode 100644 .github/workflows/d2-two-atom-floors.yml create mode 100644 reviews/d2_two_atom_floors_20261006/NOTE.md create mode 100644 reviews/d2_two_atom_floors_20261006/SOURCE_FILES.json create mode 100644 reviews/d2_two_atom_floors_20261006/test_two_atom_bounds.py create mode 100644 reviews/d2_two_atom_floors_20261006/two_atom_bounds.py create mode 100644 tests/test_d2_two_atom_floors.py diff --git a/.github/workflows/d2-two-atom-floors.yml b/.github/workflows/d2-two-atom-floors.yml new file mode 100644 index 00000000..25b0844e --- /dev/null +++ b/.github/workflows/d2-two-atom-floors.yml @@ -0,0 +1,72 @@ +name: D2 two-atom quantitative floors +'on': + pull_request: + paths: + - 'reviews/d2_two_atom_floors_20261006/**' + - 'tests/test_d2_two_atom_floors.py' + - 'formal/ResearchFormalCoreR1/D2Schur.lean' + - '.github/workflows/d2-two-atom-floors.yml' + push: + branches: [main] + paths: + - 'reviews/d2_two_atom_floors_20261006/**' + - 'tests/test_d2_two_atom_floors.py' + - 'formal/ResearchFormalCoreR1/D2Schur.lean' + - '.github/workflows/d2-two-atom-floors.yml' +permissions: + contents: read +defaults: + run: + shell: bash +jobs: + quantitative: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.11' + - name: Execute exact rational baseline and named mutations + run: | + set -euo pipefail + OUT="$RUNNER_TEMP/d2-atom-evidence" + test ! -e "$OUT" + mkdir -p "$OUT" + export OUT + python -B -S - <<'PY' + import hashlib,json,os,pathlib,subprocess,sys + out=pathlib.Path(os.environ['OUT']) + head=subprocess.check_output(['git','rev-parse','HEAD'],text=True).strip() + if head!=os.environ['GITHUB_SHA']: + raise RuntimeError('checked source mismatch') + results=[] + for mode,flags in [('normal',[]),('optimized',['-O'])]: + cmd=[sys.executable,'-B','-S',*flags,'tests/test_d2_two_atom_floors.py'] + r=subprocess.run(cmd,capture_output=True,timeout=180) + (out/(mode+'.stdout')).write_bytes(r.stdout) + (out/(mode+'.stderr')).write_bytes(r.stderr) + record={'mode':mode,'command':cmd,'returncode':r.returncode, + 'stdout_sha256':hashlib.sha256(r.stdout).hexdigest(), + 'stderr_sha256':hashlib.sha256(r.stderr).hexdigest()} + results.append(record) + (out/'context.json').write_text(json.dumps({ + 'checked_commit':head,'repository':os.environ['GITHUB_REPOSITORY'], + 'run_id':os.environ['GITHUB_RUN_ID'],'attempt':os.environ['GITHUB_RUN_ATTEMPT'], + 'python':sys.version,'results':results,'scientific_effect':'NONE', + 'meaning':'finite rational/source controls; not Lean or scientific acceptance' + },indent=2)+'\n') + print(r.stderr.decode(),end='') + if r.returncode or b'Ran 6 tests' not in r.stderr or not r.stderr.rstrip().endswith(b'OK'): + raise RuntimeError('quantitative suite did not pass: '+mode) + PY + - name: Retain available original evidence + if: always() + uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a + with: + name: d2-atom-${{ github.run_id }}-${{ github.run_attempt }} + path: ${{ runner.temp }}/d2-atom-evidence + if-no-files-found: error + retention-days: 30 diff --git a/reviews/d2_two_atom_floors_20261006/NOTE.md b/reviews/d2_two_atom_floors_20261006/NOTE.md new file mode 100644 index 00000000..cedbb44a --- /dev/null +++ b/reviews/d2_two_atom_floors_20261006/NOTE.md @@ -0,0 +1,216 @@ +# Quantitative two-atom floors for the scalar D2 expressions + +Dylan Roy — delegated AI work. Actual author: OpenAI / GPT-6 Astra Pro, +`continuation-d2-proof-execution-audit-20261006`; main#229 pickup6008048138. +Scientific effect NONE; author-exposed; organizational-independence credit0. +This is an ordinary mathematical derivation with finite rational controls, +NOT a Lean proof or a new numerical certificate for a periodic field. + +## 1. Scope and exact interfaces + +The consumed algebra is `formal/ResearchFormalCoreR1/D2Schur.lean`, +at Math- commit2f8b6f372be383d752e9dd30d38234faa977243c, Git blob +b95460c0d263a32ea274b347079cca6aaab3d2e9. In particular the ratio, determinant +interpolation, and tau endpoint identities are the existing scalar interfaces. +The current publication base preserves that blob. No primary formal source, +manifest, gate, dependency, workflow or scientific register is modified. + +The actual-integral identities also appear in the separately reviewed companion +`companions/d2_moment_bridge_20261006/D2MomentBridge.lean`, +commitb122462634460a8bb9e88406072cb7a356957407, blob +b3184107e290189b91e3e18fd2aa1cb631bb9bde. Its source-and-execution review is +5422935330, with hosted readback6007916533. That review does NOT cover this note. +The short integral arguments below are supplied explicitly rather than treating +a pending integration, historical receipt, or a digest as a new proof premise. + +Weighted square completion is elementary algebra, not a claim of discovering +a new general inequality. The useful consequence here is a transparent +atom-mass-to-scalar-floor interface. It does not identify these scalar +expressions with any actual Gaussian/Palm conditional covariance. + +## 2. Hypotheses and quantities + +Let mu be a probability measure, X a measurable real random variable, and +assume X^2, X^4 and X^6 are integrable. Write + + s = E[X^2], m4 = E[X^4], m6 = E[X^6], + g = m4 - s^2, Delta = m6 - m4^2/s. + +Choose a,b != 0 with a^2 != b^2, and p,q>0 such that + + mu{X=a} >= p, mu{X=b} >= q, p+q <= 1. + +These are lower bounds on actual atom masses; equality is not required. +The atom events are disjoint and measurable. Symmetry, independence and +Gaussianity are not assumed. Define + + u=a^2, v=b^2, A=p*u, B=q*v, + s0=A+B, + g0=p*q*(u-v)^2/(p+q), + delta0=A*B*(u-v)^2/(A+B). + +All three floors are strictly positive under the stated assumptions. + +## 3. Two-square completion and moment floors + +For A,B>0 and real u,v,c, direct expansion gives + + A*(u-c)^2 + B*(v-c)^2 + = A*B*(u-v)^2/(A+B) + + (A+B)*(c-(A*u+B*v)/(A+B))^2. (3.1) + +First, retaining the two atom contributions to the nonnegative X^2 integral +gives s>=s0>0. Thus all divisions below are legitimate. + +Put c=m4/s. Expanding the square and using the stated integrability yields + + E[(X^3-c*X)^2] = m6 - 2*c*m4 + c^2*s = Delta. (3.2) + +Keeping the disjoint atom contributions in this nonnegative integral gives + + Delta >= p*a^2*(a^2-c)^2 + q*b^2*(b^2-c)^2 + >= delta0, (3.3) + +where the second inequality is (3.1) with weights A,B. Replacing actual +atom masses by the lower bounds p,q is legitimate before completion because +each squared summand is nonnegative. No independence or cancellation of +uncontrolled terms is used. + +Probability normalization separately gives + + E[(X^2-s)^2] = m4 - 2*s*E[X^2] + s^2 = g. + +Keeping its two atom contributions and using (3.1) with weights p,q and +center c=s gives g>=g0. Consequently + + s >= s0 > 0, g >= g0 > 0, Delta >= delta0 > 0. (3.4) + +For an arbitrary finite measure of mass M, the centered identity instead +uses center E[X^2]/M and gap E[X^4]-E[X^2]^2/M. +The unnormalized gap m4-s^2 is NOT generally nonnegative. The residual +identity (3.2) does not require total mass one, but the combined result here +does: do not export the probability-only gap to an arbitrary measure. + +## 4. Sharpness and excluded boundary cases + +For fixed admissible p,q,a,b, the law + + p*delta_a + q*delta_b + (1-p-q)*delta_0 + +attains s=s0 and Delta=delta0: its residual vanishes at zero and its center +is (A*u+B*v)/(A+B). Thus the Delta floor cannot be increased using only +these four inputs over this class of probability laws. + +The gap floor is separately attained by putting the remaining mass at any +real point z with + + z^2=(p*u+q*v)/(p+q). + +Then s=z^2, the residual gap square vanishes on the added point, and (3.1) +attains equality. Such a z exists since u,v>0. These are separate sharpness +claims, not a claim that both floors are simultaneously sharp for one law. + +A zero atom together with one nonzero absolute radius is not a strict-Delta +case: P(0)=1/2, P(1)=P(-1)=1/4 gives g=1/4 but Delta=0. +Atoms a and -a have the same squared radius and also need not give strictness. +These are the distinctions recorded by AUD-309-REVIEW-STRICTNESS-01. +The floors can vanish in a varying family as an atom mass tends to zero or +the squared radii coalesce. No family-uniform floor follows without a uniform +positive bound on the displayed expressions. Two atoms are sufficient, +not necessary; continuous laws may have strictly positive gaps. + +## 5. All-direction scalar floors without moment upper bounds + +Let t be any real number in [0,1/4], including both endpoints. Put x=s^2. +The exact source formulas, expressed in s,g,Delta, are + + D0=x*(g+x), D1=g*(g+4*x)/4, + D(t)=(1-4*t)*D0+4*t*D1, + N=x*g*(g+2*x), S(t)=N/D(t), + T(t)=(1-4*t)*Delta+4*t*(Delta+9*s*g)/4. (5.1) + +D is the scalar pin determinant, S is the scalar Schur expression, and T +is the source's `d2Tau` variance expression, NOT its square root. +Their probabilistic identification remains outside this note. + +Both determinant endpoints are positive. Monotonicity of their positive +polynomials in s and g, followed by convex interpolation, gives + + D(t) >= D_floor + := min(s0^2*(g0+s0^2), g0*(g0+4*s0^2)/4) > 0. (5.2) + +For the Schur expression, it would be wrong to put lower bounds separately +into an uncontrolled quotient denominator. Instead use N>0 and the affine +D to obtain S(t)>=min(N/D0,N/D1). Direct simplification gives + + N/D0 = g*(g+2*x)/(g+x) >= g, + N/D1 = 4*x*(g+2*x)/(g+4*x) >= 2*x. + +The inequalities follow, respectively, from gx/(g+x)>=0 and +2*x*g/(g+4*x)>=0. Hence + + S(t) >= S_floor := min(g0,2*s0^2) > 0. (5.3) + +Finally both tau endpoints are monotone in the positive inputs, so + + T(t) >= T_floor + := min(delta0,(delta0+9*s0*g0)/4) > 0. (5.4) + +These are convenient lower bounds, not optimal determinant/Schur/tau +constants. They require no upper bound on the remaining moments. Their +homogeneous degrees under X -> cX are 8,4,6 respectively; the moment +floors have degrees 2,4,6. Negative c is allowed with c!=0. + +## 6. Exact example + +For p=q=1/4,a=1,b=2 and remaining mass1/2 at zero, + + s=5/4, m4=17/4, m6=65/4, g=43/16, Delta=9/5, + s0=5/4, g0=9/8, delta0=9/5. + +Equations (5.2)-(5.4) give, for every t in [0,1/4], + + D(t) >= 531/256, S(t) >= 9/8, T(t) >= 9/5. + +This is an illustrative discrete probability law, not the periodic spectral +law and not a substitute for one. + +## 7. Reproduction and interpretation + +Run the twelve finite-model methods directly: + + python -B -S reviews/d2_two_atom_floors_20261006/test_two_atom_bounds.py + python -B -O -S reviews/d2_two_atom_floors_20261006/test_two_atom_bounds.py + +Run the source-bound wrapper with the four actual code mutations: + + python -B -S tests/test_d2_two_atom_floors.py + python -B -O -S tests/test_d2_two_atom_floors.py + +The wrapper authenticates five payload files and the consumed D2Schur blob, +executes the twelve methods, checks fixed finite-case counts, and injects +four mutations in isolated temporary directories. Each must exit1 with its +specified failed test names, twelve collected methods and zero harness errors. +Missing code, crashes, timeouts and generic nonzero exit codes do not count as +successful mathematical controls. The manifest is an identity inventory, not +an independent authenticity root or a proof verdict. + +The original twelve-method test was run before its helper existed and failed; +the wrapper was similarly observed failing before the packet manifest existed. +Finite coverage includes216 square-completion cases,64 probability laws, +384 directional evaluations,16 Delta and3 gap attainment cases,2 mass-bound +cases,18 scaling checks and explicit countermodels. These counts overlap +and must not be summed into a count of independent theorems. + +The dedicated read-only workflow executes the wrapper in normal/optimized +Python, retains original output plus tested commit/run/attempt identity, and +does not modify existing required checks. Configured CI is not a passed run; +actual run identities and conclusions belong in the PR discussion. + +A future formalization should first prove (3.1) and the atom-integral lower +bound with explicit measurable disjoint events, then derive (3.3)-(5.4). +No new Lean targets, kernel receipt, actual periodic-law construction, +summability theorem, Gaussian/Palm identification, interval-quadrature result, +parent lifetime theorem, independent alignment or scientific acceptance is +asserted by this packet. Existing mathematical and execution failures remain +historical evidence and are not overwritten by these additive files. diff --git a/reviews/d2_two_atom_floors_20261006/SOURCE_FILES.json b/reviews/d2_two_atom_floors_20261006/SOURCE_FILES.json new file mode 100644 index 00000000..1c627ddf --- /dev/null +++ b/reviews/d2_two_atom_floors_20261006/SOURCE_FILES.json @@ -0,0 +1,52 @@ +{ + "author": "OpenAI / GPT-6 Astra Pro; continuation-d2-proof-execution-audit-20261006", + "consumed_sources": [ + { + "bytes": 6694, + "commit": "2f8b6f372be383d752e9dd30d38234faa977243c", + "git_blob": "b95460c0d263a32ea274b347079cca6aaab3d2e9", + "path": "formal/ResearchFormalCoreR1/D2Schur.lean", + "repository": "d6g8k5htny-coder/Math-", + "scope": "scalar definitions, Schur ratio and determinant/tau endpoint identities", + "sha256": "d3fb3ed7b4043227f1d5a06e208de9d94eb413c067e9d0f8802388407c9e15b9" + }, + { + "bytes": 10696, + "commit": "b122462634460a8bb9e88406072cb7a356957407", + "git_blob": "b3184107e290189b91e3e18fd2aa1cb631bb9bde", + "path": "companions/d2_moment_bridge_20261006/D2MomentBridge.lean", + "repository": "d6g8k5htny-coder/Math-", + "scope": "residual-square and probability gap identities; rederived in note", + "sha256": "cde3bbd96eb29eb9ab7ff1448ffab1f794fb2b80355ac618800155eea6ccc42f" + } + ], + "files": { + ".github/workflows/d2-two-atom-floors.yml": { + "bytes": 3121, + "git_blob": "25b0844e95e3573bc846280b0e2fb71fb1a1d43e", + "sha256": "57ae4bf015f9925355d7c7128b85d38fcc1c945eb924e73e53345f4fd7864300" + }, + "reviews/d2_two_atom_floors_20261006/NOTE.md": { + "bytes": 9327, + "git_blob": "cedbb44a237d1a158111dca81c30983f7efd37f1", + "sha256": "dd2c823327b1d93438a29bd14b15c804ba361723c682a41e1ff4a5ba92482661" + }, + "reviews/d2_two_atom_floors_20261006/test_two_atom_bounds.py": { + "bytes": 8916, + "git_blob": "cf4d3d6c7cfc8e6df5af381d00535f0ba30587ac", + "sha256": "82395069fcd456a6b7f651e4cab11602722720de3febe3ce2569f408a0440476" + }, + "reviews/d2_two_atom_floors_20261006/two_atom_bounds.py": { + "bytes": 2975, + "git_blob": "ae1bfe55e6bc067a219faaa75e46fc3ddb2c5fa3", + "sha256": "1b4de15f0c94cce8521de0996b27acbed42d219fb14d7e6452a2f3c62b7c6e33" + }, + "tests/test_d2_two_atom_floors.py": { + "bytes": 5785, + "git_blob": "55ee6dd86cab5617c0625aab539e5e53b23510cb", + "sha256": "4ae94381a8a1b5cba182d53e0b96c48bf213cd05e791c954a0b4cacb8502c7f7" + } + }, + "schema": 1, + "scientific_effect": "NONE" +} diff --git a/reviews/d2_two_atom_floors_20261006/test_two_atom_bounds.py b/reviews/d2_two_atom_floors_20261006/test_two_atom_bounds.py new file mode 100644 index 00000000..cf4d3d6c --- /dev/null +++ b/reviews/d2_two_atom_floors_20261006/test_two_atom_bounds.py @@ -0,0 +1,190 @@ +#!/usr/bin/env python3 +"""Exact rational tests for the separately proposed two-atom D2 floors.""" +from fractions import Fraction as F +import importlib.util +import itertools +import json +from pathlib import Path +import sys +import unittest + +SOURCE = Path(__file__).with_name("two_atom_bounds.py") +COUNTS = {} + +def counted(label, n=1): + COUNTS[label] = COUNTS.get(label, 0) + n + +class TwoAtomTests(unittest.TestCase): + def setUp(self): + self.assertTrue(SOURCE.is_file(), "quantitative implementation must exist") + if not hasattr(type(self), "m"): + spec = importlib.util.spec_from_file_location("two_atom_bounds", SOURCE) + module = importlib.util.module_from_spec(spec) + sys.modules[spec.name] = module + spec.loader.exec_module(module) + type(self).m = module + + def test_weighted_square_identity_and_optimum(self): + for A, B, u, v, c in itertools.product( + (F(1, 5), F(1), F(7, 3)), (F(1, 4), F(2)), + (F(-2), F(0), F(3)), (F(-1), F(1), F(5)), + (F(-3), F(0), F(2, 3), F(4))): + lhs = (A+B)*(A*(u-c)**2+B*(v-c)**2)-A*B*(u-v)**2 + rhs = (A*(u-c)+B*(v-c))**2 + self.assertEqual(lhs, rhs) + floor = self.m.two_square_floor(A, B, u, v) + self.assertGreaterEqual(A*(u-c)**2+B*(v-c)**2, floor) + mean = (A*u+B*v)/(A+B) + self.assertEqual(A*(u-mean)**2+B*(v-mean)**2, floor) + counted("two_square") + + def test_finite_probability_laws_and_all_d2_floors(self): + for a, b in ((F(1), F(2)), (F(-1), F(3)), + (F(1, 2), F(-3, 2)), (F(-2), F(-3))): + for p, q in ((F(1, 8), F(1, 4)), (F(1, 3), F(1, 3)), + (F(1, 5), F(4, 5)), (F(2, 5), F(1, 10))): + for extra in (F(0), F(-4), F(2, 3), F(5)): + law = [(a,p), (b,q), (extra,1-p-q)] + moments = self.m.even_moments(law) + m2, m4, m6 = moments + floors = self.m.atom_floors(p, q, a, b) + delta = m6-m4*m4/m2 + gap = m4-m2*m2 + self.assertGreaterEqual(m2, floors["m2"]) + self.assertGreaterEqual(gap, floors["gap"]) + self.assertGreaterEqual(delta, floors["delta"]) + c = m4/m2 + residual = sum(w*(x**3-c*x)**2 for x,w in law) + self.assertEqual(residual, delta) + for direction in (F(0), F(1,100), F(1,16), F(1,8), F(3,16), F(1,4)): + D,S,T = self.m.d2_values(m2,m4,m6,direction) + self.assertGreaterEqual(D, floors["det"]) + self.assertGreaterEqual(S, floors["schur"]) + self.assertGreaterEqual(T, floors["tau"]) + self.assertGreater(floors["det"],0) + self.assertGreater(floors["schur"],0) + self.assertGreater(floors["tau"],0) + counted("directional_floor") + counted("probability_law") + + def test_mass_lower_bounds_not_exact_masses(self): + for p, q, ap, aq in ((F(1,10),F(1,10),F(1,4),F(1,2)), + (F(1,6),F(1,5),F(1,3),F(1,3))): + lower = self.m.atom_floors(p,q,F(1),F(3)) + actual = self.m.atom_floors(ap,aq,F(1),F(3)) + m2,m4,m6 = self.m.even_moments([(F(1),ap),(F(3),aq),(F(0),1-ap-aq)]) + for label in lower: + self.assertLessEqual(lower[label], actual[label]) + self.assertLessEqual(lower["delta"], m6-m4*m4/m2) + counted("mass_lower_bound") + + def test_delta_floor_attains_with_zero_remainder(self): + for a,b,p,q in itertools.product( + (F(1),F(-1,2)), (F(2),F(-3)), + (F(1,10),F(1,3)), (F(1,4),F(1,2))): + m2,m4,m6 = self.m.even_moments([(a,p),(b,q),(F(0),1-p-q)]) + bounds = self.m.atom_floors(p,q,a,b) + self.assertEqual(m2,bounds["m2"]) + self.assertEqual(m6-m4*m4/m2,bounds["delta"]) + counted("delta_attainment") + + def test_gap_floor_attains_at_intermediate_squared_radius(self): + # u=1, v=9; weights in ratio 5:3 give intermediate squared radius 4. + for s in (F(1,4),F(1,2),F(1)): + p,q = s*F(5,8),s*F(3,8) + m2,m4,_ = self.m.even_moments([(F(1),p),(F(3),q),(F(2),1-s)]) + bounds = self.m.atom_floors(p,q,F(1),F(3)) + self.assertEqual(m2,F(4)) + self.assertEqual(m4-m2*m2,bounds["gap"]) + counted("gap_attainment") + + def test_scaling_has_correct_degrees(self): + base=self.m.atom_floors(F(1,5),F(1,3),F(1),F(-2)) + degrees={"m2":2,"gap":4,"delta":6,"det":8,"schur":4,"tau":6} + for c in (F(1,3),F(2),F(-3)): + scaled=self.m.atom_floors(F(1,5),F(1,3),c,-2*c) + for key,power in degrees.items(): + self.assertEqual(scaled[key],c**power*base[key]) + counted("scale_identity") + + def test_probability_normalization_is_essential(self): + law=[(F(1),F(1)),(F(2),F(1))] + m2,m4,m6=self.m.even_moments(law,probability=False) + total=F(2) + c=m2/total + centered=sum(w*(x*x-c)**2 for x,w in law) + self.assertEqual(centered,m4-m2*m2/total) + self.assertLess(m4-m2*m2,0) + self.assertGreater(centered,0) + self.assertEqual(m6-m4*m4/m2, + sum(w*(x**3-(m4/m2)*x)**2 for x,w in law)) + with self.assertRaisesRegex(ValueError,"probability mass"): + self.m.even_moments(law) + counted("nonunit_mass") + + def test_zero_and_same_radius_are_not_strict_cases(self): + m2,m4,m6=self.m.even_moments([(F(0),F(1,2)),(F(1),F(1,4)),(F(-1),F(1,4))]) + self.assertGreater(m4-m2*m2,0) + self.assertEqual(m6-m4*m4/m2,0) + for a,b in ((F(0),F(1)),(F(1),F(-1)),(F(2),F(2))): + with self.assertRaisesRegex(ValueError,"nonzero distinct squared"): + self.m.atom_floors(F(1,4),F(1,4),a,b) + counted("excluded_atom_case") + + def test_invalid_domains_and_float_inputs_refused(self): + for p,q in ((F(0),F(1,3)),(F(-1,3),F(1,3)),(F(1),F(1,2))): + with self.assertRaises(ValueError): + self.m.atom_floors(p,q,F(1),F(2)) + counted("invalid_domain") + with self.assertRaises(TypeError): + self.m.atom_floors(0.25,F(1,4),F(1),F(2)) + with self.assertRaises(ValueError): + self.m.d2_values(F(1),F(3),F(15),F(1,3)) + with self.assertRaises(ValueError): + self.m.d2_values(F(1),F(1),F(1),F(1,4)) + with self.assertRaises(ValueError): + self.m.even_moments([(F(1),F(-1))]) + counted("invalid_domain",4) + + def test_wrong_missing_factor_and_normalizer_fail_on_exact_witnesses(self): + p=q=F(1,4); a=F(1,10); b=F(1,5) + m2,m4,m6=self.m.even_moments([(a,p),(b,q),(F(0),1-p-q)]) + correct=self.m.atom_floors(p,q,a,b)["delta"] + actual=m6-m4*m4/m2 + wrong_missing_ab = p*q*(a*a-b*b)**2/(p*a*a+q*b*b) + wrong_missing_mass_denominator = correct/(p+q) + self.assertEqual(actual,correct) + self.assertGreater(wrong_missing_ab,actual) + self.assertGreater(wrong_missing_mass_denominator,actual) + counted("wrong_formula_witness",2) + + def test_endpoint_max_cannot_replace_lower_min(self): + p=q=F(1,4);a=F(1);b=F(2) + m2,m4,m6=self.m.even_moments([(a,p),(b,q),(F(0),F(1,2))]) + lower=self.m.atom_floors(p,q,a,b) + # Actual tau endpoints; using their maximum as an all-angle lower bound fails. + T0=self.m.d2_values(m2,m4,m6,F(0))[2] + T1=self.m.d2_values(m2,m4,m6,F(1,4))[2] + self.assertNotEqual(T0,T1) + self.assertGreater(max(T0,T1),min(T0,T1)) + self.assertLessEqual(lower["tau"],min(T0,T1)) + counted("wrong_extremum_witness") + + def test_scalar_formula_matches_source_subtractive_schur(self): + for a,b in ((F(1),F(2)),(F(-1,2),F(3,2))): + m2,m4,m6=self.m.even_moments([(a,F(1,4)),(b,F(1,3)),(F(0),F(5,12))]) + for t in (F(0),F(1,16),F(1,8),F(1,4)): + k4=m4-3*m2*m2 + alpha=m4-2*k4*t + gamma=m2*m2+2*k4*t + D=m2*m2*m4+k4*(m4+m2*m2)*t + subtractive=alpha-(gamma**3+(2*gamma+alpha)*k4*k4*t*(1-4*t))/D + self.assertEqual(self.m.d2_values(m2,m4,m6,t)[1],subtractive) + counted("subtractive_schur") + +if __name__=="__main__": + suite=unittest.defaultTestLoader.loadTestsFromTestCase(TwoAtomTests) + result=unittest.TextTestRunner(verbosity=2).run(suite) + print(json.dumps({"tests":result.testsRun,"failures":len(result.failures), + "errors":len(result.errors),"exact_cases":COUNTS},sort_keys=True)) + raise SystemExit(0 if result.wasSuccessful() else 1) diff --git a/reviews/d2_two_atom_floors_20261006/two_atom_bounds.py b/reviews/d2_two_atom_floors_20261006/two_atom_bounds.py new file mode 100644 index 00000000..ae1bfe55 --- /dev/null +++ b/reviews/d2_two_atom_floors_20261006/two_atom_bounds.py @@ -0,0 +1,70 @@ +#!/usr/bin/env python3 +"""Exact rational helpers for the proposed D2 two-atom floors. + +This is a finite-model checker, not interval arithmetic or a Lean proof. +All arithmetic accepts only Python int (not bool) or Fraction values. +""" +from fractions import Fraction +from typing import Iterable + +Rational = int | Fraction + +def rational(x: Rational) -> Fraction: + if isinstance(x, bool) or not isinstance(x, (int, Fraction)): + raise TypeError("exact integer or Fraction input required") + return Fraction(x) + +def two_square_floor(A: Rational, B: Rational, u: Rational, v: Rational) -> Fraction: + A, B, u, v = map(rational, (A, B, u, v)) + if A <= 0 or B <= 0: + raise ValueError("positive two-square weights required") + return A*B*(u-v)**2/(A+B) + +def even_moments(law: Iterable[tuple[Rational, Rational]], *, + probability: bool = True) -> tuple[Fraction, Fraction, Fraction]: + rows = [(rational(x), rational(w)) for x, w in law] + if not rows or any(w < 0 for _, w in rows): + raise ValueError("nonempty nonnegative finite measure required") + total = sum((w for _, w in rows), Fraction(0)) + if total <= 0: + raise ValueError("positive total mass required") + if probability and total != 1: + raise ValueError("probability mass must equal one") + return tuple(sum((w*x**j for x, w in rows), Fraction(0)) for j in (2, 4, 6)) + +def atom_floors(p: Rational, q: Rational, a: Rational, b: Rational + ) -> dict[str, Fraction]: + """Sufficient all-direction floors for a probability law with two atom masses. + + p,q are positive lower bounds for masses at a,b; a,b are nonzero and + have distinct squared radii. No actual-law realization is constructed. + """ + p, q, a, b = map(rational, (p, q, a, b)) + if p <= 0 or q <= 0 or p+q > 1: + raise ValueError("positive atom mass bounds with p+q<=1 required") + if a == 0 or b == 0 or a*a == b*b: + raise ValueError("nonzero distinct squared atom radii required") + u, v = a*a, b*b + m = p*u + q*v + gap = two_square_floor(p, q, u, v) + delta = two_square_floor(p*u, q*v, u, v) + determinant = min(m*m*(gap+m*m), gap*(gap+4*m*m)/4) + schur = min(gap, 2*m*m) + tau = min(delta, (delta+9*m*gap)/4) + return {"m2":m, "gap":gap, "delta":delta, + "det":determinant, "schur":schur, "tau":tau} + +def d2_values(m2: Rational, m4: Rational, m6: Rational, direction: Rational + ) -> tuple[Fraction, Fraction, Fraction]: + """Evaluate the source's scalar D,S,T formulas with a nonzero D guard.""" + s, m4, m6, t = map(rational, (m2, m4, m6, direction)) + if s <= 0 or not 0 <= t <= Fraction(1, 4): + raise ValueError("positive m2 and direction in [0,1/4] required") + g = m4-s*s + D = s*s*m4+(m4-3*s*s)*(m4+s*s)*t + if D <= 0: + raise ValueError("positive determinant required") + delta = m6-m4*m4/s + S = s*s*g*(g+2*s*s)/D + T = delta*(1-3*t)+9*t*s*g + return D, S, T diff --git a/tests/test_d2_two_atom_floors.py b/tests/test_d2_two_atom_floors.py new file mode 100644 index 00000000..55ee6dd8 --- /dev/null +++ b/tests/test_d2_two_atom_floors.py @@ -0,0 +1,124 @@ +#!/usr/bin/env python3 +"""Discoverable source-bound checks for the quantitative D2 note, not Lean verification.""" +import hashlib +import json +from pathlib import Path +import re +import shutil +import subprocess +import sys +import tempfile +import unittest + +ROOT = Path(__file__).resolve().parents[1] +PACKET = "reviews/d2_two_atom_floors_20261006" +WORKFLOW = ".github/workflows/d2-two-atom-floors.yml" +FILES = { + PACKET + "/NOTE.md", PACKET + "/two_atom_bounds.py", + PACKET + "/test_two_atom_bounds.py", "tests/test_d2_two_atom_floors.py", WORKFLOW, +} +CORE = "formal/ResearchFormalCoreR1/D2Schur.lean" +CORE_BLOB = "b95460c0d263a32ea274b347079cca6aaab3d2e9" +EXPECTED_CASES = { + "delta_attainment": 16, "directional_floor": 384, "excluded_atom_case": 3, + "gap_attainment": 3, "invalid_domain": 7, "mass_lower_bound": 2, + "nonunit_mass": 1, "probability_law": 64, "scale_identity": 18, + "subtractive_schur": 8, "two_square": 216, + "wrong_extremum_witness": 1, "wrong_formula_witness": 2, +} +MUTANTS = { + "M1": ("delta = two_square_floor(p*u, q*v, u, v)", + "delta = two_square_floor(p, q, u, v)", + {"test_delta_floor_attains_with_zero_remainder", + "test_finite_probability_laws_and_all_d2_floors", + "test_scaling_has_correct_degrees", + "test_wrong_missing_factor_and_normalizer_fail_on_exact_witnesses"}), + "M2": ("determinant = min(m*m*(gap+m*m), gap*(gap+4*m*m)/4)", + "determinant = max(m*m*(gap+m*m), gap*(gap+4*m*m)/4)", + {"test_finite_probability_laws_and_all_d2_floors"}), + "M3": ("schur = min(gap, 2*m*m)", "schur = max(gap, 2*m*m)", + {"test_finite_probability_laws_and_all_d2_floors"}), + "M4": ("tau = min(delta, (delta+9*m*gap)/4)", + "tau = max(delta, (delta+9*m*gap)/4)", + {"test_endpoint_max_cannot_replace_lower_min", + "test_finite_probability_laws_and_all_d2_floors"}), +} + +def identity(raw): + return {"bytes": len(raw), "sha256": hashlib.sha256(raw).hexdigest(), + "git_blob": hashlib.sha1(b"blob %d\0" % len(raw) + raw).hexdigest()} + +def unique(pairs): + result = {} + for key, value in pairs: + if key in result: + raise ValueError("duplicate JSON key") + result[key] = value + return result + +class D2TwoAtomPacketTests(unittest.TestCase): + def setUp(self): + self.side = ROOT / PACKET + manifest = self.side / "SOURCE_FILES.json" + self.assertTrue(manifest.is_file(), "quantitative packet manifest absent") + self.meta = json.loads(manifest.read_text(), object_pairs_hook=unique) + self.assertEqual(set(self.meta["files"]), FILES) + self.assertEqual(self.meta["scientific_effect"], "NONE") + self.assertEqual({x.name for x in self.side.iterdir()}, + {"NOTE.md", "two_atom_bounds.py", "test_two_atom_bounds.py", + "SOURCE_FILES.json"}) + for name in sorted(FILES): + path = ROOT / name + self.assertFalse(any((ROOT / Path(*Path(name).parts[:i])).is_symlink() + for i in range(1, len(Path(name).parts)+1))) + self.assertTrue(path.is_file(), "missing source: " + name) + self.assertEqual(identity(path.read_bytes()), self.meta["files"][name], name) + self.assertEqual(identity((ROOT/CORE).read_bytes())["git_blob"], CORE_BLOB) + + def run_suite(self, directory): + flags = ["-B", "-S"] + (["-O"] if sys.flags.optimize else []) + run = subprocess.run([sys.executable, *flags, str(directory/"test_two_atom_bounds.py")], + capture_output=True, text=True, timeout=60) + payload = json.loads(run.stdout, object_pairs_hook=unique) + self.assertEqual(set(payload), {"tests", "errors", "failures", "exact_cases"}) + self.assertEqual(payload["tests"], 12) + self.assertEqual(payload["errors"], 0) + self.assertIn("Ran 12 tests", run.stderr) + self.assertNotIn("skipped", run.stderr.lower()) + self.assertNotIn("ERROR:", run.stderr) + return run, payload + + def test_source_scope(self): + self.assertIn("NOT a Lean proof", (self.side/"NOTE.md").read_text()) + self.assertEqual(self.meta["schema"], 1) + self.assertEqual(self.meta["consumed_sources"][0]["git_blob"], CORE_BLOB) + + def test_baseline_exact_cases(self): + run, payload = self.run_suite(self.side) + self.assertEqual(run.returncode, 0, run.stderr) + self.assertEqual(payload["failures"], 0) + self.assertEqual(payload["exact_cases"], EXPECTED_CASES) + self.assertRegex(run.stderr, r"\nOK\s*$") + + def mutation(self, label): + old, new, names = MUTANTS[label] + with tempfile.TemporaryDirectory(prefix="d2-atom-mutant-") as temp: + dest = Path(temp) + raw = (self.side/"two_atom_bounds.py").read_text() + self.assertEqual(raw.count(old), 1) + (dest/"two_atom_bounds.py").write_text(raw.replace(old, new)) + shutil.copyfile(self.side/"test_two_atom_bounds.py", dest/"test_two_atom_bounds.py") + run, payload = self.run_suite(dest) + self.assertEqual(run.returncode, 1, run.stderr) + found = re.findall(r"^FAIL: ([A-Za-z0-9_]+) \(", run.stderr, re.M) + self.assertEqual(set(found), names) + self.assertEqual(len(found), len(names)) + self.assertEqual(payload["failures"], len(names)) + + def test_M1_atom_square_weights_required(self): self.mutation("M1") + def test_M2_determinant_min_required(self): self.mutation("M2") + def test_M3_schur_min_required(self): self.mutation("M3") + def test_M4_tau_min_required(self): self.mutation("M4") + +if __name__ == "__main__": + unittest.main(verbosity=2)