Build and use

This source version uses Lean leanprover/lean4:v4.35.0 and Mathlib 56a005855ea17e0b0958f73ec801ae140b0a1679. Keep the toolchain and manifest together.

The following URLs define the public dependency interface. Select a published version tag or exact commit from the repository verification record; a source API version alone does not certify a tag exists.

git clone https://github.com/chenle02/rough-heat-kernel-lean.git
cd rough-heat-kernel-lean
lake exe cache get
lake build

Use import RoughHeatKernel, or a narrower module from the API index.

Use as a Lake dependency

Use the same Lean toolchain. The version-tag spelling is shown below; verify the chosen tag or replace it with the exact source commit you need:

[[require]]
name = "RoughHeatKernel"
git = "https://github.com/chenle02/rough-heat-kernel-lean.git"
rev = "v0.7.0"

Then run lake update RoughHeatKernel in your downstream project and build it. Never update dependency pins inside a frozen verification replay.

The dependency example above uses the published 0.7 tag. The new 0.8 APIs require this source checkout and, after acceptance, its exact published commit.

Verification is separate

A normal build elaborates the source. The verification contract also requires complete ownership and axiom checks, strict negative controls, independent comparison and native kernel replay. Follow the versioned source instructions; the README verification block records actual evidence.

Current raw instructions: README · getting started.