Proof-Carrying Glyphs

A proof-carrying glyph is a small badge that says “there is a real proof behind this.” It carries the identifiers — a theorem id, a Lean declaration name, dictionary terms — needed to walk straight to the source of truth. The glyph is a handle, never a substitute for the proof it points at.

Lesson Goal

Learn what a glyph stores, what makes a glyph valid, and why the manifest and compiled Lean declaration always outrank the badge.

The Idea

A glyph is a little record:

glyph = { theorem_id, lean_name, dictionary_ids }

Projection facts let you read each field back out. A glyph is valid only when its theorem_id and lean_name match an actual entry in the theorem manifest — and that entry’s status is what decides whether the underlying claim is proved. A pretty diagram with no matching manifest entry is, by this rule, simply not certified.

This is the same discipline the whole book runs on, made into an object: the badge is convenient, but What “Proved” Means Here is the authority.

Worked Example

Suppose a glyph claims:

theorem_id = "P2G-T0001"
lean_name  = (the declaration recorded for P2G-T0001)

To trust it, you check the manifest: does P2G-T0001 exist, does its Lean name match the glyph, and is its status proved? If all three line up, the glyph is valid and you can follow it to the Lean source. If the manifest has no such id — or the names disagree — the glyph fails validation no matter how official it looks. The validity fact and the projection facts are exactly what the cards below certify.

Common Mistake

Glyphs and diagrams are not proofs. The proved layer covers certificate projections and finite metadata validity only; the Lean declaration and manifest remain the proof authority. See What “Proved” Means Here.

Checkpoint

A glyph shows a theorem-like diagram, but its theorem id is absent from the manifest. How should the Living Book treat it? (Answer: as not certified — an uncarried badge, not a proof.)

Source Trail

Paper source: Proof-Carrying Glyphs

Glyph Fixture

This fixture is generated from manifests/glyphs/proof_glyph_fixtures.yaml and resolved against theorem and dictionary data during site export.