Fidelity note — gaussian_conv_solves_heat: superfluous hypothesis & missing Mathlib primitive

Task task-20260707-ddc7 (brick M2 completion). Mathlib pin: v4.29.0.

This note records two findings surfaced while closing the three sorrys of lean/EFS/EFS/Heat.lean. Two of the three closed cleanly (0 sorry / 0 axiom):

The third, gaussian_conv_solves_heat, remains sorry-pinned. Here is why, and what it is not.

The theorem is TRUE and provable — the earlier read was wrong

The main theorem asks that the Weierstrass solution u(t,x) = (p ∗ K_t)(x) solve ∂_t u = ½ Δ_x u. The proof is dominated differentiation under the convolution integral.

A first (wrong) reading routed the domination through the growth hypothesis hp_decay : |p(x)| ≤ C·exp(a‖x‖²). Along that route the integrand |p(y)|·∂_s K_s(x−y) ∼ exp((a − 1/(2s))‖y‖²) diverges once a ≥ 1/(2s), and a is unconstrained — which would make the theorem unprovable. This route is a mistake. One must not discard p ∈ L¹ by replacing |p| with its loose upper bound.

The correct domination (von-Neumann feasibility review, 2026-07-07) keeps |p(y)| and uses that the kernel's derivatives are bounded:

∂_s K_s(z) = K_s(z)·( ‖z‖²/(2s²) − d/(2s) )      — polynomial × Gaussian → 0 at ∞

so B := sup_{s ∈ [t−ε,t+ε], z} |∂_s K_s(z)| < ∞, and the honest dominating function is B·|p(y)| ∈ L¹, integrable by hp_int alone. The same bound (the kernel's second x-derivatives are also bounded) pushes Δ_x inside. Dominated differentiation then closes it, and heatKernel_solves_heat supplies ∂_t K = ½ Δ K.

Conclusion: the theorem holds from the stated hypotheses. hp_decay is superfluous, not insufficient. Continuity (hp_cont) is likewise not needed for the interior PDE (it is what one needs for the initial trace u(t,·) → p as t ↓ 0).

Finding 1 — hypothesis hygiene (non-blocking)

hp_decay : ∃ C a, 0 < a ∧ ∀ x, |p x| ≤ C · exp(a · ‖x‖²) is a growth bound, yet it is named decay and both EFS.Heat.gaussian_conv_solves_heat and its Q3 consumer EFS.Q3.heat_equation_gaussian_convolution describe the datum as having "Gaussian decay". The name/prose and the +a‖x‖² exponent disagree — a genuine sign/name slip. A true decay bound reads exp(−a‖x‖²).

Because the hypothesis is superfluous the slip breaks nothing today, but it is a fidelity defect in a pinned signature. Options (operator's call, since the signature is consumed by Q3):

  1. Drop it — keep only hp_int (+ hp_cont for the trace). Cleanest; the theorem needs nothing more.
  2. Fix the sign — |p x| ≤ C·exp(−a‖x‖²), matching the name. Harmless and documents intent.
  3. Leave as-is — superfluous but inert.

Surfaced rather than silently edited: correcting it touches EFS.Q3.heat_equation_gaussian_convolution (D-invariant: pinned Q3 statements are fidelity anchors).

Finding 2 — missing Mathlib primitive (the reason the sorry remains)

Every convolution-differentiation lemma in Mathlib v4.29.0 requires compact support of a factor:

The Gaussian heat kernel has no compact support. So the interchange — in particular the second-order Δ_x-under-∫ — cannot reuse the library and must be assembled by hand from hasDerivAt_integral_of_dominated_loc_of_deriv_le with the L¹ domination above. That is several hundred lines: the candidate Mathlib.Analysis.PDE.Heat contribution. This is the sole obstruction keeping gaussian_conv_solves_heat pinned.

Cosmon-ward: the missing primitive is an upstream (Mathlib) gap, not a cosmon-core one; it is recorded here and in docs/lore/lean-unproved.md §2 as a tracked upstream obligation, and the hypothesis slip (Finding 1) is surfaced to the operator as a Q3-signature fidelity decision.