CKC × Lean Blueprint

The cross-history honesty layer

A Lean Blueprint is the standard way to track a formalization. CKC does not replace it. CKC points at your blueprint and reconciles it against two other sources of truth, surfacing exactly where they disagree.

01Three readings of one claim

Every formalized claim is described three times, by three fallible sources:

Blueprint \leanok

What the author claims is formalized. A manual flag (even LeanArchitect's auto-flag is only direct, not transitive). checkdecls never checks the kernel.

Commit Status:

What the git history recorded, over time. Append-only, and it can overclaim.

#print axioms

Kernel reality: clean / sorryAx / axiom, read by axiom-report. Ground truth, but silent on intent and history.

CKC unifies a claim's blueprint \label, its Lean FQN(s), and its registry slug onto one node, attaches the three readings, computes the transitive effective status, and classifies the agreement.

02The discrepancy taxonomy

CKC keeps two questions apart. Validity — does the claim hold? — is decided by the kernel. Coverage — is every concept it is built on actually formalized? — is decided by the \uses graph. They are orthogonal:

consistent             all readings agree; machine-checked, fully covered
kernel-refutes-claim   VALIDITY gap: claimed/recorded proved, but the kernel says sorryAx / axiom
blueprint-incomplete   COVERAGE gap: machine-checked, but it \uses an UNFORMALIZED concept
undocumented           kernel-clean & blueprint-proved, but no commit recorded it
stale-blueprint        commit + kernel proved, but not marked \leanok
paper-only             no Lean yet: a paper-level statement

Only kernel-refutes-claim is a real validity gap (the honesty gate fails on it). blueprint-incomplete is a coverage signal, not a hole: the theorem is genuinely machine-checked — #print axioms already certifies its full logical closure — it just \uses a concept the blueprint never formalized. A \uses to a prose definition is expository, not a logical dependency, so it never drags a clean theorem's validity down.

03Reconciled: the Four Colour Theorem

An illustrative blueprint for the machine-checked Four Colour Theorem (Gonthier & Werner, Coq, 2005), reconciled against its CKC commit history — from Guthrie's conjecture through Kempe's and Tait's refuted proofs to the kernel-checked result. This is a two-source view: blueprint \leanok vs commit Status:. The kernel column is left ungrounded here (the proof is in Coq; no #print axioms was run). Node colour is effective status; click a claim to compare its readings.

04Run it on your blueprint

Nothing to re-author. Point CKC at the blueprint you already keep:

# import + ground a blueprint against the kernel
claimgraph blueprint blueprint/src/content.tex --project lean/

# reconcile blueprint + commit history + kernel, and report disagreements
claimgraph reconcile blueprint/src/content.tex . --project lean/

# a CI honesty gate: fail if the kernel refutes a claim shown proved (a validity gap)
claimgraph audit blueprint/src/content.tex --project lean/
# --strict also fails on coverage gaps (machine-checked, but uses an unformalized concept)
claimgraph audit blueprint/src/content.tex --project lean/ --strict
Not a competitor. Keep authoring your blueprint with leanblueprint or LeanArchitect. CKC is the layer on top: it reconciles that blueprint against the commit history and the kernel, and reports where author intent, recorded history, and machine reality come apart.
See the standalone graph → The proof profile ↗