Courant Kernel

Courant Kernel is a collection of mathematical proofs — checked line by line by a computer and found airtight — about a simple, classic recipe from physics simulation: the upwind scheme, one of the oldest building blocks for modelling something carried along by a flow (dye spreading down a river, heat blown by wind).

The key idea is machine-checked. Ordinary software is trusted because it passes tests: it behaves on the cases you tried. These certificates are different — a proof assistant (Lean 4) verifies that each statement holds for every input, the way a theorem is true rather than the way a test passes. Lean refuses the proof unless it is genuinely complete.

Concretely, it proves — with that rigor — that the upwind scheme and a few relatives:

• stay stable — the simulation won't blow up into garbage, provided the time-step obeys the usual CFL limit;
• conserve mass — the total amount of "stuff" is neither created nor destroyed;
• don't invent wiggles — no fake oscillations appear (the total-variation-diminishing property);
• come with an explicit error bound — on any grid, the computed answer provably stays within an explicit first-order bound (proportional to the grid spacing Δx, with a constant that does not depend on the grid) of the true solution sampled at the grid points. A grid-independent C·Δx bound is the textbook meaning of first-order convergence, and machine-checking one for a scheme like this is rare. (What is formalized is the per-grid bound itself; a full refinement-limit theorem over a family of ever-finer grids is not yet formalized — see the claim boundary.)
• behave under rounding — under the standard (1+δ) model of floating-point rounding error (an assumption, not a theorem about real hardware), a computed step — and, over n steps, the whole computed run — provably stays within an explicit, minuscule distance of the ideal answer, the gap growing linearly in n to first order. A deliberately narrow but real step toward reasoning about machine arithmetic.

Every result is stated with an explicit claim boundary: it says exactly what it does and does not guarantee (see below). The proofs use exact real arithmetic on finite periodic grids; the floating-point results (v0.6.0) are a first, deliberately narrow step across the gap toward real machine arithmetic. This is a Lean 4 library — package and namespace CourantKernel.

What is proved

Layer	Main result
Convex updates	Range, positivity, monotonicity, sup-norm, and conservation contracts
Signed upwind	Stability and mass preservation when ∣ν∣ ≤ 1 (the usual CFL condition)
Advection–diffusion	Stability when ∣ν∣ + 2μ ≤ 1
Harten interface	TVD from state-dependent incremental coefficients
Minmod scheme	TVD when 3 ∣a∣ Δt / Δx ≤ 2, periodic mass preservation, and an exact boundary family
Convergence	First-order global error bound with an explicit constant for signed upwind for any nonzero velocity a ≠ 0 on C² periodic data: ‖numerical − exact‖∞ ≤ (1+ν) ∣a∣ (n Δt) M Δx (this per-grid bound is itself the first-order convergence statement, being ≤ C·Δx at fixed final time), plus a corollary recording that the error ceiling (1+ν)∣a∣ T M Δx → 0 as Δx → 0⁺
Floating point	Conditional forward rounding-error bounds under the standard (1+δ) binary64 model (an assumed contract, not a theorem about any concrete float type): one computed upwind step differs from the exact-real update by ≤ γ₂(u)‖v‖∞ = ‖v‖∞/(2⁵²−1) (u = 2⁻⁵³, γ₃ variant for a runtime-rounded 1−ν); and n iterated computed steps differ from n exact-real steps by ≤ ((1+γ₂(u))ⁿ−1)‖v₀‖∞, i.e. ≈ n·γ₂(u)‖v₀‖∞ — linear in n to first order (while n·γ₂ ≪ 1; the exact envelope is geometric)

Here ν = ∣a∣ Δt / Δx is the dimensionless Courant number (a nonnegative magnitude — it matches the Lean definition courant = |a| dt / dx, so the factor 1+ν is correct for both signs of a), μ = D Δt / Δx² is the dimensionless diffusion number, and M bounds |u₀''| for the convergence result (u₀ ∈ C², periodic).

The library also includes zero-velocity and zero-time cases, small-grid edge cases, negative controls, and a public axiom audit.

Use as a dependency

Add Courant Kernel to a downstream Lake project's lakefile.toml:

[[require]]
name = "CourantKernel"
git = "https://github.com/demirelo/courant-kernel.git"
rev = "v0.6.0"

Then, in your own Lean file:

import CourantKernel
open CourantKernel

The library's reusable pattern is: define your own GridOperator, prove it OrderPreserving and TranslationEquivariant, and get SupNormNonexpansive for free from GridOperator.supNormNonexpansive_of_orderPreserving_of_translationEquivariant — no per-scheme sup-norm proof required. CourantKernel/Examples.lean works this pattern end to end on a small worked example (Examples.shiftForward, a periodic forward shift): it proves shiftForward_orderPreserving and shiftForward_translationEquivariant directly, then derives shiftForward_supNormNonexpansive from the spine theorem rather than reproving it from scratch.

Build and test

The repository pins Lean v4.31.0 and the Mathlib revision in the committed lake-manifest.json. On a fresh checkout, hydrate precompiled dependencies from that manifest:

lake exe cache get

The committed manifest is authoritative. Use lake update only when intentionally refreshing the dependency lock; inspect and review any resulting lake-manifest.json diff before committing it. If no compatible cache is available, build from the pinned sources with lake build --wfail.

Then run the full local gate:

lake build --wfail
while IFS= read -r -d '' test_file; do
  lake env lean -E warning "$test_file"
done < <(find Tests -type f -name '*.lean' -print0 | sort -z)
python3 tools/check_repo_contracts.py
python3 tools/check_axiom_manifest.py
python3 tools/check_methodology_events.py
python3 experiments/reproduce.py --check
python3 -m unittest -v experiments/test_reproductions.py
python3 -m unittest -v tools/test_check_repo_contracts.py
python3 -m unittest -v tools/test_check_axiom_manifest.py
python3 -m unittest -v tools/test_methodology_events.py

The warning-fatal build checks the library; the Tests/**/*.lean loop checks every acceptance module, including newly added modules; the three tools/test_*.py suites regression-test the checkers themselves. CI runs this same dynamically discovered Lean surface, the frozen contract checks, the numerical reproduction checks, and the checker test suites.

Repository guide

• CourantKernel/ — definitions and proofs
• Tests/ — signatures, behavior, boundaries, and axiom audits
• specs/ — scheme definitions, signed declaration bundles, source map, and prior art
• docs/THEOREM-INVENTORY.md — theorem groups and acceptance coverage
• docs/API.md — public API surface and layer map
• docs/REAL-VS-FLOAT.md — exact-real and floating-point boundary
• experiments/ — independent numerical reproductions

The Lake package and Lean namespace are CourantKernel.

Tests/R0Signatures.lean through Tests/R9Signatures.lean mechanically pin the public bundle types and definition bodies; the signed text bundles and their SHA-256 identities remain the statement-level source of truth.

Claim boundary

The upstream Lanyon repository publishes flux, wave, diffusion, and reconstruction components but not a complete time-stepping driver. Courant Kernel therefore certifies mathematical schemes reconstructed from those published components and explicit project choices. The exact mapping is in specs/SOURCE-MAP.md.

R6 certified a first-order per-grid error bound for the signed-upwind scheme at a > 0 on C² periodic initial data, with an explicit constant. The constant is not claimed to be sharp: the local Taylor-remainder step is within a factor 2 of the textbook M/2, but the assembled global constant ν(1+ν)M is looser still (for instance it does not vanish at ν = 1, where upwind is an exact grid shift with zero error). R7 extends this to a < 0 and unifies both signed branches: the bound holds for any nonzero velocity a ≠ 0, stated using |a|, subsuming R6's a > 0 result. Note this is a per-grid error bound ‖·‖ ≤ C·Δx with C independent of the grid — the standard meaning of first-order convergence — not a formalized limit theorem over a refinement family (the Δx → 0 corollary only sends the scalar bound to zero). See docs/THEOREM-INVENTORY.md (R6-CONVERGENCE v1, R7-CONVERGENCE-SIGNED v1), specs/R6-convergence.md, and specs/R7-convergence-signed.md for the exact statements and hypotheses.

R8 is the first result that touches floating-point execution, and it does so only conditionally: under the standard Higham (1+δ) rounding model — stated as a hypothesis over ℝ and assumed, not proved about Lean's Float, Mathlib's FP.Float, generated C, or hardware — one signed-upwind step (a>0, ν = courant a dt dx) deviates from the certified exact-real update by at most γ₂(u)‖v‖∞. It is one step, one cell, axiom-clean, and non-vacuous (the identity oracle inhabits the model). See docs/REAL-VS-FLOAT.md and specs/R8-float-bridge.md.

The project does not claim:

• equivalence to a complete generated solver;
• correspondence with generated C or IEEE-754 execution, or that any concrete float type satisfies the (1+δ) model R8/R9 assume;
• any unconditional floating-point guarantee: the R8 one-step and R9 n-step bounds hold only under the assumed (1+δ) model, are computed-vs-exact-scheme (not vs the true PDE solution), and are scoped to a > 0; they say nothing about overflow / underflow / subnormal / NaN behavior;
• accuracy order beyond first order, a sharp constant, convergence for a = 0 (the zero-velocity case is a trivial identity and is deliberately excluded), or convergence for any scheme besides signed upwind; or
• new numerical-analysis mathematics.

See the theorem inventory, source map, scheme specifications, and real-vs-float boundary for details.