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

The two categories in red are gaps a green blueprint graph hides:

consistent             all three agree; effectively machine-checked
kernel-refutes-claim   claimed/recorded proved, but the kernel says sorryAx / axiom
effective-gap          itself clean & claimed proved, but a DEPENDENCY is a hole
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

The headline is effective-gap: a node green in the blueprint and clean in its own #print axioms, but transitively resting on an unproved step. Blueprint green does not propagate; CKC's effective status does.

03Reconciled, live

The paper-igl formalization, reconciled across all three sources. Node colour is effective status; a red double ring marks a discrepancy. Click a claim to see its blueprint / history / kernel / effective 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 anything is shown proved but is effectively open
claimgraph audit blueprint/src/content.tex --project lean/
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 ↗