d6g8k5htny-coder · Oct 5, 2026 · Oct 5, 2026 · Oct 5, 2026
@@ -0,0 +1,90 @@
+# Finite-measure and interval-only companions
+
+Scientific effect: NONE. Executable adaptation, tests and packaging: Dylan Roy —
+delegated AI work; actual performer OpenAI / GPT-6 Astra Pro, 2026-10-05.
+Proposal contributors: Grok Bot agents 6 (L6 / MT-N2) and 7 (L7 / MT-N1).
+Their underlying providers/models are not established by their role labels.
+Source progress is proof supplied; only an exact execution receipt establishes
+kernel evidence. Source-to-statement alignment requires a separate actual review.
+
+## Consumed sources and authorship
+
+All references below are in `d6g8k5htny-coder/Math-`.
+
+- Integration base: `a44db48f10ea27c93595840118457a39a5bbbea4`.
+- Retained `formal/ResearchFormalCoreR1/MomentTail.lean`: SHA256
+  `87fe3ee90afc52d8c2652881f1ae195d1b0b15a2ffc18c84d6166d1a4d0de2aa`.
+- Audit motivating the two generalizations: #276,
+  `reviews/moment_tail_alignment_20261005/REVIEW.md` at
+  `0cb17c1b836651144486d55788eef8d7cf532081`, notes MT-N1 and MT-N2.
+- Agent 6 proposal, #277 at `d1267a6106e8180eeb75fa008ce09de9ad8065ca`:
+  `reviews/lean_cycle2_20261005/agent6/MomentTail_finite_MT_N2.lean.txt`.
+- Agent 7 proposal, #278 at `cf58e5b812699cd7016441c0b477b86fecb7017f`:
+  `reviews/lean_cycle2_20261005/agent7/MomentTail_family_interval_MT_N1.lean.txt`.
+
+Those immutable proposal files remain UNCOMPILED historical proposals; their PR
+checks do not compile text files. This new module preserves all four proposed
+theorem types and the first three proofs, apart from comments/packaging. The final
+specialization proof uses a direct conjunction pair instead of repeatedly
+projecting and reconstructing the same hypothesis tuple. No original source or
+proposal is overwritten, and no contributor is silently relabeled as OpenAI.
+
+## Exact four-target extension: 36 to 40
+
+All names below are in `ResearchFormalCoreR1`.
+
+| Target | Exact conclusion and retained requirements |
+|---|---|
+| `p02_lm009_moment40_tail_finite` | For a finite measure, positive r and epsilon, integrable R^40 and its integral bounded by M, the real mass of `{epsilon < r R^5}` is at most `(M/epsilon^8)r^8`. |
+| `p02_lm009_moment40_tail_of_finite` | Recovers the probability-measure version as a specialization of the finite-measure companion. |
+| `p02_lm009_moment40_family_r3_interval` | Produces one nonnegative C for every 0<r<=r0, assuming probability and all moment/normalizer hypotheses only on that interval. The constant is chosen before r. |
+| `p02_lm009_moment40_family_r3_of_interval` | Recovers the earlier globally-probability family interface from the interval-only theorem. |
+
+The finite-measure statement is about MASS, not normalized probability. There is
+no division by total measure mass, and event masses may exceed one. The zero
+measure is allowed. Signed R, strict threshold boundaries, and null atoms are
+retained. Integrability is explicit; no divergent totalized integral is used.
+The ambient measure is finite, not arbitrary or merely sigma-finite.
+
+The interval theorem assumes 0<r0<=1, positive epsilon and cZ, nonnegative M and
+cW, and for each 0<r<=r0: probability of mu_r, nonnegative L2 weight W_r,
+measurable R_r, integrable R_r^40, its integral <=M, weight second moment
+<=cW*r^4, and the LOWER normalizer cZ*r^2<=integral W_r. It concludes the
+weighted-law probability property and the cubic bound, with witness
+
+    C = (sqrt(cW)/cZ) * sqrt(M/epsilon^8).
+
+All constants are outside the r quantifier. Mu_r can be the zero measure outside
+the interval. The two specialization targets deliberately have the old stronger
+premises; they show compatibility, not two further generalizations. No theorem
+asserts that every pointwise collection of constants admits one uniform constant.
+
+## Nonclaims and review boundaries
+
+No concrete Gaussian/typed Palm model, supremum moment, lower normalizer, global
+good-event complement, P0.2 or parent persistence theorem is proved. The earlier
+36 source theorem statements/proofs and their scope notes remain unchanged.
+MT-N1/N2 remain accurate descriptions of the earlier theorem types; only the new
+companions remove those restrictions. This is not a theorem-wide acceptance.
+
+A reviewer must compare these exact statements to the two original proposals and
+the retained formal sources, disclose actual lineage and any proposer exposure,
+and distinguish new execution evidence from prior 36-target acceptance. Unknown
+proposal-provider identity does not create cross-provider or organizational
+independence. Full-package alignment must be explicit, not a relabeled old JSON.
+
+## Tests and execution contract
+
+Twelve focused standard-library Python tests include 729 rational finite-measure
+cases (total mass 0, 1/2 and 2), scaling, strict/signed/null edges, a countermodel
+to extra normalization, an interval family that is zero outside its domain, and
+a diagnostic for r-dependent transfer constants. These are source-wiring and
+finite-model checks, not kernel proofs or a formalization of the test models.
+
+The previous moment-tail inventory test now binds its exact retained 29:36 slice;
+the new test binds the exact 36:40 extension and total 40. The unchanged gate
+independently checks the complete declaration inventory, builds and rechecks the
+package, extracts all target types and transitive axioms, and runs the same five
+rejection controls. Lean 4.34.1, mathlib
+`d13f23b723b8a846827a245b89c10fc7d3f11612`, dependency pins, workflows and scientific
+registers are unchanged. Source-only tests do not imply Lean execution.
@@ -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 36 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 40 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.
 
@@ -34,6 +34,10 @@ The additive [WeightedLaw](WEIGHTED_LAW.md) contributes nine declarations. It co
 
 The additive [MomentTail](MOMENT_TAIL.md) contributes seven declarations. It proves the actual Markov step from an integrable fortieth-moment bound to the strict fifth-power event's eighth-order probability bound, then the constructed weighted law's fourth-order and cubic bounds. A family theorem supplies one constant only when the model premises are explicitly uniform. Concrete Gaussian/Palm moments and normalizers are not proved by this implication.
 
+## Generality companions
+
+The additive [MomentGenerality](MOMENT_GENERALITY.md) registers the agent 6/7 proposal adaptations: finite-measure unweighted tail and interval-only probability-family assembly, plus two specialization bridges. It preserves the exact tail constant and all concrete model hypotheses. Earlier proof bytes and the verification gate remain unchanged; the two proposal PRs are not themselves compiled evidence.
+
 ## Next agents
 
 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.

@@ -3,3 +3,4 @@ import ResearchFormalCoreR1.ProbabilityCompanionsV2
 import ResearchFormalCoreR1.MeasureBridge
 import ResearchFormalCoreR1.WeightedLaw
 import ResearchFormalCoreR1.MomentTail
+import ResearchFormalCoreR1.MomentGenerality
@@ -0,0 +1,95 @@
+import ResearchFormalCoreR1.MomentTail
+
+/-!
+# Finite-measure and interval-only moment-tail companions
+
+Executable adaptation by OpenAI / GPT-6 Astra Pro of the separately attributed
+Grok Bot agent 6 and agent 7 proposals in Math-#277/#278. Their underlying model
+providers are not inferred from their role labels. See ../MOMENT_GENERALITY.md.
+The original 36 theorem statements and proofs are unchanged.
+-/
+
+namespace ResearchFormalCoreR1
+
+open MeasureTheory
+open scoped ENNReal
+
+set_option autoImplicit false
+
+variable {Ω : Type*} [MeasurableSpace Ω]
+
+/-- The fortieth-moment event bound for any finite measure. The event mass is
+not normalized by the total mass; both sides scale with the ambient measure. -/
+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ε]
+
+/-- The original probability-space conclusion specializes from the finite
+measure companion. This does not replace or edit the original declaration. -/
+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
+
+/-- One fixed cubic constant, with probability and all model bounds required
+only on 0 < r ≤ r0. No probability assumption is made outside that interval. -/
+theorem p02_lm009_moment40_family_r3_interval
+    (μ : ℝ → Measure Ω)
+    (W R : ℝ → Ω → ℝ) (r0 ε M cW cZ : ℝ)
+    (hr0 : 0 < r0 ∧ r0 ≤ 1) (hε : 0 < ε)
+    (hM : 0 ≤ M) (hcW : 0 ≤ cW) (hcZ : 0 < cZ)
+    (hdata : ∀ r, 0 < r → r ≤ r0 →
+      IsProbabilityMeasure (μ r) ∧
+      MemLp (W r) 2 (μ r) ∧ (0 ≤ᵐ[μ r] W r) ∧ Measurable (R r) ∧
+      Integrable (fun x => R r x ^ 40) (μ r) ∧
+      (∫ x, R r x ^ 40 ∂(μ r)) ≤ M ∧
+      (∫ x, W r x ^ 2 ∂(μ r)) ≤ cW * r ^ 4 ∧
+      cZ * r ^ 2 ≤ ∫ x, W r x ∂(μ r)) :
+    ∃ C : ℝ, 0 ≤ C ∧ ∀ r, 0 < r → r ≤ r0 →
+      IsProbabilityMeasure (weightedLaw (μ r) (W r)) ∧
+      (weightedLaw (μ r) (W r) (badJetEvent (R r) r ε)).toReal ≤ C * r ^ 3 := by
+  refine ⟨(Real.sqrt cW / cZ) * Real.sqrt (M / ε ^ 8), by positivity, ?_⟩
+  intro r hr hrr0
+  obtain ⟨hProb, hW, hW0, hR, hRi, hMb, hsecond, hlower⟩ := hdata r hr hrr0
+  letI : IsProbabilityMeasure (μ r) := hProb
+  exact p02_lm009_moment40_weighted_r3 (μ r) (W r) (R r) hW hW0 hR
+    r ε M cW cZ hr (hrr0.trans hr0.2) hε hM hcW hcZ hRi hMb hsecond hlower
+
+/-- A globally supplied probability family is a specialization of the interval
+version, so the previous interface is retained without changing its source. -/
+theorem p02_lm009_moment40_family_r3_of_interval
+    (μ : ℝ → Measure Ω) [∀ r, IsProbabilityMeasure (μ r)]
+    (W R : ℝ → Ω → ℝ) (r0 ε M cW cZ : ℝ)
+    (hr0 : 0 < r0 ∧ r0 ≤ 1) (hε : 0 < ε)
+    (hM : 0 ≤ M) (hcW : 0 ≤ cW) (hcZ : 0 < cZ)
+    (hdata : ∀ r, 0 < r → r ≤ r0 →
+      MemLp (W r) 2 (μ r) ∧ (0 ≤ᵐ[μ r] W r) ∧ Measurable (R r) ∧
+      Integrable (fun x => R r x ^ 40) (μ r) ∧
+      (∫ x, R r x ^ 40 ∂(μ r)) ≤ M ∧
+      (∫ x, W r x ^ 2 ∂(μ r)) ≤ cW * r ^ 4 ∧
+      cZ * r ^ 2 ≤ ∫ x, W r x ∂(μ r)) :
+    ∃ C : ℝ, 0 ≤ C ∧ ∀ r, 0 < r → r ≤ r0 →
+      IsProbabilityMeasure (weightedLaw (μ r) (W r)) ∧
+      (weightedLaw (μ r) (W r) (badJetEvent (R r) r ε)).toReal ≤ C * r ^ 3 :=
+  p02_lm009_moment40_family_r3_interval μ W R r0 ε M cW cZ hr0 hε hM hcW hcZ
+    (fun r hr hrr0 => ⟨inferInstance, hdata r hr hrr0⟩)
+
+end ResearchFormalCoreR1
@@ -57,7 +57,7 @@ No existing review is silently rebound to the changed manifest or scope.
 
 ## Additive moment-to-tail composition (seven further declarations)
 
-The current total is 36 theorem targets. [MOMENT_TAIL.md](MOMENT_TAIL.md) is the
+This retained layer has 36 theorem targets. [MOMENT_TAIL.md](MOMENT_TAIL.md) is the
 hash-bound scope for `MomentTail.lean`: actual finite-measure Markov inequality,
 strict-event measurability/threshold inclusion, the fortieth-moment-to-eighth-order
 event tail, fourth-order and cubic weighted probability bounds, and an explicit
@@ -69,6 +69,19 @@ parent theorem is established. All earlier29 proof bytes, the executable gate
 and its five rejection controls are unchanged. Existing package-level alignment
 records do not automatically cover these new targets or changed scope.
 
+## Additive generality companions (four further declarations)
+
+The total is now 40 theorem targets. [MOMENT_GENERALITY.md](MOMENT_GENERALITY.md)
+binds the exact scope and contributor/source identities for `MomentGenerality.lean`.
+The finite-measure fortieth-moment tail keeps the exact `(M/epsilon^8)r^8`
+constant, with no normalization by total mass. The interval-only family requires
+probability and all fixed model bounds only for 0<r<=r0, not for every real r.
+Two specialization declarations recover the earlier probability/global-instance
+interfaces. The earlier 36 proof bytes and their stronger types remain unchanged.
+No concrete model moment, Palm identification, lower normalizer or uniform bound
+is supplied; all corresponding assumptions remain explicit. The old 36-target
+alignment does not cover this changed manifest/scope without a new review.
+
 ## 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.
 

@@ -24,7 +24,8 @@
     "ResearchFormalCoreR1/ProbabilityCompanionsV2.lean",
     "ResearchFormalCoreR1/MeasureBridge.lean",
     "ResearchFormalCoreR1/WeightedLaw.lean",
-    "ResearchFormalCoreR1/MomentTail.lean"
+    "ResearchFormalCoreR1/MomentTail.lean",
+    "ResearchFormalCoreR1/MomentGenerality.lean"
   ],
   "targets": [
     "ResearchFormalCoreR1.ec005_fold_gap",
@@ -62,17 +63,21 @@
     "ResearchFormalCoreR1.p02_lm009_moment40_tail",
     "ResearchFormalCoreR1.p02_lm009_moment40_weighted_r4",
     "ResearchFormalCoreR1.p02_lm009_moment40_weighted_r3",
-    "ResearchFormalCoreR1.p02_lm009_moment40_family_r3"
+    "ResearchFormalCoreR1.p02_lm009_moment40_family_r3",
+    "ResearchFormalCoreR1.p02_lm009_moment40_tail_finite",
+    "ResearchFormalCoreR1.p02_lm009_moment40_tail_of_finite",
+    "ResearchFormalCoreR1.p02_lm009_moment40_family_r3_interval",
+    "ResearchFormalCoreR1.p02_lm009_moment40_family_r3_of_interval"
   ],
   "files": {
     ".gitignore": "b34af236d1df9e39ed4f98fca51702530ce76bdee4e1a69512f6caed933c3374",
     "COMPATIBILITY.md": "33721aad32f82131a6956a06b58c5bc41f5d28f26efe840a99a4d51ad60cf247",
     "GLOSSARY.md": "6bdda2ce054915efc26e8db462dbe8fd9d0c1db30e02328857bebc6568e05ce9",
-    "README.md": "dec5318053317dde0f0b1158d1359804a64d23b72199a4fc0e8dd89d33fb1d02",
+    "README.md": "35f4aab13f9dc69c0810d7fcd16d9e13bf03f41e227423e9e254983978fa2b08",
     "ResearchFormalCoreR1/AlgebraV2.lean": "4480708263c40a2f7f03f12ef7e15f0eb4f8193c2dccbb253921a7ec251863c3",
     "ResearchFormalCoreR1/ProbabilityCompanionsV2.lean": "338452a0c2ba24d016059354d543cc995b8cb29c9d4a41d98bb93499f5f8cb8f",
-    "ResearchFormalCoreR1.lean": "ffe0de34c8d3830357d6952d150a21ff12cef27e750cde8950362b92b4f285fb",
-    "SCOPE.md": "21c4ce34ff1e7536c88de86661c796a0751ad8572b034650631052ad0791f4a1",
+    "ResearchFormalCoreR1.lean": "bfb77a7b6c3d7cbd550ddcbac3842a5581f28c0ae68f861c795bf5f715fabb30",
+    "SCOPE.md": "198bbc6c60fdb9148ae21c0f25b52d3b612de20c373dc1e6df818767987da452",
     "blueprint/src/content.tex": "e00ee78344ed27c097bccb8c6360f6bb86a223ab06319a407de2dd0104fd2e28",
     "evidence/initial-build-failure.log": "43393d2e2b3148a2453e3092a1ff04e257dbd4a6dc97eb2853a8bc0451002591",
     "gate.py": "958b149ea3a4ce735644a2079f817b5deddf5dc0d5ca347904ad09db6ad47d68",
@@ -90,8 +95,11 @@
     "tests/test_weighted_law.py": "e4cb5f2cdc58ac1e3af09b548c6dbb24ff3f060a101636589d2db994c0d66b94",
     "ResearchFormalCoreR1/MomentTail.lean": "87fe3ee90afc52d8c2652881f1ae195d1b0b15a2ffc18c84d6166d1a4d0de2aa",
     "MOMENT_TAIL.md": "20ecddcd830c41935dc4b366882db4d0432240932af6632d025b981f90e044bd",
-    "tests/test_moment_tail.py": "d5cafe83b3d7afa575cc521e7b6617b4535af217ecab02316307eebbe28a175a",
+    "tests/test_moment_tail.py": "4019207cb4df25f5776856e348ca1eba2d96ade955aef9df60ccd99204ed82b0",
     "evidence/moment-tail-initial-build-failure.log": "61bee2d55d0dd548b0bccc4d2e40970f654fca8ab1385af7f371592d45c0ab08",
+    "ResearchFormalCoreR1/MomentGenerality.lean": "fdec55f1602938cd8fdb5b71535962e76a9671bf230dea53868b14147fb3b509",
+    "MOMENT_GENERALITY.md": "5386c763f95ecd0946e0f23a22d1ba90e7956ff1a1bfcada0d454d1b5ace0cf2",
+    "tests/test_moment_generality.py": "7cd25876b9b0f4ed46168e4cf493030470cd7300d6ff06b9d242642eb9659a17",
     "tests/test_alignment_lineage.py": "c510c6566d7689bebde76843582e9936dfa9e62e783b816b5e4f63d83434b893",
     "LINEAGE_VALIDATION.md": "bba9d0a859f1ba45670fe122e4e72ae1094a2226de98aa814d838b0baaf61815"
   }