Lean: weighted squares and upper-moment-free D2 Schur bound

.github/workflows/d2-square-schur.yml

@@ -0,0 +1,51 @@
+name: D2 square and Schur scalar companion
+'on':
+  pull_request:
+    paths:
+      - 'companions/d2_square_schur_20261006/**'
+      - '.github/workflows/d2-square-schur.yml'
+      - 'formal/**'
+  push:
+    branches: [main]
+    paths:
+      - 'companions/d2_square_schur_20261006/**'
+      - '.github/workflows/d2-square-schur.yml'
+      - 'formal/**'
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  d2-square-schur:
+    runs-on: ubuntu-latest
+    timeout-minutes: 25
+    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 complete suites and exact scalar contracts
+        shell: bash
+        run: bash companions/d2_square_schur_20261006/replay.sh
+      - name: Preserve original success or failure evidence
+        if: always()
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a
+        with:
+          name: d2-square-schur-${{ github.run_id }}-${{ github.run_attempt }}
+          path: |
+            .lake/d2-square-schur-evidence/
+            formal/.lake/formal-evidence/
+          include-hidden-files: true
+          if-no-files-found: error
+          retention-days: 30

companions/d2_square_schur_20261006/Contract.lean

@@ -0,0 +1,22 @@
+import D2SquareSchur
+
+open ResearchFormalCoreR1
+
+example (u v a b c : ℝ) (huv : u + v ≠ 0) :
+    u * (a-c)^2 + v * (b-c)^2 =
+      u*v/(u+v)*(a-b)^2 + (u+v)*(c-(u*a+v*b)/(u+v))^2 :=
+  D2SquareSchur.weighted_square_identity u v a b c huv
+
+example (u v a b c : ℝ) (hu : 0 < u) (hv : 0 < v) :
+    u*v/(u+v)*(a-b)^2 ≤ u*(a-c)^2 + v*(b-c)^2 :=
+  D2SquareSchur.weighted_square_lower u v a b c hu hv
+
+example (m2 m4 q : ℝ) (hm2 : 0 < m2) (hm4 : m2^2 < m4)
+    (hq0 : 0 ≤ q) (hq1 : q ≤ 1/4) :
+    min (m4-m2^2) (2*m2^2) ≤ d2Schur m2 m4 q :=
+  D2SquareSchur.schur_no_upper m2 m4 q hm2 hm4 hq0 hq1
+
+example (m2 m4 q s0 g0 : ℝ) (hs0 : 0 < s0) (hg0 : 0 < g0)
+    (hm2 : s0 ≤ m2) (hgap : g0 ≤ m4-m2^2) (hq0 : 0 ≤ q) (hq1 : q ≤ 1/4) :
+    min g0 (2*s0^2) ≤ d2Schur m2 m4 q :=
+  D2SquareSchur.schur_from_lower_inputs m2 m4 q s0 g0 hs0 hg0 hm2 hgap hq0 hq1

companions/d2_square_schur_20261006/D2SquareSchur.lean

@@ -0,0 +1,77 @@
+import ResearchFormalCoreR1.D2Schur
+
+/-!
+Four real scalar statements from #328 sections 3 and 5. This module does not
+construct a measure, a field, or a conditional covariance. All strict moment
+and direction assumptions remain in the exact-type Contract.
+-/
+namespace D2SquareSchur
+
+open ResearchFormalCoreR1
+set_option autoImplicit false
+
+theorem weighted_square_identity (u v a b c : ℝ) (huv : u + v ≠ 0) :
+    u * (a-c)^2 + v * (b-c)^2 =
+      u*v/(u+v)*(a-b)^2 + (u+v)*(c-(u*a+v*b)/(u+v))^2 := by
+  field_simp [huv]
+  ring
+
+theorem weighted_square_lower (u v a b c : ℝ) (hu : 0 < u) (hv : 0 < v) :
+    u*v/(u+v)*(a-b)^2 ≤ u*(a-c)^2 + v*(b-c)^2 := by
+  rw [weighted_square_identity u v a b c (ne_of_gt (add_pos hu hv))]
+  exact le_add_of_nonneg_right (mul_nonneg (add_pos hu hv).le (sq_nonneg _))
+
+/-- Endpoint upper control of the denominator, not lower-bound substitution. -/
+theorem schur_no_upper (m2 m4 q : ℝ) (hm2 : 0 < m2) (hm4 : m2^2 < m4)
+    (hq0 : 0 ≤ q) (hq1 : q ≤ 1/4) :
+    min (m4-m2^2) (2*m2^2) ≤ d2Schur m2 m4 q := by
+  let x : ℝ := m2^2
+  let g : ℝ := m4-x
+  let A : ℝ := x*m4
+  let B : ℝ := g*(m4+3*x)/4
+  let N : ℝ := d2Numerator m2 m4
+  let h : ℝ := min g (2*x)
+  have hx : 0 < x := sq_pos_of_pos hm2
+  have hg : 0 < g := sub_pos.mpr hm4
+  have hm4pos : 0 < m4 := lt_trans hx hm4
+  have hA : 0 < A := mul_pos hx hm4pos
+  have hB : 0 < B := by
+    dsimp [B]
+    positivity
+  have hNA : N-g*A = x^2*g := by
+    dsimp [N, g, A, x, d2Numerator]
+    ring
+  have hNB : N-(2*x)*B = x*g^2/2 := by
+    dsimp [N, g, B, x, d2Numerator]
+    ring
+  have hga : g*A ≤ N := by
+    have hp := mul_nonneg (sq_nonneg x) hg.le
+    linarith [hNA]
+  have h2xb : (2*x)*B ≤ N := by
+    have hp : 0 ≤ x*g^2/2 := div_nonneg (mul_nonneg hx.le (sq_nonneg g)) (by norm_num)
+    linarith [hNB]
+  have hmulA : h*A ≤ N :=
+    le_trans (mul_le_mul_of_nonneg_right (min_le_left g (2*x)) hA.le) hga
+  have hmulB : h*B ≤ N :=
+    le_trans (mul_le_mul_of_nonneg_right (min_le_right g (2*x)) hB.le) h2xb
+  have hM : 0 < max A B := lt_of_lt_of_le hA (le_max_left _ _)
+  have hmax : h*max A B ≤ N := by
+    rcases le_total A B with hab | hba
+    · simpa only [max_eq_right hab] using hmulB
+    · simpa only [max_eq_left hba] using hmulA
+  have hquot : h ≤ N/max A B := (le_div_iff₀ hM).2 hmax
+  exact le_trans hquot (d2_schur_endpoint_lower m2 m4 q hm2 hm4 hq0 hq1)
+
+theorem schur_from_lower_inputs (m2 m4 q s0 g0 : ℝ) (hs0 : 0 < s0) (hg0 : 0 < g0)
+    (hm2 : s0 ≤ m2) (hgap : g0 ≤ m4-m2^2) (hq0 : 0 ≤ q) (hq1 : q ≤ 1/4) :
+    min g0 (2*s0^2) ≤ d2Schur m2 m4 q := by
+  have hm2pos : 0 < m2 := lt_of_lt_of_le hs0 hm2
+  have hm4 : m2^2 < m4 := by linarith
+  have hsquare : s0^2 ≤ m2^2 := by
+    have hp := mul_nonneg (sub_nonneg.mpr hm2) (add_nonneg hm2pos.le hs0.le)
+    nlinarith
+  have hmin : min g0 (2*s0^2) ≤ min (m4-m2^2) (2*m2^2) :=
+    min_le_min hgap (by linarith)
+  exact le_trans hmin (schur_no_upper m2 m4 q hm2pos hm4 hq0 hq1)
+
+end D2SquareSchur

companions/d2_square_schur_20261006/SCOPE.md

@@ -0,0 +1,78 @@
+# Weighted squares and upper-moment-free D2 Schur bound
+
+Dylan Roy — delegated AI work. Author: OpenAI / GPT-6 Astra Pro,
+`d2-square-schur-formal-20261006`, pickup main#229/6008966287.
+Continuation: `d2-square-schur-resume-math-audit-20261006`, #343/6009354574.
+Scientific effect NONE; author-exposed; organizational-independence credit 0.
+
+## Four target statements
+
+1. `weighted_square_identity`: weighted completion for real u,v,a,b,c with
+   u+v nonzero. The signed-weight algebra is valid; no positivity is asserted.
+2. `weighted_square_lower`: the first term is a lower bound when both weights
+   are positive. These sufficient assumptions are intentionally retained.
+3. `schur_no_upper`: for m2>0, m4>m2^2 and 0<=q<=1/4,
+   `min (m4-m2^2) (2*m2^2) <= ResearchFormalCoreR1.d2Schur m2 m4 q`.
+4. `schur_from_lower_inputs`: substitute actual positive lower inputs
+   s0<=m2 and g0<=m4-m2^2 to obtain `min g0 (2*s0^2) <= d2Schur ...`.
+
+The source is #328 NOTE sections 3 and 5 at 31f7a6b5a36045be7795a6461da067a8ada96343,
+blob cedbb44a237d1a158111dca81c30983f7efd37f1. The shared two-mass calculation is
+already in #326, not a second discovery. The stronger optional proposal in
+#328 comment6008747995 Part B is NOT incorporated. This companion uses only
+unchanged D2Schur.lean blob b95460c0d263a32ea274b347079cca6aaab3d2e9,
+from the primary formal tree d7422c6b1acbf3e20c75a1ed7fc13fc30125ec14.
+
+## Proof route
+
+Field simplification proves the weighted identity; nonnegative square gives
+the lower bound. Write x=m2^2 and g=m4-x. The two determinant endpoints are
+A=x(g+x) and B=g(g+4x)/4, and numerator N=xg(g+2x). With h=min(g,2x),
+hA<=gA<=N and hB<=2xB<=N. The exact nonnegative remainders are
+N-gA=x^2*g and N-2xB=x*g^2/2. Hence h*max(A,B)<=N. The existing positive
+endpoint-denominator theorem bounds N/max(A,B) below the actual d2Schur.
+This never substitutes a lower determinant into a denominator and uses no
+moment upper bound. Monotonicity of squares on positive inputs gives the last
+target. The unchanged exact-type Contract preserves all hypotheses and the
+original subtractive d2Schur definition, not a redefinition of the quotient.
+
+## Verification and exclusions
+
+Initial publication f9d478e was a test-first stub. Its dedicated run37411527600
+failed historical Git reachability BEFORE Lean, not the missing-name contract.
+Original artifact11389791199 (8911 bytes) has SHA256
+430b82d3da185c92f17927d5e0e8b507a05791c80131b27c6cc65371b07172e6.
+The successor3479b6e added fetch-depth0 and one regression while retaining every
+root test and the stub. That regression failed on the old workflow before its
+repair. Dedicated37414215874 then passed both189-method root suites, both133-method
+core suites and the unchanged primary kernel replay; the stub compiled and
+Contract.lean failed on EXACTLY the four absent target names, with exit1.
+Original artifact11390508232 (37549 bytes) has SHA256
+a03f164e08d4c34ea778eb3131c6f2e404af638ca340b03dc3d2a4b82cb973dc.
+
+The four bodies are supplied only after that observed contract failure. Source
+supply, successful hosted execution and a distinct source-alignment review are
+separate states recorded in the PR. No configured workflow, empty stub, finite
+Python model or successful OLD core build proves these new declarations.
+
+The adapted #317 driver runs the complete root and primary formal Python suites
+in normal and optimized modes, the pinned primary kernel check, then this
+module's warnings-as-errors build, exact-type Contract, all four axiom/type
+reports and fresh leanchecker. Three concrete false propositions must fail with
+exact source-bound False-goal diagnostics: signed negative weights, replacing
+the lower minimum by an endpoint maximum, and leaving the q interval.
+Original raw logs/statuses and source/run identity are retained on failure.
+The core audit function is reused by exact hash; this small explicit inventory
+is not the independently owned general RF-GATE-01 declaration scanner.
+
+These are FOUR scalar theorem targets, ZERO new definitions; the primary63-target
+manifest and all older proof bytes are unchanged. No atom-measure integral
+lower bound, moment realizability, periodic spectral law, trigonometric
+parameterization, Gaussian/Palm covariance identification, quadrature or
+persistence theorem is supplied. No full independent alignment or scientific
+acceptance is claimed. #317's actual-law review is not transferred here.
+
+From repository root: `bash companions/d2_square_schur_20261006/replay.sh`
+after setting up the existing pinned formal toolchain. Python-only tests:
+`python -B -S companions/d2_square_schur_20261006/test_check.py` and the same
+command with -O. Python finite controls supplement, never replace, Lean.

companions/d2_square_schur_20261006/SOURCE_FILES.json

@@ -0,0 +1,48 @@
+{
+  "core_tree": "d7422c6b1acbf3e20c75a1ed7fc13fc30125ec14",
+  "files": {
+    ".github/workflows/d2-square-schur.yml": {
+      "bytes": 1650,
+      "git_blob": "cfb4b10be7662fb8f01cc8d248c8f68e065de4fb",
+      "sha256": "1e597b0a0b9f2956153a97bb24578f5cb80cac6f8f93a0845e75c57869c2afb1"
+    },
+    "companions/d2_square_schur_20261006/Contract.lean": {
+      "bytes": 869,
+      "git_blob": "1ba8dc0d38ca1e3afdd6b8044d2298a2dbd2275c",
+      "sha256": "17d29f16a788be98145ac76e55ab4103378e453770eb8ac4bde58281747d2eea"
+    },
+    "companions/d2_square_schur_20261006/D2SquareSchur.lean": {
+      "bytes": 3004,
+      "git_blob": "4855c92d55254969e1de7f8cf8dec2bdc027cf69",
+      "sha256": "e0f9560e6f129216cd989cea3cdf97254972ca9b1cae7bab57df664329ae78fa"
+    },
+    "companions/d2_square_schur_20261006/SCOPE.md": {
+      "bytes": 4725,
+      "git_blob": "411e410b4c5ee3dbbb07372c74730520d2aee8b0",
+      "sha256": "f35a30b7221800489f8fb97fb573434273876d9d43937a631a0c52b6abe9e0d7"
+    },
+    "companions/d2_square_schur_20261006/check.py": {
+      "bytes": 7611,
+      "git_blob": "bdeba903304f39e775ee0f9d2d7e1eb2904d0a48",
+      "sha256": "3e96eeca42e3f17997b2cbea97bee01da3f3f88bbbaed414c1683403ecc80367"
+    },
+    "companions/d2_square_schur_20261006/replay.sh": {
+      "bytes": 2473,
+      "git_blob": "f5bc850272b3823fde320894142078abafdc6d0d",
+      "sha256": "2240cd236425f31e9cd549b1d180645da50e0e19099d9f1a53ec4b17a2217934"
+    },
+    "companions/d2_square_schur_20261006/test_check.py": {
+      "bytes": 4038,
+      "git_blob": "547ac0e50e36846c98999fc2d94150054468829e",
+      "sha256": "95277602acfddce10e585722144bb9759a69d76a597a1511788a93d143f9ea60"
+    }
+  },
+  "scientific_effect": "NONE",
+  "targets": [
+    "D2SquareSchur.weighted_square_identity",
+    "D2SquareSchur.weighted_square_lower",
+    "D2SquareSchur.schur_no_upper",
+    "D2SquareSchur.schur_from_lower_inputs"
+  ],
+  "version": 1
+}