RoughHeatKernel v0.12.0

RoughHeatKernel v0.12.0 renames its comparator entry modules to package-qualified roots. Breaking for anything that imports the old module names; no definition, theorem or proof changes.

• Renamed modules. The Lean libraries Challenge and Solution are now RoughHeatKernelChallenge and RoughHeatKernelSolution, with the files and the Challenge/Reference/... tree moved to match (Challenge.Reference.* -> RoughHeatKernelChallenge.Reference.*). comparator.json names the new modules. Theorem names, which live in the RoughHeatKernel namespace, are unchanged, and in the .lean sources only import and module lines changed.
• Why. A top-level Challenge or Solution module in a dependency shadows the same root of any downstream package: Palomar's full preflight refuses such a package with challenge.module_root_shadowed (it resolves the dependency's Challenge.lean instead of the submitted statement file). Package-qualified roots, as lean-pkg new scaffolds them, remove the collision for every package that depends on RoughHeatKernel. lean-pkg palomar check detects the case since lean-pkg #405 (0.24.0, unreleased).
• Verification. Fresh receipts at the rename commit 16946e1: the lower-tier systemd receipt (verification gate PASS, no sorry, standard axioms only, claim axioms 56/56) and the comparator receipt (mechanism toolchain, result pass), both in .lean-receipts/; the package is re-gated in the lab registry.
• Upgrading. Replace imports of Challenge/Solution (and Challenge.Reference.*) from this library with the new names. Packages that only import RoughHeatKernel need no change.

RoughHeatKernel v0.11.0

RoughHeatKernel v0.11.0 adds general-purpose lemmas extracted from a Lean verification of Chen–Dalang (Ann. Probab. 2015), where three independent proof efforts each needed them.

• RoughHeatKernel.Erf: the derivative erf' x = (2/√π) e^{-x²} (and erfc' = -erf'), continuity, erf 0 = 0, erfc 0 = 1, oddness, signs, and the limits erf → ±1 at ±∞ and erfc → 0 at +∞; the standard normal density is nonnegative with total mass one; normalCDF takes values in [0, 1], is monotone, and is at least 1/2 on [0, ∞).
• RoughHeatKernel.ChenDalang: the shifted semigroup identity ∫ p_a(y − m) p_b(x − y) dy = p_{a+b}(x − m) and its integrability, and lheatFlow_sq_eq, all previously module-private and now public; the pointwise-in-time step of the Chen–Dalang estimate, ∫ J(r,y)² p_{(R−r)/2}(x − y) dy ≤ 2√(R/r) J(2R,x)² for 0 < r < R (J = lheatFlow ν); and ENNReal.ofReal (∫ f dμ) ≤ ∫⁻ ENNReal.ofReal f dμ for nonnegative f, with no integrability hypothesis.

Every v0.10.0 statement, hypothesis and definition is unchanged: the raw types of all 172 v0.10.0 public constants are byte-identical, and 24 constants are new (22 theorems, three of them previously module-private, and the generated equation lemmas erf.eq_1, erfc.eq_1).

Scientific source 6a35f44f2d51 passed the complete fresh verifier: the 142-proposition inventory, all-owned declaration/axiom audits (326 production/positive-test declarations in 33 modules, 297 reference declarations in 16 modules), eleven strict negative/witness pairs, compiled escape controls and exact native module replay. The Lean toolchain comparator (lake comparator, con-ron kernel replay) accepted all 51 curated claims. Permitted axioms are Classical.choice, Quot.sound and propext.

Pinned Lean: leanprover/lean4:v4.35.0. Mathlib: 56a005855ea17e0b0958f73ec801ae140b0a1679. License: Apache-2.0.

No new research result or Palomar submission readiness is claimed; these are standard facts.

Documentation · Source and verification record

RoughHeatKernel v0.10.0

RoughHeatKernel v0.10.0 adds three modules of general-purpose analysis, extracted from a Lean verification of Chen–Dalang (Ann. Probab. 2015).

• RoughHeatKernel.Beta: the real Beta integral on [0, t], ∫₀ᵗ s^{a-1}(t-s)^{b-1} ds = t^{a+b-1} Γ(a)Γ(b)/Γ(a+b) for a, b, t > 0 (DLMF 5.12.1), and the integrability of its integrand.
• RoughHeatKernel.Scaled: the squared-kernel and semigroup identities for heatKernel (ν * t) at general ν > 0.
• RoughHeatKernel.Erf: the error function erf and erfc, the standard normal density normalDensity and distribution function normalCDF, with normalCDF 0 = 1/2, its derivative and continuity, normalCDF x = (1 + erf (x/√2))/2, the integral ∫₀ᶻ (z² − u²)^m du, and the series Σ_k z^k / Γ(k/2 + 1) = e^{z²}(1 + erf z) for z ≥ 0 (DLMF 7.6.2). erf is written exactly as Tau Ceti's, so a future bridge is definitional.

Every v0.9.0 statement, hypothesis and definition is unchanged: the raw types of all 140 v0.9.0 public constants are byte-identical, and 20 constants are new.

Scientific source 0ca762dbce91 passed the complete fresh verifier: the 120-proposition inventory, all-owned declaration/axiom audits (304 production/positive-test declarations in 33 modules, 275 reference declarations in 16 modules), eleven strict negative/witness pairs, compiled escape controls and exact native module replay. The Lean toolchain comparator (lake comparator, con-ron kernel replay) accepted all 44 curated claims. Permitted axioms are Classical.choice, Quot.sound and propext.

Pinned Lean: leanprover/lean4:v4.35.0. Mathlib: 56a005855ea17e0b0958f73ec801ae140b0a1679. License: Apache-2.0.

No new research result or Palomar submission readiness is claimed; these are standard identities.

Documentation · Source and verification record

RoughHeatKernel v0.9.0

RoughHeatKernel v0.9.0 ports the library to the Lean module system. Every file now starts with module, imports are public import, and modules that define objects use @[expose] public section, so a downstream module file can public import RoughHeatKernel and unfold its definitions.

All theorem statements, hypotheses, definitions, names and namespaces are unchanged from v0.8.0: the raw type expressions of all 140 public library constants are byte-identical to v0.8.0. Two IsFiniteMeasure instances on RoughMeasure.ofSignedMeasure now carry set_option backward.inferInstanceAs.wrap false, so that the proved reference copy and the library declare identical constants for the comparator (the module system would otherwise give their auxiliary proofs module-specific private names). Test and audit tooling were adapted to module-system sources.

Scientific source 3b16158a4974 passed the complete fresh verifier: the 104-proposition inventory, all-owned declaration/axiom audits (248 production/positive-test declarations in 30 modules, 219 reference declarations in 13 modules), eleven strict negative/witness pairs, compiled escape controls and exact native module replay. The Lean toolchain comparator (lake comparator, con-ron kernel replay) accepted all 37 curated claims. Permitted axioms are Classical.choice, Quot.sound and propext.

Pinned Lean: leanprover/lean4:v4.35.0. Mathlib: 56a005855ea17e0b0958f73ec801ae140b0a1679. License: Apache-2.0.

The mathematical scope is that of v0.8.0. Continuity at time zero, a weak initial trace, higher dimensions and stochastic PDE well-posedness remain outside this release. No new mathematical theorem or Palomar submission readiness is claimed.

Documentation · Source and verification record

RoughHeatKernel v0.8.0

RoughHeatKernel v0.8.0 formalizes deterministic one-dimensional heat kernels and heat flow for rough positive and signed measures.

New APIs provide joint time-space continuity at every positive time for Gaussian-tempered positive measures and signed Jordan-pair data, without a finite-total-variation assumption. A uniform quarter-Hölder spatial increment envelope has the explicit universal constant 2 * exp(1).

This release exposes 104 public theorem/lemma declarations across 12 library modules and 37 curated reusable claims. Scientific source 133f3aec2c12 passed the complete fresh verifier, all-owned declaration/axiom audits (250 production/positive-test and 221 reference declarations), 39 nonempty-module replays, eleven strict negative/witness pairs and three compiled escape controls. The independent default comparator group accepted all 37 claims through con-ron, nanoda and Lean's default kernel. Permitted axioms are Classical.choice, Quot.sound and propext.

An anonymous public-HTTPS downstream project compiled all 24 dependency/consumer modules freshly at the exact released Rough revision and WalshIntegral v0.6 revision, including signed/infinite-variation joint-continuity examples, the quarter spatial envelope and an actual completed-noise/nonzero-integral example. Its six exact named axiom reports were within the permitted set. Pages built the exact release commit, and all 16 anonymous site/source requests matched tracked bytes. These consumer checks supplement the source-bound canonical receipts; they do not expand the mathematical statements.

Pinned Lean: leanprover/lean4:v4.35.0. Mathlib: 56a005855ea17e0b0958f73ec801ae140b0a1679. License: Apache-2.0.

Continuity at time zero, a weak initial trace, higher dimensions and stochastic PDE well-posedness remain outside this release. No new mathematical theorem or Palomar submission readiness is claimed.

Documentation · Source and verification record

RoughHeatKernel 0.7.0

Standalone Lean 4 library for one-dimensional heat kernels and Gaussian-tempered rough initial data. Apache-2.0.

The complete fresh build and local verification gate passed; all 33 curated claims passed independent comparator checks. Source-bound receipts, logs and scope exclusions are committed with this release. Lean 4.35.0; exact Mathlib and transitive pins are in lake-manifest.json.

Documentation: https://chenle02.github.io/rough-heat-kernel-lean/

This release does not assert verification of a complete SPDE existence or uniqueness theorem.