cursor · Oct 6, 2026 · Oct 5, 2026 · Oct 6, 2026 · Oct 6, 2026 · Oct 6, 2026
@@ -0,0 +1,101 @@
+# D2 Schur and endpoint positivity: exact formal scope
+
+**Scientific effect NONE.** Dylan Roy — delegated AI work. Actual author OpenAI /
+GPT-6 Astra Pro, session `lean-d2-schur-expansion-20261005`. This is a continuation
+of that provider's informal derivation, not a nonauthor or blind review.
+Alignment remains PENDING_INDEPENDENT_REVIEW; source progress is not an observed
+kernel run. No source record, scientific register, prize or Boolean is advanced.
+
+## Exact source interface
+
+At Math- commit `ec61d0a4e1d7c29554c0af93fca983092327b618`, consume
+`reviews/side24_d2_certified_small_L_claude_20261005/NOTE.md` section2,
+Git blob `852f7403a8a06a1ef061e363df9502ae16f7a341`, SHA256
+`407828facb8dde26a036a08a5b3978eb74d6d8a508c68e2758c291e16e911588`.
+The exact Schur cancellation and endpoint observation were recorded separately
+in Math-#302 comment6005199919. That mutable comment is attribution/context;
+the complete formulas and Lean definitions here are the bound proof input.
+
+The variables are arbitrary real scalars `m2`, `m4`, `m6`, `q`. The intended
+interpretation is raw one-coordinate spectral moments and
+`q=cos(theta)^2*sin(theta)^2`. The interpretation is NOT constructed in Lean.
+The source covariance uses the raw spectral Gram of quadratic monomials, NOT
+centered spectral covariance and NOT conditioning on the field height.
+
+Set `k4=m4-3*m2^2`. Definitions in D2Schur.lean are
+
+```
+alpha = m4 - 2*k4*q
+gamma = m2^2 + 2*k4*q
+D = m2^2*m4 + k4*(m4+m2^2)*q
+N = m2^2*(m4^2-m2^4)
+S = alpha - (gamma^3+(2*gamma+alpha)*k4^2*q*(1-4*q))/D
+Delta = m6-m4^2/m2
+T = (1-4*q)*Delta + 4*q*(Delta+9*m2*(m4-m2^2))/4
+```
+
+The first14 declarations prove identities/inequalities of these expressions.
+The last2 are positive reference and singular-boundary controls. No additional
+rejection-run count is claimed for those2 ordinary audited declarations.
+
+## Declaration-by-declaration mapping
+
+| Declaration | Statement and hypotheses |
+|---|---|
+| d2_schur_numerator | `alpha*D-gamma^3-(2gamma+alpha)*k4^2*q*(1-4q)=N`; no denominator hypothesis |
+| d2_det_axis | `D(0)=m2^2*m4` |
+| d2_det_diagonal | `D(1/4)=(m4-m2^2)*(m4+3m2^2)/4` |
+| d2_det_interpolation | D is the convex interpolation of those endpoints when q is in the intended interval; the equality holds for every real q |
+| d2_schur_ratio | `S=N/D` requires `D!=0` |
+| d2_numerator_pos | `N>0` from `m2>0` and `m4>m2^2` |
+| d2_det_pos | `D>0` from those moment conditions and `0<=q<=1/4` |
+| d2_schur_pos | `S>0` under the same conditions |
+| d2_det_le_endpoint_max | D at `0<=q<=1/4` is at most the larger endpoint, without moment positivity hypotheses |
+| d2_schur_endpoint_lower | `N/max(D(0),D(1/4))<=S` under strict moment conditions and the q interval |
+| d2_tau_cumulant_eq | The original sixth/fourth cumulant formula equals T, with `m2!=0` |
+| d2_tau_axis | `T(0)=Delta` |
+| d2_tau_diagonal | `T(1/4)=(Delta+9*m2*(m4-m2^2))/4` |
+| d2_tau_pos | T is positive from `m2>0`, `m4>m2^2`, `Delta>0`, `0<=q<=1/4` |
+| d2_gaussian_control | At `m2=1,m4=3,m6=15`, `D=3`, `S=8/3`, `T=6`, for every real q |
+| d2_degenerate_control | At `m2=m4=m6=1,q=1/4`, D=0, S=2 but N/D=0; axis T=0. The unguarded quotient identity and strict positivity at the moment boundary are false |
+
+The positive lower-bound value follows from N>0 and positive endpoint maximum;
+this is not a computation of its value for any period. Empty/nonreal/negative
+moment inputs are not silently treated as probability laws. The mathematical
+proofs are for arbitrary reals satisfying the written hypotheses; rational
+Python controls are only falsification and implementation checks.
+
+## Integration and verification
+
+The existing47 theorem proof files, gate.py, pinned Lean4.34.1, mathlib commit
+`d13f23b723b8a846827a245b89c10fc7d3f11612`, dependencies, old rejection controls,
+original archives and historical alignment records remain unchanged.
+The new16 targets extend the exact inventory to63. The predecessor weight test
+checks its original slice40:47 instead of claiming to be the terminal suffix;
+this new test checks the exact remaining suffix and exact total63. No old
+weight inequality or test case is removed. The executable gate still requires
+all declared sources/hashes and transitive axiom reports and all5 real negative
+controls. The full type log remains part of the execution evidence.
+
+```
+python -B -S -m unittest discover -s formal/tests -v
+python -B -O -S -m unittest discover -s formal/tests -v
+python -B -S formal/gate.py
+python -B -S formal/gate.py --execute
+```
+
+A source-only result does not run Lean. This author environment has no Lean
+installation and cannot resolve GitHub DNS. Hosted build/recheck/axiom/negative
+execution on the actual candidate is therefore required before a kernel claim.
+Nonauthor exact-scope review is also required, independently of execution.
+
+## Explicit exclusions and preserved obligations
+
+Not formalized: construction or covariance identification of the random field;
+actual matrix inverse/Schur complement or Gram rotation; derivation/realizability
+of the moment assumptions; `q`'s trigonometric representation; finite-L tails;
+interval arithmetic or quadrature; coefficient formula(15.2), Gamma normalization
+or lifetime laws; higher dimensions; persistence matching; CapI4 transport;
+any whole-package independent alignment or the earlier #281 lineage issue.
+The source-bound numerical implementation remains unchanged. These algebraic
+companions may assist its future review but do not retroactively validate it.
@@ -14,7 +14,7 @@ cd ..
 python formal/gate.py --execute
 ```
 
-The source-only command does not run Lean. The execute command fails unless the pinned project builds, `leanchecker` rechecks the package, all 47 declarations have transitive axiom reports restricted to propext/Classical.choice/Quot.sound, and five executable negative controls are rejected. It writes logs and a receipt in `.lake/formal-evidence/`; the workflow uploads them even on failure. A receipt from arbitrary input is not trusted evidence: use the successful read-only workflow and checked Git commit.
+The source-only command does not run Lean. The execute command fails unless the pinned project builds, `leanchecker` rechecks the package, all 63 declarations have transitive axiom reports restricted to propext/Classical.choice/Quot.sound, and five executable negative controls are rejected. It writes logs and a receipt in `.lake/formal-evidence/`; the workflow uploads them even on failure. A receipt from arbitrary input is not trusted evidence: use the successful read-only workflow and checked Git commit.
 
 Sources: [scope](SCOPE.md), [glossary](GLOSSARY.md), [manifest](manifest.json), [blueprint source](blueprint/src/content.tex). The original GP-FOR-192 bytes are preserved under originals/*.lean.txt; separately named V2 companions carry the documented compiler-only repairs in [COMPATIBILITY.md](COMPATIBILITY.md). No historical Status.lean or claimed status is imported. [Alignment contract](SCOPE.md#review-contract) remains distinct from kernel evidence.
 
@@ -47,3 +47,7 @@ The additive [WeightPerturbation](WEIGHT_PERTURBATION.md) supplies seven declara
 Read the current source-bound PR and exact head first; main #95 is historical rollout context. A non-OpenAI alignment reviewer should inspect all assumptions, the source correspondence and the explicit nonclaims. An independent engineering reviewer should attack omitted targets, imports carrying custom axioms, stale scope/hash/review records and altered toolchains. A probability formalizer should next identify the constructed weighted law with the concrete typed Palm model and discharge its same-law moment/lower-normalizer interface. Do not import GP214's upper bound as the lower bound. The MeasureBridge source is supplied but has no self-awarded kernel or alignment status. Coordinate before editing; a review request is not a claim that a reviewer is active.
 
 Blueprint declaration links are checked against the target inventory and compiled declarations, not by semantic equivalence. The full plasTeX/LaTeX website is not installed in this pilot. Optional independent checkers or AI proof generators may be added with pinned versions/budgets; their availability and execution must be separately recorded. Never treat AlphaProof as an assumed publicly callable CI service or a generator's success as an independent alignment review.
+
+## D2 Schur and endpoint positivity
+
+The additive [D2Schur](D2_SCHUR.md) supplies sixteen real-algebra declarations: exact Schur cancellation, determinant endpoint interpolation, positive conditional-expression bounds, cubic-variance cumulant conversion, and reference/singular controls. The earlier47 Lean proof bytes and the gate remain unchanged. The total inventory is63. Moment realizability, Gaussian/Palm identification and coefficient quadrature are not formalized by these conditional expressions; independent alignment remains pending.
@@ -5,3 +5,4 @@ import ResearchFormalCoreR1.WeightedLaw
 import ResearchFormalCoreR1.MomentTail
 import ResearchFormalCoreR1.MomentGenerality
 import ResearchFormalCoreR1.WeightPerturbation
+import ResearchFormalCoreR1.D2Schur
@@ -0,0 +1,169 @@
+import Mathlib.Data.Real.Basic
+import Mathlib.Tactic
+
+/-!
+# Algebraic d=2 Schur and positivity companion
+
+Dylan Roy — delegated AI work. Actual author: OpenAI / GPT-6 Astra Pro.
+Source: Math-#302 NOTE section 2 and additive identity comment 6005199919.
+These are real algebraic expressions with explicit hypotheses, not a
+construction of the Gaussian field or a proof of the coefficient integral.
+-/
+
+namespace ResearchFormalCoreR1
+
+noncomputable def d2Alpha (m2 m4 q : ℝ) : ℝ :=
+  m4 - 2 * (m4 - 3 * m2 ^ 2) * q
+
+noncomputable def d2Gamma (m2 m4 q : ℝ) : ℝ :=
+  m2 ^ 2 + 2 * (m4 - 3 * m2 ^ 2) * q
+
+noncomputable def d2DetV (m2 m4 q : ℝ) : ℝ :=
+  m2 ^ 2 * m4 + (m4 - 3 * m2 ^ 2) * (m4 + m2 ^ 2) * q
+
+noncomputable def d2Numerator (m2 m4 : ℝ) : ℝ :=
+  m2 ^ 2 * (m4 ^ 2 - m2 ^ 4)
+
+noncomputable def d2Schur (m2 m4 q : ℝ) : ℝ :=
+  d2Alpha m2 m4 q -
+    (d2Gamma m2 m4 q ^ 3 +
+      (2 * d2Gamma m2 m4 q + d2Alpha m2 m4 q) *
+        (m4 - 3 * m2 ^ 2) ^ 2 * q * (1 - 4 * q)) / d2DetV m2 m4 q
+
+noncomputable def d2Delta (m2 m4 m6 : ℝ) : ℝ := m6 - m4 ^ 2 / m2
+
+noncomputable def d2Tau (m2 m4 m6 q : ℝ) : ℝ :=
+  (1 - 4 * q) * d2Delta m2 m4 m6 +
+    4 * q * ((d2Delta m2 m4 m6 + 9 * m2 * (m4 - m2 ^ 2)) / 4)
+
+/-- Exact polynomial cancellation; it does not divide by the pin determinant. -/
+theorem d2_schur_numerator (m2 m4 q : ℝ) :
+    d2Alpha m2 m4 q * d2DetV m2 m4 q - d2Gamma m2 m4 q ^ 3 -
+      (2 * d2Gamma m2 m4 q + d2Alpha m2 m4 q) *
+        (m4 - 3 * m2 ^ 2) ^ 2 * q * (1 - 4 * q) = d2Numerator m2 m4 := by
+  unfold d2Alpha d2Gamma d2DetV d2Numerator
+  ring
+
+theorem d2_det_axis (m2 m4 : ℝ) : d2DetV m2 m4 0 = m2 ^ 2 * m4 := by
+  simp [d2DetV]
+
+theorem d2_det_diagonal (m2 m4 : ℝ) :
+    d2DetV m2 m4 (1 / 4) = (m4 - m2 ^ 2) * (m4 + 3 * m2 ^ 2) / 4 := by
+  unfold d2DetV
+  ring
+
+theorem d2_det_interpolation (m2 m4 q : ℝ) :
+    d2DetV m2 m4 q = (1 - 4 * q) * (m2 ^ 2 * m4) +
+      4 * q * ((m4 - m2 ^ 2) * (m4 + 3 * m2 ^ 2) / 4) := by
+  unfold d2DetV
+  ring
+
+/-- The nonzero hypothesis is essential even with Lean's total division. -/
+theorem d2_schur_ratio (m2 m4 q : ℝ) (hD : d2DetV m2 m4 q ≠ 0) :
+    d2Schur m2 m4 q = d2Numerator m2 m4 / d2DetV m2 m4 q := by
+  have h := d2_schur_numerator m2 m4 q
+  unfold d2Schur
+  apply (eq_div_iff hD).2
+  rw [sub_mul, div_mul_cancel₀ _ hD]
+  linarith
+
+theorem d2_numerator_pos (m2 m4 : ℝ) (hm2 : 0 < m2) (hm4 : m2 ^ 2 < m4) :
+    0 < d2Numerator m2 m4 := by
+  have hx : 0 < m2 ^ 2 := sq_pos_of_pos hm2
+  have hv : 0 < m4 - m2 ^ 2 := sub_pos.mpr hm4
+  have hs : 0 < m4 + m2 ^ 2 := by linarith
+  have he : d2Numerator m2 m4 = m2 ^ 2 * (m4 - m2 ^ 2) * (m4 + m2 ^ 2) := by
+    unfold d2Numerator
+    ring
+  rw [he]
+  exact mul_pos (mul_pos hx hv) hs
+
+theorem d2_det_pos (m2 m4 q : ℝ) (hm2 : 0 < m2) (hm4 : m2 ^ 2 < m4)
+    (hq0 : 0 ≤ q) (hq1 : q ≤ 1 / 4) : 0 < d2DetV m2 m4 q := by
+  have hx : 0 < m2 ^ 2 := sq_pos_of_pos hm2
+  have hm4pos : 0 < m4 := lt_trans hx hm4
+  have ha : 0 < m2 ^ 2 * m4 := mul_pos hx hm4pos
+  have hv : 0 < m4 - m2 ^ 2 := sub_pos.mpr hm4
+  have hs : 0 < m4 + 3 * m2 ^ 2 := by positivity
+  have hb : 0 < (m4 - m2 ^ 2) * (m4 + 3 * m2 ^ 2) / 4 := by positivity
+  rw [d2_det_interpolation]
+  by_cases hq : q = 0
+  · simpa [hq] using ha
+  · have hqp : 0 < q := lt_of_le_of_ne hq0 (Ne.symm hq)
+    have hw : 0 ≤ 1 - 4 * q := by linarith
+    exact add_pos_of_nonneg_of_pos (mul_nonneg hw ha.le) (mul_pos (by positivity) hb)
+
+theorem d2_schur_pos (m2 m4 q : ℝ) (hm2 : 0 < m2) (hm4 : m2 ^ 2 < m4)
+    (hq0 : 0 ≤ q) (hq1 : q ≤ 1 / 4) : 0 < d2Schur m2 m4 q := by
+  have hD := d2_det_pos m2 m4 q hm2 hm4 hq0 hq1
+  rw [d2_schur_ratio m2 m4 q (ne_of_gt hD)]
+  exact div_pos (d2_numerator_pos m2 m4 hm2 hm4) hD
+
+theorem d2_det_le_endpoint_max (m2 m4 q : ℝ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1 / 4) :
+    d2DetV m2 m4 q ≤
+      max (m2 ^ 2 * m4) ((m4 - m2 ^ 2) * (m4 + 3 * m2 ^ 2) / 4) := by
+  have hw : 0 ≤ 1 - 4 * q := by linarith
+  have hv : 0 ≤ 4 * q := by positivity
+  rw [d2_det_interpolation]
+  calc
+    _ ≤ (1 - 4 * q) * max (m2 ^ 2 * m4) ((m4 - m2 ^ 2) * (m4 + 3 * m2 ^ 2) / 4) +
+        4 * q * max (m2 ^ 2 * m4) ((m4 - m2 ^ 2) * (m4 + 3 * m2 ^ 2) / 4) :=
+      add_le_add (mul_le_mul_of_nonneg_left (le_max_left _ _) hw)
+        (mul_le_mul_of_nonneg_left (le_max_right _ _) hv)
+    _ = _ := by ring
+
+/-- A uniform positive lower bound on q in [0,1/4], with moment premises explicit. -/
+theorem d2_schur_endpoint_lower (m2 m4 q : ℝ) (hm2 : 0 < m2) (hm4 : m2 ^ 2 < m4)
+    (hq0 : 0 ≤ q) (hq1 : q ≤ 1 / 4) :
+    d2Numerator m2 m4 /
+        max (m2 ^ 2 * m4) ((m4 - m2 ^ 2) * (m4 + 3 * m2 ^ 2) / 4) ≤
+      d2Schur m2 m4 q := by
+  have hD := d2_det_pos m2 m4 q hm2 hm4 hq0 hq1
+  have hbound := d2_det_le_endpoint_max m2 m4 q hq0 hq1
+  have hM := lt_of_lt_of_le hD hbound
+  rw [d2_schur_ratio m2 m4 q (ne_of_gt hD)]
+  exact (div_le_div_iff₀ hM hD).2
+    (mul_le_mul_of_nonneg_left hbound (d2_numerator_pos m2 m4 hm2 hm4).le)
+
+theorem d2_tau_cumulant_eq (m2 m4 m6 q : ℝ) (hm2 : m2 ≠ 0) :
+    6 * m2 ^ 3 + 9 * m2 * (m4 - 3 * m2 ^ 2) * (1 - 2 * q) +
+      (m6 - 15 * m4 * m2 + 30 * m2 ^ 3 - (m4 - 3 * m2 ^ 2) ^ 2 / m2) *
+        (1 - 3 * q) = d2Tau m2 m4 m6 q := by
+  unfold d2Tau d2Delta
+  field_simp [hm2]
+  <;> ring
+
+theorem d2_tau_axis (m2 m4 m6 : ℝ) : d2Tau m2 m4 m6 0 = d2Delta m2 m4 m6 := by
+  simp [d2Tau]
+
+theorem d2_tau_diagonal (m2 m4 m6 : ℝ) :
+    d2Tau m2 m4 m6 (1 / 4) =
+      (d2Delta m2 m4 m6 + 9 * m2 * (m4 - m2 ^ 2)) / 4 := by
+  unfold d2Tau
+  ring
+
+theorem d2_tau_pos (m2 m4 m6 q : ℝ) (hm2 : 0 < m2) (hm4 : m2 ^ 2 < m4)
+    (hDelta : 0 < d2Delta m2 m4 m6) (hq0 : 0 ≤ q) (hq1 : q ≤ 1 / 4) :
+    0 < d2Tau m2 m4 m6 q := by
+  have hv : 0 < m4 - m2 ^ 2 := sub_pos.mpr hm4
+  have hb : 0 < (d2Delta m2 m4 m6 + 9 * m2 * (m4 - m2 ^ 2)) / 4 := by positivity
+  unfold d2Tau
+  by_cases hq : q = 0
+  · simpa [hq] using hDelta
+  · have hqp : 0 < q := lt_of_le_of_ne hq0 (Ne.symm hq)
+    have hw : 0 ≤ 1 - 4 * q := by linarith
+    exact add_pos_of_nonneg_of_pos (mul_nonneg hw hDelta.le) (mul_pos (by positivity) hb)
+
+/-- Gaussian-reference algebra, for all real q, not a probabilistic identification. -/
+theorem d2_gaussian_control (q : ℝ) :
+    d2DetV 1 3 q = 3 ∧ d2Schur 1 3 q = 8 / 3 ∧ d2Tau 1 3 15 q = 6 := by
+  norm_num [d2DetV, d2Schur, d2Alpha, d2Gamma, d2Tau, d2Delta]
+  <;> ring
+
+/-- At a singular moment boundary the unguarded quotient identity is false. -/
+theorem d2_degenerate_control :
+    d2DetV 1 1 (1 / 4) = 0 ∧ d2Schur 1 1 (1 / 4) = 2 ∧
+      d2Numerator 1 1 / d2DetV 1 1 (1 / 4) = 0 ∧ d2Tau 1 1 1 0 = 0 := by
+  norm_num [d2DetV, d2Schur, d2Alpha, d2Gamma, d2Numerator, d2Tau, d2Delta]
+
+end ResearchFormalCoreR1
@@ -99,6 +99,26 @@ proof bytes, the gate, dependency pins and historical review records remain
 unchanged. The prior withheld lineage does not become accepted through this
 extension or through successful execution; a new scoped review is required.
 
+## Additive D2 Schur and endpoint positivity (sixteen further declarations)
+
+The total is now 63 theorem targets. [D2_SCHUR.md](D2_SCHUR.md) gives the
+hash-bound declaration-by-declaration mapping. D2Schur.lean proves exact
+polynomial Schur cancellation, its quotient form only for a nonzero denominator,
+affine determinant endpoint identities, positivity and an endpoint-based lower
+bound from explicit strict moment and q-interval hypotheses, and the cubic
+variance cumulant conversion with positive-mixture consequences. Two ordinary
+audited declarations retain the Gaussian-reference and singular-moment controls.
+They are not two additional rejection runs.
+
+Earlier47 Lean proof bytes, gate.py, dependencies, the original5 executable
+negative controls and historical reviews remain unchanged. The old weight test
+continues to check its exact40:47 slice; the new test checks the exact16-target
+suffix and total63. No realizability of the raw moments, actual matrix/field
+identification, trigonometric parametrization, interval arithmetic, coefficient
+quadrature or persistence theorem is supplied. The informal numerical packet
+is unchanged. Kernel execution and a new source-specific alignment review remain
+distinct; older withheld lineage and all wider scientific obligations survive.
+
 ## Review contract
 The source manifest is an evidence sidecar, not another scientific register. A trusted successful workflow establishes kernel evidence only for these target declarations and their displayed hypotheses, relative to Lean's kernel/standard foundations/toolchain. Independent review must compare each Lean statement and definition to this scope note and the source actually cited. Review author, provider, family and agent must be explicit. Validate an authenticated record with `python formal/gate.py --alignment review.json`; then the existing controlling gate must decide whether its wider requirements are met. The validator does not authenticate a review merely because a JSON string names a reviewer.
 

@@ -56,3 +56,17 @@ \section{Same-law measure-theoretic bridge}
 \end{lemma}
 \begin{proof}Bound the numerator, derive a positive normalizer, and use
 the unchanged scalar quotient theorem.\end{proof}
+
+
+\section{D2 Schur algebra and endpoint positivity}
+\begin{lemma}[Endpoint lower bound for the conditional expression]
+\label{lem:d2-schur}
+\lean{ResearchFormalCoreR1.d2_schur_endpoint_lower}
+For the expressions defined in D2Schur, assume $m_2>0$, $m_4>m_2^2$
+and $0\le q\le1/4$. Put $N=m_2^2(m_4^2-m_2^4)$ and
+$D(q)=m_2^2m_4+(m_4-3m_2^2)(m_4+m_2^2)q$.
+Then $N/\max\{D(0),D(1/4)\}\le S(q)$, and $S(q)>0$.
+The scalar-to-Gaussian covariance identification is not formalized here.
+\end{lemma}
+\begin{proof}Cancel the Schur numerator, bound the positive affine denominator
+by its endpoint maximum, and reverse that comparison upon reciprocation.\end{proof}