The ½-factor / kernel-variance discrepancy in the heat step

Detected 2026-06-24 by task-20260624-aa26 (brick M2 — Lean heat_equation_gaussian_convolution). Filed under the galaxy rule: "si vous détectez une boucle/incohérence, documentez-la explicitement avant de chercher à sortir" (CLAUDE.md). Surfaced as a fidelity-anchor finding, not silently patched.

TL;DR

Etienne's PDF (docs/problem.md) pins three facts that cannot all hold at once — they are off by a factor of 2:

Source Statement
eq. (2) γ_σ(x) = (2πσ²)^(−d/2) exp(−‖x‖²/(2σ²)) — variance σ²
eq. (84) convolution kernel is γ_{√(2t)} — i.e. variance 2t
eq. (88) ∂_t (p ∗ γ_{√(2t)}) = ½ Δ (p ∗ γ_{√(2t)}) — factor ½

The variance-2t kernel γ_{√(2t)} is Evans' fundamental solution; it satisfies ∂_t = Δ (factor 1), not ½ Δ. The kernel satisfying ∂_t = ½ Δ is the probabilist's variance-t kernel γ_{√t} (density of N(0, t·I)). So (84) and (88) disagree by a factor of 2.

Symbolic verification

With K_t(x) = (2πt)^{−d/2} exp(−‖x‖²/(2t)) (variance t):

∂_t K_t − ½ Δ_x K_t = 0           ✓   (probabilist kernel ↔ ½Δ)
∂_t K_t −   Δ_x K_t ≠ 0

With G_t(x) = (4πt)^{−d/2} exp(−‖x‖²/(4t)) = γ_{√(2t)}(x) (variance 2t):

∂_t G_t −   Δ_x G_t = 0           ✓   (Evans kernel ↔ Δ, no ½)
∂_t G_t − ½ Δ_x G_t ≠ 0

(Both checked with sympy in d = 1; the multivariate case is identical coordinatewise since the kernel factorises.)

Why it is harmless to the answer but load-bearing for fidelity

The factor 2 is a pure reparametrisation of time t ↦ 2t. The characterisation of admissible φ (Q1's algebraic closure under f ↦ ½‖∇f‖² − ½Δf) is invariant under it: rescaling time multiplies both sides of (6) by the same constant. So the mathematical content of Q1/Q2/Q3 is unaffected.

But a formal statement must be true, not just true-up-to-rescaling. The two self-consistent readings are:

  1. Keep the ½ (and the canonical Cole–Hopf / Bakry–Émery operator 𝓛 f = ½‖∇f‖² − ½Δf, equation (6) with its ½'s, coleHopfRHS, and the SilentHeatFactor guard) ⇒ the kernel must be γ_{√t} (variance t, time substitution t = σ²).
  2. Keep γ_{√(2t)} (variance 2t, t = σ²/2, the RegularStable.consistent linkage path.θ_t (σ²/2)) ⇒ the heat equation is ∂_t = Δ and (6) loses its ½'s.

Decision taken in EFS.Heat (M2)

Reading 1. The ½-operator is central to Q1/Q3 — it is the Bakry–Émery carré-du-champ generator, it appears in the Q1 closure problem (docs/problem.md Remarque 2: closure under f ↦ ½‖∇f‖² − ½Δf), and it is pinned by EFS.Q3.coleHopfRHS and four adversarial entries. Touching it would ripple through the whole corpus. Reparametrising the kernel time is local and cheap. So EFS.Heat.heatKernel is the variance-t kernel and EFS.Heat.gaussian_conv_solves_heat states ∂_t u = ½ Δ u, a true statement.

Residual reconciliation — operator decision

What still carries the slip (and is not patched by M2, because it touches the fidelity-anchor statements pinned in EFS.Q3):

Enriching/realigning these is a design decision on the fidelity anchor (it changes what the pinned theorem says), the same class flagged in docs/lore/lean-unproved.md §5. It is surfaced to the operator, not taken unilaterally. A typed cosmon-ward signal (this galaxy → cosmon discipline, "le réacteur apprend de ce qu'il brûle") and/or a follow-up task-* to realign the time convention across problem.md-derived notes + Q3.lean is the clean next step.

Note on SilentHeatFactor

The adversarial entry EFS/Adversarial/Q3/SilentHeatFactor.lean asserts that ∂_t u = Δ u (no ½) is the wrong normalisation "that matches the choice σ² = 2t". Under the analysis above, ∂_t = Δ is in fact the correct factor for the variance-2t kernel γ_{√(2t)}. The guard still does its mechanical job (it pins that coleHopf_density_heat_iff uses ½, and a bare 1 fails to unify), so it keeps rejecting — but its header rationale has the factor-vs-variance mapping backwards. Correcting that comment is part of the same operator-level reconciliation (it does not affect the guard's pass/fail behaviour).