3.5. Mind the Fibration Gap🔗

When you read "this theorem is machine-checked," two follow-up questions are worth asking:

How significant is this theorem? Is it a deep statement about how the code behaves, or a shallow observation about the code's shape?
Would this theorem break if we changed the code? If a refactor silently broke the parser, would the kernel catch it — or would the theorem quietly survive the change?

These are not philosophical questions. They have a mechanical, kernel-objective answer that is read directly off the proof term the kernel has already accepted. The answer comes from stitching together two natural bipartite graphs —

the function call graph (f calls f'), and
the theorem dependency graph (T cites T' in its proof) —

using the about relation (the theorem T mentions the function f in its type) as the bridge between them. A theorem that threads all three relations tightly together is said to fibrate over the call graph; one that does not leaves a fibration gap.

Two natural fibrations run through every proof module, corresponding to the three relations above:

The "about" fibration — each theorem projects to the set of project functions mentioned in its type. This is what #about_functions reports.
The "uses" fibration — each theorem projects to the set of other project theorems cited in its proof term. This is what #proof_deps reports.

A theorem is deep when the two fibrations align: the lemmas cited in its proof are themselves about the callees of the functions the root theorem is about. The FGM.ExploreGraph.findFunctorialChains analyzer walks this alignment one step at a time, and the ChainDepth classifier tags the result as deep, propBridge, weak, or noAbout.

3.5.1. Why Fibration Matters: The Canary Theorem🔗

A deeply fibrated theorem acts as a canary. Because its proof term cites specific lemmas about specific callees, any code change that invalidates the underlying behaviour invalidates those lemmas, which invalidates the theorem, which the kernel then refuses to re-accept. The build breaks at the theorem that pinned the claim, pointing directly at the layer of the pipeline whose behaviour has shifted. The deeper the fibration, the more callees are pinned, and the more sensitive the canary.

A weak, unfibrated theorem gives no such signal. Because its proof never descends into the callees, it can survive code changes that genuinely affect parser behaviour. parse_sound_shallow is a working example: its statement asserts only that some token stream exists for which the pipeline decomposition equation holds — it says nothing about which tokens came out of the scanner, nor what the parsed documents actually contain. A refactor that shuffles the parser's internal decision tree, or silently corrupts the emitted document content, can leave parse_sound_shallow intact and the kernel silent. Strong behavioural guarantees must come from somewhere else — from the underlying parser-correctness lemmas, or from a canary like parse_sound_deep that explicitly cites them.

This does not mean structurally weak theorems are worthless. They may still carry value — as witnesses that two definitions are definitionally equal, as type-class coherence lemmas, as rewriting hints, or as quick sanity checks on API shape. Those uses are legitimate, but they answer a different question than fibration does. For the specific question "does this theorem catch breaking code changes?", the fibration structure is the right instrument, and it is the one this document measures.

3.5.2. The Alignment Rule🔗

A chain link (T, f) — a root theorem T paired with a function f that T is about — extends to (T', f') iff all three conditions hold:

T' ∈ thmDeps(T) — T' is a project theorem cited in the proof term of T
f' ∈ about(T') — the type of T' mentions f'
f' ∈ fnDeps(f) — f's body calls f'

Informally, the square

     T  --uses-->  T'
     |              |
   about          about
     v              v
     f  --calls--> f'

must commute. Each arrow corresponds to one edge colour in the bipartite graph — green for uses, blue for calls, purple for about. Alignment requires three simultaneous edges at every step, which is exactly categorical base-change: the functorial chain is the lifting of the call-graph path f → f' along the about-fibration, guided by the proof-chain T → T'.

3.5.3. What Breaks Alignment🔗

Prop-wrapping — stating the theorem as … → SomeProp args pushes the about-fibration into the definition body of SomeProp. collectAbout only inspects the raw type, so the analyzer sees SomeProp as a single opaque target. The three-way alignment collapses before step 1.
Tactic-only proofs — unfold; split; injection, rfl, grind, decide, and friends produce proof terms with no project-theorem citations. Condition 1 fails trivially and no chain extends.
Co-location — citing only lemmas that are about the same top-level function the root is about. The alignment square collapses to the identity on the function side: condition 3 fails because no new call edge is exposed.

3.5.4. The Engineering Rule🔗

When engineering a headline theorem intended for dependency-analysis consumption:

Expose the fibration in the type. Name the pipeline functions explicitly in the statement; avoid Prop-wrappers that hide them.
Cite lemmas about callees. Every project lemma used in the proof should itself be about a function that is a strict callee of the function the root theorem is about.
Prefer a step-wise proof over a tactic blob. Each have ⟨…⟩ := lemma … contributes one functorial step; each uncited unfold/split/grind discards one.