# Trust and reproducibility

Allowed foundational axioms: Classical.choice, Quot.sound, propext.

Analytic estimates state positive-time hypotheses. <code>heatKernel</code> has value zero at nonpositive time. <code>heatFlow</code> is a real Bochner integral; rough-data theorems prove the required integrability. <code>lheatFlow</code> is an extended-real lower integral and may be infinite. Signed data are represented by mutually singular Gaussian-tempered Jordan parts, with no finite-total-mass assumption unless explicitly stated.

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.