1.3. Generated facts and semantic facts🔗

Triptych can prove facts whose ingredients it generated. For example, it proves that decodeView agrees with the surface predicates and that parse is sound, complete, and rejecting exactly the invalid strings.

It cannot infer that an unrelated hand-written parser implements this grammar, or that a chosen serializer is canonical. A parser or explicit printer clause therefore emits small typed obligations. Once users prove those semantic facts, Triptych derives the larger API: external-parser views, parse/print roundtrips, injectivity, and normalization.

The Cedar examples provide concrete evidence for this division. The compiler generated the bookkeeping theorems; format proofs supply the Cedar-specific semantics; the final modules are checked without sorryAx.