3.6. Formal search-cost evidence🔗

The proof-only scanner profile returns the parser result together with the exact number of completed root candidates tested by the search phase:

scanProfile_result : ∀ (g : Grammar) (input : String), (scanProfile g input).result = scan g input#check @Triptych.scanProfile_result
scannerCandidateChecks_le : ∀ (g : Grammar) (input : String),
  scannerCandidateChecks g input ≤ scannerCandidateBudget g input#check @Triptych.scannerCandidateChecks_le
scannerCandidateChecks_eq_zero_of_fastScan : ∀ (g : Grammar) (input : String),
  g.staticUnique = true →
    ∀ {captures : CaptureMap}, fastScan g input = some captures → scannerCandidateChecks g input = 0#check @Triptych.scannerCandidateChecks_eq_zero_of_fastScan
Decimal.parse_profile_result : ∀ (s : String),
  (scannerParseProfile Decimal.grammar Decimal.constraints Decimal.valueExpr Int64.ofInt s).result = Decimal.parse s#check @Decimal.parse_profile_result
Decimal.parse_candidateChecks_le : ∀ (s : String),
  (scannerParseProfile Decimal.grammar Decimal.constraints Decimal.valueExpr Int64.ofInt s).candidateChecks ≤
    scannerCandidateBudget Decimal.grammar s#check @Decimal.parse_candidateChecks_le
Decimal.parse_candidateChecks_eq_zero_of_fastScan : ∀ (s : String),
  Decimal.grammar.staticUnique = true →
    ∀ {captures : CaptureMap},
      fastScan Decimal.grammar s = some captures →
        (scannerParseProfile Decimal.grammar Decimal.constraints Decimal.valueExpr Int64.ofInt s).candidateChecks = 0#check @Decimal.parse_candidateChecks_eq_zero_of_fastScan

These theorems establish three facts:

profiling does not describe a different parser;
every generated parse stays within the finite candidate-tree budget; and
a successful certified fast scan performs zero complete-candidate backtracking.

This is a formal search guarantee, not a blanket linear-time theorem. Ambiguous grammar choices can still yield an exponential candidate tree, and user-supplied value' or constraints' functions can perform arbitrary work. For a fixed deterministic generated grammar, the fast path avoids root-candidate backtracking; wall-clock time and allocation remain properties measured by benchmarks rather than hidden inside the theorem statement.