Trust and reproducibility

The permitted foundational axioms are Classical.choice, Quot.sound and propext. A theorem remains conditional on every hypothesis in its Lean type.

Different checks establish different facts

• A clean package build elaborates all selected source modules against the pinned dependencies.
• Compiled-environment ownership audits include private helpers, definitions, instances and generated declarations; public theorem counts alone do not establish this coverage.
• Strict negative fixtures must fail for the intended single False goal, after their positive witnesses compile.
• Native kernel replay checks compiled proof modules. Independent statement comparison checks the configured claimed results against their reference statements.
• Receipts must identify the actual scientific commit, inputs and retained sealed outputs. Historical evidence cannot certify changed scientific source.

Read the domain

Analytic estimates state positive-time hypotheses. heatKernel has value zero at nonpositive time. heatFlow is a real Bochner integral; rough-data theorems prove the required integrability. lheatFlow 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.

The repository README verification block and canonical receipts record the actual verification route and named scientific content. This page explains the contract, not a current pass state. See raw trust guide.