Lean: same-law weight perturbation and stable normalization

formal/README.md

@@ -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 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.
+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.
 
 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.
 
@@ -38,6 +38,10 @@ The additive [MomentTail](MOMENT_TAIL.md) contributes seven declarations. It pro
 
 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.
 
+## Weight perturbation and stable normalization
+
+The additive [WeightPerturbation](WEIGHT_PERTURBATION.md) supplies seven declarations. A positive reference normalizer and a same-law L1 weight-error budget yield a positive perturbed normalizer and a uniform bound on measurable-event probabilities. Its r² specialization cancels the common vanishing scale. Concrete field error estimates, reference lower bounds and any common-law identification remain premises; earlier forty proof bytes and the hardened gate stay unchanged.
+
 ## 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.

formal/ResearchFormalCoreR1.lean

@@ -4,3 +4,4 @@ import ResearchFormalCoreR1.MeasureBridge
 import ResearchFormalCoreR1.WeightedLaw
 import ResearchFormalCoreR1.MomentTail
 import ResearchFormalCoreR1.MomentGenerality
+import ResearchFormalCoreR1.WeightPerturbation

formal/ResearchFormalCoreR1/WeightPerturbation.lean

@@ -0,0 +1,141 @@
+import ResearchFormalCoreR1.WeightedLaw
+
+/-!
+# Same-law stability of normalized nonnegative weights
+
+An actual L1 error controls the normalizer and every measurable-event probability.
+The reference lower bound and the concrete L1 estimate remain premises. Both
+weights use the same underlying measure. See ../WEIGHT_PERTURBATION.md.
+-/
+
+namespace ResearchFormalCoreR1
+
+open MeasureTheory
+open scoped ENNReal
+
+set_option autoImplicit false
+
+variable {Ω : Type*} [MeasurableSpace Ω]
+
+/-- Integrability, not a totalized divergent integral, justifies subtraction. -/
+theorem weightPerturbation_integral
+    (μ : Measure Ω) (W V : Ω → ℝ) (hW : Integrable W μ) (hV : Integrable V μ) :
+    |(∫ x, W x ∂μ) - (∫ x, V x ∂μ)| ≤ ∫ x, |W x - V x| ∂μ := by
+  rw [← integral_sub hW hV]
+  exact abs_integral_le_integral_abs
+
+/-- Restricting to any set cannot increase the integral absolute error. The
+probability formula below separately requires measurable events. -/
+theorem weightPerturbation_setIntegral
+    (μ : Measure Ω) (W V : Ω → ℝ) (A : Set Ω)
+    (hW : Integrable W μ) (hV : Integrable V μ) :
+    |(∫ x in A, W x ∂μ) - (∫ x in A, V x ∂μ)| ≤ ∫ x, |W x - V x| ∂μ := by
+  exact (weightPerturbation_integral (μ.restrict A) W V
+    hW.integrableOn hV.integrableOn).trans
+    (setIntegral_le_integral (hW.sub hV).abs
+      (Filter.Eventually.of_forall (fun x => abs_nonneg (W x - V x))))
+
+/-- A reference normalizer lower bound loses at most the supplied L1 budget. -/
+theorem weightPerturbation_normalizer_lower
+    (μ : Measure Ω) (W V : Ω → ℝ) (hW : Integrable W μ) (hV : Integrable V μ)
+    (c δ : ℝ) (hreference : c ≤ ∫ x, V x ∂μ)
+    (herror : (∫ x, |W x - V x| ∂μ) ≤ δ) :
+    c - δ ≤ ∫ x, W x ∂μ := by
+  have h := (abs_le.mp ((weightPerturbation_integral μ W V hW hV).trans herror)).1
+  linarith
+
+/-- A nonnegative event numerator lies between zero and its own normalizer. -/
+theorem weightPerturbation_event_integral_bounds
+    (μ : Measure Ω) (W : Ω → ℝ) (A : Set Ω)
+    (hW : Integrable W μ) (hW0 : 0 ≤ᵐ[μ] W) :
+    0 ≤ (∫ x in A, W x ∂μ) ∧ (∫ x in A, W x ∂μ) ≤ ∫ x, W x ∂μ := by
+  exact ⟨integral_nonneg_of_ae (ae_restrict_of_ae hW0),
+    setIntegral_le_integral hW hW0⟩
+
+/-- Scalar ratio stability with the reference denominator t. The factor 2 is
+convenient, not claimed optimal. No sign premise on b is needed for this lemma. -/
+theorem weightPerturbation_quotient_bound
+    (a b z t δ : ℝ) (hz : 0 < z) (ht : 0 < t)
+    (ha : 0 ≤ a) (haz : a ≤ z) (hab : |a - b| ≤ δ) (hzt : |z - t| ≤ δ) :
+    |a / z - b / t| ≤ 2 * δ / t := by
+  have hfrac0 : 0 ≤ a / z := div_nonneg ha hz.le
+  have hfrac1 : a / z ≤ 1 := (div_le_one hz).2 haz
+  have hgap : |t - z| ≤ δ := by
+    rw [abs_sub_comm]
+    exact hzt
+  have hprod : |a / z| * |t - z| ≤ δ := by
+    rw [abs_of_nonneg hfrac0]
+    calc
+      (a / z) * |t - z| ≤ 1 * |t - z| :=
+        mul_le_mul_of_nonneg_right hfrac1 (abs_nonneg _)
+      _ ≤ δ := by simpa only [one_mul] using hgap
+  have heq : a / z - b / t = ((a - b) + (a / z) * (t - z)) / t := by
+    field_simp [ne_of_gt hz, ne_of_gt ht] <;> ring
+  calc
+    |a / z - b / t| = |(a - b) + (a / z) * (t - z)| / t := by
+      rw [heq, abs_div, abs_of_pos ht]
+    _ ≤ (|a - b| + |(a / z) * (t - z)|) / t :=
+      div_le_div_of_nonneg_right (abs_add_le _ _) ht.le
+    _ ≤ (δ + δ) / t := by
+      apply div_le_div_of_nonneg_right _ ht.le
+      rw [abs_mul]
+      exact add_le_add hab hprod
+    _ = 2 * δ / t := by ring
+
+/-- Under one common measure, a small L1 weight error transfers a positive
+reference normalizer to W and controls all measurable-event probabilities.
+The ambient measure need not be finite or a probability measure. -/
+theorem weightedLaw_event_perturbation
+    (μ : Measure Ω) (W V : Ω → ℝ) (hW : Integrable W μ) (hV : Integrable V μ)
+    (hW0 : 0 ≤ᵐ[μ] W) (hV0 : 0 ≤ᵐ[μ] V)
+    (c δ : ℝ) (hc : 0 < c) (hreference : c ≤ ∫ x, V x ∂μ)
+    (herror : (∫ x, |W x - V x| ∂μ) ≤ δ) (hsmall : δ ≤ c / 2) :
+    c / 2 ≤ (∫ x, W x ∂μ) ∧
+      IsProbabilityMeasure (weightedLaw μ W) ∧
+      IsProbabilityMeasure (weightedLaw μ V) ∧
+      ∀ A : Set Ω, MeasurableSet A →
+        |(weightedLaw μ W A).toReal - (weightedLaw μ V A).toReal| ≤ 2 * δ / c := by
+  have hL1nonneg : 0 ≤ ∫ x, |W x - V x| ∂μ :=
+    integral_nonneg (fun x => abs_nonneg (W x - V x))
+  have hδ0 : 0 ≤ δ := hL1nonneg.trans herror
+  have hlower := weightPerturbation_normalizer_lower μ W V hW hV c δ hreference herror
+  have hz : 0 < ∫ x, W x ∂μ := by linarith
+  have ht : 0 < ∫ x, V x ∂μ := lt_of_lt_of_le hc hreference
+  refine ⟨by linarith, weightedLaw_isProbabilityMeasure μ W hW hW0 hz,
+    weightedLaw_isProbabilityMeasure μ V hV hV0 ht, ?_⟩
+  intro A hA
+  rw [weightedLaw_event_real μ W A hW hW0 hA hz,
+    weightedLaw_event_real μ V A hV hV0 hA ht]
+  have hb := weightPerturbation_event_integral_bounds μ W A hW hW0
+  exact (weightPerturbation_quotient_bound _ _ _ _ δ hz ht hb.1 hb.2
+    ((weightPerturbation_setIntegral μ W V A hW hV).trans herror)
+    ((weightPerturbation_integral μ W V hW hV).trans herror)).trans
+      (div_le_div_of_nonneg_left (mul_nonneg (by norm_num) hδ0) hc hreference)
+
+/-- The natural r² normalizer and L1-error scales cancel. No r ≤ 1 restriction
+is needed. Uniform application requires uniform c and the displayed budgets. -/
+theorem weightedLaw_event_perturbation_r2
+    (μ : Measure Ω) (W V : Ω → ℝ) (hW : Integrable W μ) (hV : Integrable V μ)
+    (hW0 : 0 ≤ᵐ[μ] W) (hV0 : 0 ≤ᵐ[μ] V)
+    (r c η : ℝ) (hr : 0 < r) (hc : 0 < c)
+    (hreference : c * r ^ 2 ≤ ∫ x, V x ∂μ)
+    (herror : (∫ x, |W x - V x| ∂μ) ≤ η * r ^ 2) (hsmall : η ≤ c / 2) :
+    (c * r ^ 2) / 2 ≤ (∫ x, W x ∂μ) ∧
+      IsProbabilityMeasure (weightedLaw μ W) ∧
+      IsProbabilityMeasure (weightedLaw μ V) ∧
+      ∀ A : Set Ω, MeasurableSet A →
+        |(weightedLaw μ W A).toReal - (weightedLaw μ V A).toReal| ≤ 2 * η / c := by
+  have hs : η * r ^ 2 ≤ (c * r ^ 2) / 2 := by
+    calc
+      η * r ^ 2 ≤ (c / 2) * r ^ 2 :=
+        mul_le_mul_of_nonneg_right hsmall (sq_nonneg r)
+      _ = (c * r ^ 2) / 2 := by ring
+  obtain ⟨hlower, hpW, hpV, hA⟩ := weightedLaw_event_perturbation μ W V hW hV hW0 hV0
+    (c * r ^ 2) (η * r ^ 2) (mul_pos hc (sq_pos_of_pos hr)) hreference herror hs
+  refine ⟨hlower, hpW, hpV, ?_⟩
+  intro A hmeas
+  have heq : 2 * (η * r ^ 2) / (c * r ^ 2) = 2 * η / c := by
+    field_simp [ne_of_gt hr, ne_of_gt hc]
+  simpa only [heq] using hA A hmeas
+
+end ResearchFormalCoreR1

formal/SCOPE.md

@@ -71,7 +71,7 @@ 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)
+This retained layer has 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
@@ -82,6 +82,23 @@ 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.
 
+## Additive same-law weight perturbation (seven further declarations)
+
+The total is now 47 theorem targets. [WEIGHT_PERTURBATION.md](WEIGHT_PERTURBATION.md)
+binds the new WeightPerturbation module's exact seven-target scope. Genuine L1
+weight error controls ordinary/set integral differences; a reference lower
+normalizer loses at most that error. Under a common measure and nonnegative
+integrable weights, reference integral >= c > 0 and error <= delta <= c/2 give
+perturbed integral >= c/2, both probability properties, and every measurable-event
+probability error <= 2delta/c. The r^2-scaled version gives 2eta/c from error
+<= eta*r^2 and reference integral >= c*r^2. The constant is not claimed optimal.
+
+No underlying measure transfer, concrete field estimate, reference normalizer
+floor, asymptotic convergence or parent theorem is established. Earlier forty
+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.
+
 ## 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.
 

formal/WEIGHT_PERTURBATION.md

@@ -0,0 +1,101 @@
+# Same-law weight perturbation and stable normalization
+
+Scientific effect: NONE. Dylan Roy — delegated AI work. New proof author and
+implementer: OpenAI / GPT-6 Astra Pro, session `lean-weight-perturbation-20261005`.
+No parent theorem or independent alignment status is promoted.
+
+## Purpose and source identity
+
+A bound on an unnormalized weight is not automatically a bound on its normalized
+probability law. This module supplies the missing abstract error-propagation
+interface: use a positive reference normalizer and a genuine L1 error, then derive
+a lower normalizer for the perturbed weight and an error bound for every measurable
+event. Concrete field estimates and identification of the two weights remain the
+application's responsibility.
+
+Consumed construction: `formal/ResearchFormalCoreR1/WeightedLaw.lean` in
+`d6g8k5htny-coder/Math-` at `5b012335b279d1f93b930e7b906da09164332c47`,
+SHA256 `f31dfd2cd048cc0c0446c54c46d89c9cdd5d7bb9d76e9d8d16b7c034f351d736`.
+All six earlier Lean modules and their forty theorem proofs are unchanged.
+The new module imports WeightedLaw directly, not the later generality proposals.
+
+Pinned mathlib is `d13f23b723b8a846827a245b89c10fc7d3f11612`;
+`MeasureTheory.abs_integral_le_integral_abs` and `integral_sub` are in
+`Mathlib/MeasureTheory/Integral/Bochner/Basic.lean`, and
+`MeasureTheory.setIntegral_le_integral` is in the companion `Bochner/Set.lean`.
+Lean stays at 4.34.1. No new dependency, custom axiom, or gate exemption is added.
+
+## Exact seven-target scope
+
+Every declaration is in `ResearchFormalCoreR1`.
+
+| Target | Established statement |
+|---|---|
+| `weightPerturbation_integral` | Integrable W,V give absolute difference of integrals at most the integral of their absolute difference. Signed weights are allowed here. |
+| `weightPerturbation_setIntegral` | The same bound holds for set integrals over any set A; the bound uses the total L1 error. |
+| `weightPerturbation_normalizer_lower` | Reference integral at least c and L1 error at most delta imply perturbed integral at least c-delta. No positivity is needed for this inequality alone. |
+| `weightPerturbation_event_integral_bounds` | A nonnegative integrable weight has every set integral between zero and its total integral. |
+| `weightPerturbation_quotient_bound` | For positive z,t, 0<=a<=z, and both abs(a-b), abs(z-t) <=delta, the ratio error is at most 2delta/t. No sign premise on b is needed for this scalar statement. |
+| `weightedLaw_event_perturbation` | With integrable a.e.-nonnegative W,V, integral(V)>=c>0 and L1 error<=delta<=c/2, conclude integral(W)>=c/2, both weighted laws are probability measures, and every measurable-event error is <=2delta/c. |
+| `weightedLaw_event_perturbation_r2` | With r>0, reference integral>=cr^2 and L1 error<=eta*r^2, eta<=c/2, conclude integral(W)>=(cr^2)/2, both probability properties and every measurable-event error<=2eta/c. No r<=1 assumption. |
+
+The ambient measure is arbitrary: it need not have finite mass or be a probability
+measure. W and V always use the SAME underlying measure, and A is the SAME event
+in both laws. Its dependence on either weight is unrestricted. Integrability is
+an actual premise; no totalized divergent integral is used. Nonnegativity is only
+almost everywhere, so values on null sets are irrelevant. The error-budget
+hypotheses themselves imply delta>=0 (and eta>=0 in the scaled theorem).
+
+## Mathematical argument and interpretation
+
+Write a=int_A W, b=int_A V, z=int W, t=int V and Delta=int |W-V|.
+Integral subtraction and the triangle inequality give abs(z-t)<=Delta and
+abs(a-b)<=Delta. In particular z>=c-delta>=c/2>0. The existing weighted-law
+construction then supplies the probability properties and event-ratio identities.
+For the ratio bound use the exact identity
+
+    a/z - b/t = ((a-b) + (a/z)*(t-z))/t.
+
+Since 0<=a/z<=1, the numerator's absolute value is at most 2delta. Division by
+t>=c gives the stated result uniformly over measurable A. The constant 2 is a
+convenient valid bound; optimality is NOT claimed. The r^2 theorem is an algebraic
+specialization with positive r, so the common vanishing scale cancels.
+
+This is a uniform measurable-event bound. It does not instantiate mathlib's total
+variation API or use a particular convention for the total variation norm.
+The bound may exceed one; no sharpness or nontriviality at every budget is claimed.
+A family application needs a fixed positive c and an actually controlled relative
+budget eta(r). The module proves neither that eta(r) tends to zero nor that a
+particular field has such a uniform bound.
+
+## Nonclaims and review
+
+No concrete Gaussian/typed Palm law, coupling of different base measures,
+convergence of a density, reference normalizer floor, determinant approximation,
+QS transfer, good-event complement, or persistence theorem is supplied. This
+module does not replace a proof under mu_r with one under mu_0. Such applications
+must first provide a legitimate common-measure representation and all displayed
+estimates. A small absolute error alone is insufficient near a zero normalizer.
+An absolute value AFTER integrating W-V cannot replace integrating |W-V|.
+
+The earlier forty-target provenance and withheld alignment record remain exactly
+as recorded. This seven-target addition requires its own nonauthor statement read;
+it does not convert earlier withheld lineage into a full-package accepted record.
+Any future complete alignment record must bind the new manifest and scope and
+satisfy the unchanged lineage validator, including disclosed contributors.
+
+## Controls
+
+Sixteen focused Python methods cover exact signed integral inequalities, event
+restriction, scalar ratios including negative b, all events on finite models,
+nonunit and zero ambient masses, null-set changes, the half-budget endpoint and
+r>1 scale cancellation. Countermodels reject omitting the normalizer, cancellation
+inside a signed integral, substituting a different base law, signed-density
+clipping, and normalizing a zero weight. These finite controls are not a Lean
+formalization of the finite models or a proof for arbitrary measures.
+
+The old generality test keeps its exact 36:40 inventory slice; the new test binds
+the exact 40:47 extension and total 47. The unchanged gate independently checks
+all declarations, hashes, build, leanchecker, transitive axioms and the original
+five executable rejection controls. A supplied proof is not a successful run;
+actual exact-commit execution and review evidence remain separate records.