# Calculemus artifacts — the downloadable underpinnings

These are the **exact, kernel-checked** source files behind the work-log cycles — published here so the
fundamental underpinnings are **publicly auditable**, independent of any private repository. Each file linked
from a cycle's *"Re-runnable artifacts"* section is served verbatim from this directory, with its SHA-256 shown
on the page so you can confirm you have the byte-identical artifact that was verified.

## How to re-verify (Lean certificates)

Toolchain: **`leanprover/lean4:v4.31.0`** + a matching **Mathlib**. Two ways:

1. **Lean REPL / `lake env lean`.** Drop the file into a Lean 4.31 project with Mathlib as a dependency and
   elaborate it. A clean run reports **0 errors, 0 sorries**. Append `#print axioms <name>` for any theorem to
   see its axiom footprint — a genuine certificate depends only on the standard axioms
   `[propext, Classical.choice, Quot.sound]` (some, like the Problem-41 certificate, are fully computational and
   depend on **no axioms at all**).
2. **`lake build`.** Place the file in a project's source tree and `lake exe cache get && lake build`; a clean
   build is the kernel's acceptance.

Each file carries a header stating its imports and the expected verdict. The value being audited is the *proof
object*, not a number: the same statement checked by an independent Lean 4.31 kernel yields the same verdict.

## Provenance

Each artifact's SHA-256 is recorded on its cycle page and in the published ledger
(`ledger/calculemus.json`). The source repository and exact commit/PR that produced each file are listed in the
cycle's *"Repositories — the code trail"* section. Where that repository is private, **this public copy is the
authoritative, auditable artifact.**