diff --git a/formal/README.md b/formal/README.md index 668014f52..e4e0fa6ee 100644 --- a/formal/README.md +++ b/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. diff --git a/formal/ResearchFormalCoreR1.lean b/formal/ResearchFormalCoreR1.lean index f666fece7..0cd5a62af 100644 --- a/formal/ResearchFormalCoreR1.lean +++ b/formal/ResearchFormalCoreR1.lean @@ -4,3 +4,4 @@ import ResearchFormalCoreR1.MeasureBridge import ResearchFormalCoreR1.WeightedLaw import ResearchFormalCoreR1.MomentTail import ResearchFormalCoreR1.MomentGenerality +import ResearchFormalCoreR1.WeightPerturbation diff --git a/formal/ResearchFormalCoreR1/WeightPerturbation.lean b/formal/ResearchFormalCoreR1/WeightPerturbation.lean new file mode 100644 index 000000000..8dfd69326 --- /dev/null +++ b/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 diff --git a/formal/SCOPE.md b/formal/SCOPE.md index 5b959f619..f8b7c74b7 100644 --- a/formal/SCOPE.md +++ b/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. diff --git a/formal/WEIGHT_PERTURBATION.md b/formal/WEIGHT_PERTURBATION.md new file mode 100644 index 000000000..dbd204fbf --- /dev/null +++ b/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. diff --git a/formal/evidence/weight-perturbation-initial-build-failure.log b/formal/evidence/weight-perturbation-initial-build-failure.log new file mode 100644 index 000000000..734bc14ea --- /dev/null +++ b/formal/evidence/weight-perturbation-initial-build-failure.log @@ -0,0 +1,44 @@ +⚠ [8924/8932] Built ResearchFormalCoreR1.ProbabilityCompanionsV2 (4.0s) +warning: ResearchFormalCoreR1/ProbabilityCompanionsV2.lean:22:18: Variable name `hcW` is not explicitly referenced. + +Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: + [apply] _hcW + +Note: This linter can be disabled with `set_option linter.unusedVariables false` +warning: ResearchFormalCoreR1/ProbabilityCompanionsV2.lean:22:48: Variable name `hq` is not explicitly referenced. + +Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: + [apply] _hq + +Note: This linter can be disabled with `set_option linter.unusedVariables false` +✔ [8925/8932] Built ResearchFormalCoreR1.AlgebraV2 (5.3s) +✔ [8926/8932] Built ResearchFormalCoreR1.MeasureBridge (4.4s) +✔ [8927/8932] Built ResearchFormalCoreR1.WeightedLaw (4.2s) +✖ [8928/8932] Building ResearchFormalCoreR1.WeightPerturbation (4.4s) +trace: .> LEAN_PATH=/home/runner/work/Math-/Math-/formal/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/Math-/Math-/formal/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/Math-/Math-/formal/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/Math-/Math-/formal/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/Math-/Math-/formal/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/Math-/Math-/formal/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/Math-/Math-/formal/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/Math-/Math-/formal/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/Math-/Math-/formal/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/Math-/Math-/formal/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.34.1/bin/lean /home/runner/work/Math-/Math-/formal/ResearchFormalCoreR1/WeightPerturbation.lean -o /home/runner/work/Math-/Math-/formal/.lake/build/lib/lean/ResearchFormalCoreR1/WeightPerturbation.olean -i /home/runner/work/Math-/Math-/formal/.lake/build/lib/lean/ResearchFormalCoreR1/WeightPerturbation.ilean -c /home/runner/work/Math-/Math-/formal/.lake/build/ir/ResearchFormalCoreR1/WeightPerturbation.c --setup /home/runner/work/Math-/Math-/formal/.lake/build/ir/ResearchFormalCoreR1/WeightPerturbation.setup.json --json +error: ResearchFormalCoreR1/WeightPerturbation.lean:78:34: Unknown identifier `abs_add` +warning: ResearchFormalCoreR1/WeightPerturbation.lean:138:46: this tactic is never executed + +Note: This linter can be disabled with `set_option linter.unreachableTactic false` +warning: ResearchFormalCoreR1/WeightPerturbation.lean:138:46: Unused tactic linter: `ring` does nothing + +Note: This linter can be disabled with `set_option linter.unusedTactic false` +⚠ [8929/8932] Built ResearchFormalCoreR1.MomentTail (4.8s) +warning: ResearchFormalCoreR1/MomentTail.lean:49:0: automatically included section variable(s) unused in theorem `ResearchFormalCoreR1.p02_lm009_badJet_subset`: + [MeasurableSpace Ω] +consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: + omit [MeasurableSpace Ω] in theorem ... + +Note: This linter can be disabled with `set_option linter.unusedSectionVars false` +⚠ [8930/8932] Built ResearchFormalCoreR1.MomentGenerality (4.2s) +warning: ResearchFormalCoreR1/MomentGenerality.lean:72:2: Try this: + letI̵ + +The goal is a proposition, so `let` is preferred over `letI`. +The difference between `let` and `letI` is that `letI` inlines the value. +But this is not relevant for proofs because of proof irrelevance. + +Note: This linter can be disabled with `set_option linter.style.haveILetI false` +Some required targets logged failures: +- ResearchFormalCoreR1.WeightPerturbation +error: build failed diff --git a/formal/manifest.json b/formal/manifest.json index d306e6495..45c10dde0 100644 --- a/formal/manifest.json +++ b/formal/manifest.json @@ -25,7 +25,8 @@ "ResearchFormalCoreR1/MeasureBridge.lean", "ResearchFormalCoreR1/WeightedLaw.lean", "ResearchFormalCoreR1/MomentTail.lean", - "ResearchFormalCoreR1/MomentGenerality.lean" + "ResearchFormalCoreR1/MomentGenerality.lean", + "ResearchFormalCoreR1/WeightPerturbation.lean" ], "targets": [ "ResearchFormalCoreR1.ec005_fold_gap", @@ -67,17 +68,24 @@ "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" + "ResearchFormalCoreR1.p02_lm009_moment40_family_r3_of_interval", + "ResearchFormalCoreR1.weightPerturbation_integral", + "ResearchFormalCoreR1.weightPerturbation_setIntegral", + "ResearchFormalCoreR1.weightPerturbation_normalizer_lower", + "ResearchFormalCoreR1.weightPerturbation_event_integral_bounds", + "ResearchFormalCoreR1.weightPerturbation_quotient_bound", + "ResearchFormalCoreR1.weightedLaw_event_perturbation", + "ResearchFormalCoreR1.weightedLaw_event_perturbation_r2" ], "files": { ".gitignore": "b34af236d1df9e39ed4f98fca51702530ce76bdee4e1a69512f6caed933c3374", "COMPATIBILITY.md": "33721aad32f82131a6956a06b58c5bc41f5d28f26efe840a99a4d51ad60cf247", "GLOSSARY.md": "6bdda2ce054915efc26e8db462dbe8fd9d0c1db30e02328857bebc6568e05ce9", - "README.md": "35f4aab13f9dc69c0810d7fcd16d9e13bf03f41e227423e9e254983978fa2b08", + "README.md": "35e3a29206c592947ff7ff44e2ee6eb796ca9791937adbe3eb03bfa0ed6aa1bf", "ResearchFormalCoreR1/AlgebraV2.lean": "4480708263c40a2f7f03f12ef7e15f0eb4f8193c2dccbb253921a7ec251863c3", "ResearchFormalCoreR1/ProbabilityCompanionsV2.lean": "338452a0c2ba24d016059354d543cc995b8cb29c9d4a41d98bb93499f5f8cb8f", - "ResearchFormalCoreR1.lean": "bfb77a7b6c3d7cbd550ddcbac3842a5581f28c0ae68f861c795bf5f715fabb30", - "SCOPE.md": "198bbc6c60fdb9148ae21c0f25b52d3b612de20c373dc1e6df818767987da452", + "ResearchFormalCoreR1.lean": "e648c41573b1ddc4e12af2ef1e3d3bff0d2c923f01b63e75186735f10eb35860", + "SCOPE.md": "36e0714bcb79a158a6e50ff5b1e5e772939800ba023d865944901e4e7ae34838", "blueprint/src/content.tex": "e00ee78344ed27c097bccb8c6360f6bb86a223ab06319a407de2dd0104fd2e28", "evidence/initial-build-failure.log": "43393d2e2b3148a2453e3092a1ff04e257dbd4a6dc97eb2853a8bc0451002591", "gate.py": "958b149ea3a4ce735644a2079f817b5deddf5dc0d5ca347904ad09db6ad47d68", @@ -99,8 +107,12 @@ "evidence/moment-tail-initial-build-failure.log": "61bee2d55d0dd548b0bccc4d2e40970f654fca8ab1385af7f371592d45c0ab08", "ResearchFormalCoreR1/MomentGenerality.lean": "fdec55f1602938cd8fdb5b71535962e76a9671bf230dea53868b14147fb3b509", "MOMENT_GENERALITY.md": "5386c763f95ecd0946e0f23a22d1ba90e7956ff1a1bfcada0d454d1b5ace0cf2", - "tests/test_moment_generality.py": "7cd25876b9b0f4ed46168e4cf493030470cd7300d6ff06b9d242642eb9659a17", + "tests/test_moment_generality.py": "cba72a9747670e269bbec414f89fd2e8291dcf331d01a8e1e88ad6c7f2841383", "tests/test_alignment_lineage.py": "c510c6566d7689bebde76843582e9936dfa9e62e783b816b5e4f63d83434b893", - "LINEAGE_VALIDATION.md": "bba9d0a859f1ba45670fe122e4e72ae1094a2226de98aa814d838b0baaf61815" + "LINEAGE_VALIDATION.md": "bba9d0a859f1ba45670fe122e4e72ae1094a2226de98aa814d838b0baaf61815", + "ResearchFormalCoreR1/WeightPerturbation.lean": "50ce15709a133da12a0b4333cc653d26c5fd8a412976c975a7c2f3b25ed5c00f", + "WEIGHT_PERTURBATION.md": "0ac969b86f5b2cc4e84b4bb61790c7497164b923dc5f3fc5be99195b75b1b212", + "tests/test_weight_perturbation.py": "a83f272236a2d315d20561b862c952963b825c24baef42972f368eba11a897d7", + "evidence/weight-perturbation-initial-build-failure.log": "2abe4ec4bcfa4de282e7983ffebb225af21308c60b84083a1696bcced31b9c7c" } } diff --git a/formal/tests/test_moment_generality.py b/formal/tests/test_moment_generality.py index c143973ab..b43e8e74b 100644 --- a/formal/tests/test_moment_generality.py +++ b/formal/tests/test_moment_generality.py @@ -36,8 +36,8 @@ def test_module_and_exact_declarations(self): def test_exact_inventory(self): m = json.loads((ROOT/'manifest.json').read_text()) - self.assertEqual(m['targets'][36:], ['ResearchFormalCoreR1.'+n for n in NAMES]) - self.assertEqual(len(m['targets']), 40) + self.assertEqual(m['targets'][36:40], ['ResearchFormalCoreR1.'+n for n in NAMES]) + self.assertGreaterEqual(len(m['targets']), 40) self.assertIn(MODULE, m['source_modules']) def test_source_scope_and_tests_bound(self): diff --git a/formal/tests/test_weight_perturbation.py b/formal/tests/test_weight_perturbation.py new file mode 100644 index 000000000..f411c2450 --- /dev/null +++ b/formal/tests/test_weight_perturbation.py @@ -0,0 +1,179 @@ +"""Exact finite-model controls and source wiring; not a Lean kernel replay.""" +from fractions import Fraction as F +import hashlib +import itertools +import json +from pathlib import Path +import re +import unittest + +ROOT = Path(__file__).resolve().parents[1] +MODULE = 'ResearchFormalCoreR1/WeightPerturbation.lean' +NAMES = [ + 'weightPerturbation_integral', + 'weightPerturbation_setIntegral', + 'weightPerturbation_normalizer_lower', + 'weightPerturbation_event_integral_bounds', + 'weightPerturbation_quotient_bound', + 'weightedLaw_event_perturbation', + 'weightedLaw_event_perturbation_r2', +] + + +def integral(masses, values): + if len(masses) != len(values) or any(m < 0 for m in masses): + raise ValueError('invalid finite nonnegative measure') + return sum((m * x for m, x in zip(masses, values)), F(0)) + + +def l1_error(masses, w, v): + if len(w) != len(v): + raise ValueError('weights have different domains') + return integral(masses, tuple(abs(x-y) for x, y in zip(w, v))) + + +def event_integral(masses, values, event): + if len(event) != len(values): + raise ValueError('event has a different domain') + return integral(masses, tuple(x if yes else F(0) for x, yes in zip(values, event))) + + +class WeightPerturbationSourceTests(unittest.TestCase): + def test_module_and_exact_declarations(self): + self.assertTrue((ROOT/MODULE).is_file(), 'weight perturbation module absent') + text = (ROOT/MODULE).read_text() + self.assertEqual(re.findall(r'^theorem\s+([A-Za-z_][A-Za-z0-9_]*)', text, re.M), NAMES) + + def test_exact_extension_inventory(self): + m = json.loads((ROOT/'manifest.json').read_text()) + self.assertEqual(m['targets'][40:], ['ResearchFormalCoreR1.'+n for n in NAMES]) + self.assertEqual(len(m['targets']), 47) + self.assertIn(MODULE, m['source_modules']) + + def test_source_scope_and_tests_are_bound(self): + m = json.loads((ROOT/'manifest.json').read_text()) + for path in (MODULE, 'WEIGHT_PERTURBATION.md', 'tests/test_weight_perturbation.py'): + self.assertIn(path, m['files']) + self.assertEqual(hashlib.sha256((ROOT/path).read_bytes()).hexdigest(), m['files'][path]) + + def test_root_import(self): + self.assertIn('import ResearchFormalCoreR1.WeightPerturbation\n', + (ROOT/'ResearchFormalCoreR1.lean').read_text()) + + def test_predecessor_and_gate_identity_contract(self): + m = json.loads((ROOT/'manifest.json').read_text()) + pins = { + 'ResearchFormalCoreR1/WeightedLaw.lean': 'f31dfd2cd048cc0c0446c54c46d89c9cdd5d7bb9d76e9d8d16b7c034f351d736', + 'ResearchFormalCoreR1/MomentGenerality.lean': 'fdec55f1602938cd8fdb5b71535962e76a9671bf230dea53868b14147fb3b509', + 'gate.py': '958b149ea3a4ce735644a2079f817b5deddf5dc0d5ca347904ad09db6ad47d68', + } + for path, digest in pins.items(): + self.assertEqual(m['files'][path], digest) + self.assertEqual(m['scientific_effect'], 'NONE') + self.assertEqual(m['alignment_status'], 'PENDING_INDEPENDENT_REVIEW') + + +class WeightPerturbationFiniteTests(unittest.TestCase): + def test_generic_integral_bound_including_signed_weights(self): + m = (F(0), F(1, 4), F(3, 4)) + vectors = list(itertools.product((F(-2), F(0), F(2)), repeat=3)) + for w, v in itertools.product(vectors, repeat=2): + delta = l1_error(m, w, v) + z, t = integral(m, w), integral(m, v) + self.assertLessEqual(abs(z-t), delta) + self.assertLessEqual(t-delta, z) + + def test_set_integral_domination_and_nonnegative_bounds(self): + m = (F(1, 4), F(1, 4), F(1, 2)) + for w in itertools.product((F(0), F(1), F(2)), repeat=3): + v = (F(2), F(0), F(1)) + delta, z = l1_error(m, w, v), integral(m, w) + for event in itertools.product((False, True), repeat=3): + a, b = event_integral(m, w, event), event_integral(m, v, event) + self.assertGreaterEqual(a, 0) + self.assertLessEqual(a, z) + self.assertLessEqual(abs(a-b), delta) + + def test_quotient_bound_does_not_need_b_nonnegative(self): + for z, t in itertools.product((F(1, 2), F(1), F(2)), repeat=2): + for a in (F(0), z/2, z): + for b in (F(-1), F(0), t/2, t, 2*t): + delta = max(abs(a-b), abs(z-t)) + self.assertLessEqual(abs(a/z-b/t), 2*delta/t) + + def test_normalized_laws_uniform_over_all_events(self): + tested = 0 + vectors = list(itertools.product((F(0), F(1), F(2)), repeat=3)) + for total in (F(0), F(1, 2), F(1), F(2)): + m = tuple(total*x for x in (F(1, 4), F(1, 4), F(1, 2))) + for w, v in itertools.product(vectors, repeat=2): + z, t, delta = integral(m, w), integral(m, v), l1_error(m, w, v) + if t <= 0 or delta > t/2: + continue + self.assertGreaterEqual(z, t/2) + self.assertEqual(sum(x*y/z for x, y in zip(m, w)), 1) + for event in itertools.product((False, True), repeat=3): + a, b = event_integral(m, w, event), event_integral(m, v, event) + self.assertLessEqual(abs(a/z-b/t), 2*delta/t) + tested += 1 + self.assertGreater(tested, 0) + + def test_zero_error_and_null_set_changes(self): + m = (F(0), F(1, 2), F(1, 2)) + w, v = (F(-100), F(2), F(1)), (F(100), F(2), F(1)) + self.assertEqual(l1_error(m, w, v), 0) + self.assertEqual(integral(m, w), integral(m, v)) + for event in itertools.product((False, True), repeat=3): + self.assertEqual(event_integral(m, w, event), event_integral(m, v, event)) + + def test_half_budget_endpoint_still_normalizes(self): + m, w, v = (F(1),), (F(1, 2),), (F(1),) + c, delta = F(1), l1_error(m, w, v) + self.assertEqual(delta, c/2) + self.assertEqual(integral(m, w), c/2) + self.assertGreater(integral(m, w), 0) + + def test_r2_scale_cancels_without_r_le_one(self): + m, w0, v0 = (F(1, 2), F(1, 2)), (F(3, 4), F(1)), (F(1), F(1)) + eta = l1_error(m, w0, v0) + for r in (F(1, 100), F(1, 2), F(1), F(4)): + w, v = tuple(r*r*x for x in w0), tuple(r*r*x for x in v0) + self.assertEqual(l1_error(m, w, v), eta*r*r) + self.assertEqual(2*l1_error(m, w, v)/integral(m, v), 2*eta) + + def test_small_absolute_error_without_normalizer_scale_is_insufficient(self): + m, event = (F(1, 2), F(1, 2)), (True, False) + for eps in (F(1, 100), F(1, 10000)): + w, v = (eps, F(0)), (F(0), eps) + self.assertEqual(l1_error(m, w, v), eps) + difference = abs(event_integral(m, w, event)/integral(m, w) + - event_integral(m, v, event)/integral(m, v)) + self.assertEqual(difference, 1) + self.assertGreater(difference, 2*eps) # omitting the denominator is false + + def test_absolute_integral_cannot_replace_integral_absolute(self): + m, w, v = (F(1, 2), F(1, 2)), (F(1), F(3)), (F(3), F(1)) + self.assertEqual(abs(integral(m, w)-integral(m, v)), 0) + self.assertEqual(l1_error(m, w, v), 2) + self.assertNotEqual(event_integral(m, w, (True, False)), + event_integral(m, v, (True, False))) + + def test_same_weight_under_different_laws_is_not_zero_error_transfer(self): + w = (F(1), F(1)) + mu, nu = (F(1), F(0)), (F(0), F(1)) + self.assertEqual(l1_error(mu, w, w), 0) + self.assertNotEqual(event_integral(mu, w, (True, False)), + event_integral(nu, w, (True, False))) + + def test_signed_clipping_and_zero_normalizer_are_not_probability_cases(self): + m, w = (F(1, 2), F(1, 2)), (F(-1), F(3)) + z = integral(m, w) + self.assertEqual(z, 1) + self.assertEqual(integral(m, tuple(max(x, F(0)) for x in w))/z, F(3, 2)) + v, zero = (F(1), F(1)), (F(0), F(0)) + self.assertEqual(integral(m, zero), 0) + self.assertGreater(l1_error(m, zero, v), integral(m, v)/2) + + +if __name__ == '__main__': + unittest.main()