ScannerCorrectness.lean

259 theorems + 1,063 guards

Character-to-token correctness for all scanner operations

Completeness.lean

63 theorems

Valid YAML inputs are accepted

Soundness.lean

28 theorems

Output corresponds to valid grammar derivations

RoundTrip.lean

58 theorems + 63 guards

Parse-emit-parse cycle properties

Composition.lean

12 theorems

Scanner + parser pipeline correctness

ScannerEmitBridge.lean

12 theorems + 64 guards

Bridge between scanner emissions and grammar predicates

ParserSoundness.lean

12 theorems

Grammar-to-implementation correspondence

ParserWfaProofs.lean

50 theorems

Well-formed anchors through entire parser pipeline

ParserNodeProofs.lean

57 theorems

Anchor growth and alias resolution

ParserWellBehaved.lean

102 theorems

Flow nesting, token preservation, scannable properties

ScannerProgress.lean

24 theorems

Offset strictly increases on every scanner step

ScannerSimpleKey.lean

Multiple theorems

Simple key lifecycle well-formedness

ScannerDispatch.lean

Multiple theorems

Dispatch pipeline preserves all invariants