From 559e1223658f9b7cc20154824e3d13e6348b9b2f Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 11:58:06 -0700 Subject: [PATCH 1/6] formal: add same-law weight perturbation and stable normalization MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Seven additive declarations derive a positive perturbed normalizer and uniform measurable-event bounds from a genuine L1 error under one measure. Preserve the earlier forty theorem proofs, hardened gate and dependency pins. Dylan Roy — delegated AI work; actual performer OpenAI / GPT-6 Astra Pro. Scientific effect NONE. Source progress only; execution and review are separate. --- formal/README.md | 6 +- formal/ResearchFormalCoreR1.lean | 1 + .../WeightPerturbation.lean | 141 ++++++++++++++ formal/SCOPE.md | 19 +- formal/WEIGHT_PERTURBATION.md | 101 ++++++++++ formal/manifest.json | 25 ++- formal/tests/test_moment_generality.py | 4 +- formal/tests/test_weight_perturbation.py | 179 ++++++++++++++++++ 8 files changed, 465 insertions(+), 11 deletions(-) create mode 100644 formal/ResearchFormalCoreR1/WeightPerturbation.lean create mode 100644 formal/WEIGHT_PERTURBATION.md create mode 100644 formal/tests/test_weight_perturbation.py 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..559df2bd5 --- /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 _ _) 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] <;> ring + 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/manifest.json b/formal/manifest.json index d306e6495..b9b53002c 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,11 @@ "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": "27d9714eef848d180700fb0fb1d82da2388393ae5e6dfa5be603b0287cfccd13", + "WEIGHT_PERTURBATION.md": "0ac969b86f5b2cc4e84b4bb61790c7497164b923dc5f3fc5be99195b75b1b212", + "tests/test_weight_perturbation.py": "a83f272236a2d315d20561b862c952963b825c24baef42972f368eba11a897d7" } } 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() From 8739dbe20ecc7321cfc640738405c2c995edca94 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 12:05:32 -0700 Subject: [PATCH 2/6] formal: repair pinned triangle-inequality lemma reference Use abs_add_le and remove an unreachable scaled-proof ring tactic. All seven theorem declarations and scope are unchanged. Preserve the first hosted build failure verbatim in a hash-bound log. OpenAI / GPT-6 Astra Pro, author-side compiler correction; scientific effect NONE. --- .../WeightPerturbation.lean | 4 +- ...ght-perturbation-initial-build-failure.log | 44 +++++++++++++++++++ formal/manifest.json | 5 ++- 3 files changed, 49 insertions(+), 4 deletions(-) create mode 100644 formal/evidence/weight-perturbation-initial-build-failure.log diff --git a/formal/ResearchFormalCoreR1/WeightPerturbation.lean b/formal/ResearchFormalCoreR1/WeightPerturbation.lean index 559df2bd5..8dfd69326 100644 --- a/formal/ResearchFormalCoreR1/WeightPerturbation.lean +++ b/formal/ResearchFormalCoreR1/WeightPerturbation.lean @@ -75,7 +75,7 @@ theorem weightPerturbation_quotient_bound |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 _ _) ht.le + 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] @@ -135,7 +135,7 @@ theorem weightedLaw_event_perturbation_r2 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] <;> ring + field_simp [ne_of_gt hr, ne_of_gt hc] simpa only [heq] using hA A hmeas end ResearchFormalCoreR1 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 b9b53002c..45c10dde0 100644 --- a/formal/manifest.json +++ b/formal/manifest.json @@ -110,8 +110,9 @@ "tests/test_moment_generality.py": "cba72a9747670e269bbec414f89fd2e8291dcf331d01a8e1e88ad6c7f2841383", "tests/test_alignment_lineage.py": "c510c6566d7689bebde76843582e9936dfa9e62e783b816b5e4f63d83434b893", "LINEAGE_VALIDATION.md": "bba9d0a859f1ba45670fe122e4e72ae1094a2226de98aa814d838b0baaf61815", - "ResearchFormalCoreR1/WeightPerturbation.lean": "27d9714eef848d180700fb0fb1d82da2388393ae5e6dfa5be603b0287cfccd13", + "ResearchFormalCoreR1/WeightPerturbation.lean": "50ce15709a133da12a0b4333cc653d26c5fd8a412976c975a7c2f3b25ed5c00f", "WEIGHT_PERTURBATION.md": "0ac969b86f5b2cc4e84b4bb61790c7497164b923dc5f3fc5be99195b75b1b212", - "tests/test_weight_perturbation.py": "a83f272236a2d315d20561b862c952963b825c24baef42972f368eba11a897d7" + "tests/test_weight_perturbation.py": "a83f272236a2d315d20561b862c952963b825c24baef42972f368eba11a897d7", + "evidence/weight-perturbation-initial-build-failure.log": "2abe4ec4bcfa4de282e7983ffebb225af21308c60b84083a1696bcced31b9c7c" } } From 993ec716ccb42e6649a8c333b03596fdacca0245 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Mon, 5 Oct 2026 19:06:04 +0000 Subject: [PATCH 3/6] Record the new-seven weight-perturbation review at head 559e122. The read confirms WP-CI-001: hosted build failed on unknown identifier abs_add. Theorem types are unchanged by the required abs_add_le repair. Scientific effect none. Co-authored-by: Dylan Roy --- .../REVIEW.md | 168 ++++++++++++++++++ 1 file changed, 168 insertions(+) create mode 100644 reviews/weight_perturbation_new7_20261005/REVIEW.md diff --git a/reviews/weight_perturbation_new7_20261005/REVIEW.md b/reviews/weight_perturbation_new7_20261005/REVIEW.md new file mode 100644 index 000000000..55691ff6d --- /dev/null +++ b/reviews/weight_perturbation_new7_20261005/REVIEW.md @@ -0,0 +1,168 @@ +# Review — same-law weight perturbation, seven new targets + +Scientific effect: **NONE**. Organizational-independence credit: **0**. +This is a statement-and-engineering read of the new seven declarations. +It does not accept the package, does not relabel the inherited #281 withheld +lineage, and does not manufacture a 47-target alignment record. + +Dylan Roy — delegated AI review. +Actual performer: xAI Grok 4.7, Cursor cloud agent, model `grok-4.7-high-fast`, +session `bc-b8309e55-05c6-40e7-bc27-a1223d285487` +(https://cursor.com/agents/bc-b8309e55-05c6-40e7-bc27-a1223d285487). +Runtime: Cursor-managed cloud VM, public worker. No self-hosted worker was +connected. `lake`, `lean`, and `leanchecker` are absent on this VM, so no local +kernel replay was run or claimed. + +Reviewed source (frozen at verdict time): +`d6g8k5htny-coder/Math-` branch `chatgpt/lean-weight-perturbation-20261005` +head `559e1223658f9b7cc20154824e3d13e6348b9b2f`, +base `dcd2a886e322738324a745adcad12fd3735bd2c5`. +Source author: OpenAI / GPT-6 Astra Pro, session `lean-weight-perturbation-20261005`. +Remote head was still `559e1223658f9b7cc20154824e3d13e6348b9b2f` when this +verdict was written. This review branch does not edit that head. + +## Verdict + +**AMEND**, finding **WP-CI-001** only. + +The seven theorem types match `formal/WEIGHT_PERTURBATION.md` and the unchanged +`weightedLaw` construction. Hosted execution of this exact head failed before +`leanchecker`, the axiom audit, and the rejection controls. The failure is one +unknown identifier in the quotient proof script. + +### WP-CI-001 — required repair + +Hosted run `37360023323` at head `559e1223658f9b7cc20154824e3d13e6348b9b2f` +(https://github.com/d6g8k5htny-coder/Math-/actions/runs/37360023323): + +- `downstream-replay`: success +- `formal / formal-evidence`: failure in **Build, recheck, audit axioms and execute negative controls** +- `math-downstream-gates`: failure, as required when formal evidence fails + +Artifact `formal-evidence-37360023323-1` (id `11366965020`) contains `build.log` +with SHA256 `2abe4ec4bcfa4de282e7983ffebb225af21308c60b84083a1696bcced31b9c7c`. +That log's only error is: + +``` +error: ResearchFormalCoreR1/WeightPerturbation.lean:78:34: Unknown identifier `abs_add` +``` + +`ResearchFormalCoreR1.WeightedLaw` built in the same log. The new module did not. +There is no successful execution receipt on this run. + +Pinned mathlib `d13f23b723b8a846827a245b89c10fc7d3f11612`, +`Mathlib/Algebra/Order/Group/Unbundled/Abs.lean`, declares + +```lean +@[to_additive /-- The absolute value satisfies the triangle inequality. -/] +lemma mabs_mul_le (a b : α) : |a * b|ₘ ≤ |a|ₘ * |b|ₘ +``` + +The additive name is `abs_add_le`, with statement `|a + b| ≤ |a| + |b|`. +Line 78 uses that inequality: + +```lean +div_le_div_of_nonneg_right (abs_add _ _) ht.le +``` + +Exact repair on the source branch, by the source author: + +1. Replace `abs_add` with `abs_add_le` at that call. +2. Rebind `formal/manifest.json` key + `ResearchFormalCoreR1/WeightPerturbation.lean` to the new file SHA256. + +The seven declarations through `:= by` stay unchanged. Leave the target list, +hypotheses, factor, SCOPE mathematical claims, gate, lineage validator, +dependencies, and workflows unchanged. + +Same-commit cleanup that is **not** a second finding: line 138 is +`field_simp [ne_of_gt hr, ne_of_gt hc] <;> ring`, and the same log warns that +`ring` is never executed. Deleting ` <;> ring` may ride with the repair. +Preserving `build.log` under `formal/evidence/` and binding its hash may also +ride with the repair. A later readback checks the byte diff. + +This ID is the one already published in PR #292 comment 6001159217. +The log line and the pinned `mabs_mul_le` / `abs_add_le` declaration were +checked again here. No second identifier, and no parallel repair branch. + +## Statement read of the new seven + +Consumed construction `formal/ResearchFormalCoreR1/WeightedLaw.lean` is blob +`b51ca969a13b27b7e41a1401ea9e10e7dee39fb8` at `559e122`, at base `dcd2a88`, and +at `5b012335b279d1f93b930e7b906da09164332c47`. SHA256 +`f31dfd2cd048cc0c0446c54c46d89c9cdd5d7bb9d76e9d8d16b7c034f351d736`. +`weightedLaw` is `(ENNReal.ofReal (∫ W))⁻¹ • μ.withDensity (ENNReal.ofReal ∘ W)`. +`ofReal` clips negatives, so the probability theorems carry `0 ≤ᵐ[μ]`. + +| Target | Read | +|---|---| +| `weightPerturbation_integral` | Integrable `W`,`V` give `\|∫W − ∫V\| ≤ ∫\|W−V\|` via `integral_sub` and `abs_integral_le_integral_abs`. Signed weights stay allowed. Pinned `abs_integral_le_integral_abs` needs no extra integrability argument. | +| `weightPerturbation_setIntegral` | The same comparison on `μ.restrict A`, then `setIntegral_le_integral`. Pinned mathlib states that lemma for an arbitrary set from `Integrable` and `0 ≤ᵐ[μ]`, with no `MeasurableSet` argument. | +| `weightPerturbation_normalizer_lower` | `\|∫W − ∫V\| ≤ δ` and `c ≤ ∫V` give `∫W ≥ c − δ` from the lower half of `abs_le`. | +| `weightPerturbation_event_integral_bounds` | `0 ≤ᵐ[μ] W` gives `0 ≤ ∫_A W ≤ ∫ W` by `ae_restrict_of_ae` and `setIntegral_le_integral`. | +| `weightPerturbation_quotient_bound` | Identity `a/z − b/t = ((a−b) + (a/z)·(t−z))/t` holds for `z,t ≠ 0`. With `0 ≤ a/z ≤ 1` the numerator is at most `2δ`, so the quotient is at most `2δ/t`. The denominator kept in the statement is the reference `t`. No sign hypothesis on `b`. The factor is attained when `a = z`, `b = a − δ`, and `t = z + δ`. The note calls 2 convenient and does not claim optimality. | +| `weightedLaw_event_perturbation` | One measure `μ`. `∫\|W−V\| ≥ 0` and `≤ δ` produce `δ ≥ 0`. Then `∫W ≥ c − δ ≥ c/2 > 0`, so both `weightedLaw μ W` and `weightedLaw μ V` are probability measures. For every `MeasurableSet A`, `weightedLaw_event_real` rewrites both probabilities as integral ratios, the scalar lemma bounds them by `2δ/(∫V)`, and `∫V ≥ c > 0` weakens the denominator to `c`. | +| `weightedLaw_event_perturbation_r2` | `η ≤ c/2` and `r > 0` give `η r² ≤ (c r²)/2` with `sq_nonneg`, including `r > 1`. The parent theorem supplies the probability bound `2 (η r²) / (c r²)`, and `field_simp` cancels to `2η/c`. | + +Attack notes, each checked on the frozen text: + +- Ambient measure versus finite integral. The measure is an arbitrary `Measure Ω`. Finiteness enters as the `Integrable` hypotheses, which make the Bochner integrals the ones appearing in `weightedLaw`. There is no `[IsProbabilityMeasure μ]` and no finite-mass hypothesis. +- Almost-everywhere signs. Probability and event-ratio steps use `0 ≤ᵐ[μ]`. Values on null sets are outside those hypotheses. Theorems 1–3 do not require a sign. +- Reference versus perturbed normalizer. The scalar bound divides by `t = ∫ V`. The event theorem then uses `c ≤ ∫ V` to replace that denominator by `c`. It does not divide by the perturbed normalizer. +- Signed `b`. The scalar lemma's hypotheses are `0 < z`, `0 < t`, `0 ≤ a ≤ z`, `|a−b| ≤ δ`, and `|z−t| ≤ δ`. The probability application gets `a`'s bounds from the nonnegative weight `W`; `b` is controlled only through `|a−b|`. +- Every measurable `A`. The quantifier is `∀ A, MeasurableSet A → …`, and `hA` is passed to `weightedLaw_event_real`. +- `δ ≥ 0`. Derived in `weightedLaw_event_perturbation` as `0 ≤ ∫|W−V| ≤ δ`. The scaled theorem inherits it for `η r²` with `r² > 0`. +- `r²` cancellation for `r > 1`. Algebraic, using `r ≠ 0` and `c ≠ 0`. No `r ≤ 1` hypothesis is present. The sibling transfer `p02_lm009_probability_transfer_r8_to_r3` still has `r ≤ 1`; this module does not import that restriction. +- Different base measures. Both laws are `weightedLaw μ _`. The type has one `μ`. The note says a different-base application needs its own common-measure representation. +- Concrete L1 estimate and reference floor. `c`, `δ`, `η`, and the integral hypotheses are premises. No Gaussian, Palm, determinant, or numerical floor is proved. +- Factor 2. Documented as unoptimized. The scalar inequality is sharp for its own hypotheses; the module does not claim a smaller universal constant. + +No `sorry`, axiom, or `native_decide` appears in the new module. + +## Engineering inventory + +Diff `dcd2a88...559e122` is exactly these eight paths: + +- `formal/ResearchFormalCoreR1/WeightPerturbation.lean` +- `formal/WEIGHT_PERTURBATION.md` +- `formal/SCOPE.md` +- `formal/README.md` +- `formal/ResearchFormalCoreR1.lean` (one import) +- `formal/manifest.json` +- `formal/tests/test_weight_perturbation.py` +- `formal/tests/test_moment_generality.py` (`targets[36:40]` kept, length lower bound `≥ 40`) + +SHA256 at `559e122`, matching the request pins and the manifest: + +| Path | SHA256 | +|---|---| +| `WeightPerturbation.lean` | `27d9714eef848d180700fb0fb1d82da2388393ae5e6dfa5be603b0287cfccd13` | +| `manifest.json` | `02536325ff94f6fa1377b79667ad9753ef8f6c078e04196278238e6ef8b470a7` | +| `SCOPE.md` | `36e0714bcb79a158a6e50ff5b1e5e772939800ba023d865944901e4e7ae34838` | +| `WEIGHT_PERTURBATION.md` | `0ac969b86f5b2cc4e84b4bb61790c7497164b923dc5f3fc5be99195b75b1b212` | + +Declaration order equals `manifest.targets`: 47 names, and the first 40 equal the base manifest. The new test locks `targets[40:]` and `len == 47`. `gate.py` `source_check` requires `names == targets` and is byte-identical to base (blob `f946c38aa38a`). `alignment_status` remains `PENDING_INDEPENDENT_REVIEW`. `scientific_effect` remains `NONE`. `LINEAGE_VALIDATION.md`, `test_alignment_lineage.py`, `lakefile.toml`, `lake-manifest.json`, `lean-toolchain`, and `.github/workflows/formal-lean.yml` match the base blobs. The six earlier Lean modules match the base blobs. README's execute sentence says 47 declarations, and the unchanged gate audits `m['targets']`. + +`python3 -B -S formal/gate.py` on `559e122` printed +`SOURCE_IDENTITY_PASS (not a Lean build or scientific acceptance): 02536325ff94f6fa1377b79667ad9753ef8f6c078e04196278238e6ef8b470a7`. + +## Finite controls actually run + +These are stdlib fraction checks. They are not a Lean replay. + +On `559e122`, Python 3.12.3: + +```sh +python3 -B -S -m unittest formal.tests.test_weight_perturbation formal.tests.test_moment_generality -v +python3 -B -O -S -m unittest formal.tests.test_weight_perturbation formal.tests.test_moment_generality -v +``` + +Both runs: 28 tests, OK. The weight-perturbation file contributes 16, and both modes agree. The hosted gate step of run `37360023323` also logged those 16 as ok before the Lean build failed. + +A separate fraction script, not the package test, checked the scalar identity, sharpness of factor 2, a negative `b`, the reference-denominator direction, a non-probability ambient mass with a null atom, `r = 7` cancellation, distinct base measures, signed-integral cancellation against `∫|W−V|`, the half-budget endpoint, and a vanishing-normalizer pair whose probability gap stays 1. That script printed `independent finite checks PASS`. + +## Reconciliation and limits + +PR #292 comment 6001128958 (CoS) records that this cloud agent already holds the @cursor ask. Numbered Grok lanes were asked to stand by. Comment 6001159217 is a read-only diagnosis of the same compiler line. Comment 6001157499 is the author describing this repair before publication. This verdict does not edit `chatgpt/lean-weight-perturbation-20261005`. + +Not claimed: `leanchecker`, transitive axiom audit, or the five rejection controls on this head. Those steps stand after the build. Not claimed: full-package alignment, a change to #281, or scientific acceptance. From 03ceeee2e9f3aeec7188eceb80975a304ee73096 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Mon, 5 Oct 2026 19:06:46 +0000 Subject: [PATCH 4/6] Record the 8739dbe readback of the triangle-inequality repair. The successor matches WP-CI-001: abs_add_le, manifest rebind, and the original build.log bytes. Kernel evidence on that head was still running. Co-authored-by: Dylan Roy --- .../REVIEW.md | 43 ++++++++++++++++--- 1 file changed, 38 insertions(+), 5 deletions(-) diff --git a/reviews/weight_perturbation_new7_20261005/REVIEW.md b/reviews/weight_perturbation_new7_20261005/REVIEW.md index 55691ff6d..fc58e93c6 100644 --- a/reviews/weight_perturbation_new7_20261005/REVIEW.md +++ b/reviews/weight_perturbation_new7_20261005/REVIEW.md @@ -13,13 +13,14 @@ Runtime: Cursor-managed cloud VM, public worker. No self-hosted worker was connected. `lake`, `lean`, and `leanchecker` are absent on this VM, so no local kernel replay was run or claimed. -Reviewed source (frozen at verdict time): -`d6g8k5htny-coder/Math-` branch `chatgpt/lean-weight-perturbation-20261005` -head `559e1223658f9b7cc20154824e3d13e6348b9b2f`, +Reviewed source: +`d6g8k5htny-coder/Math-` branch `chatgpt/lean-weight-perturbation-20261005`, base `dcd2a886e322738324a745adcad12fd3735bd2c5`. +The read opened on head `559e1223658f9b7cc20154824e3d13e6348b9b2f`. +Before this record was pushed, the branch moved to successor +`8739dbe20ecc7321cfc640738405c2c995edca94`. The readback of that successor +is below. This review branch does not edit the source branch. Source author: OpenAI / GPT-6 Astra Pro, session `lean-weight-perturbation-20261005`. -Remote head was still `559e1223658f9b7cc20154824e3d13e6348b9b2f` when this -verdict was written. This review branch does not edit that head. ## Verdict @@ -85,6 +86,10 @@ This ID is the one already published in PR #292 comment 6001159217. The log line and the pinned `mabs_mul_le` / `abs_add_le` declaration were checked again here. No second identifier, and no parallel repair branch. +Current source disposition: `8739dbe` contains that repair. See the successor +readback. The open item on `8739dbe` is the hosted kernel run, which had not +finished when this file was written. + ## Statement read of the new seven Consumed construction `formal/ResearchFormalCoreR1/WeightedLaw.lean` is blob @@ -161,6 +166,34 @@ Both runs: 28 tests, OK. The weight-perturbation file contributes 16, and both m A separate fraction script, not the package test, checked the scalar identity, sharpness of factor 2, a negative `b`, the reference-denominator direction, a non-probability ambient mass with a null atom, `r = 7` cancellation, distinct base measures, signed-integral cancellation against `∫|W−V|`, the half-budget endpoint, and a vanishing-normalizer pair whose probability gap stays 1. That script printed `independent finite checks PASS`. +## Successor readback — `559e122..8739dbe` + +Commit `8739dbe20ecc7321cfc640738405c2c995edca94`, message +`formal: repair pinned triangle-inequality lemma reference`, changes three paths: + +- `WeightPerturbation.lean`: `abs_add` becomes `abs_add_le` at the quotient + triangle step, and the unused ` <;> ring` after `field_simp` is deleted. +- `manifest.json`: the module digest becomes + `50ce15709a133da12a0b4333cc653d26c5fd8a412976c975a7c2f3b25ed5c00f`, + and the failure log is bound. Manifest SHA256 + `db678e22bc6cee792a3918fd501b94b6253d4bac276909ea5663cd8c4710d14b`. +- `formal/evidence/weight-perturbation-initial-build-failure.log`, SHA256 + `2abe4ec4bcfa4de282e7983ffebb225af21308c60b84083a1696bcced31b9c7c`. + `cmp` against artifact `11366965020`'s `build.log` was equal. + +`grep '^theorem'` is identical on the two heads. SCOPE, the extension note, +the test, the target list, the gate, and `WeightedLaw.lean` are outside the +diff. The statement read above therefore stands on `8739dbe`. + +WP-CI-001 is closed as a source defect on `8739dbe`. That closure is the +byte readback. It is not kernel success. + +Hosted run `37360921503` on `8739dbe` was **in progress** when this readback +was recorded +(https://github.com/d6g8k5htny-coder/Math-/actions/runs/37360921503). +`leanchecker`, the axiom audit, and the rejection controls are not claimed +for `8739dbe`. + ## Reconciliation and limits PR #292 comment 6001128958 (CoS) records that this cloud agent already holds the @cursor ask. Numbered Grok lanes were asked to stand by. Comment 6001159217 is a read-only diagnosis of the same compiler line. Comment 6001157499 is the author describing this repair before publication. This verdict does not edit `chatgpt/lean-weight-perturbation-20261005`. From 80f99e42e47ed5b1f6722f8b4e7346e060dd266b Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Mon, 5 Oct 2026 19:16:43 +0000 Subject: [PATCH 5/6] Append the WP-CI-001 execution close for head 8739dbe. The original AMEND record stays byte-identical. Run 37360921503 attempt 1 succeeded on the tree-identical tested merge, with the receipt and artifact hashes recomputed from the original ZIP. Co-authored-by: Dylan Roy --- .../CLOSING_WP-CI-001.md | 129 ++++++++++++++++++ 1 file changed, 129 insertions(+) create mode 100644 reviews/weight_perturbation_new7_20261005/CLOSING_WP-CI-001.md diff --git a/reviews/weight_perturbation_new7_20261005/CLOSING_WP-CI-001.md b/reviews/weight_perturbation_new7_20261005/CLOSING_WP-CI-001.md new file mode 100644 index 000000000..fb980c3db --- /dev/null +++ b/reviews/weight_perturbation_new7_20261005/CLOSING_WP-CI-001.md @@ -0,0 +1,129 @@ +# Closing readback — WP-CI-001 execution on `8739dbe` + +Scientific effect: **NONE**. Organizational-independence credit: **0**. +This note closes the runtime side of WP-CI-001. It does not replace the +statement read or the historical AMEND, and it does not accept the 47-target +package. #281 stays WITHHELD. `alignment_status` stays +`PENDING_INDEPENDENT_REVIEW`. No integration reservation. + +Dylan Roy — delegated AI review. +Actual performer: xAI Grok 4.7, Cursor cloud agent, model `grok-4.7-high-fast`, +session `bc-b8309e55-05c6-40e7-bc27-a1223d285487`. +Runtime: Cursor-managed public VM. No local `lake` / `lean` / `leanchecker` +replay. The evidence below is the hosted run and its original artifact. + +History left unchanged: `reviews/weight_perturbation_new7_20261005/REVIEW.md` +at commit `03ceeee2e9f3aeec7188eceb80975a304ee73096`, +SHA256 `e082a8b7d46237c7bde63e9f0f21f4fd8f78e46b0e158d584fcce642a36475cd`, +git blob `fc58e93c61dd394f16fc02608c255c7b0f756b80`. +That file records **AMEND WP-CI-001** on `559e1223658f9b7cc20154824e3d13e6348b9b2f` +and the source readback of `8739dbe20ecc7321cfc640738405c2c995edca94`. + +## Disposition + +**Scoped new-seven execution PASS** on corrected head +`8739dbe20ecc7321cfc640738405c2c995edca94`. + +WP-CI-001's unknown identifier `abs_add` is absent from this run. The fresh +build of `ResearchFormalCoreR1.WeightPerturbation` completed, `leanchecker` +returned exit 0, and all 47 axiom and type reports were extracted. This PASS +covers the corrected seven-target module's hosted kernel execution together +with the unchanged gate's package run. It is not a full-47 alignment acceptance. + +## Run identity + +[Run 37360921503](https://github.com/d6g8k5htny-coder/Math-/actions/runs/37360921503), +attempt 1, event `pull_request`, conclusion **success** on head +`8739dbe20ecc7321cfc640738405c2c995edca94`. + +| Job | id | conclusion | +|---|---|---| +| `downstream-replay` | 111935011339 | success | +| `formal / formal-evidence` | 111935011660 | success | +| `math-downstream-gates` | 111936563229 | success | + +Tested commit in the receipt and in the aggregate output: +`90edceb281fb9eaa01dfe9e233d51ece0671e8b8`. +Parents: `dcd2a886e322738324a745adcad12fd3735bd2c5` and +`8739dbe20ecc7321cfc640738405c2c995edca94`. +Tree: `e6923fa5baf798617631343c7a8a00b59404ba63`, the same tree as `8739dbe`. +The aggregate log checks that commit out as +`Merge 8739dbe20ecc7321cfc640738405c2c995edca94 into dcd2a886e322738324a745adcad12fd3735bd2c5`. + +## Artifact recomputed here + +Artifact `formal-evidence-37360921503-1`, id `11366797243`, 13213 bytes. + +| Object | SHA256 | +|---|---| +| ZIP | `6e65e1d423029614de005ca52bd3771f78170cbbb8ed339459fd3cac50bad23c` | +| `receipt.json` | `facf45479aff1318ea01b5195cafb9df7b1aec8e595872b5a3f5f9c0db1b66bf` | + +`required-check-binding.json` carries the same receipt digest, repository +`d6g8k5htny-coder/Math-`, run `37360921503`, attempt `1`, and checked commit +`90edceb281fb9eaa01dfe9e233d51ece0671e8b8`. + +All 10 receipt log digests match the ZIP members. Manifest digest in the +receipt is `db678e22bc6cee792a3918fd501b94b6253d4bac276909ea5663cd8c4710d14b`. +Lean version string is 4.34.1, commit `5045d0056413266e57c625dcd7c365b10e377c52`. +Mathlib revision is `d13f23b723b8a846827a245b89c10fc7d3f11612`. Nine dependency +revisions are recorded. `scientific_effect` is `NONE`. + +## What the formal job log shows + +Step "Gate tests and exact source identity": `Ran 125 tests` / `OK`, then +`Ran 125 tests` / `OK`, then + +`SOURCE_IDENTITY_PASS (not a Lean build or scientific acceptance): db678e22bc6cee792a3918fd501b94b6253d4bac276909ea5663cd8c4710d14b`. + +`leanprover/lean-action` is invoked with `leanchecker: false`, and its own +leanchecker, nanoda, and axiom-audit actions end `skipped`. The executing +command is the later `python3 formal/gate.py --execute`, which prints: + +- `build: exit 0` +- `leanchecker: exit 0` +- `axioms: exit 0` +- `elaborated-types: exit 0` +- `false_fold: exit 1` +- `false_power: exit 1` +- `sorry: exit 0` +- `custom_imported: exit 0` +- `native: exit 0` +- `version: exit 0` + +`leanchecker.log` is empty. Its digest is the empty-file SHA256 +`e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855`, +paired with `leanchecker: exit 0` from that gate command. + +`build.log` records `Built ResearchFormalCoreR1.WeightPerturbation` and +`Build completed successfully (8932 jobs)`. One nonblocking linter hint remains +at `WeightPerturbation.lean:73` (`unnecessarySeqFocus` on `<;>`). It did not +fail the build. No new source repair is requested for it. + +The receipt lists 47 axiom reports. Every report is exactly +`Classical.choice`, `Quot.sound`, and `propext`. The seven +`weightPerturbation_*` / `weightedLaw_event_perturbation*` names are present +in both `axioms.log` and `elaborated-types.log`. + +Negative controls in the receipt and in the logs: + +| Control | Receipt | Log | +|---|---|---| +| `false_fold` | `REJECTED_BY_LEAN` | `unsolved goals` / `⊢ False` | +| `false_power` | `REJECTED_BY_LEAN` | `unsolved goals` / `⊢ False` | +| `sorry` | `REJECTED_BY_AXIOM_GATE` | `'injected' depends on axioms: [sorryAx]` | +| `custom_imported` | `REJECTED_BY_AXIOM_GATE` | `'injected' depends on axioms: [hiddenPremise]` | +| `native` | `REJECTED_BY_AXIOM_GATE` | native_decide axiom | + +`math-downstream-gates` prints `conclusion: success` for run `37360921503`, +attempt `1`, receipt `facf45479aff1318ea01b5195cafb9df7b1aec8e595872b5a3f5f9c0db1b66bf`, +checked commit `90edceb281fb9eaa01dfe9e233d51ece0671e8b8`, with the aggregate's +own meaning line: required engineering checks and current-run formal evidence +only. + +Initial run `37360023323` stays a failed build. Its preserved log is not +relabeled. + +The earlier failed head `559e122` remains the AMEND record. This closing PASS +binds only the corrected head `8739dbe` and the tree-identical tested merge +`90edceb`. From 4b0a8f59c3b7df182985fc7c02415eacd80b37d1 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 12:18:40 -0700 Subject: [PATCH 6/6] IBA2-009: localize the half-power matching band and exhibit an estimate-level obstruction Dylan Roy delegated AI work; actual author OpenAI / GPT-6 Astra Pro, session github-rules-and-closure-round5-20261005. Three new review packet files only. Derive exact k^3/r band identity, abstract compact-parity obstruction, and sufficient matched-residual tail conditions. Actual Gaussian coefficient remains unresolved; no original proof, status, workflow or formal source edits. Claims main259/6001167816 and main229/6001312122. Standard-library controls verified normal and optimized; nonauthor review required. --- reviews/iba2_009_matching_20261005/REPORT.md | 245 ++++++++++++++++++ .../iba2_009_matching_20261005/SOURCES.json | 34 +++ .../boundary_layer_check.py | 124 +++++++++ 3 files changed, 403 insertions(+) create mode 100644 reviews/iba2_009_matching_20261005/REPORT.md create mode 100644 reviews/iba2_009_matching_20261005/SOURCES.json create mode 100644 reviews/iba2_009_matching_20261005/boundary_layer_check.py diff --git a/reviews/iba2_009_matching_20261005/REPORT.md b/reviews/iba2_009_matching_20261005/REPORT.md new file mode 100644 index 000000000..a0b398f55 --- /dev/null +++ b/reviews/iba2_009_matching_20261005/REPORT.md @@ -0,0 +1,245 @@ +# IBA2-009: a half-power matching layer invisible to compact cusp parity + +**Object:** IBA2-009-MATCHING-20261005-v1. **Date:** 2026-10-05. +**Actual author:** OpenAI / GPT-6 Astra Pro, session +`github-rules-and-closure-round5-20261005`, Dylan Roy — delegated AI work. +**Scientific effect: NONE.** Author-side analytical audit contribution, requiring +nonauthor review; no historical verdict, proof, flag or register is changed. +Organizational-independence credit: 0. This is not a claim of informational +blindness: the original audit's coverage map and repository discussion were read. + +## 1. Result, limits, and source pin + +The compact-to-global implication in main#259 IBA2-009 needs a genuine matching +estimate. Here are three concrete outputs: + +1. An exact formula for the actual rejected-density contribution in the moving + band `a <= k^3/r <= b`: it has an `ell^(1/2)` prefactor and an explicitly + weighted rescaled-kernel integral. +2. An abstract kernel family with a nonzero half-power contribution that is + invisible in every fixed compact cusp window and at every fixed positive + gap. It obeys the selected upper bounds below, including the C7 K2 scale. +3. Sufficient weighted-tail conditions for a correctly matched residual to be + `o(ell^(1/2))`, stating exactly what compact parity does not supply. + +**Not proved:** that the Gaussian field has this nonzero profile, that its +half-power coefficient exists or vanishes, or that all its other probabilistic +interfaces admit the abstract family. This is not a counterexample to Theorem N +or to the persistence law. It is a counterexample to inferring global absence +from the listed estimate-level premises alone. IBA2-009 remains open for the +actual field. A positive contribution from one moving band alone also does not +establish the coefficient of a full asymptotic expansion after other regions and +lower-order terms are matched. + +All source reads use Math- commit +`dcd2a886e322738324a745adcad12fd3735bd2c5`: + +| Source | Exact path / Git blob | Scope read and consumed | +|---|---|---| +| N | `frontiers/elder_cusp_parity_20261002/PROOF.md` / `16a1db0658918057ff741df888c13702763d9919` | Statement, Corollary N-prime and its section 6 proof; section 7 Remark 1. Selected section 5 bookkeeping was read, not re-audited. | +| T | `frontiers/third_order_rate_20261001/PROOF.md` / `110ed33a57902bef11873807e722fde3888b59fb` | Section 0 kernel definitions, E3-plus/R-plus remainders and W-plus small-gap window. | +| K | `frontiers/c7_total_bounded_20260929/PROOF.md` / `28748b086ec6761ef467dc67cba475fbdf8b7455` | K1/K2 and section 4 unnormalized marked-intensity identity and Gaussian pin-density envelope. | + +N already explicitly limits its no-linear-term theorem to fixed compact +`kappa=k/r` intervals. Its Remark 1 distinguishes the two uncontrolled ends and +says that even a hypothetical uniform `O(r^2+k^2)` estimate would not finish the +global half-power question. This report quantifies a specific obstruction to +that inference; it does not attribute an unrestricted claim to N. + +## 2. Exact moving-band formula for the actual nonnegative kernel + +Use the source conventions, without dividing by the full normalizer: + + A_rej(r,b,k,u) = 12 pi_r(v_r) E_Q[(W_r/r^2)(1-e)], + B_r(k) = integral_b integral_u A_rej(r,b,k,u) d sigma(u) db >= 0, + nu_rej^near(ell) = integral_0^r0 r^(-2) B_r(ell/r^3) dr. + +This is K section 4 in the separation variable. The cap implication +`1-e <= 1_{G_r^c}`, K2 and the Gaussian pin-density envelope give + + 0 <= B_r(k) <= C r^3/k, 0 < r <= min(k,r0), 0 < k <= 1. (2.1) + +Integration over birth and direction, and absorption of polynomial gap growth +on `0 J` almost everywhere on [a,b], dominated convergence yields + + ell^(-1/2) nu_[a,b](ell) -> (1/10) integral_a^b J(y)y^(-3/2)dy. (2.4) + +More generally convergence of that weighted integral suffices. A uniform +`J_ell -> 0` proves a little-o contribution from this band. K2 supplies a +bounded J, not a vanishing J. Establishing its actual limit is a sharply +localized analytic task; the present report does not assume a limit exists. + +The band has + + r ~ ell^(3/10), k ~ ell^(1/10), kappa ~ ell^(-1/5). (2.5) + +Thus k tends to zero while kappa tends to infinity. Neither fixed-positive-k +Taylor expansion nor compact-kappa parity describes the passage uniformly. + +## 3. An explicit estimate-level obstruction + +First omit a harmless gap cutoff. Let + + h(t) = (t-1)^4(2-t)^4 for 1<=t<=2, and 0 otherwise, + psi(y) = h(sqrt(y)), + H(r,kappa) = r^2 kappa^2 psi(r^2 kappa^3) + = k^2 psi(k^3/r), k=kappa r. (3.1) + +Here H is a **scaled** kernel perturbation; its raw kernel is `D=r^2 H`. +The polynomial bump is C^3, is nonnegative, and is bounded by 1. The support +is `1<=k^3/r<=4`. + +### 3.1 Why the usual estimates do not see it + +- At fixed kappa, (3.1) is even in r. On every fixed compact kappa interval it + is identically zero for all sufficiently small |r|. In particular it has + zero linear term and satisfies compact `O(r^2)` estimates. +- At any fixed k>0 it is identically zero once `r=1`, and replace H,D by theta(k)H,theta(k)D. +As an explicit abstract nonnegative split on `0=0`. These raw kernels obey a K1-sized +majorant; on the compact k support they also obey a polynomial times +`exp(-c k^2)` majorant, after enlarging the constant. Multiplication by a +normalized Gaussian birth envelope and normalized angular measure preserves +these statements. This is only an abstract kernel construction, not a +realization as Gaussian critical points, an elder mark, or a Palm law. + +### 3.2 Exact half-power mass + +For ell sufficiently small that the whole support is inside `00`. +The explicit rational coefficient (3.3) is reserved for the polynomial h; +no closed-form value is asserted for the smooth variant. + +An added half-power correction is smaller than the existing +`O(ell^(3/7))` remainder and `O(ell^(4/9)log(1/ell))` upper scale. It is +therefore not excluded merely by those error orders. The model's perturbation +is zero on the small-kappa region; it does not purport to reconstruct the +sources' complete leading laws or all cross-region matching identities. + +## 4. A sufficient global passage, with the required subtraction explicit + +Let E_ell(kappa) denote a **correctly matched residual**: the known fold, cusp, +and common terms must already have been subtracted with no double counting. +Constructing this residual is itself part of the missing analysis. It is NOT +permissible simply to label the raw difference in N.1 as this residual: +that difference can still contain the fold contribution to the ell^(1/3) +coefficient when integrated globally. + +Suppose the residual density has the exact representation + + R(ell) = ell^(1/4)/4 * integral_0^infinity + E_ell(kappa) kappa^(-5/4) d kappa + F(ell), (4.1) + +where the integrand is extended by zero below the physical lower cutoff +`kappa=ell/r0^4`, and `F(ell)=o(ell^(1/2))` accounts for separately controlled +far/matching remainders. Assume on every fixed `03/4, and +M=O(kappa^q) near infinity, q<3/4. These are sufficient assumptions, not +established properties of the actual Gaussian kernel. + +The obstruction (3.1) violates (4.2): its normalized weighted mass stays +positive while its support escapes to kappa=infinity. Pointwise convergence +and compact parity thus cannot replace quantitative control of these tails. + +## 5. Reproduction, coverage and next mathematical target + +Run `python3 -B -S boundary_layer_check.py`, and repeat with `-O`. +The deterministic JSON reports 25 moving-layer, 30 compact-cusp, 25 fixed-gap, +20 small-gap and 3 exact-integral cases. The explicit finite checks verify +identities and inequalities, not the Gaussian realization or the general +claims by sampling; the proofs are sections 2–4 above. + +Negative controls (each must exit 1 with its named failure): + +| Variant | Deliberate error | Failure | +|---|---|---| +| M1 | k^3/r^2 instead of k^3/r | MOVING_LAYER_ARGUMENT | +| M2 | omit r^2 between raw and scaled kernels | LIFETIME_JACOBIAN | +| M3 | omit the 1/5 substitution factor | INTEGRATION_FACTOR_ONE_FIFTH | +| M4 | ignore the moving support at fixed kappa | COMPACT_CUSP_VANISHING | +| M5 | replace the half-power x^5 by x^6, ell=x^10 | HALF_POWER_SCALING | + +Example: `python3 -B -S boundary_layer_check.py --mutant M2`. +Invalid arguments exit 2. All fourteen CLI cases were run in normal/optimized +modes, and the positive JSON was byte-identical. A separate seven-test local +contract suite passed both modes after its expected missing-source failure. +No local Lean execution is claimed. Existing hosted repository checks are +separate and do not automatically execute this newly added standalone script. + +**Actionable target:** determine the actual nonnegative profile in (2.2) on a +fixed positive y-band, rather than extrapolating fixed-kappa parity. Uniform +vanishing would remove that band's half-power mass; a nonzero limiting profile +would require explicit incorporation into global matching. Neither outcome is +assumed. Both ends of the matched residual in (4.2) still require control before +a global absence statement. Historical IBA2-009, IBA2-010, IBA2-012 and all +scientific acceptance fields remain unchanged by this contribution. diff --git a/reviews/iba2_009_matching_20261005/SOURCES.json b/reviews/iba2_009_matching_20261005/SOURCES.json new file mode 100644 index 000000000..be41c7922 --- /dev/null +++ b/reviews/iba2_009_matching_20261005/SOURCES.json @@ -0,0 +1,34 @@ +{ + "scientific_effect": "NONE", + "scientific_acceptance": false, + "source_commit": "dcd2a886e322738324a745adcad12fd3735bd2c5", + "sources": [ + { + "path": "frontiers/elder_cusp_parity_20261002/PROOF.md", + "blob": "16a1db0658918057ff741df888c13702763d9919", + "scope": "statement; section 6; section 7 Remark 1" + }, + { + "path": "frontiers/third_order_rate_20261001/PROOF.md", + "blob": "110ed33a57902bef11873807e722fde3888b59fb", + "scope": "section 0: definitions and stated remainder/window bounds" + }, + { + "path": "frontiers/c7_total_bounded_20260929/PROOF.md", + "blob": "28748b086ec6761ef467dc67cba475fbdf8b7455", + "scope": "K1/K2; section 4 rejected intensity and pin-density envelope" + } + ], + "files": [ + { + "path": "REPORT.md", + "bytes": 12716, + "sha256": "570a8bf7fdd78e56e6edd04d6a1f7431312daa5839c05a210aa72a76336dc27a" + }, + { + "path": "boundary_layer_check.py", + "bytes": 4892, + "sha256": "58ba3205d390b685344e19c989efe2ef90fd7837237b47ed8a7c1eef8ac49385" + } + ] +} diff --git a/reviews/iba2_009_matching_20261005/boundary_layer_check.py b/reviews/iba2_009_matching_20261005/boundary_layer_check.py new file mode 100644 index 000000000..96fb621bf --- /dev/null +++ b/reviews/iba2_009_matching_20261005/boundary_layer_check.py @@ -0,0 +1,124 @@ +#!/usr/bin/env python3 +"""Exact finite checks for IBA2-009's moving-layer obstruction. + +Standard library only. This diagnostic is not a Gaussian-field counterexample, +not an independent audit of imported estimates, and not a proof by sampling. +The general calculation is in REPORT.md. No check uses an assert statement. + +Usage: python3 -B -S boundary_layer_check.py [--mutant M1|M2|M3|M4|M5] +Valid source exits 0 with deterministic JSON. Each documented mutant exits 1. +Invalid arguments exit 2. Optimized Python has the same behavior. +""" +from fractions import Fraction as F +import argparse +import json +from math import comb, factorial +import sys + + +class CheckFailure(ValueError): + """An exact diagnostic invariant was violated.""" + + +def require(condition, label): + if not condition: + raise CheckFailure(label) + + +def bump(t): + """C^3 bump (t-1)^4(2-t)^4 supported on [1,2].""" + t = F(t) + return (t - 1)**4 * (2 - t)**4 if 1 < t < 2 else F(0) + + +def bump_integral(order=4): + """Integral_1^2 (t-1)^m(2-t)^m dt by exact polynomial integration.""" + if not isinstance(order, int) or isinstance(order, bool) or order < 1: + raise ValueError('positive integer order required') + return sum((F((-1)**j * comb(order,j), order+j+1) + for j in range(order+1)), F(0)) + + +def lifetime_coefficient(): + return bump_integral() / 5 + + +def scaling_exponents(): + # ell=k*r^3 and k^3/r fixed: solve a+3b=1 and 3a-b=0. + return F(3,10), F(1,10), F(-1,5) # r, k, kappa + + +def run_checks(mutant=None): + if mutant not in (None, 'M1','M2','M3','M4','M5'): + raise ValueError('unknown mutation') + counts = dict(moving_layer=0,compact_cusp=0,fixed_gap=0,small_gap=0,integrals=0) + xs = (F(1,64),F(1,32),F(1,16),F(1,8),F(1,4)) + ss = (F(1),F(21,20),F(11,10),F(9,8),F(8,7)) + for x in xs: + for s in ss: + ell=x**10; r=x**3/s; k=x*s**3; kappa=k/r; t=s**5 + y=k**3/(r**2 if mutant=='M1' else r) + require(ell==k*r**3, 'CUBIC_LIFETIME') + require(y==t**2==r**2*kappa**3, 'MOVING_LAYER_ARGUMENT') + require(1<=t<2 and 04, 'FIXED_GAP_VANISHING') + counts['fixed_gap']+=1 + for r in (F(1,16),F(1,8),F(1,4),F(1,2),F(1)): + for q in (F(1,4),F(1,2),F(3,4),F(1)): + k=q*r + require(k**3/r<=1, 'SMALL_GAP_REGION_UNCHANGED') + counts['small_gap']+=1 + for m in (1,2,4): + require(bump_integral(m)==F(factorial(m)**2,factorial(2*m+1)), 'BUMP_INTEGRAL') + counts['integrals']+=1 + coefficient=bump_integral() if mutant=='M3' else lifetime_coefficient() + require(coefficient==F(1,3150), 'INTEGRATION_FACTOR_ONE_FIFTH') + rpower,kpower,kappapower=scaling_exponents() + require(kpower+3*rpower==1 and 3*kpower-rpower==0, 'BAND_POWERS') + require(2*kpower+rpower==F(1,2), 'HALF_POWER_EXPONENT') + require(kpower-rpower==kappapower, 'ESCAPING_KAPPA') + return {'status':'ESTIMATE_LEVEL_OBSTRUCTION_PASS','coefficient':str(coefficient), + 'counts':counts,'scientific_effect':'NONE','scientific_acceptance':False, + 'gaussian_counterexample':False,'global_absence_proved':False} + + +def main(argv=None): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--mutant',choices=('M1','M2','M3','M4','M5')) + args=parser.parse_args(argv) + try: + result=run_checks(args.mutant) + except CheckFailure as exc: + print('BOUNDARY_LAYER_CHECK_FAIL: '+str(exc),file=sys.stderr) + return 1 + print(json.dumps(result,sort_keys=True,separators=(',',':'))) + return 0 + + +if __name__=='__main__': + raise SystemExit(main())