3.4. Correctness of the switch🔗

The proof proceeds compositionally. Scanning a symbol, sequence, and production is proved equal to ordered search over the corresponding reference candidates. At the root, the continuation accepts only an empty suffix:

scanSymK_eq_matchSym : ∀ (g : Grammar) (qual : String) {α : Type} (fuel : Nat) (sym : Sym) (input : List Char)
  (k : CaptureMap → List Char → Option α),
  scanSymK g qual fuel sym input k =
    List.findSome? (fun result => k result.fst result.snd) (matchSym g qual fuel sym input)#check @Triptych.scanSymK_eq_matchSym
scanSeqK_eq_matchSeq : ∀ (g : Grammar) (qual : String) (fuel : Nat) {α : Type} (seq : Triptych.Seq) (input : List Char)
  (k : CaptureMap → List Char → Option α),
  scanSeqK g qual fuel seq input k =
    List.findSome? (fun result => k result.fst result.snd) (matchSeq g qual fuel seq input)#check @Triptych.scanSeqK_eq_matchSeq
scanProdK_eq_matchProd : ∀ (g : Grammar) (qual : String) (fuel : Nat) {α : Type} (production : Production)
  (input : List Char) (k : CaptureMap → List Char → Option α),
  scanProdK g qual fuel production input k =
    List.findSome? (fun result => k result.fst result.snd) (matchProd g qual fuel production input)#check @Triptych.scanProdK_eq_matchProd
scanSearch_eq_decode : ∀ (g : Grammar) (input : String), scanSearch g input = decode g input#check @Triptych.scanSearch_eq_decode
scan_eq_decode : ∀ (g : Grammar) (input : String), scan g input = decode g input#check @Triptych.scan_eq_decode

The last theorem is the behavioral replacement guarantee:

∀ grammar input, Triptych.scan grammar input = Triptych.decode grammar input

It covers successful captures, rejection, and ambiguous grammars where choosing the same first complete parse matters.