-
Executable private parser and schema validation, with explicit refusals where persistence, proof checking and interchange remain incomplete.
-
Direct-evidence narration: typed accounts and warrants, focalization, declared telling order, a limited rival relation and hypothetical withdrawal.
-
A
.gnplprojection surface, versioned evidence import and executable CLI. -
Five passing Lean suites, including acceptance and rejection controls.
-
Two checked narration properties and a default-build transitive axiom audit.
Implement a read-only Lithoglyph adapter for the snapshot contract. Demonstrate an account over real stored evidence, invalidate it after a cited withdrawal, and preserve it after an unrelated withdrawal. Preserve revision identity and historical accounts. See the integration contract.
-
Checked derivation chains with named inference rules and compositional warrant.
-
Event identity and partial-order/temporal semantics, separate from telling order.
-
Richer account relations, with the intended argumentation semantics explicit.
-
A justified confidence-composition policy; declared integer thresholds do not settle PROMPT averaging, probability or epistemic entrenchment.
Each extension needs an acceptance case, a meaningful refusal case and a precise proof obligation. Keep useful selection and storage operations as private machinery; no additional public language or fixed lowering target is assumed.