3.6.1. parse_sound_shallow — fibration-hidden🔗

theorem parse_sound_shallow (input : String) (docs : Array YamlDocument)
    (h : TokenParser.parseYaml input = .ok docs) :
    ValidYamlProp input docs

• Type mentions parseYaml, YamlDocument, ScanError, and ValidYamlProp. The pipeline stages (scanFiltered, parseStream, YamlDocument.compose) are hidden inside the existential body of ValidYamlProp.

• Proof is four tactics: unfold; split; injection; …. No project theorem is cited.

• Consequence: condition 1 of the alignment rule fails at every root function, so the chain walker returns zero functorial chains. The ChainDepth classifier tags this theorem propBridge — recognisable by its Prop-typed target — and renders a diagnostic overlay labelled "NOT proof deps of the headline."

3.6.2. parse_sound_deep — fibration-aligned🔗

theorem parse_sound_deep (input : String) (docs : Array YamlDocument)
    (h : TokenParser.parseYaml input = .ok docs) :
    ∃ (tokens : Array (Positioned YamlToken))
      (raw_docs : Array YamlDocument),
      Scanner.scanFiltered input = .ok tokens ∧
      TokenParser.parseYamlRaw input = .ok raw_docs ∧
      TokenParser.parseStream tokens = .ok raw_docs ∧
      docs = raw_docs.map YamlDocument.compose ∧
      (∀ doc ∈ docs.toList, ∃ node : ValidNode,
         stripAnnotations (toYamlValue node) = stripAnnotations doc.value)

• Type mentions parseYaml, parseYamlRaw, parseStream, scanFiltered, YamlDocument.compose, toYamlValue, and ValidNode directly. Every pipeline stage is a first-class citizen of the about-fibration.

• Proof cites parseYamlRaw_ok_decompose (about parseYamlRaw, scanFiltered, parseStream) and parseYaml_produces_valid_nodes (about parseYaml, toYamlValue), the second of which transitively drags in parseStream_output_grammable (about parseStream).

• Consequence: conditions 1, 2, and 3 of the alignment rule close simultaneously at multiple root functions. The ChainDepth classifier tags this theorem deep.

3.6.3. Chain-Analysis Confirmation🔗

Running the FGM theoremgraph tool in --chain mode on both theorems produces the following metrics (tool output captured on 2026-04-24).

The proof-dep theorems surfaced on parse_sound_deep are:

• parseYamlRaw_ok_decompose (module Composition) — splits a successful parseYamlRaw into a successful scanFiltered step and a successful parseStream step

• parseYaml_produces_valid_nodes (module ParserGrammable) — bridges parseYaml success to per-document ValidNode witnesses

• parseStream_output_grammable (module ParserGrammable) — guarantees every parseStream-produced document is grammable

Each of these is about a strict callee of parseYaml, so the alignment square closes at every step of the descent:

parse_sound_deep --uses--> parseYamlRaw_ok_decompose --uses--> parseStream_output_grammable
         |                          |                                  |
       about                      about                              about
         v                          v                                  v
     parseYaml --calls--> parseYamlRaw --calls--> parseStream

parse_sound_shallow's chain graph, by contrast, is a diagnostic overlay: it enumerates the catalogue entries that would be relevant if the alignment existed, and the legend explicitly labels those nodes "NOT proof deps of the headline." The absence of any uses or calls edge is the fibration gap made visible.

Takeaway: a theorem passing the kernel is a statement about correctness; a theorem passing the chain walker is additionally a statement about traceability. The two are not the same. The deep / propBridge / weak / noAbout classification in FGM.TheoremGraph is the knob that surfaces this distinction across the catalogue.