3.7. Dependent continuation🔗

Fixed grammar boundaries are not enough for formats whose header determines the payload shape. Triptych now supports two increasingly general cases.

The public dependent-width form handles one final payload after a literal delimiter:

Graph ::= Order ":" Cells
Order ::= digit+
Cells ::= bit{upperTriangleSize Order}

The delimiter fixes where Order ends and Cells begins. Triptych scans the ordinary lexical grammar and generates cells.length = upperTriangleSize order as an intrinsic well-formedness condition. Because this path stays inside the ordinary generator, it receives the normal readable predicates, typed view and derivation, parser contracts, and cost theorem.

The more general architecture API Triptych.scanDependent scans a header prefix, passes the resulting captures to a tail-grammar function, and requires that generated grammar to consume the remaining input.

For example, the Graph6 architecture example decodes the one-, four-, or eight-character vertex count header and constructs a payload grammar whose exact width is ceil(n(n-1)/2 / 6). The payload still runs through the ordinary verified scanner; the dependent combinator changes which ordinary grammar is selected.

The proof follows the same reference/implementation pattern as the flat scanner:

scanDependent_eq_decodeDependent : ∀ (header : Grammar) (body : CaptureMap → Grammar) (input : String),
  scanDependent header body input = decodeDependent header body input#check @Triptych.scanDependent_eq_decodeDependent
scanDependent_isSome_iff : ∀ (header : Grammar) (body : CaptureMap → Grammar) (input : String),
  (scanDependent header body input).isSome = true ↔ DependentAccepts header body input#check @Triptych.scanDependent_isSome_iff
dependentScanProfile_result : ∀ (header : Grammar) (body : CaptureMap → Grammar) (input : String),
  (dependentScanProfile header body input).result = scanDependent header body input#check @Triptych.dependentScanProfile_result
dependentCandidateChecks_le : ∀ (header : Grammar) (body : CaptureMap → Grammar) (input : String),
  (dependentScanProfile header body input).headerCandidateChecks +
      (dependentScanProfile header body input).tailCandidateChecks ≤
    dependentCandidateBudget header body input#check @Triptych.dependentCandidateChecks_le

The first theorem preserves the source-ordered reference result. The second characterizes recognition independently of which successful captures are selected. The final two connect the executable result to a profile and bound all completed header and tail candidates.

This staged form remains an architecture API. It is required when accepting or rejecting a tail must make the parser try a different header candidate, as in Graph6's one-, four-, and eight-character header alternatives. The triptych command does not yet generate the combined view and derivation artifacts for that general case.