diff --git a/reviews/lean_cycle2_20261005/agent6/BUILD_STATUS.md b/reviews/lean_cycle2_20261005/agent6/BUILD_STATUS.md new file mode 100644 index 000000000..a6960b05c --- /dev/null +++ b/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). diff --git a/reviews/lean_cycle2_20261005/agent6/MomentTail_finite_MT_N2.lean.txt b/reviews/lean_cycle2_20261005/agent6/MomentTail_finite_MT_N2.lean.txt new file mode 100644 index 000000000..7c9278baa --- /dev/null +++ b/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 diff --git a/reviews/lean_cycle2_20261005/agent6/NOTES_MT_N2.md b/reviews/lean_cycle2_20261005/agent6/NOTES_MT_N2.md new file mode 100644 index 000000000..a408e765a --- /dev/null +++ b/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