Using this almanac by hand

This is a complete record of one small mathematical result: the informal proof a mathematician would read, a computer program that computes with the objects, and a machine-checked formal proof — together with a per-claim account of what actually warrants each one.

If you only want to look, open index.html in any browser. It is fully self-contained, works offline, and is the right starting point. This file is for when you want to check things yourself.

Part 0 — What to read first, in order

The single most important idea in this almanac: the concordance's warrant field. It records, per result, what certifies it — and the values are not interchangeable:

• — an argument written out for a human reader and refereed, pinned to a hashed document at a named location. A warrant in its own right, not the absence of one: it is what the other two are checked against. None of eleven results, in this edition.
• — verified by computation over a stated bound, and over nothing else. The bound is part of the claim. Two of eleven results.
• — a proof assistant's kernel checked a proof of that statement, and the axioms it used were measured to be exactly the three standard ones. Nine of eleven results.

A green result of one kind is never quietly upgraded into another. That discipline is the point of the edition.

Part 1 — Checking the files are intact (5 minutes, with tools already on your machine)

Every file's fingerprint is listed in CHECKSUMS.txt.

macOS:

cd almanacA0a
shasum -a 256 -c CHECKSUMS.txt

Linux:

cd almanacA0a
sha256sum -c CHECKSUMS.txt

Windows (PowerShell):

cd almanacA0a
Get-Content CHECKSUMS.txt | Where-Object { $_ -notmatch '^#' } | ForEach-Object {
  $h,$f = $_ -split '\s+',2
  if ((Get-FileHash $f -Algorithm SHA256).Hash -ieq $h) { "OK   $f" } else { "FAIL $f" }
}

Every line should say OK. If a line fails, the file has been altered since assembly — the almanac is still readable, but stop trusting that file until you know why.

DIST_MANIFEST.json additionally records, per file, whether its bytes matched the edition's own manifest at assembly time, and its build_class says whether every file matched. Read that there rather than here. This page is written once and travels with every build, so it cannot know which one you are holding; a number printed here would be true of at most one of them. A build with any mismatch says so on its own front page, and one with none says nothing, because there is nothing to say.

Part 2 — Installing the software

You need three things, and you only need the ones you actually want to use. The checks are independent: Lean alone suffices for the formal proofs, and Julia alone for the computations.

2.1 Python 3 — for the almanac's own scripts (almost certainly already installed)

python3 --version        # anything 3.8+ is fine

• macOS: ships with it; or brew install python
• Linux: sudo apt install python3 (Debian/Ubuntu) / sudo dnf install python3 (Fedora)
• Windows: install from https://www.python.org/downloads/ and tick "Add python.exe to PATH"

Optional, only for validating the Palomar disclosure file against its published schema:

python3 -m venv .venv
.venv/bin/pip install pyyaml jsonschema        # Windows: .venv\Scripts\pip install ...

2.2 Lean 4 — to re-check the formal proofs yourself

Lean is installed through elan, a version manager. Never install a Lean version directly: this almanac is pinned to an exact toolchain, and elan is what makes the pin work.

macOS / Linux:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
# then restart your shell, or:
source $HOME/.elan/env
elan --version

Windows (PowerShell):

curl.exe -sSf -o elan-init.ps1 https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1

The exact pins this almanac was certified against:

elan toolchain install leanprover/lean4:v4.30.0

Be warned about size and time. A Mathlib-dependent Lean project downloads several gigabytes of prebuilt artifacts, and building from source instead can take hours. Always fetch the cache first (lake exe cache get) rather than compiling Mathlib yourself.

One command rebuilds every proof and prints the axioms each one used:

cd almanacA0a/edition/replay
./replay.sh

It fetches the pinned Mathlib, builds the proofs, runs #print axioms on all 31 certified declarations, writes the transcript to replay_axioms.txt, and ends in PASS or FAIL. A build that succeeds is not a proof that anything is certified — the axiom lines are, which is why the script fails on any sorryAx or any axiom outside [propext, Classical.choice, Quot.sound] even when the build is clean.

replay/ carries the complete transitive closure — 17 modules, 5,344 lines, including the rank-1 modules the seven certified ones import — together with lakefile.toml, lean-toolchain and lake-manifest.json, so every revision is pinned and nothing is fetched from this project. replay/SOURCES.json lists each module with the sha256 of the record file it was copied from.

source/lean/ is the reading copy — the same seven certified modules, flat and without directories, for opening one at a time. It is not buildable and is not meant to be: use replay/ to rebuild, source/lean/ to read. source/record/formal/RELEASE_20260721_source_all_clean.log is the certification log from the original run of record, for comparison against what your own replay prints.

2.3 Julia + OSCAR — to run the computational instrument

Install Julia via juliaup:

macOS / Linux:

curl -fsSL https://install.julialang.org | sh
# restart your shell, then:
julia --version

Windows:

winget install julia -s msstore

The pins:

Run the instrument's own test battery (this is the honest check — the outcome is a plain pass or fail):

cd almanacA0a/edition/source/instrument
julia --project=. -e 'using Pkg; Pkg.instantiate(); Pkg.test()'

Expected: 87 of 87 tests pass. The first run installs OSCAR and its dependencies and is slow — budget 20–40 minutes and several GB. Later runs take seconds.

Manifest.toml is the real pin — it records exact resolved versions. Project.toml only states compatible ranges. If you want the exact environment that was certified, keep Manifest.toml.

Part 3 — Checking the mathematics yourself

3.1 Read the statement, then decide whether it is the statement you care about

This is the step no software can do for you, and it is the one that matters most. Open source/informal/goalv0a.pdf — the signed goal — and source/informal/proofv0a.pdf — the proof.

A crucial warning about notation. The Lean files were written before a notation change and use older symbols than the manuscripts:

The sources keep their original bytes deliberately, because the signed goal's fingerprint is part of the closure record and survives only while every byte stays put. To bridge the notations, every concordance row carries the convention frame telling you how to read it. If you skip that field you will misread the Lean.

3.2 Check the axioms of a formal result

Each certified row in CONCORDANCE.json names a Lean declaration and records the axioms measured for it. Inside a working copy of the full Lean development:

#print axioms HybridQuantumLean.A1.GL1Newton.clause_i

What you should see: exactly [propext, Classical.choice, Quot.sound] — the three standard axioms of Lean's kernel — propositional extensionality (propext), the axiom of choice (Classical.choice) and quotient soundness (Quot.sound) — the base every Mathlib proof shares; a certificate is clean when these three are all it needs.

What must never appear: sorryAx (an admitted gap) or Lean.ofReduceBool (a proof by compiled evaluation). Either one means the result is not certified, whatever else is green.

3.3 Understand exactly what a certificate covers

A kernel certifies the Lean statement, and nothing else. It does not tell you the Lean statement faithfully expresses the mathematics — that is a human judgement, and it is precisely what the concordance and the convention frames are there to let you make. EMBEDDING_NOTE.md sets out what the computational layer does and does not establish; it is deliberately not a certificate.

Part 4 — If something goes wrong