From 496bc31a689d84a0b5f209fe26f9390924b087ba Mon Sep 17 00:00:00 2001
From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com>
Date: Tue, 6 Oct 2026 06:05:29 -0700
Subject: [PATCH 1/2] Specify actual squared-radius integral floor contracts
 before implementation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Dylan Roy — delegated AI work. OpenAI / GPT-6 Astra Pro, d2-atom-integral-r12-20261006-1255, main229 pickup6016691076. Separate six-target actual-integral companion consuming unchanged landed D2MomentBridge and D2SquareSchur; eight new files only, scientific effect NONE. This initial imported stub defines no targets: exact Contract must actually fail before proof bodies are supplied. Eight Python methods first failed missing-helper assertions and now pass in both modes; not local Lean execution. Preserve all old proof/core/gate/dependency/receipt bytes and full-history/full-suite/warnings-as-errors policies. No source verdict or merge readiness claimed.
---
 .github/workflows/d2-atom-integral.yml        |  55 +++++++
 .../d2_atom_integral_20261006/Contract.lean   |  64 ++++++++
 .../D2AtomIntegral.lean                       |   6 +
 companions/d2_atom_integral_20261006/SCOPE.md | 101 +++++++++++++
 .../SOURCE_FILES.json                         |  50 ++++++
 companions/d2_atom_integral_20261006/check.py | 142 ++++++++++++++++++
 .../d2_atom_integral_20261006/replay.sh       |  52 +++++++
 .../d2_atom_integral_20261006/test_check.py   | 101 +++++++++++++
 8 files changed, 571 insertions(+)
 create mode 100644 .github/workflows/d2-atom-integral.yml
 create mode 100644 companions/d2_atom_integral_20261006/Contract.lean
 create mode 100644 companions/d2_atom_integral_20261006/D2AtomIntegral.lean
 create mode 100644 companions/d2_atom_integral_20261006/SCOPE.md
 create mode 100644 companions/d2_atom_integral_20261006/SOURCE_FILES.json
 create mode 100644 companions/d2_atom_integral_20261006/check.py
 create mode 100644 companions/d2_atom_integral_20261006/replay.sh
 create mode 100644 companions/d2_atom_integral_20261006/test_check.py

diff --git a/.github/workflows/d2-atom-integral.yml b/.github/workflows/d2-atom-integral.yml
new file mode 100644
index 000000000..e656ee5df
--- /dev/null
+++ b/.github/workflows/d2-atom-integral.yml
@@ -0,0 +1,55 @@
+name: D2 quantitative radius-mass integral companion
+'on':
+  pull_request:
+    paths:
+      - 'companions/d2_atom_integral_20261006/**'
+      - '.github/workflows/d2-atom-integral.yml'
+      - 'companions/d2_moment_bridge_20261006/D2MomentBridge.lean'
+      - 'companions/d2_square_schur_20261006/D2SquareSchur.lean'
+      - 'formal/**'
+  push:
+    branches: [main]
+    paths:
+      - 'companions/d2_atom_integral_20261006/**'
+      - '.github/workflows/d2-atom-integral.yml'
+      - 'companions/d2_moment_bridge_20261006/D2MomentBridge.lean'
+      - 'companions/d2_square_schur_20261006/D2SquareSchur.lean'
+      - 'formal/**'
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  d2-atom-integral:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    env:
+      LEAN_NUM_THREADS: 2
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+          fetch-depth: 0
+      - name: Install pinned Lean and retrieve dependency cache
+        uses: leanprover/lean-action@f061402b660e0c34644504b324e830f2991d4865
+        with:
+          lake-package-directory: formal
+          auto-config: 'false'
+          build: 'false'
+          test: 'false'
+          lint: 'false'
+          use-mathlib-cache: 'true'
+          use-github-cache: 'false'
+      - name: Replay suites, exact integral contracts and kernel controls
+        shell: bash
+        run: bash companions/d2_atom_integral_20261006/replay.sh
+      - name: Preserve original success or failure evidence
+        if: always()
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a
+        with:
+          name: d2-atom-integral-${{ github.run_id }}-${{ github.run_attempt }}
+          path: |
+            .lake/d2-atom-integral-evidence/
+            formal/.lake/formal-evidence/
+          include-hidden-files: true
+          if-no-files-found: error
+          retention-days: 30
diff --git a/companions/d2_atom_integral_20261006/Contract.lean b/companions/d2_atom_integral_20261006/Contract.lean
new file mode 100644
index 000000000..06b8329fb
--- /dev/null
+++ b/companions/d2_atom_integral_20261006/Contract.lean
@@ -0,0 +1,64 @@
+import D2AtomIntegral
+
+open MeasureTheory D2MomentBridge ResearchFormalCoreR1
+
+variable {Ω : Type*} [MeasurableSpace Ω]
+
+example (μ : Measure Ω) [IsProbabilityMeasure μ] (f : Ω → ℝ)
+    (S T : Set Ω) (hS : MeasurableSet S) (hT : MeasurableSet T)
+    (hST : Disjoint S T) (hf : Integrable f μ) (hf0 : ∀ w, 0 ≤ f w)
+    (a b : ℝ) (ha : ∀ w ∈ S, a ≤ f w) (hb : ∀ w ∈ T, b ≤ f w) :
+    μ.real S * a + μ.real T * b ≤ ∫ w, f w ∂μ :=
+  D2AtomIntegral.two_event_integral_lower μ f S T hS hT hST hf hf0 a b ha hb
+
+example (μ : Measure Ω) [IsProbabilityMeasure μ] (X f : Ω → ℝ)
+    (s t p q a b : ℝ)
+    (hS : MeasurableSet {w | X w ^ 2 = s})
+    (hT : MeasurableSet {w | X w ^ 2 = t}) (hst : s ≠ t)
+    (hp : p ≤ μ.real {w | X w ^ 2 = s}) (hq : q ≤ μ.real {w | X w ^ 2 = t})
+    (ha0 : 0 ≤ a) (hb0 : 0 ≤ b) (hf : Integrable f μ) (hf0 : ∀ w, 0 ≤ f w)
+    (ha : ∀ w, X w ^ 2 = s → f w = a) (hb : ∀ w, X w ^ 2 = t → f w = b) :
+    p * a + q * b ≤ ∫ w, f w ∂μ :=
+  D2AtomIntegral.two_radius_integral_lower μ X f s t p q a b hS hT hst hp hq ha0 hb0 hf hf0 ha hb
+
+example (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ)
+    (s t p q : ℝ) (hs : 0 < s) (ht : 0 < t) (hst : s ≠ t)
+    (hS : MeasurableSet {w | X w ^ 2 = s})
+    (hT : MeasurableSet {w | X w ^ 2 = t})
+    (hp : p ≤ μ.real {w | X w ^ 2 = s}) (hq : q ≤ μ.real {w | X w ^ 2 = t})
+    (h2 : Integrable (fun w => X w ^ 2) μ) :
+    p*s + q*t ≤ moment μ X 2 :=
+  D2AtomIntegral.second_moment_floor μ X s t p q hs ht hst hS hT hp hq h2
+
+example (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ)
+    (s t p q : ℝ) (hp0 : 0 < p) (hq0 : 0 < q) (hst : s ≠ t)
+    (hS : MeasurableSet {w | X w ^ 2 = s})
+    (hT : MeasurableSet {w | X w ^ 2 = t})
+    (hp : p ≤ μ.real {w | X w ^ 2 = s}) (hq : q ≤ μ.real {w | X w ^ 2 = t})
+    (h2 : Integrable (fun w => X w ^ 2) μ)
+    (h4 : Integrable (fun w => X w ^ 4) μ) :
+    p*q/(p+q)*(s-t)^2 ≤ moment μ X 4 - (moment μ X 2)^2 :=
+  D2AtomIntegral.fourth_gap_floor μ X s t p q hp0 hq0 hst hS hT hp hq h2 h4
+
+example (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ)
+    (s t p q : ℝ) (hs : 0 < s) (ht : 0 < t) (hp0 : 0 < p) (hq0 : 0 < q)
+    (hst : s ≠ t) (hS : MeasurableSet {w | X w ^ 2 = s})
+    (hT : MeasurableSet {w | X w ^ 2 = t})
+    (hp : p ≤ μ.real {w | X w ^ 2 = s}) (hq : q ≤ μ.real {w | X w ^ 2 = t})
+    (h2 : Integrable (fun w => X w ^ 2) μ)
+    (h4 : Integrable (fun w => X w ^ 4) μ)
+    (h6 : Integrable (fun w => X w ^ 6) μ) :
+    (p*s)*(q*t)/(p*s+q*t)*(s-t)^2 ≤
+      d2Delta (moment μ X 2) (moment μ X 4) (moment μ X 6) :=
+  D2AtomIntegral.residual_moment_floor μ X s t p q hs ht hp0 hq0 hst hS hT hp hq h2 h4 h6
+
+example (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ)
+    (s t p q u : ℝ) (hs : 0 < s) (ht : 0 < t) (hp0 : 0 < p) (hq0 : 0 < q)
+    (hst : s ≠ t) (hS : MeasurableSet {w | X w ^ 2 = s})
+    (hT : MeasurableSet {w | X w ^ 2 = t})
+    (hp : p ≤ μ.real {w | X w ^ 2 = s}) (hq : q ≤ μ.real {w | X w ^ 2 = t})
+    (h2 : Integrable (fun w => X w ^ 2) μ)
+    (h4 : Integrable (fun w => X w ^ 4) μ) (hu0 : 0 ≤ u) (hu1 : u ≤ 1/4) :
+    min (p*q/(p+q)*(s-t)^2) (2*(p*s+q*t)^2) ≤
+      d2Schur (moment μ X 2) (moment μ X 4) u :=
+  D2AtomIntegral.schur_floor_of_radius_masses μ X s t p q u hs ht hp0 hq0 hst hS hT hp hq h2 h4 hu0 hu1
diff --git a/companions/d2_atom_integral_20261006/D2AtomIntegral.lean b/companions/d2_atom_integral_20261006/D2AtomIntegral.lean
new file mode 100644
index 000000000..840d32724
--- /dev/null
+++ b/companions/d2_atom_integral_20261006/D2AtomIntegral.lean
@@ -0,0 +1,6 @@
+import D2MomentBridge
+import D2SquareSchur
+import Mathlib.MeasureTheory.Integral.Bochner.Set
+
+/- Test-first stage: Contract.lean must fail on the six missing theorem names.
+No theorem placeholder or custom axiom is supplied by this empty module. -/
diff --git a/companions/d2_atom_integral_20261006/SCOPE.md b/companions/d2_atom_integral_20261006/SCOPE.md
new file mode 100644
index 000000000..4b1f89740
--- /dev/null
+++ b/companions/d2_atom_integral_20261006/SCOPE.md
@@ -0,0 +1,101 @@
+# Quantitative squared-radius masses to actual D2 moment floors
+
+Dylan Roy — delegated AI work. Actual author OpenAI / GPT-6 Astra Pro,
+`d2-atom-integral-r12-20261006-1255`, pickup main#229/6016691076.
+Scientific effect NONE. Author-exposed D2 lineage; organizational independence0.
+
+This is a separate six-target Lean companion. Initial publication contains an
+empty imported module so the unchanged exact-type Contract can genuinely fail
+before any proof body is supplied. Configuration or old-core success is not
+proof of these new targets; actual runs and amendments are recorded on the PR.
+
+## Source correspondence and preserved sources
+
+The quantitative inequalities are the existing #326 two-squared-radius result,
+not a new moment discovery. #328's individual signed atoms are a sufficient
+specialization, not the premise silently used here. #343 supplies the conservative
+upper-moment-free Schur inequality. #371's sharper optional Part B is not included.
+
+This companion consumes `D2MomentBridge.lean`, blob
+b3184107e290189b91e3e18fd2aa1cb631bb9bde (landed #317), and
+`D2SquareSchur.lean`, blob4855c92d55254969e1de7f8cf8dec2bdc027cf69
+(landed #343, merge11f9127f00ce922e5d39b0da42af76134eb78a21).
+The exact primary formal tree d7422c6b1acbf3e20c75a1ed7fc13fc30125ec14,
+its63-target manifest, gate and all old proof bytes are unchanged. The driver
+checks both additional consumed module blobs against Git HEAD and working bytes,
+compiles them under the pinned toolchain and audits transitive axioms of every
+new target. It does not reuse an upstream receipt as new execution.
+
+## Six exact targets
+
+1. `two_event_integral_lower`: for disjoint measurable events S,T in a probability
+   space, integrable nonnegative f, and constants a,b bounding f below on their
+   respective events, `mu.real S*a + mu.real T*b <= integral f`. The constants
+   need not be positive; disjointness and nonnegativity outside the union suffice.
+2. `two_radius_integral_lower`: specialize to S={X^2=s}, T={X^2=t}, with s!=t,
+   supplied real event-mass lower bounds p,q and nonnegative constant values a,b
+   of f on those events. Its result is p*a+q*b<=integral f.
+3. `second_moment_floor`: m2>=p*s+q*t, requiring integrable X^2 and positive s,t.
+4. `fourth_gap_floor`: m4-m2^2>=p*q/(p+q)*(s-t)^2 for p,q>0, distinct s,t and
+   integrable powers2/4. This statement need not require positive s,t separately.
+5. `residual_moment_floor`: Delta>=((p*s)*(q*t)/(p*s+q*t))*(s-t)^2, with
+   positive s,t,p,q, distinct radii, and integrable powers2/4/6. Delta is the
+   original d2Delta at actual moments. Positivity of m2 follows from target3;
+   no division-by-zero convention is used to manufacture the inequality.
+6. `schur_floor_of_radius_masses`: under the same positive radius/mass premises
+   and powers2/4, for every u in closed[0,1/4], the original d2Schur is at least
+   `min(p*q/(p+q)*(s-t)^2, 2*(p*s+q*t)^2)`.
+
+All six use an actual Measure and Bochner integrals through the inherited
+`moment` definition. Event measurability is an explicit hypothesis; no global
+measurability of X, independence, symmetry, Gaussianity or signed-atom premise
+is silently inserted. Probability normalization stays explicit. No upper
+moment input is needed for the Schur conclusion. Supplied positive masses imply
+their compatibility with probability; p+q<=1 need not be an extra premise.
+
+## Proof route and boundary cases
+
+Integrate the sum of two constant indicators. Each is integrable because the
+measure is finite; disjointness makes the sum pointwise <=f. Integral monotonicity
+and the constant-indicator formula give target1. Target2 multiplies actual
+mass bounds by nonnegative event values. Target3 uses f=X^2. Target4 uses
+f=(X^2-m2)^2 and the already-proved probability gap identity, followed by #343's
+weighted-square inequality at weights p,q. Target5 uses the already-proved
+residual-square identity and weights p*s,q*t. Target6 supplies the two positive
+floors to #343's lower-input theorem, retaining its denominator and closed-angle
+hypotheses. This is the quantitative integral edge absent from the earlier
+qualitative strictness companion.
+
+Overlapping identical events cannot be added twice. The finite measure
+delta_1+delta_2 has m4-m2^2=-8, so normalization cannot be removed. Mass at zero
+and one nonzero radius can have positive fourth gap but Delta=0. Mass at both
+signs of a radius counts together; neither sign alone need carry p. The finite
+Python models and exact Lean false-proposition controls retain these distinctions.
+The controls are explicit scalar consequences of the described finite laws,
+not another general measure construction or a test of every possible omitted
+hypothesis. The unchanged Contract fixes the actual theorem types.
+
+## Reproduction and assurance
+
+From repository root after the existing pinned Lean setup:
+`bash companions/d2_atom_integral_20261006/replay.sh`.
+Python-only controls: `python -B -S companions/d2_atom_integral_20261006/test_check.py`
+and the same with -O. The eight-method helper suite first failed eight explicit
+missing-helper assertions before implementation. Finite tests supplement the
+proofs; they do not prove the arbitrary-measure statements.
+
+The adapted #343 workflow retains full-history checkout, complete root/formal
+Python suites in both modes, unchanged63-target core kernel replay, new source
+build and exact Contract with warnings-as-errors, six ordered axiom/type reports,
+fresh leanchecker and three precise False-goal failures. Original logs/statuses
+and source/run/attempt bindings are preserved even on failure. The manifest is
+an identity inventory, not an external trust root. The fixed inventory/type-name
+parser is not a general Lean syntax or definitional-equality verifier; compiled
+Contract and scoped source review provide different assurance.
+
+Six new theorems, zero new definitions; no primary manifest expansion. Formal
+sharpness, an actual periodic spectral measure and its summability, numerical
+values/radii, uniform-L/family floors, Gaussian/Palm conditioning, the coefficient
+integral, persistence matching and scientific acceptance are not supplied.
+All older results/reviews retain their scopes. This author's proof and replay
+need an actual separate nonauthor read before eligible integration; no self-merge.
diff --git a/companions/d2_atom_integral_20261006/SOURCE_FILES.json b/companions/d2_atom_integral_20261006/SOURCE_FILES.json
new file mode 100644
index 000000000..57e6a594e
--- /dev/null
+++ b/companions/d2_atom_integral_20261006/SOURCE_FILES.json
@@ -0,0 +1,50 @@
+{
+  "core_tree": "d7422c6b1acbf3e20c75a1ed7fc13fc30125ec14",
+  "files": {
+    ".github/workflows/d2-atom-integral.yml": {
+      "bytes": 1942,
+      "git_blob": "e656ee5df02cffa29947342a8e2f172f950a2401",
+      "sha256": "27a5d61d97ad5e502111a8a7815fe2474cd9dde3cd37ce8b0aa3bfdb6a8dd69b"
+    },
+    "companions/d2_atom_integral_20261006/Contract.lean": {
+      "bytes": 3433,
+      "git_blob": "06b8329fb2d7229e84fff7c5e65203086cb24b41",
+      "sha256": "746523ec422f3325029bb476f254b8d584692534f9cde00d95901209e6d81ccb"
+    },
+    "companions/d2_atom_integral_20261006/D2AtomIntegral.lean": {
+      "bytes": 249,
+      "git_blob": "840d32724f01a720f173c52bfa78167efa5fbab7",
+      "sha256": "c1a5d57231c8e421b2b819a3472487c22fc17cce1dfa515045cbe2ac1e5f55a1"
+    },
+    "companions/d2_atom_integral_20261006/SCOPE.md": {
+      "bytes": 6299,
+      "git_blob": "4b1f897400f0c0eb11f33abf3fde588036ec40c6",
+      "sha256": "d9b69c99bf6dc4c486b6677875dcfe6ae065b39398217699bdb8bd2707293c4d"
+    },
+    "companions/d2_atom_integral_20261006/check.py": {
+      "bytes": 7852,
+      "git_blob": "ab02ee91b989f2f2357cc94932ea4c9cec870825",
+      "sha256": "6c5f5abced836580c5a1d25b9f1d282fcfbe7b4319383eca2a668f319edf0ffe"
+    },
+    "companions/d2_atom_integral_20261006/replay.sh": {
+      "bytes": 2879,
+      "git_blob": "a4247be9ff3eff0229fef62c9b4a6b792159a6c7",
+      "sha256": "66387fcea3e2795fbe69856b0b0c37013f3b0540c2fe2e11dc2a97b373285bcf"
+    },
+    "companions/d2_atom_integral_20261006/test_check.py": {
+      "bytes": 5418,
+      "git_blob": "cd9a642876878d1f18b494f5bee2cf30a6da3f83",
+      "sha256": "b6448618b35e44a2181a12703a7ec464409a1b35ea641b95c690a60c6184247d"
+    }
+  },
+  "scientific_effect": "NONE",
+  "targets": [
+    "D2AtomIntegral.two_event_integral_lower",
+    "D2AtomIntegral.two_radius_integral_lower",
+    "D2AtomIntegral.second_moment_floor",
+    "D2AtomIntegral.fourth_gap_floor",
+    "D2AtomIntegral.residual_moment_floor",
+    "D2AtomIntegral.schur_floor_of_radius_masses"
+  ],
+  "version": 1
+}
diff --git a/companions/d2_atom_integral_20261006/check.py b/companions/d2_atom_integral_20261006/check.py
new file mode 100644
index 000000000..ab02ee91b
--- /dev/null
+++ b/companions/d2_atom_integral_20261006/check.py
@@ -0,0 +1,142 @@
+#!/usr/bin/env python3
+"""Fixed six-target companion driver, adapted from #343 check.py bdeba903.
+
+Exact source/run custody plus the unchanged core axiom parser. This explicit
+small-module inventory is not the separate general Lean declaration scanner.
+"""
+import argparse
+import hashlib
+import importlib.util
+import json
+import os
+from pathlib import Path
+import re
+import subprocess
+
+SIDE=Path(__file__).resolve().parent
+ROOT=SIDE.parents[1]
+PACKAGE='companions/d2_atom_integral_20261006'
+WORKFLOW='.github/workflows/d2-atom-integral.yml'
+REPO='d6g8k5htny-coder/Math-'
+CORE_TREE='d7422c6b1acbf3e20c75a1ed7fc13fc30125ec14'
+CORE_MANIFEST='5d7ccdb0885af7bf4a2aa6ec4dce5f5c41435bb10a0a7a426a8af286d4f035e4'
+CORE_GATE='958b149ea3a4ce735644a2079f817b5deddf5dc0d5ca347904ad09db6ad47d68'
+CONSUMED={
+ 'companions/d2_moment_bridge_20261006/D2MomentBridge.lean':'b3184107e290189b91e3e18fd2aa1cb631bb9bde',
+ 'companions/d2_square_schur_20261006/D2SquareSchur.lean':'4855c92d55254969e1de7f8cf8dec2bdc027cf69'}
+TARGETS=tuple('D2AtomIntegral.'+n for n in ('two_event_integral_lower','two_radius_integral_lower',
+    'second_moment_floor','fourth_gap_floor','residual_moment_floor','schur_floor_of_radius_masses'))
+FALSE_STATEMENTS={
+ 'RejectOverlappingEvents':'(1 : ℝ) * 1 + 1 * 1 ≤ 1',
+ 'RejectNonProbabilityGap':'(1 : ℝ) * 1 / (1+1) * (1-4)^2 ≤ 17-5^2',
+ 'RejectZeroRadiusStrictness':'(0 : ℝ) < 1/2-(1/2)^2/(1/2)'}
+CONTROLS=tuple(FALSE_STATEMENTS)
+PAYLOADS={PACKAGE+'/'+n for n in ('D2AtomIntegral.lean','Contract.lean','SCOPE.md','check.py','test_check.py','replay.sh')}|{WORKFLOW}
+
+def require(ok,message):
+    if not ok:raise ValueError(message)
+
+def sha(raw):return hashlib.sha256(raw).hexdigest()
+
+def identity(raw):
+    return {'bytes':len(raw),'sha256':sha(raw),
+            'git_blob':hashlib.sha1(b'blob %d\0'%len(raw)+raw).hexdigest()}
+
+def strict(raw):
+    def pairs(items):
+        out={}
+        for k,v in items:
+            require(k not in out,'duplicate JSON key');out[k]=v
+        return out
+    def reject(_):raise ValueError('noninteger JSON number')
+    return json.loads(raw,object_pairs_hook=pairs,parse_constant=reject,parse_float=reject)
+
+def git(*args):
+    return subprocess.run(['git',*args],cwd=ROOT,check=True,capture_output=True,text=True,timeout=30).stdout.strip()
+
+def source():
+    meta=strict((SIDE/'SOURCE_FILES.json').read_bytes());head=git('rev-parse','HEAD')
+    require(set(meta)=={'version','scientific_effect','core_tree','targets','files'},'manifest schema')
+    require(type(meta['version']) is int and meta['version']==1,'manifest version')
+    require(meta['scientific_effect']=='NONE' and meta['core_tree']==CORE_TREE,'scope')
+    require(meta['targets']==list(TARGETS) and set(meta['files'])==PAYLOADS,'fixed inventory')
+    require(re.fullmatch('[0-9a-f]{40}',head) is not None,'invalid HEAD')
+    require(git('rev-parse',head+':formal')==CORE_TREE,'core tree changed')
+    require(sha((ROOT/'formal/manifest.json').read_bytes())==CORE_MANIFEST,'core manifest changed')
+    require(sha((ROOT/'formal/gate.py').read_bytes())==CORE_GATE,'core verifier changed')
+    if os.environ.get('GITHUB_ACTIONS')=='true':
+        require(os.environ.get('GITHUB_SHA')==head and os.environ.get('GITHUB_REPOSITORY')==REPO,'host/source mismatch')
+        require(os.environ.get('GITHUB_RUN_ID') and os.environ.get('GITHUB_RUN_ATTEMPT'),'missing run identity')
+    expected=PAYLOADS|{PACKAGE+'/SOURCE_FILES.json'}
+    actual=set(git('ls-tree','-r','--name-only',head,'--',PACKAGE).splitlines())|{WORKFLOW}
+    require(actual==expected,'tracked membership')
+    ids={}
+    for name in sorted(expected|set(CONSUMED)):
+        path=ROOT/name
+        require(not any(p.is_symlink() for p in (path,*path.parents)),'symlink source')
+        ids[name]=identity(path.read_bytes())
+        require(git('rev-parse',head+':'+name)==ids[name]['git_blob'],'dirty source: '+name)
+        if name in PAYLOADS:require(meta['files'][name]==ids[name],'source identity: '+name)
+        if name in CONSUMED:require(CONSUMED[name]==ids[name]['git_blob'],'consumed source changed: '+name)
+    git('diff','--exit-code','HEAD','--','formal',PACKAGE,WORKFLOW,*CONSUMED)
+    return {'checked_commit':head,'repository':REPO,'run_id':os.environ.get('GITHUB_RUN_ID','local'),
+       'run_attempt':os.environ.get('GITHUB_RUN_ATTEMPT','local'),'core_tree':CORE_TREE,
+       'sources':ids,'declarations':list(TARGETS),'scientific_effect':'NONE'}
+
+def types(text):
+    require('error:' not in text and 'warning:' not in text,'type diagnostic')
+    matches=list(re.finditer(r'^D2AtomIntegral\.[A-Za-z][A-Za-z0-9_]*',text,re.M))
+    require([m.group() for m in matches]==list(TARGETS),'type inventory')
+    require(not text[:matches[0].start()].strip(),'type preamble')
+    return list(TARGETS)
+
+def negative(text,control,status):
+    require(control in CONTROLS,'unknown control')
+    require(type(status) is int and status==1,'negative exit must be exactly one')
+    pattern=r'(?:[^\r\n]*[/\\])?'+control+r'\.lean:[0-9]+:[0-9]+: error: unsolved goals\s*\n⊢ False\s*'
+    require(re.fullmatch(pattern,text) is not None,'not the intended False-goal diagnostic')
+    return control
+
+def core_gate():
+    path=ROOT/'formal/gate.py'
+    require(sha(path.read_bytes())==CORE_GATE,'core verifier changed')
+    spec=importlib.util.spec_from_file_location('bound_core_gate',path)
+    module=importlib.util.module_from_spec(spec);spec.loader.exec_module(module)
+    return module
+
+def emit(out):
+    (out/'Audit.lean').write_text('import D2AtomIntegral\n'+'\n'.join('#print axioms '+n for n in TARGETS)+'\n')
+    (out/'Types.lean').write_text('import D2AtomIntegral\nset_option pp.explicit true\n'+'\n'.join('#check '+n for n in TARGETS)+'\n')
+    for label,statement in FALSE_STATEMENTS.items():
+        (out/(label+'.lean')).write_text('import D2AtomIntegral\nexample : '+statement+' := by\n  norm_num\n')
+
+def finish(out):
+    current=source();require(strict((out/'source.json').read_bytes())==current,'source changed during execution')
+    ax=core_gate().audit_axioms((out/'axioms.log').read_text(),list(TARGETS))
+    types((out/'types.log').read_text())
+    for label in ('dependency-moment','dependency-square','build','contract','axioms','types','leanchecker'):
+        require((out/(label+'.status')).read_bytes()==b'0\n','unsuccessful process: '+label)
+    for label in CONTROLS:
+        require((out/(label+'.status')).read_bytes()==b'1\n','negative status: '+label)
+        negative((out/(label+'.log')).read_text(),label,1)
+    raw=(ROOT/'formal/.lake/formal-evidence/receipt.json').read_bytes();core=strict(raw)
+    require(core['checked_commit']==current['checked_commit'] and core['manifest_sha256']==CORE_MANIFEST,'core identity')
+    require(core['formalization_status']=='kernel-checked','no core kernel receipt')
+    result={**current,'axioms':ax,'theorem_count':6,'definition_count':0,'core_receipt_sha256':sha(raw),
+       'formalization_status':'kernel-checked','alignment_status':'PENDING_INDEPENDENT_REVIEW',
+       'scientific_acceptance':False,'log_sha256':{p.name:sha(p.read_bytes()) for p in sorted(out.iterdir()) if p.is_file()}}
+    (out/'receipt.json').write_text(json.dumps(result,sort_keys=True,indent=2)+'\n')
+    return result
+
+def main():
+    ap=argparse.ArgumentParser(description=__doc__)
+    ap.add_argument('command',choices=('source','emit','finish','negative'))
+    ap.add_argument('path',type=Path,nargs='?');ap.add_argument('--control',choices=CONTROLS);ap.add_argument('--status',type=int)
+    a=ap.parse_args()
+    if a.command=='source':out=source()
+    elif a.command=='emit':emit(a.path);out={'emitted':True}
+    elif a.command=='finish':out=finish(a.path)
+    else:out={'negative':negative(a.path.read_text(),a.control,a.status)}
+    print(json.dumps(out,sort_keys=True,indent=2))
+
+if __name__=='__main__':main()
diff --git a/companions/d2_atom_integral_20261006/replay.sh b/companions/d2_atom_integral_20261006/replay.sh
new file mode 100644
index 000000000..a4247be9f
--- /dev/null
+++ b/companions/d2_atom_integral_20261006/replay.sh
@@ -0,0 +1,52 @@
+#!/usr/bin/env bash
+# Adapted from the landed #343 replay.sh; no live tee/receipt hash race.
+set -euo pipefail
+ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
+SIDE="$ROOT/companions/d2_atom_integral_20261006"
+OUT="$ROOT/.lake/d2-atom-integral-evidence"
+cd "$ROOT"
+test ! -e "$OUT"
+mkdir -p "$OUT"
+python3 -B -S "$SIDE/check.py" source > "$OUT/source.json"
+python3 -B -S "$SIDE/test_check.py" 2>&1 | tee "$OUT/tests.log"
+python3 -B -O -S "$SIDE/test_check.py" 2>&1 | tee "$OUT/tests-optimized.log"
+python3 -B -S -m unittest discover -s tests -v 2>&1 | tee "$OUT/repository-tests.log"
+python3 -B -O -S -m unittest discover -s tests -v 2>&1 | tee "$OUT/repository-tests-optimized.log"
+python3 -B -S -m unittest discover -s formal/tests -v 2>&1 | tee "$OUT/core-tests.log"
+python3 -B -O -S -m unittest discover -s formal/tests -v 2>&1 | tee "$OUT/core-tests-optimized.log"
+python3 -B -S formal/gate.py --execute 2>&1 | tee "$OUT/core-execute.log"
+python3 -B -S "$SIDE/check.py" emit "$OUT"
+export ATOM_SIDE="$SIDE" ATOM_OUT="$OUT" ATOM_ROOT="$ROOT"
+cd "$ROOT/formal"
+lake env bash <<'INNER'
+set -euo pipefail
+MOMENT="$ATOM_ROOT/companions/d2_moment_bridge_20261006"
+SQUARE="$ATOM_ROOT/companions/d2_square_schur_20261006"
+export LEAN_PATH="$ATOM_SIDE:$MOMENT:$SQUARE:${LEAN_PATH:-}"
+export LEAN_SRC_PATH="$ATOM_SIDE:$MOMENT:$SQUARE:${LEAN_SRC_PATH:-}"
+lean --version | tee "$ATOM_OUT/toolchain.log"
+run_lean() {
+  local label="$1"; shift
+  local code=0
+  "$@" >"$ATOM_OUT/$label.log" 2>&1 || code=$?
+  printf '%s\n' "$code" >"$ATOM_OUT/$label.status"
+  cat "$ATOM_OUT/$label.log"
+  test "$code" -eq 0
+}
+run_lean dependency-moment lean -DwarningAsError=true --root="$MOMENT" -o "$MOMENT/D2MomentBridge.olean" "$MOMENT/D2MomentBridge.lean"
+run_lean dependency-square lean -DwarningAsError=true --root="$SQUARE" -o "$SQUARE/D2SquareSchur.olean" "$SQUARE/D2SquareSchur.lean"
+run_lean build lean -DwarningAsError=true --root="$ATOM_SIDE" -o "$ATOM_SIDE/D2AtomIntegral.olean" "$ATOM_SIDE/D2AtomIntegral.lean"
+run_lean contract lean -DwarningAsError=true --root="$ATOM_SIDE" "$ATOM_SIDE/Contract.lean"
+run_lean axioms lean -DwarningAsError=true --root="$ATOM_OUT" "$ATOM_OUT/Audit.lean"
+run_lean types lean -DwarningAsError=true --root="$ATOM_OUT" "$ATOM_OUT/Types.lean"
+run_lean leanchecker leanchecker --fresh D2AtomIntegral
+for control in RejectOverlappingEvents RejectNonProbabilityGap RejectZeroRadiusStrictness; do
+  code=0
+  lean -DwarningAsError=true --root="$ATOM_OUT" "$ATOM_OUT/$control.lean" >"$ATOM_OUT/$control.log" 2>&1 || code=$?
+  printf '%s\n' "$code" >"$ATOM_OUT/$control.status"
+  python3 -B -S "$ATOM_SIDE/check.py" negative "$ATOM_OUT/$control.log" --control "$control" --status "$code"
+done
+INNER
+cd "$ROOT"
+python3 -B -S "$SIDE/check.py" finish "$OUT"
+echo 'PASS: six actual-integral/scalar targets only; concrete field and independent alignment remain.'
diff --git a/companions/d2_atom_integral_20261006/test_check.py b/companions/d2_atom_integral_20261006/test_check.py
new file mode 100644
index 000000000..cd9a64287
--- /dev/null
+++ b/companions/d2_atom_integral_20261006/test_check.py
@@ -0,0 +1,101 @@
+#!/usr/bin/env python3
+"""Exact finite controls and evidence-driver tests; not Lean proof execution."""
+from fractions import Fraction as F
+import importlib.util
+import itertools
+from pathlib import Path
+import tempfile
+import unittest
+
+SIDE=Path(__file__).resolve().parent
+
+class AtomIntegralTests(unittest.TestCase):
+    def setUp(self):
+        self.assertTrue((SIDE/'check.py').is_file(), 'quantitative integral evidence helper absent')
+        spec=importlib.util.spec_from_file_location('atom_check',SIDE/'check.py')
+        self.c=importlib.util.module_from_spec(spec);spec.loader.exec_module(self.c)
+
+    def test_json_and_byte_identity(self):
+        self.assertEqual(self.c.strict('{"n":1}'), {'n':1})
+        for raw in ('{"x":1,"x":2}','{"x":NaN}','{"x":1.0}'):
+            with self.assertRaises(ValueError): self.c.strict(raw)
+        self.assertNotEqual(self.c.identity(b'x'),self.c.identity(b'x\n'))
+
+    def test_negative_reason_not_generic_failure(self):
+        for label in self.c.CONTROLS:
+            good=f'/tmp/{label}.lean:4:2: error: unsolved goals\n⊢ False\n'
+            self.assertEqual(self.c.negative(good,label,1),label)
+            for bad in (good.replace('False','True'),good.replace(label,'Wrong'),good+'extra\n',''):
+                with self.assertRaises(ValueError): self.c.negative(bad,label,1)
+            for code in (0,2,True):
+                with self.assertRaises(ValueError): self.c.negative(good,label,code)
+
+    def test_exact_inventory_and_emitted_commands(self):
+        self.assertEqual(len(self.c.TARGETS),6)
+        good='\n'.join(n+' : True' for n in self.c.TARGETS)+'\n'
+        self.assertEqual(self.c.types(good),list(self.c.TARGETS))
+        for bad in (good+good,'warning: bad\n'+good,good.replace(self.c.TARGETS[0],'Other.first')):
+            with self.assertRaises(ValueError):self.c.types(bad)
+        with tempfile.TemporaryDirectory() as td:
+            out=Path(td);self.c.emit(out)
+            self.assertEqual(set(p.name for p in out.iterdir()),
+                             {'Audit.lean','Types.lean'}|{n+'.lean' for n in self.c.CONTROLS})
+            self.assertEqual((out/'Audit.lean').read_text().count('#print axioms '),6)
+            for name,statement in self.c.FALSE_STATEMENTS.items():
+                self.assertIn('example : '+statement,(out/(name+'.lean')).read_text())
+
+    def test_disjoint_event_integral_lower(self):
+        weights=(F(1,6),F(1,3),F(1,2))
+        for f in itertools.product((F(0),F(1),F(3)),repeat=3):
+            for membership in itertools.product((0,1,2),repeat=3):
+                S=[i for i in range(3) if membership[i]==1]
+                T=[i for i in range(3) if membership[i]==2]
+                a=min((f[i] for i in S),default=F(7))
+                b=min((f[i] for i in T),default=F(9))
+                lhs=sum(weights[i] for i in S)*a+sum(weights[i] for i in T)*b
+                self.assertLessEqual(lhs,sum(weights[i]*f[i] for i in range(3)))
+
+    def test_squared_radius_floors_and_schur(self):
+        for a,b,p,q,extra in itertools.product((F(1),F(-1,2)),(F(2),F(-3)),
+                (F(1,10),F(1,4)),(F(1,5),F(1,3)),(F(0),F(1,7),F(-4))):
+            # Split every retained squared-radius mass equally over both signs.
+            law=[(a,p/2),(-a,p/2),(b,q/2),(-b,q/2),(extra,1-p-q)]
+            s,t=a*a,b*b
+            m2,m4,m6=[sum(w*x**n for x,w in law) for n in (2,4,6)]
+            s0=p*s+q*t;g0=p*q/(p+q)*(s-t)**2;d0=p*s*q*t/s0*(s-t)**2
+            g=m4-m2*m2;delta=m6-m4*m4/m2
+            self.assertGreaterEqual(m2,s0);self.assertGreaterEqual(g,g0);self.assertGreaterEqual(delta,d0)
+            for u in (F(0),F(1,16),F(1,4)):
+                x=m2*m2;D=(1-4*u)*x*m4+4*u*g*(m4+3*x)/4
+                self.assertLessEqual(min(g0,2*s0*s0),x*g*(g+2*x)/D)
+            if extra==0:self.assertEqual(delta,d0)
+
+    def test_magnitude_mass_is_not_one_signed_atom(self):
+        law=[(F(1),F(1,8)),(F(-1),F(1,8)),(F(2),F(1,8)),(F(-2),F(1,8)),(F(0),F(1,2))]
+        self.assertEqual(sum(w for x,w in law if x*x==1),F(1,4))
+        self.assertLess(sum(w for x,w in law if x==1),F(1,4))
+
+    def test_necessary_boundaries_have_countermodels(self):
+        # Coincident full events each mass1 cannot contribute twice to integral1.
+        self.assertGreater(F(1)+F(1),F(1))
+        # Non-probability measure delta_1+delta_2: unnormalised gap is negative.
+        self.assertEqual(F(17)-F(5)**2,F(-8))
+        # Half at0 and half on radius1: positive fourth gap, zero cubic residual.
+        self.assertGreater(F(1,2)-F(1,2)**2,0)
+        self.assertEqual(F(1,2)-F(1,2)**2/F(1,2),0)
+
+    def test_workflow_preserves_history_and_execution(self):
+        root=SIDE.parents[1]
+        workflow=(root/self.c.WORKFLOW).read_text()
+        self.assertIn('fetch-depth: 0',workflow)
+        self.assertIn('persist-credentials: false',workflow)
+        for path in self.c.CONSUMED:
+            self.assertIn(path,workflow)
+        shell=(SIDE/'replay.sh').read_text()
+        for required in ('formal/gate.py --execute','-DwarningAsError=true','leanchecker --fresh D2AtomIntegral',
+                         '-m unittest discover -s tests','-m unittest discover -s formal/tests','Contract.lean'):
+            self.assertIn(required,shell)
+        self.assertNotIn('continue-on-error',workflow)
+        self.assertNotIn('linter.unnecessarySeqFocus false',shell)
+
+if __name__=='__main__':unittest.main(verbosity=2)

From 90ea72462dc112542493b180a5911382177a11f2 Mon Sep 17 00:00:00 2001
From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com>
Date: Tue, 6 Oct 2026 06:26:01 -0700
Subject: [PATCH 2/2] Prove six actual integral contracts for D2 squared-radius
 moment floors
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Dylan Roy — delegated AI work. Actual OpenAI / GPT-6 Astra Pro, d2-atom-integral-r13-resume-20261006, continuation of main229/6016691076 and PR375/6017150557. Original dedicated37468233479 genuinely fails the fixed Contract at six missing names after full8/224/133 suites and dependency/core builds; original artifact11416640065 authenticated and retained. Supply the six proof bodies and module-only source identity. Preserve Contract06b8329f, source scope, driver/tests/workflow, both imported companions and primary formal tree. Integrate disjoint constant indicators, transfer squared-radius event-mass bounds, use actual residual/gap identities, then the existing scalar Schur lower-input theorem. This is an authored candidate pending actual new Lean execution and a separate scoped review, not local kernel success or scientific acceptance. Scientific effect NONE; no self-merge.
---
 .../D2AtomIntegral.lean                       | 147 +++++++++++++++++-
 .../SOURCE_FILES.json                         |   6 +-
 2 files changed, 148 insertions(+), 5 deletions(-)

diff --git a/companions/d2_atom_integral_20261006/D2AtomIntegral.lean b/companions/d2_atom_integral_20261006/D2AtomIntegral.lean
index 840d32724..adbbf5557 100644
--- a/companions/d2_atom_integral_20261006/D2AtomIntegral.lean
+++ b/companions/d2_atom_integral_20261006/D2AtomIntegral.lean
@@ -2,5 +2,148 @@ import D2MomentBridge
 import D2SquareSchur
 import Mathlib.MeasureTheory.Integral.Bochner.Set
 
-/- Test-first stage: Contract.lean must fail on the six missing theorem names.
-No theorem placeholder or custom axiom is supplied by this empty module. -/
+/-!
+Quantitative squared-radius event masses give actual Bochner-integral floors.
+This supplies the six previously published contracts; no finite-model surrogate
+or changed definition of moment, residual or Schur expression is introduced.
+-/
+noncomputable section
+namespace D2AtomIntegral
+
+open MeasureTheory D2MomentBridge ResearchFormalCoreR1
+set_option autoImplicit false
+
+variable {Ω : Type*} [MeasurableSpace Ω]
+
+theorem two_event_integral_lower (μ : Measure Ω) [IsProbabilityMeasure μ] (f : Ω → ℝ)
+    (S T : Set Ω) (hS : MeasurableSet S) (hT : MeasurableSet T)
+    (hST : Disjoint S T) (hf : Integrable f μ) (hf0 : ∀ w, 0 ≤ f w)
+    (a b : ℝ) (ha : ∀ w ∈ S, a ≤ f w) (hb : ∀ w ∈ T, b ≤ f w) :
+    μ.real S * a + μ.real T * b ≤ ∫ w, f w ∂μ := by
+  classical
+  have hsi : Integrable (S.indicator (fun _ : Ω => a)) μ :=
+    (integrable_const a).indicator hS
+  have hti : Integrable (T.indicator (fun _ : Ω => b)) μ :=
+    (integrable_const b).indicator hT
+  have hle : ∀ w, S.indicator (fun _ : Ω => a) w +
+      T.indicator (fun _ : Ω => b) w ≤ f w := by
+    intro w
+    by_cases hs : w ∈ S
+    · have ht : w ∉ T := fun ht => Set.disjoint_left.mp hST hs ht
+      simpa only [Set.indicator_of_mem hs, Set.indicator_of_notMem ht, add_zero]
+        using ha w hs
+    · by_cases ht : w ∈ T
+      · simpa only [Set.indicator_of_notMem hs, Set.indicator_of_mem ht, zero_add]
+          using hb w ht
+      · simpa only [Set.indicator_of_notMem hs, Set.indicator_of_notMem ht, zero_add]
+          using hf0 w
+  calc
+    μ.real S * a + μ.real T * b =
+        ∫ w, S.indicator (fun _ : Ω => a) w + T.indicator (fun _ : Ω => b) w ∂μ := by
+      rw [integral_add hsi hti, integral_indicator hS, integral_indicator hT]
+      simp [Measure.real, smul_eq_mul]
+    _ ≤ ∫ w, f w ∂μ := integral_mono (hsi.add hti) hf hle
+
+theorem two_radius_integral_lower (μ : Measure Ω) [IsProbabilityMeasure μ] (X f : Ω → ℝ)
+    (s t p q a b : ℝ)
+    (hS : MeasurableSet {w | X w ^ 2 = s})
+    (hT : MeasurableSet {w | X w ^ 2 = t}) (hst : s ≠ t)
+    (hp : p ≤ μ.real {w | X w ^ 2 = s}) (hq : q ≤ μ.real {w | X w ^ 2 = t})
+    (ha0 : 0 ≤ a) (hb0 : 0 ≤ b) (hf : Integrable f μ) (hf0 : ∀ w, 0 ≤ f w)
+    (ha : ∀ w, X w ^ 2 = s → f w = a) (hb : ∀ w, X w ^ 2 = t → f w = b) :
+    p * a + q * b ≤ ∫ w, f w ∂μ := by
+  have hd : Disjoint {w | X w ^ 2 = s} {w | X w ^ 2 = t} := by
+    apply Set.disjoint_left.mpr
+    intro w hwS hwT
+    exact hst (hwS.symm.trans hwT)
+  have hmass := add_le_add (mul_le_mul_of_nonneg_right hp ha0)
+    (mul_le_mul_of_nonneg_right hq hb0)
+  exact le_trans hmass (two_event_integral_lower μ f _ _ hS hT hd hf hf0 a b
+    (fun w hw => (ha w hw).symm.le) (fun w hw => (hb w hw).symm.le))
+
+theorem second_moment_floor (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ)
+    (s t p q : ℝ) (hs : 0 < s) (ht : 0 < t) (hst : s ≠ t)
+    (hS : MeasurableSet {w | X w ^ 2 = s})
+    (hT : MeasurableSet {w | X w ^ 2 = t})
+    (hp : p ≤ μ.real {w | X w ^ 2 = s}) (hq : q ≤ μ.real {w | X w ^ 2 = t})
+    (h2 : Integrable (fun w => X w ^ 2) μ) :
+    p*s + q*t ≤ moment μ X 2 := by
+  exact two_radius_integral_lower μ X (fun w => X w ^ 2) s t p q s t
+    hS hT hst hp hq hs.le ht.le h2 (fun w => sq_nonneg (X w))
+    (fun _ h => h) (fun _ h => h)
+
+theorem fourth_gap_floor (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ)
+    (s t p q : ℝ) (hp0 : 0 < p) (hq0 : 0 < q) (hst : s ≠ t)
+    (hS : MeasurableSet {w | X w ^ 2 = s})
+    (hT : MeasurableSet {w | X w ^ 2 = t})
+    (hp : p ≤ μ.real {w | X w ^ 2 = s}) (hq : q ≤ μ.real {w | X w ^ 2 = t})
+    (h2 : Integrable (fun w => X w ^ 2) μ)
+    (h4 : Integrable (fun w => X w ^ 4) μ) :
+    p*q/(p+q)*(s-t)^2 ≤ moment μ X 4 - (moment μ X 2)^2 := by
+  have h := two_radius_integral_lower μ X (fun w => (X w ^ 2 - moment μ X 2)^2)
+    s t p q ((s-moment μ X 2)^2) ((t-moment μ X 2)^2)
+    hS hT hst hp hq (sq_nonneg _) (sq_nonneg _)
+    (square_gap_integrable μ X h2 h4) (fun _ => sq_nonneg _)
+    (by intro w hw; rw [hw]) (by intro w hw; rw [hw])
+  rw [square_gap_integral μ X h2 h4] at h
+  exact le_trans (D2SquareSchur.weighted_square_lower p q s t (moment μ X 2) hp0 hq0) h
+
+theorem residual_moment_floor (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ)
+    (s t p q : ℝ) (hs : 0 < s) (ht : 0 < t) (hp0 : 0 < p) (hq0 : 0 < q)
+    (hst : s ≠ t) (hS : MeasurableSet {w | X w ^ 2 = s})
+    (hT : MeasurableSet {w | X w ^ 2 = t})
+    (hp : p ≤ μ.real {w | X w ^ 2 = s}) (hq : q ≤ μ.real {w | X w ^ 2 = t})
+    (h2 : Integrable (fun w => X w ^ 2) μ)
+    (h4 : Integrable (fun w => X w ^ 4) μ)
+    (h6 : Integrable (fun w => X w ^ 6) μ) :
+    (p*s)*(q*t)/(p*s+q*t)*(s-t)^2 ≤
+      d2Delta (moment μ X 2) (moment μ X 4) (moment μ X 6) := by
+  let c : ℝ := moment μ X 4 / moment μ X 2
+  have hsecond := second_moment_floor μ X s t p q hs ht hst hS hT hp hq h2
+  have hm2 : 0 < moment μ X 2 :=
+    lt_of_lt_of_le (add_pos (mul_pos hp0 hs) (mul_pos hq0 ht)) hsecond
+  have h := two_radius_integral_lower μ X (fun w => cubicResidual c (X w)^2)
+    s t p q (s*(s-c)^2) (t*(t-c)^2) hS hT hst hp hq
+    (mul_nonneg hs.le (sq_nonneg _)) (mul_nonneg ht.le (sq_nonneg _))
+    (residual_sq_integrable μ X c h2 h4 h6) (fun _ => sq_nonneg _)
+    (by
+      intro w hw
+      calc
+        cubicResidual c (X w)^2 = X w ^ 2 * (X w ^ 2-c)^2 := by
+          unfold cubicResidual
+          ring
+        _ = s*(s-c)^2 := by rw [hw])
+    (by
+      intro w hw
+      calc
+        cubicResidual c (X w)^2 = X w ^ 2 * (X w ^ 2-c)^2 := by
+          unfold cubicResidual
+          ring
+        _ = t*(t-c)^2 := by rw [hw])
+  have hr : (∫ w, cubicResidual c (X w)^2 ∂μ) =
+      d2Delta (moment μ X 2) (moment μ X 4) (moment μ X 6) :=
+    residual_integral_eq_delta μ X h2 h4 h6 (ne_of_gt hm2)
+  rw [hr] at h
+  have hl := D2SquareSchur.weighted_square_lower (p*s) (q*t) s t c
+    (mul_pos hp0 hs) (mul_pos hq0 ht)
+  exact le_trans hl (by simpa only [mul_assoc] using h)
+
+theorem schur_floor_of_radius_masses (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ)
+    (s t p q u : ℝ) (hs : 0 < s) (ht : 0 < t) (hp0 : 0 < p) (hq0 : 0 < q)
+    (hst : s ≠ t) (hS : MeasurableSet {w | X w ^ 2 = s})
+    (hT : MeasurableSet {w | X w ^ 2 = t})
+    (hp : p ≤ μ.real {w | X w ^ 2 = s}) (hq : q ≤ μ.real {w | X w ^ 2 = t})
+    (h2 : Integrable (fun w => X w ^ 2) μ)
+    (h4 : Integrable (fun w => X w ^ 4) μ) (hu0 : 0 ≤ u) (hu1 : u ≤ 1/4) :
+    min (p*q/(p+q)*(s-t)^2) (2*(p*s+q*t)^2) ≤
+      d2Schur (moment μ X 2) (moment μ X 4) u := by
+  have hm := second_moment_floor μ X s t p q hs ht hst hS hT hp hq h2
+  have hg := fourth_gap_floor μ X s t p q hp0 hq0 hst hS hT hp hq h2 h4
+  have hm0 : 0 < p*s+q*t := add_pos (mul_pos hp0 hs) (mul_pos hq0 ht)
+  have hg0 : 0 < p*q/(p+q)*(s-t)^2 :=
+    mul_pos (div_pos (mul_pos hp0 hq0) (add_pos hp0 hq0))
+      (sq_pos_of_ne_zero (sub_ne_zero.mpr hst))
+  exact D2SquareSchur.schur_from_lower_inputs (moment μ X 2) (moment μ X 4) u
+    (p*s+q*t) (p*q/(p+q)*(s-t)^2) hm0 hg0 hm hg hu0 hu1
+
+end D2AtomIntegral
diff --git a/companions/d2_atom_integral_20261006/SOURCE_FILES.json b/companions/d2_atom_integral_20261006/SOURCE_FILES.json
index 57e6a594e..8854ae431 100644
--- a/companions/d2_atom_integral_20261006/SOURCE_FILES.json
+++ b/companions/d2_atom_integral_20261006/SOURCE_FILES.json
@@ -12,9 +12,9 @@
       "sha256": "746523ec422f3325029bb476f254b8d584692534f9cde00d95901209e6d81ccb"
     },
     "companions/d2_atom_integral_20261006/D2AtomIntegral.lean": {
-      "bytes": 249,
-      "git_blob": "840d32724f01a720f173c52bfa78167efa5fbab7",
-      "sha256": "c1a5d57231c8e421b2b819a3472487c22fc17cce1dfa515045cbe2ac1e5f55a1"
+      "bytes": 7278,
+      "git_blob": "adbbf555771830a9c4c6c3262a485cd9a1ab0273",
+      "sha256": "247507c4b7aeaccc033cd4d648442172d61227bb27239a7dacccd0f2fa1ba6c3"
     },
     "companions/d2_atom_integral_20261006/SCOPE.md": {
       "bytes": 6299,