Lean: quantitative squared-radius mass to actual moment and Schur floors

.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

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

companions/d2_atom_integral_20261006/D2AtomIntegral.lean

@@ -0,0 +1,149 @@
+import D2MomentBridge
+import D2SquareSchur
+import Mathlib.MeasureTheory.Integral.Bochner.Set
+
+/-!
+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

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.