Status and scope

This source API exposes 37 reusable claims. This is a count of curated declaration entries, not a percentage of all mathematical work.

Claim 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.

Evidence state

Evidence applies only to the scientific content and dependency pins it names. Read the generated README verification block for the recorded source commit and checks; inspect canonical receipts rather than inferring verification from a version number.

Read every hypothesis in the declaration index. Formal proof checking establishes the elaborated Lean statement; explanatory prose is reviewed separately.