Qualify the repaired all-orders smooth carrier on current Math main

frontiers/source_smooth_realization_20261011/.gitignore

@@ -0,0 +1 @@
+.lake/

frontiers/source_smooth_realization_20261011/DESIGN.md

@@ -0,0 +1,54 @@
+The first C261 Stage A construction supplies a smooth probability-one carrier for
+the existing infinite Gaussian Fourier field. It preserves the exact product
+coefficient law under inclusion and hence the existing finite Gaussian field
+laws and spectral covariance. The represented samples must satisfy every finite
+smoothness order, on one explicit measurable event. The source remains the full
+Fourier sum with the same normalized weights and period, at every point.
+
+The new module SourceSmooth derives order-indexed summable majorants from the
+existing summable_decay_pow theorem, bounds every iterated derivative of each
+mode, and proves smoothness on the countable intersection of weighted absolute
+summability events. SourceSmoothCarrier proves that event is measurable, gives
+its actual full-measure subtype and comap probability measure, and transports
+the existing source laws through the literal inclusion. SourceSmoothControls
+will distinguish this result from the old order-four theorem and verify law and
+sample identities, including higher orders and finite-coordinate changes.
+
+Dependencies are literal source copies from F7 head
+1a7fc4be83043f2e313927019db85fff61eeac3f, tree
+3b3c0f16f848712a9eb53bb1b412a06bab787b91. SourceFreeze SHA-256 is
+3b7d85ab24e872b1afe4c52e7cd69d596a247141449519e2074d4a95af3c7e28.
+That baseline is a qualified draft stack, not Math- main. The observed current
+Math- main is 298b26319cff27cc22db5ca8ec545c70ba6cc92e. PR419's statement
+source is 873c6c01b768acf66c8968e5fb8b734e2d8d61d0. The incidental R17 WE1890
+notes phrase "native Main1a?" is a placeholder with no identity effect; these
+exact identities control it. Historical claim bytes are preserved.
+
+ROOT holds source claim e2f875ef-55a0-46d5-b85d-9b94cb6bc6c6,
+2026-10-11T20:58:16.222Z through 2026-10-11T22:58:16.223Z. Its actual native
+discussion is Math- PR419 comment6113682633; its R17 Work Events1890 claim was
+read back in all14 literal/effective/format fields before material source edits.
+These cooperative claims do not exclude unregistered writers. ROOT authors
+SourceSmooth; f3 authors SourceSmoothCarrier; f5 independently reviews the exact
+new sources. All are OpenAI/Codex, source-exposed and not organizationally
+independent. No human mathematical review is inferred.
+
+Only this subconstruction is allocated. No Field or Lifetime nominal type,
+Claude-owned adapter, C262–C264 source/gate, or existing workflow is changed.
+Euclidean coordinate transport, theta/Poisson covariance identification,
+first-jet rank, the canonical fixed-pin conditional kernel, fixed-fiber
+genericity, full weighted global elder probability and count/density remain
+separate C261 Stage A/B/C obligations. Neither a generic ratio identity nor an
+assumed realization record can close them.
+
+Every new proof is UNCOMPILED until a fresh, exact-source hosted qualification
+with meaningful controls and kernel/axiom audit. Local project execution,
+Lean/Lake/Python imports/tests and old run retries remain excluded by the current
+HOSTED_ONLY boundary. No native ref, runtime slot, workflow or run has been
+created by this source preparation. A prospective initial hosted plan needs
+separate complete source/resource/trigger review before source publication.
+
+This advances an essential actual-field prerequisite. It does not close the
+universality exponent, marked point-process convergence, global uniqueness,
+higher homology, coefficient, blind50 numerical validation, publications, or
+scientific/community uptake. Scientific effect NONE; full goal ACTIVE_UNMET.

frontiers/source_smooth_realization_20261011/GaussianSeriesFoundation.lean

@@ -0,0 +1,96 @@
+import Mathlib.Probability.Distributions.Gaussian.Real
+import Mathlib.Probability.Independence.InfinitePi
+import Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum
+import Mathlib.MeasureTheory.Function.LpSeminorm.SMul
+
+/-! The actual product law and the almost-sure absolute-series foundation.
+This does not assert a Fourier covariance, sample smoothness or finite-jet rank. -/
+
+noncomputable section
+
+open MeasureTheory ProbabilityTheory
+open scoped ENNReal
+
+namespace I4Foundation
+
+/-- The same actual probability measure used for every coefficient and series assertion. -/
+def coefficientLaw (ι : Type*) : Measure (ι → ℝ) :=
+  Measure.infinitePi (fun _ : ι => gaussianReal 0 1)
+
+instance coefficientLaw_isProbabilityMeasure (ι : Type*) :
+    IsProbabilityMeasure (coefficientLaw ι) := by
+  unfold coefficientLaw
+  infer_instance
+
+theorem coordinate_measurePreserving {ι : Type*} (i : ι) :
+    MeasurePreserving (fun ω : ι → ℝ => ω i) (coefficientLaw ι)
+      (gaussianReal 0 1) := by
+  exact measurePreserving_eval_infinitePi (fun _ : ι => gaussianReal 0 1) i
+
+theorem coordinate_marginal {ι : Type*} (i : ι) :
+    (coefficientLaw ι).map (fun ω => ω i) = gaussianReal 0 1 := by
+  exact (coordinate_measurePreserving i).map_eq
+
+theorem coordinates_independent (ι : Type*) :
+    iIndepFun (fun i (ω : ι → ℝ) => ω i) (coefficientLaw ι) := by
+  exact iIndepFun_infinitePi (P := fun _ : ι => gaussianReal 0 1)
+    (X := fun _ : ι => id) (fun _ => measurable_id)
+
+theorem coordinate_memLp {ι : Type*} (i : ι) (p : ℝ≥0∞) (hp : p ≠ ∞) :
+    MemLp (fun ω : ι → ℝ => ω i) p (coefficientLaw ι) := by
+  exact (memLp_id_gaussianReal' p hp).comp_measurePreserving
+    (coordinate_measurePreserving i)
+
+theorem coordinate_integrable {ι : Type*} (i : ι) :
+    Integrable (fun ω : ι → ℝ => ω i) (coefficientLaw ι) := by
+  exact memLp_one_iff_integrable.mp (coordinate_memLp i 1 (by simp))
+
+theorem coordinate_abs_integrable {ι : Type*} (i : ι) :
+    Integrable (fun ω : ι → ℝ => |ω i|) (coefficientLaw ι) := by
+  simpa only [Real.norm_eq_abs] using (coordinate_integrable i).norm
+
+theorem weighted_abs_summable_ae {ι : Type*} [Countable ι]
+    (a : ι → ℝ) (ha : ∀ i, 0 ≤ a i) (hs : Summable a) :
+    ∀ᵐ ω ∂coefficientLaw ι, Summable (fun i => a i * |ω i|) := by
+  let C := eLpNorm id 1 (gaussianReal 0 1)
+  have hC : C < ∞ := (memLp_id_gaussianReal' 1 (by simp)).eLpNorm_lt_top
+  have hcoord (i : ι) :
+      eLpNorm (fun ω : ι → ℝ => ω i) 1 (coefficientLaw ι) = C := by
+    exact eLpNorm_comp_measurePreserving
+      (memLp_id_gaussianReal' 1 (by simp)).aestronglyMeasurable
+      (coordinate_measurePreserving i)
+  have hnorm (i : ι) :
+      eLpNorm (fun ω : ι → ℝ => a i * ω i) 1 (coefficientLaw ι) =
+        ENNReal.ofReal (a i) * C := by
+    change eLpNorm (a i • (fun ω : ι → ℝ => ω i)) 1 (coefficientLaw ι) = _
+    rw [eLpNorm_const_smul, Real.enorm_eq_ofReal (ha i), hcoord]
+  have hsum : (∑' i, eLpNorm (fun ω : ι → ℝ => a i * ω i) 1
+      (coefficientLaw ι)) ≠ ∞ := by
+    simp_rw [hnorm]
+    rw [ENNReal.tsum_mul_right]
+    exact ENNReal.mul_ne_top hs.tsum_ofReal_ne_top hC.ne
+  have h := summable_norm_of_tsum_eLpNorm_ne_top (p := 1) (le_refl 1) hsum
+  filter_upwards [h] with ω hω
+  simpa only [Real.norm_eq_abs, abs_mul, abs_of_nonneg (ha _)] using hω
+
+/-- The actual scalar sum; its convergence is proved separately on the product law. -/
+def scalarSeries {ι : Type*} (a : ι → ℝ) (ω : ι → ℝ) : ℝ :=
+  ∑' i, a i * ω i
+
+theorem scalarSeries_measurable {ι : Type*} [Countable ι] (a : ι → ℝ) :
+    Measurable (scalarSeries a) := by
+  unfold scalarSeries
+  apply Measurable.tsum
+  intro i
+  exact measurable_const.mul (measurable_pi_apply i)
+
+theorem scalarSeries_hasSum_ae {ι : Type*} [Countable ι]
+    (a : ι → ℝ) (hs : Summable a) :
+    ∀ᵐ ω ∂coefficientLaw ι, HasSum (fun i => a i * ω i) (scalarSeries a ω) := by
+  filter_upwards [weighted_abs_summable_ae (fun i => |a i|)
+    (fun i => abs_nonneg _) hs.abs] with ω hω
+  have hnorm : Summable (fun i => ‖a i * ω i‖) := by
+    simpa only [Real.norm_eq_abs, abs_mul] using hω
+  exact hnorm.of_norm.hasSum
+
+end I4Foundation