L6/MT-N2: UNCOMPILED finite-measure 40th-moment companion (agent6 reviews only)

reviews/lean_cycle2_20261005/agent6/BUILD_STATUS.md

@@ -0,0 +1,17 @@
+# BUILD_STATUS — L6 / MT-N2
+
+**COMPILE_STATUS:** UNCOMPILED
+**KERNEL_CHECKED:** NO
+**PROVED_CLAIM:** NO (proposal only)
+
+Frozen Math-#275 head: `7206526ed53f7539838711ee45257a13b4b07e99`
+Lean on box: 4.34.1 (`5045d0056413266e57c625dcd7c365b10e377c52`)
+mathlib pin (package): `d13f23b723b8a846827a245b89c10fc7d3f11612`
+olean cache for MeasureTheory: ABSENT (0 oleans under shared mathlib package)
+lake build of companion: NOT EXECUTED (blocker: would require full mathlib build)
+
+No type/axiom/build log is attached because no successful (or failed) kernel
+run of this companion was produced. Do not infer success from hosted #275 CI.
+
+Blocker for integrator: run `lake build` / leanchecker on an authorized branch
+after importing this companion into the formal graph (integration owner only).

reviews/lean_cycle2_20261005/agent6/MomentTail_finite_MT_N2.lean.txt

@@ -0,0 +1,67 @@
+/- 
+L6 / MT-N2 PROPOSAL — UNCOMPILED
+Frozen Math-#275 head: 7206526ed53f7539838711ee45257a13b4b07e99
+Source ask: main#229 comment 5995761095
+Worker: Grok Bot agent 6 (non-Claude, nonauthor lane)
+Status: UNCOMPILED — not kernel-checked; do NOT treat as accepted Lean.
+Do not edit/rename the accepted theorem p02_lm009_moment40_tail.
+This file is an isolated companion proposal under reviews/ only.
+-/
+
+import ResearchFormalCoreR1.MomentTail
+
+namespace ResearchFormalCoreR1
+
+open MeasureTheory
+open scoped ENNReal
+
+set_option autoImplicit false
+
+variable {Ω : Type*} [MeasurableSpace Ω]
+
+/-- Finite-measure companion to `p02_lm009_moment40_tail` (MT-N2).
+
+Same statement and exact constant `(M / ε ^ 8) * r ^ 8`, with the same
+`Integrable (fun x => R x ^ 40) μ` premise, but the ambient measure is only
+required to be finite, not a probability measure.
+
+Rationale (from frozen #276 note MT-N2 / REVIEW.md): the proof of
+`p02_lm009_moment40_tail` invokes only `p02_lm009_markov_event`, which already
+takes `[IsFiniteMeasure μ]`, plus algebraic identities that do not use
+`μ(Ω) = 1`. The probability instance on the accepted theorem is therefore
+stronger than needed for the unweighted tail.
+
+This declaration is separately named. It does not rename, edit, or replace
+`p02_lm009_moment40_tail`. Weighted / family theorems are out of L6 scope.
+-/
+theorem p02_lm009_moment40_tail_finite
+    (μ : Measure Ω) [IsFiniteMeasure μ] (R : Ω → ℝ)
+    (r ε M : ℝ) (hr : 0 < r) (hε : 0 < ε)
+    (hRi : Integrable (fun x => R x ^ 40) μ)
+    (hMbound : (∫ x, R x ^ 40 ∂μ) ≤ M) :
+    (μ (badJetEvent R r ε)).toReal ≤ (M / ε ^ 8) * r ^ 8 := by
+  have hnonneg : 0 ≤ᵐ[μ] (fun x => R x ^ 40) := by
+    apply Filter.Eventually.of_forall
+    intro x
+    positivity
+  have ha : 0 < (ε / r) ^ 8 := pow_pos (div_pos hε hr) 8
+  calc
+    (μ (badJetEvent R r ε)).toReal ≤ (∫ x, R x ^ 40 ∂μ) / (ε / r) ^ 8 :=
+      p02_lm009_markov_event μ (fun x => R x ^ 40) (badJetEvent R r ε)
+        hRi hnonneg ((ε / r) ^ 8) ha (p02_lm009_badJet_subset R r ε hr hε)
+    _ ≤ M / (ε / r) ^ 8 := div_le_div_of_nonneg_right hMbound ha.le
+    _ = (M / ε ^ 8) * r ^ 8 := by
+      field_simp [ne_of_gt hr, ne_of_gt hε]
+
+/-- Optional specialization: the accepted probability theorem follows from the
+finite-measure companion (IsProbabilityMeasure ⇒ IsFiniteMeasure). Kept as a
+named corollary for the L6 check list; not a rewrite of the frozen module. -/
+theorem p02_lm009_moment40_tail_of_finite
+    (μ : Measure Ω) [IsProbabilityMeasure μ] (R : Ω → ℝ)
+    (r ε M : ℝ) (hr : 0 < r) (hε : 0 < ε)
+    (hRi : Integrable (fun x => R x ^ 40) μ)
+    (hMbound : (∫ x, R x ^ 40 ∂μ) ≤ M) :
+    (μ (badJetEvent R r ε)).toReal ≤ (M / ε ^ 8) * r ^ 8 :=
+  p02_lm009_moment40_tail_finite μ R r ε M hr hε hRi hMbound
+
+end ResearchFormalCoreR1

reviews/lean_cycle2_20261005/agent6/NOTES_MT_N2.md

@@ -0,0 +1,72 @@
+# L6 / MT-N2 — finite-measure 40th-moment tail companion
+
+**Status:** UNCOMPILED proposal (`.lean.txt`). Scientific effect **NONE**.
+**Worker:** Grok Bot agent 6 (Grok Bot support agent; non-Claude, nonauthor lane)
+**Pickup:** main#229 [5996213216](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-5996213216)
+**Readback:** [5996215908](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-5996215908)
+**Ask:** [5995761095](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-5995761095)
+**Frozen head used:** `7206526ed53f7539838711ee45257a13b4b07e99` (Math-#275 live head)
+**Alignment note:** #276 REVIEW.md §MT-N2 at `reviews/moment_tail_alignment_20261005/` (head `3718fc1564c537971636a3f4091224964e20f9f9`)
+
+## What changed (proposal only)
+
+| Item | Accepted (frozen) | L6 companion |
+|---|---|---|
+| Name | `p02_lm009_moment40_tail` | `p02_lm009_moment40_tail_finite` (new) |
+| Measure hypothesis | `[IsProbabilityMeasure μ]` | `[IsFiniteMeasure μ]` |
+| Constant | `(M / ε ^ 8) * r ^ 8` | **exact same** |
+| Integrable premise | `Integrable (fun x => R x ^ 40) μ` | **exact same** |
+| Proof body | Markov via `p02_lm009_markov_event` + field_simp | **same steps** (that lemma already needs finite measure) |
+
+No edit/rename of the accepted theorem. No weighted/family theorems. No formal-source / manifest / workflow edits on this lane.
+
+## Why this is a real relaxation (not wording)
+
+`p02_lm009_markov_event` already assumes `[IsFiniteMeasure μ]`. The unweighted tail proof never uses `μ(Ω) = 1`, renormalization, or any probability-only identity. Requiring `IsProbabilityMeasure` therefore excludes legitimate finite measures of mass ≠ 1 that still satisfy the same Markov arithmetic.
+
+## Explicit finite-measure checks (analytic / finite-model; not Lean kernel)
+
+### Mass = 2
+
+Ω = {*}, μ = 2 · Dirac(*), R(*) = 2, r = ε = 1.
+badJetEvent = Ω, μ(A) = 2. ∫ R^40 dμ = 2 · 2^40. With M = ∫, RHS = M. Markov at threshold (ε/r)^8 = 1 gives μ(A) ≤ ∫ = 2·2^40 (true). Mass-2 scales both sides; probability instance not required.
+
+### Mass = 1/2
+
+Same singleton, μ = (1/2) · Dirac(*), R(*) = 2, r = ε = 1.
+μ(A) = 1/2, ∫ R^40 = (1/2)·2^40. With M = ∫, RHS = M ≥ μ(A). Finite-measure Markov applies; no μ(Ω) normalization.
+
+### Strict event / boundary
+
+badJetEvent is `{ε < r R^5}` (strict). Equality ε = r R^5 is outside the event. Subset weakens to ≤ on the 40th-power threshold. Matches frozen `test_strict_boundary_and_signed_jet`.
+
+### Zero / null cases
+
+- Empty A ⇒ μ(A)=0 ≤ RHS whenever hypotheses hold.
+- Null sets do not affect Bochner ∫ or a.e. nonnegativity of R^40.
+- Zero measure μ ≡ 0 is finite: both sides 0 when Integrable and M ≥ 0.
+
+### Signed R
+
+On the event, R^5 > ε/r > 0. R^40 ≥ 0 globally. No global sign hypothesis.
+
+## Compile / toolchain honesty
+
+| Probe | Result |
+|---|---|
+| Lean on box | 4.34.1 (`5045d005…`) |
+| mathlib pin | `d13f23b723b8…` |
+| Shared mathlib oleans | **0** |
+| lake build of companion | **NOT EXECUTED** |
+
+**Verdict:** UNCOMPILED `.lean.txt`. Proof-containing text ≠ accepted Lean. Do not cite #275 CI as kernel evidence for this companion.
+
+## Out of scope (respected)
+
+formal-source / manifest / workflow edits; merges; flag flips; weighted/family (L7); SoT invention; OBL stays OPEN.
+
+## Files
+
+- `MomentTail_finite_MT_N2.lean.txt` — proposed companion (UNCOMPILED)
+- `NOTES_MT_N2.md` — this file
+- `BUILD_STATUS.md` — compact compile status receipt