Observation horizon: the local working tree, Lean 4.15.0, lake build and
lake test on 2026-09-07. These results do not establish remote CI, deployment,
a live Lithoglyph integration or whole-repository proof completeness. The current
machine-readable checkpoint is .machine_readable/descriptiles/STATE.a2ml.
-
src/Gnpl/contains an independent direct-evidence narration kernel, projection parser and versioned evidence importer;src/GnplMain.leanprovides the CLI. -
Accounts carry witnesses indexed by the exact evidence snapshot, focalization and requested assertions. Requested telling order is preserved.
-
Focalization checks supplied audience declarations. Evidence must be active, match the requested claim and meet the projection’s declared integer threshold.
-
A limited rival relation detects conflicting single-valued subject/slot values across two checked accounts. It neither searches for accounts nor picks a winner.
-
Hypothetical withdrawal re-evaluates the projection on a changed in-memory snapshot. The CLI preserves the original evidence file byte for byte.
-
The private substrate parses complete statements, validates inserts against a supplied schema, and supports its tested in-memory insertion/retrieval fragment. Its historical namespace is a compatibility detail, not a public language.
lake build passes. lake test passes five suites: the existing lexer, parser
and type-safety suites, 26 private-substrate checks and 35 narration checks.
The narration suite includes real CLI invocations, success and refusal paths,
rival accounts and both dependent and unrelated withdrawals.
Lean checks that withdrawn evidence cannot satisfy the direct-evidence support
rule and that a checked narration contains exactly the requested claims in their
order. test/NarrationProofAudit.lean is a default build target: Lean’s transitive
axiom report must remain [propext] for narrate and both theorems.
This establishes properties of the encoded rule. It does not establish external truth, authenticated provenance, persuasive reasoning or a portable proof certificate in the emitted JSON. The new kernel imports Lean/Std independently of the private substrate’s floating-point equality assumption.
The saved successful build log also passes scripts/check-lean-proofs.sh
--build-log. That diagnostic gate checks for incomplete proofs reported by Lean;
it does not establish an axiom-free repository. Historical totals in
docs/proof-debt.adoc predate the executable parser and insert-witness fixes.
-
Build the read-only Lithoglyph journal adapter and test withdrawal against a real store revision. See the integration contract.
-
Define additional warrant derivation rules before allowing inferred claims.
-
Add explicit event identity and partial-order/temporal semantics; current assertion order describes telling only.
-
Resolve confidence composition and account relations as language design questions. The current threshold does not settle PROMPT averaging or probabilistic interpretation.
-
Connect durable account storage and Glyphbase rendering with visible refusals.
The private pipeline still refuses attached-proof mode, persistent execution,
complete IR wire interchange and unchecked update/delete lowering. lake test
does not cover the separate FFI boundary. No FFI or remote CI result is asserted
by this checkpoint.
Repository initialisation also retains unresolved governance/security tokens in
REQUIRES_INITIALISATION.adoc. This implementation does not invent those values.
lake build
lake test
.lake/build/bin/gnpl narrate --evidence examples/narration/evidence.json --projection examples/narration/inspection.gnpl
.lake/build/bin/gnpl counterfactual --evidence examples/narration/evidence.json --projection examples/narration/inspection.gnpl --withdraw inspection-17The counterfactual command intentionally exits 1 with invalidated. Full surface,
JSON trust boundary and exit-code documentation: narration-slice.adoc.