From f9d478e0be4cf9db46a854606e00eb2c43fcbfda Mon Sep 17 00:00:00 2001
From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com>
Date: Mon, 5 Oct 2026 20:58:14 -0700
Subject: [PATCH 1/4] Specify D2 square and Schur Lean contracts before
 implementation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Dylan Roy — delegated AI work. Author OpenAI / GPT-6 Astra Pro, d2-square-schur-formal-20261006. Test-first stub: four exact-type contracts must fail on absent declarations. New isolated companion and read-only workflow; all existing formal/proof/gate bytes preserved. Python helper tests first failed 8 missing-helper assertions, then pass 8/8 in both modes. No kernel-proof or scientific-acceptance claim. Scientific effect NONE.
---
 .github/workflows/d2-square-schur.yml         |  50 +++++++
 .../d2_square_schur_20261006/Contract.lean    |  22 +++
 .../D2SquareSchur.lean                        |   4 +
 companions/d2_square_schur_20261006/SCOPE.md  |  64 ++++++++
 .../SOURCE_FILES.json                         |  48 ++++++
 companions/d2_square_schur_20261006/check.py  | 140 ++++++++++++++++++
 companions/d2_square_schur_20261006/replay.sh |  48 ++++++
 .../d2_square_schur_20261006/test_check.py    |  77 ++++++++++
 8 files changed, 453 insertions(+)
 create mode 100644 .github/workflows/d2-square-schur.yml
 create mode 100644 companions/d2_square_schur_20261006/Contract.lean
 create mode 100644 companions/d2_square_schur_20261006/D2SquareSchur.lean
 create mode 100644 companions/d2_square_schur_20261006/SCOPE.md
 create mode 100644 companions/d2_square_schur_20261006/SOURCE_FILES.json
 create mode 100644 companions/d2_square_schur_20261006/check.py
 create mode 100644 companions/d2_square_schur_20261006/replay.sh
 create mode 100644 companions/d2_square_schur_20261006/test_check.py

diff --git a/.github/workflows/d2-square-schur.yml b/.github/workflows/d2-square-schur.yml
new file mode 100644
index 000000000..b4d62e2bb
--- /dev/null
+++ b/.github/workflows/d2-square-schur.yml
@@ -0,0 +1,50 @@
+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
+      - 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
diff --git a/companions/d2_square_schur_20261006/Contract.lean b/companions/d2_square_schur_20261006/Contract.lean
new file mode 100644
index 000000000..1ba8dc0d3
--- /dev/null
+++ b/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
diff --git a/companions/d2_square_schur_20261006/D2SquareSchur.lean b/companions/d2_square_schur_20261006/D2SquareSchur.lean
new file mode 100644
index 000000000..0c912ddc0
--- /dev/null
+++ b/companions/d2_square_schur_20261006/D2SquareSchur.lean
@@ -0,0 +1,4 @@
+import ResearchFormalCoreR1.D2Schur
+
+/- Test-first stub: the exact-type Contract must reject missing declarations.
+No proof placeholder, custom axiom or scientific assertion is admitted here. -/
diff --git a/companions/d2_square_schur_20261006/SCOPE.md b/companions/d2_square_schur_20261006/SCOPE.md
new file mode 100644
index 000000000..4db0587fc
--- /dev/null
+++ b/companions/d2_square_schur_20261006/SCOPE.md
@@ -0,0 +1,64 @@
+# 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.
+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. 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 exact-type Contract preserves all hypotheses and the original
+subtractive d2Schur definition, not an unrelated redefinition of the quotient.
+
+## Verification and exclusions
+
+Initial publication is a test-first stub; Contract.lean must fail on the four
+missing names. Source supply, successful hosted execution and a distinct
+source-alignment review are separate states recorded in the PR. A configured
+workflow or an empty stub module does not establish these theorems.
+
+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 theorems, ZERO new definitions; the primary 63-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.
diff --git a/companions/d2_square_schur_20261006/SOURCE_FILES.json b/companions/d2_square_schur_20261006/SOURCE_FILES.json
new file mode 100644
index 000000000..a6096ab56
--- /dev/null
+++ b/companions/d2_square_schur_20261006/SOURCE_FILES.json
@@ -0,0 +1,48 @@
+{
+  "core_tree": "d7422c6b1acbf3e20c75a1ed7fc13fc30125ec14",
+  "files": {
+    ".github/workflows/d2-square-schur.yml": {
+      "bytes": 1625,
+      "git_blob": "b4d62e2bb3c467068b4e1f22a434c8d569395256",
+      "sha256": "6937c1b88b7627904ca8bdc49416b24210515c0bad1c937255158c7d605ba0cb"
+    },
+    "companions/d2_square_schur_20261006/Contract.lean": {
+      "bytes": 869,
+      "git_blob": "1ba8dc0d38ca1e3afdd6b8044d2298a2dbd2275c",
+      "sha256": "17d29f16a788be98145ac76e55ab4103378e453770eb8ac4bde58281747d2eea"
+    },
+    "companions/d2_square_schur_20261006/D2SquareSchur.lean": {
+      "bytes": 195,
+      "git_blob": "0c912ddc09d91f5a7f4069832a418190f5c89526",
+      "sha256": "7c0b4ffb956545a36209506880452bc9d16560e7ef7c1f8c5beac134c9f188ea"
+    },
+    "companions/d2_square_schur_20261006/SCOPE.md": {
+      "bytes": 3771,
+      "git_blob": "4db0587fc38ae46498f79eb538231f1b3d858781",
+      "sha256": "8d8ef0a7b7d3f4327f13ec20f43fbe55913e63c95cffa04bbb958fa9a7251a8f"
+    },
+    "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": 3503,
+      "git_blob": "61fc09bcf5351e6619e9b6f09879ace280f25d96",
+      "sha256": "c080ee5b94b54bf9ac99ccec02184c7c138629cf07a7ff77318ada3d644eaaff"
+    }
+  },
+  "scientific_effect": "NONE",
+  "targets": [
+    "D2SquareSchur.weighted_square_identity",
+    "D2SquareSchur.weighted_square_lower",
+    "D2SquareSchur.schur_no_upper",
+    "D2SquareSchur.schur_from_lower_inputs"
+  ],
+  "version": 1
+}
diff --git a/companions/d2_square_schur_20261006/check.py b/companions/d2_square_schur_20261006/check.py
new file mode 100644
index 000000000..bdeba9033
--- /dev/null
+++ b/companions/d2_square_schur_20261006/check.py
@@ -0,0 +1,140 @@
+#!/usr/bin/env python3
+"""Bounded companion driver, adapted from #317 check.py (812d0262).
+
+Reuses the pinned core axiom audit. Neither this small inventory nor a receipt
+is a general Lean declaration scanner or independent scientific acceptance.
+"""
+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_square_schur_20261006'
+WORKFLOW='.github/workflows/d2-square-schur.yml'
+REPO='d6g8k5htny-coder/Math-'
+CORE_TREE='d7422c6b1acbf3e20c75a1ed7fc13fc30125ec14'
+CORE_MANIFEST='5d7ccdb0885af7bf4a2aa6ec4dce5f5c41435bb10a0a7a426a8af286d4f035e4'
+CORE_GATE='958b149ea3a4ce735644a2079f817b5deddf5dc0d5ca347904ad09db6ad47d68'
+TARGETS=tuple('D2SquareSchur.'+n for n in ('weighted_square_identity','weighted_square_lower',
+    'schur_no_upper','schur_from_lower_inputs'))
+CONTROLS=('RejectSignedWeights','RejectEndpointMaximum','RejectOutsideDirection')
+PAYLOADS={PACKAGE+'/'+n for n in ('D2SquareSchur.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 metadata():return strict((SIDE/'SOURCE_FILES.json').read_bytes())
+
+def source():
+    meta=metadata();head=git('rev-parse','HEAD')
+    require(set(meta)=={'version','scientific_effect','core_tree','targets','files'},'manifest schema')
+    require(meta['version']==1 and type(meta['version']) is int,'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):
+        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)
+    git('diff','--exit-code','HEAD','--','formal',PACKAGE,WORKFLOW)
+    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'^D2SquareSchur\.[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 D2SquareSchur\n'+'\n'.join('#print axioms '+n for n in TARGETS)+'\n')
+    (out/'Types.lean').write_text('import D2SquareSchur\nset_option pp.explicit true\n'+'\n'.join('#check '+n for n in TARGETS)+'\n')
+    expressions={
+      'RejectSignedWeights':'(-2 : ℝ) * 1 / (-2 + 1) * (0 - 1)^2 ≤ (-2) * (0 - 2)^2 + 1 * (1 - 2)^2',
+      'RejectEndpointMaximum':'max (2 - (1 : ℝ)^2) (2 * 1^2) ≤ d2Schur 1 2 0',
+      'RejectOutsideDirection':'min (2 - (1 : ℝ)^2) (2 * 1^2) ≤ d2Schur 1 2 1'}
+    for label,statement in expressions.items():
+        (out/(label+'.lean')).write_text('import D2SquareSchur\nopen ResearchFormalCoreR1\nexample : '+statement+' := by\n  norm_num [d2Schur, d2Alpha, d2Gamma, d2DetV]\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 ('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':4,'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_square_schur_20261006/replay.sh b/companions/d2_square_schur_20261006/replay.sh
new file mode 100644
index 000000000..f5bc85027
--- /dev/null
+++ b/companions/d2_square_schur_20261006/replay.sh
@@ -0,0 +1,48 @@
+#!/usr/bin/env bash
+# Derived from #317 replay.sh, blob 85c0de87; no live tee/hash race.
+set -euo pipefail
+ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
+SIDE="$ROOT/companions/d2_square_schur_20261006"
+OUT="$ROOT/.lake/d2-square-schur-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 SQUARE_SIDE="$SIDE" SQUARE_OUT="$OUT"
+cd "$ROOT/formal"
+lake env bash <<'INNER'
+set -euo pipefail
+export LEAN_PATH="$SQUARE_SIDE:${LEAN_PATH:-}"
+export LEAN_SRC_PATH="$SQUARE_SIDE:${LEAN_SRC_PATH:-}"
+lean --version | tee "$SQUARE_OUT/toolchain.log"
+run_lean() {
+  local label="$1"; shift
+  local code=0
+  "$@" >"$SQUARE_OUT/$label.log" 2>&1 || code=$?
+  printf '%s\n' "$code" >"$SQUARE_OUT/$label.status"
+  cat "$SQUARE_OUT/$label.log"
+  test "$code" -eq 0
+}
+run_lean build lean -DwarningAsError=true --root="$SQUARE_SIDE" -o "$SQUARE_SIDE/D2SquareSchur.olean" "$SQUARE_SIDE/D2SquareSchur.lean"
+run_lean contract lean -DwarningAsError=true --root="$SQUARE_SIDE" "$SQUARE_SIDE/Contract.lean"
+run_lean axioms lean -DwarningAsError=true --root="$SQUARE_OUT" "$SQUARE_OUT/Audit.lean"
+run_lean types lean -DwarningAsError=true --root="$SQUARE_OUT" "$SQUARE_OUT/Types.lean"
+run_lean leanchecker leanchecker --fresh D2SquareSchur
+for control in RejectSignedWeights RejectEndpointMaximum RejectOutsideDirection; do
+  code=0
+  lean -DwarningAsError=true --root="$SQUARE_OUT" "$SQUARE_OUT/$control.lean" >"$SQUARE_OUT/$control.log" 2>&1 || code=$?
+  printf '%s\n' "$code" >"$SQUARE_OUT/$control.status"
+  python3 -B -S "$SQUARE_SIDE/check.py" negative "$SQUARE_OUT/$control.log" --control "$control" --status "$code"
+done
+INNER
+cd "$ROOT"
+python3 -B -S "$SIDE/check.py" finish "$OUT"
+echo 'PASS: four scalar targets only; model/atom-integral/independent-alignment obligations remain.'
diff --git a/companions/d2_square_schur_20261006/test_check.py b/companions/d2_square_schur_20261006/test_check.py
new file mode 100644
index 000000000..61fc09bcf
--- /dev/null
+++ b/companions/d2_square_schur_20261006/test_check.py
@@ -0,0 +1,77 @@
+#!/usr/bin/env python3
+"""Finite diagnostics and exact evidence-parser controls, not Lean execution."""
+from fractions import Fraction as F
+import importlib.util
+import itertools
+from pathlib import Path
+import unittest
+
+SIDE = Path(__file__).resolve().parent
+
+class Controls(unittest.TestCase):
+    def setUp(self):
+        self.assertTrue((SIDE/'check.py').is_file(), 'missing evidence helper')
+        spec = importlib.util.spec_from_file_location('d2_square_check', SIDE/'check.py')
+        self.c = importlib.util.module_from_spec(spec)
+        spec.loader.exec_module(self.c)
+
+    def test_strict_json(self):
+        self.assertEqual(self.c.strict('{"ok":true,"n":1}'), {'ok':True,'n':1})
+        for raw in ('{"x":1,"x":2}', '{"x":NaN}', '{"x":1.0}', '{}{}'):
+            with self.assertRaises(ValueError): self.c.strict(raw)
+
+    def test_negative_controls_accept_exact_reason(self):
+        for name in self.c.CONTROLS:
+            msg = f'/tmp/{name}.lean:4:2: error: unsolved goals\n⊢ False\n'
+            self.assertEqual(self.c.negative(msg,name,1), name)
+
+    def test_negative_controls_reject_wrong_reason(self):
+        name = self.c.CONTROLS[0]
+        good = f'{name}.lean:4:2: error: unsolved goals\n⊢ False\n'
+        bads = (good.replace('False','True'), good.replace(name,'Other'),
+                good+'error: another problem\n', 'error: unknown identifier\n', '')
+        for text in bads:
+            with self.assertRaisesRegex(ValueError,'intended False'): self.c.negative(text,name,1)
+        for code in (0,2,True):
+            with self.assertRaisesRegex(ValueError,'exit'): self.c.negative(good,name,code)
+
+    def test_type_inventory(self):
+        names = self.c.TARGETS
+        good = '\n'.join(n+' : True' for n in names)+'\n'
+        self.assertEqual(self.c.types(good), list(names))
+        for bad in (good+good, good.replace(names[0],'Other.first'),
+                    'warning: unused\n'+good, good.replace(names[-1]+' : True\n','')):
+            with self.assertRaises(ValueError): self.c.types(bad)
+
+    def test_weighted_square(self):
+        for u,v,a,b,c in itertools.product((F(1,3),F(2)),(F(1,4),F(3)),
+                (F(-2),F(0),F(2)),(F(-1),F(3)),(F(-2),F(0),F(4))):
+            lhs=u*(a-c)**2+v*(b-c)**2
+            floor=u*v/(u+v)*(a-b)**2
+            rhs=floor+(u+v)*(c-(u*a+v*b)/(u+v))**2
+            self.assertEqual(lhs,rhs);self.assertLessEqual(floor,lhs)
+
+    def test_schur_endpoints_and_input_floors(self):
+        for s0,g0,sadd,gadd,q in itertools.product((F(1,3),F(1),F(3)),
+                (F(1,4),F(2),F(5)),(F(0),F(2)),(F(0),F(3)),
+                (F(0),F(1,16),F(1,4))):
+            s,g=s0+sadd,g0+gadd;x=s*s
+            a=x*(g+x);b=g*(g+4*x)/4;n=x*g*(g+2*x)
+            d=(1-4*q)*a+4*q*b
+            self.assertLessEqual(min(g,2*x),n/d)
+            self.assertLessEqual(min(g0,2*s0*s0),n/d)
+
+    def test_false_witnesses(self):
+        # These are also executable Lean rejection contracts, not generalized facts.
+        u,v,a,b,c=map(F,(-2,1,0,1,2))
+        self.assertGreater(u*v/(u+v)*(a-b)**2,u*(a-c)**2+v*(b-c)**2)
+        self.assertGreater(max(F(1),F(2)),F(3,2))
+        self.assertGreater(min(F(1),F(2)),F(-3))
+
+    def test_identity_binds_every_byte(self):
+        a=self.c.identity(b'abc\n');b=self.c.identity(b'abc')
+        self.assertEqual(a['bytes'],4)
+        self.assertNotEqual(a['sha256'],b['sha256'])
+        self.assertNotEqual(a['git_blob'],b['git_blob'])
+
+if __name__=='__main__':unittest.main(verbosity=2)

From 3479b6e127b05e953f84feef3f3fb7e88de625ac Mon Sep 17 00:00:00 2001
From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com>
Date: Mon, 5 Oct 2026 21:32:32 -0700
Subject: [PATCH 2/4] Repair D2 companion checkout history before its Lean
 contract stage
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-square-schur-resume-math-audit-20261006, pickup343/6009354574. Original dedicated37411527600 fails historical proof reachability before Lean:187 root tests,4 failures/24 errors; artifact11389791199 retained. Add one meaningful checkout regression (1 failure on predecessor,9/9 green in both local modes after fix); fetch-depth0 supplies the historical source objects required by the unchanged complete root suite. Contract and four-declaration stub remain unchanged. No claim of a Lean missing-declaration failure yet. Scientific effect NONE.
---
 .github/workflows/d2-square-schur.yml                |  1 +
 .../d2_square_schur_20261006/SOURCE_FILES.json       | 12 ++++++------
 companions/d2_square_schur_20261006/test_check.py    |  9 +++++++++
 3 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/d2-square-schur.yml b/.github/workflows/d2-square-schur.yml
index b4d62e2bb..cfb4b10be 100644
--- a/.github/workflows/d2-square-schur.yml
+++ b/.github/workflows/d2-square-schur.yml
@@ -24,6 +24,7 @@ jobs:
       - 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:
diff --git a/companions/d2_square_schur_20261006/SOURCE_FILES.json b/companions/d2_square_schur_20261006/SOURCE_FILES.json
index a6096ab56..dd017fd0c 100644
--- a/companions/d2_square_schur_20261006/SOURCE_FILES.json
+++ b/companions/d2_square_schur_20261006/SOURCE_FILES.json
@@ -2,9 +2,9 @@
   "core_tree": "d7422c6b1acbf3e20c75a1ed7fc13fc30125ec14",
   "files": {
     ".github/workflows/d2-square-schur.yml": {
-      "bytes": 1625,
-      "git_blob": "b4d62e2bb3c467068b4e1f22a434c8d569395256",
-      "sha256": "6937c1b88b7627904ca8bdc49416b24210515c0bad1c937255158c7d605ba0cb"
+      "bytes": 1650,
+      "git_blob": "cfb4b10be7662fb8f01cc8d248c8f68e065de4fb",
+      "sha256": "1e597b0a0b9f2956153a97bb24578f5cb80cac6f8f93a0845e75c57869c2afb1"
     },
     "companions/d2_square_schur_20261006/Contract.lean": {
       "bytes": 869,
@@ -32,9 +32,9 @@
       "sha256": "2240cd236425f31e9cd549b1d180645da50e0e19099d9f1a53ec4b17a2217934"
     },
     "companions/d2_square_schur_20261006/test_check.py": {
-      "bytes": 3503,
-      "git_blob": "61fc09bcf5351e6619e9b6f09879ace280f25d96",
-      "sha256": "c080ee5b94b54bf9ac99ccec02184c7c138629cf07a7ff77318ada3d644eaaff"
+      "bytes": 4038,
+      "git_blob": "547ac0e50e36846c98999fc2d94150054468829e",
+      "sha256": "95277602acfddce10e585722144bb9759a69d76a597a1511788a93d143f9ea60"
     }
   },
   "scientific_effect": "NONE",
diff --git a/companions/d2_square_schur_20261006/test_check.py b/companions/d2_square_schur_20261006/test_check.py
index 61fc09bcf..547ac0e50 100644
--- a/companions/d2_square_schur_20261006/test_check.py
+++ b/companions/d2_square_schur_20261006/test_check.py
@@ -68,6 +68,15 @@ def test_false_witnesses(self):
         self.assertGreater(max(F(1),F(2)),F(3,2))
         self.assertGreater(min(F(1),F(2)),F(-3))
 
+    def test_workflow_fetches_required_history(self):
+        # The complete root suite resolves historical proof commits.
+        text = (SIDE.parents[1]/'.github/workflows/d2-square-schur.yml').read_text()
+        checkout = text.split('uses: actions/checkout@', 1)[1].split('\n      - ', 1)[0]
+        settings = [line.strip() for line in checkout.splitlines()
+                    if not line.lstrip().startswith('#')]
+        self.assertIn('fetch-depth: 0', settings)
+        self.assertIn('persist-credentials: false', settings)
+
     def test_identity_binds_every_byte(self):
         a=self.c.identity(b'abc\n');b=self.c.identity(b'abc')
         self.assertEqual(a['bytes'],4)

From b438976778ddf3b97893ca65da596ef674e77317 Mon Sep 17 00:00:00 2001
From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com>
Date: Mon, 5 Oct 2026 21:44:28 -0700
Subject: [PATCH 3/4] Implement the four exact D2 square and Schur scalar proof
 contracts
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, d2-square-schur-resume-math-audit-20261006, scope343/6009354574 and main229/6009422632. Original dedicated37414215874 reached the unchanged Contract and failed on exactly four absent names after both189 root suites,133 core suites and core kernel replay passed; original artifact11390508232 retained. Supply only four proof bodies, update scope/history and their manifest identities. No Contract, core, gate, dependency or scientific-status change. Schur floor uses endpoint upper denominator control with exact nonnegative remainders x^2*g and x*g^2/2. Local9/9 helper tests pass both modes; new Lean source execution is pending, not claimed. Scientific effect NONE; no author self-merge.
---
 .../D2SquareSchur.lean                        | 77 ++++++++++++++++++-
 companions/d2_square_schur_20261006/SCOPE.md  | 30 ++++++--
 .../SOURCE_FILES.json                         | 12 +--
 3 files changed, 103 insertions(+), 16 deletions(-)

diff --git a/companions/d2_square_schur_20261006/D2SquareSchur.lean b/companions/d2_square_schur_20261006/D2SquareSchur.lean
index 0c912ddc0..ba85a816c 100644
--- a/companions/d2_square_schur_20261006/D2SquareSchur.lean
+++ b/companions/d2_square_schur_20261006/D2SquareSchur.lean
@@ -1,4 +1,77 @@
 import ResearchFormalCoreR1.D2Schur
 
-/- Test-first stub: the exact-type Contract must reject missing declarations.
-No proof placeholder, custom axiom or scientific assertion is admitted here. -/
+/-!
+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
diff --git a/companions/d2_square_schur_20261006/SCOPE.md b/companions/d2_square_schur_20261006/SCOPE.md
index 4db0587fc..411e410b4 100644
--- a/companions/d2_square_schur_20261006/SCOPE.md
+++ b/companions/d2_square_schur_20261006/SCOPE.md
@@ -2,6 +2,7 @@
 
 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
@@ -27,19 +28,32 @@ from the primary formal tree d7422c6b1acbf3e20c75a1ed7fc13fc30125ec14.
 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. Hence h*max(A,B)<=N. The existing positive
+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 exact-type Contract preserves all hypotheses and the original
-subtractive d2Schur definition, not an unrelated redefinition of the quotient.
+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 is a test-first stub; Contract.lean must fail on the four
-missing names. Source supply, successful hosted execution and a distinct
-source-alignment review are separate states recorded in the PR. A configured
-workflow or an empty stub module does not establish these theorems.
+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
@@ -51,7 +65,7 @@ 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 theorems, ZERO new definitions; the primary 63-target
+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
diff --git a/companions/d2_square_schur_20261006/SOURCE_FILES.json b/companions/d2_square_schur_20261006/SOURCE_FILES.json
index dd017fd0c..17e30bf13 100644
--- a/companions/d2_square_schur_20261006/SOURCE_FILES.json
+++ b/companions/d2_square_schur_20261006/SOURCE_FILES.json
@@ -12,14 +12,14 @@
       "sha256": "17d29f16a788be98145ac76e55ab4103378e453770eb8ac4bde58281747d2eea"
     },
     "companions/d2_square_schur_20261006/D2SquareSchur.lean": {
-      "bytes": 195,
-      "git_blob": "0c912ddc09d91f5a7f4069832a418190f5c89526",
-      "sha256": "7c0b4ffb956545a36209506880452bc9d16560e7ef7c1f8c5beac134c9f188ea"
+      "bytes": 3008,
+      "git_blob": "ba85a816c58bfa9350b98e1788bbb769d8a1fb8d",
+      "sha256": "f10a5e0a9fbd5b6e713196f5747bab2a38bca5387d3665dd62f52dd22054bfe2"
     },
     "companions/d2_square_schur_20261006/SCOPE.md": {
-      "bytes": 3771,
-      "git_blob": "4db0587fc38ae46498f79eb538231f1b3d858781",
-      "sha256": "8d8ef0a7b7d3f4327f13ec20f43fbe55913e63c95cffa04bbb958fa9a7251a8f"
+      "bytes": 4725,
+      "git_blob": "411e410b4c5ee3dbbb07372c74730520d2aee8b0",
+      "sha256": "f35a30b7221800489f8fb97fb573434273876d9d43937a631a0c52b6abe9e0d7"
     },
     "companions/d2_square_schur_20261006/check.py": {
       "bytes": 7611,

From cc8b2d5bd7505b7f185607880bc0aa1403c8c148 Mon Sep 17 00:00:00 2001
From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com>
Date: Mon, 5 Oct 2026 21:55:52 -0700
Subject: [PATCH 4/4] Remove redundant Lean tactic sequencing without relaxing
 warning policy
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Dylan Roy — delegated AI work. Author OpenAI / GPT-6 Astra Pro, d2-square-schur-resume-math-audit-20261006. Original dedicated37415147443/1 failed only the unnecessarySeqFocus linter at line17; artifact11390843962 retained with exact SHA2568be34660b4c9b180f45173140ee85f8f0203435fb7d23e701a9dd72f74a84fb3. Remove four redundant tactic characters and update the source identity. All four theorem signatures, exact Contract, SCOPE, proofs after the first theorem, drivers, workflow, primary formal tree and warnings-as-errors setting are unchanged. History is recorded in343/6009602978, not an additional scope edit. New actual execution and reader delta remain required. Scientific effect NONE.
---
 companions/d2_square_schur_20261006/D2SquareSchur.lean | 2 +-
 companions/d2_square_schur_20261006/SOURCE_FILES.json  | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/companions/d2_square_schur_20261006/D2SquareSchur.lean b/companions/d2_square_schur_20261006/D2SquareSchur.lean
index ba85a816c..4855c92d5 100644
--- a/companions/d2_square_schur_20261006/D2SquareSchur.lean
+++ b/companions/d2_square_schur_20261006/D2SquareSchur.lean
@@ -14,7 +14,7 @@ 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
+  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
diff --git a/companions/d2_square_schur_20261006/SOURCE_FILES.json b/companions/d2_square_schur_20261006/SOURCE_FILES.json
index 17e30bf13..fb92861c8 100644
--- a/companions/d2_square_schur_20261006/SOURCE_FILES.json
+++ b/companions/d2_square_schur_20261006/SOURCE_FILES.json
@@ -12,9 +12,9 @@
       "sha256": "17d29f16a788be98145ac76e55ab4103378e453770eb8ac4bde58281747d2eea"
     },
     "companions/d2_square_schur_20261006/D2SquareSchur.lean": {
-      "bytes": 3008,
-      "git_blob": "ba85a816c58bfa9350b98e1788bbb769d8a1fb8d",
-      "sha256": "f10a5e0a9fbd5b6e713196f5747bab2a38bca5387d3665dd62f52dd22054bfe2"
+      "bytes": 3004,
+      "git_blob": "4855c92d55254969e1de7f8cf8dec2bdc027cf69",
+      "sha256": "e0f9560e6f129216cd989cea3cdf97254972ca9b1cae7bab57df664329ae78fa"
     },
     "companions/d2_square_schur_20261006/SCOPE.md": {
       "bytes": 4725,