# RoughHeatKernel — source API 0.8.0

Gaussian kernels and heat flow for positive and signed Gaussian-tempered measures, including data of infinite mass.

Mathematical capsule:
- One-dimensional Gaussian kernel: mass, semigroup, exact Lq norms, derivatives and L1 increments.
- Gaussian-tempered positive measures: convergent heat flow, joint positive-time continuity and weighted bounds.
- Signed Jordan-pair data: total-variation domination, finite SignedMeasure interoperability and nontrivial examples.
- Chen–Dalang, squared-kernel, heat-flow semigroup and doubled-profile convolution estimates.

Not established:
- Continuity at time zero and weak convergence to the initial datum.
- Higher dimensions, higher derivatives, Fourier estimates and stochastic integration.
- Stochastic PDE well-posedness or a general converse from rough measures to finite SignedMeasure.

Verification authority: https://github.com/chenle02/rough-heat-kernel-lean/blob/main/README.md#verification-at-a-glance
Canonical receipts: https://github.com/chenle02/rough-heat-kernel-lean/tree/main/.lean-receipts
These static docs do not assert live release/CI/acceptance state. Each receipt covers only its named scientific content.

New source includes the uniform quarter-Holder Gaussian kernel envelope. Complete current-source verification and all 37 independent three-kernel comparisons passed for scientific source 133f3aec2c12; historical receipts apply only to their recorded source.