Pinned external evidence · 10 October 2026

Know what this check establishes.

Independent, source-pinned observations of the L4YAML parser. The finite results are reproducible. Broader correctness remains an explicit open question.

52 source-bound Lean guards passed Universal theorem: UNKNOWNNo project endorsement
48/48
Independent YAML case decisions matched
31 accepts / 17 rejects
52/52
Pinned Lean executable guards passed
4 targeted extra controls
UNKNOWN
Universal source-to-parser equivalence
Not established by this record

Exactly what was checked

MathGraph replayed a fixed independent YAML test set against the original, pinned Lean parser function and separately checked the upstream source's named serialization lemmas. Its prior compiled command-line run remains an independent historical observation.

External test-suite acceptance48/48 REPLAYED
Lean executable source guards52/52 PASSED
Known cyclic-anchor behaviorSCOPED DISTINCTION
Whole YAML language correctnessUNKNOWN
Natural-language statement fidelityUNKNOWN
Requalification against future commitsNOT CHECKED
An important distinction. The input &x [*x] is accepted by the restricted early-anchor event model but rejected by this pinned version of L4YAML. This difference was already documented by its contributors. The correspondence from all possible YAML inputs to event traces is not proved here.