From 68122616008829317cc440ba3b13187d11233747 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 29 Jul 2026 08:26:53 +0100 Subject: [PATCH] docs: bring the repo's account of itself in line with what is true MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Documentation pass for humans and for machines. Everything here was measured or path-checked; nothing is asserted. ## Machine-readable `.machine_readable/6a2/STATE.a2ml` was stale and partly corrupt: it named the project "gql-dt", was dated 2026-02-01, claimed 45% completion, listed already-completed milestones ("Create bridge/lith_types.zig", "Begin Milestone 6") as CRITICAL NEXT ACTIONS, and its `purpose` field held a fragment of a build error — "References to removed .tracked and .confidence constructors" — rather than a purpose. Rewritten with measured figures, plus sections that did not exist: [verification] naming each gate and its result, [caveat] stating that a green proof gate does not mean nothing is assumed, [history-landmines] recording the squash-extract and the sweep branches, and [evidence] giving the command that reproduces every claim. `0-AI-MANIFEST.a2ml` identified the repo as "GQL-DT / Dependently-Typed Glyph Query Language". It is GNPL; GQLdt is the layer beneath. Corrected, and the purpose now states the two-layer structure explicitly so an agent reading it does not conclude the `GqlDt` namespace is a mistake. Its `canonical-locations` block was worse: **all six paths were dead**. The .scm state/meta/ecosystem/roadmap files were converted to .a2ml under `.machine_readable/6a2/` and never repointed, and neither `AI.a2ml` nor `justfile` has ever existed here. Replaced with 20 paths, each verified to exist, plus an (evidence) block and a (caveat-for-agents) warning against reporting this repository as "verified" on the strength of a green build. ## Human-readable `docs/STATE-OF-PLAY.adoc` (new) — the human twin of STATE.a2ml. What is established and *by which command*, the gates and why they are trusted (each was canary-tested), what is known missing, the two open decisions, and the sequencing. It also lists the four gates this repo has shipped and removed that could not fail, because that history is the reason the standard is what it is. `docs/proof-debt.md` §(b) said this repo has "no executable test coverage" and that adding a `@[test_driver]` was "a prerequisite for moving any item into this section". That prerequisite is now met — 163 checks. Corrected, while keeping the section empty: coverage existing is NOT the same as a given axiom being covered, and the policy wants a citable refutation budget. D4's entry updated likewise — its blocker is no longer "no coverage at all" but "this path is not property-tested", which is a materially different and now-reachable problem. `README.adoc` links both new documents from the design-documents table. No code changes; `lake test` still 163/163. Co-Authored-By: Claude Opus 5 --- .machine_readable/6a2/STATE.a2ml | 118 +++++++++++++++++------ 0-AI-MANIFEST.a2ml | 67 ++++++++++--- README.adoc | 9 ++ docs/STATE-OF-PLAY.adoc | 155 +++++++++++++++++++++++++++++++ docs/proof-debt.md | 32 +++++-- 5 files changed, 333 insertions(+), 48 deletions(-) create mode 100644 docs/STATE-OF-PLAY.adoc diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index f3a0556..38e7c9a 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -1,50 +1,116 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# STATE.a2ml — Gql Dt project state +# STATE.a2ml — hyperpolymath/gnpl project state +# +# Rewritten 2026-07-28. The previous revision was stale and partly corrupt: it named the +# project "gql-dt", was dated 2026-02-01, listed already-completed milestones as critical +# next actions, and its `purpose` field held a fragment of a build error rather than a +# purpose. Every figure below is measured, not estimated; see [evidence]. + [metadata] -project = "gql-dt" -version = "0.2.0" -last-updated = "2026-02-01" +project = "gnpl" +version = "0.3.0" +last-updated = "2026-07-28" status = "active" -session = "converted from scheme — 2026-04-11" +session = "proof-debt foundation; PRs #6 #7 #8 merged" [project-context] -name = "Gql Dt" -purpose = """References to removed .tracked and .confidence constructors, missing API updates""" -completion-percentage = 45 +name = "GNPL" +purpose = """ +GNPL is Lithoglyph's narration/projection language: it turns an evidence base into an +account — for forensic histories, counterfactual paths, plural meanings, and +synchronic/diachronic evidence interpretation. Where a query language answers "what is +true in the store?", GNPL answers "what account does this evidence support, told from +whose stance, with what warrant, and what rival accounts does the same evidence also +support?". + +It is built as a layer ON TOP OF GQLdt in this repository and lowers to it: +GNPL (what account) -> GQLdt (what is) -> Zig FFI -> Lithoglyph (the store). +This is why sources are namespaced GqlDt in a repository named gnpl. +""" +completion-percentage = 40 [position] phase = "partial-implementation" # design | implementation | testing | maintenance | archived -maturity = "experimental" # experimental | alpha | beta | production | lts +maturity = "experimental" # experimental | alpha | beta | production | lts + +[layers] +# Two layers, one repo. Nothing is being extracted or discarded. +gqldt = "built and tested — the extensional query core, src/GqlDt/" +gnpl = "design only — docs/THEORY.adoc + docs/LITHOGLYPH.adoc; no src/Gnpl/ yet" + +[verification] +# What is actually established, and by what. A gate that has never gone red is not +# evidence; both gates below were canary-tested in both directions. +lean-build = "pass" # lake build, 34/35 targets +lean-tests = "pass" # lake test, 163 checks, 3 suites +lean-test-count = 163 +lean-test-suites = ["lexer_test", "parser_test", "type_safety_test"] +zig-bridge-build = "pass" # cd bridge && zig build && zig build test +incomplete-proofs = 0 # Lean reports no `sorry` +trusted-base-axioms = 16 # `axiom` does NOT trigger Lean's sorry warning +trusted-base-doc = "docs/proof-debt.md" +gates-canary-tested = true + +[caveat] +# The single most important thing for a machine reading this file to carry forward. +note = """ +A green proof gate here means "nothing is admitted mid-proof". It does NOT mean "nothing +is assumed". Lean 4 emits `declaration uses 'sorry'` for sorry/sorryAx only — `axiom` +produces no warning at all. This repository declares 16 axioms, all stubs, none necessary +in the trusted-base-policy sense. FIVE are in EXECUTABLE position (parseToIR, +deserializeIR, many, many1, sepBy) and therefore have no implementation: code calling them +typechecks and cannot run. So "34/35 targets build" is a claim about TYPECHECKING, not +about a working parser. Read docs/proof-debt.md before relying on any verification claim. +""" [route-to-mvp] milestones = [ - # No milestones recorded + "DONE 2026-07-21 — identity: repo established as GNPL-over-GQLdt; licence restored to MPL-2.0", + "DONE 2026-07-21 — design: docs/THEORY.adoc (the general case) + docs/LITHOGLYPH.adoc (the tethered case)", + "DONE 2026-07-27 — dead code: two pre-0.15-API Zig trees removed; bridge/ is the only one", + "DONE 2026-07-28 — foundation: lake test wired, 163 checks, suites can fail", + "DONE 2026-07-28 — lexer conformance: 19 spec defects fixed (peek off-by-one)", + "NEXT — proof debt D1: delete or prove executePreservesTypes (currently vacuous)", + "NEXT — proof debt D3: construct the six asserted PromptScores examples (gated on averaging decision)", + "THEN — proof debt D2: implement many/many1/sepBy, unblocking four parse* axioms", + "THEN — src/Gnpl/ skeleton: Fabula, Projection, Focalization, Account, Warrant", ] [blockers-and-issues] issues = [ - # No blockers recorded + "DECISION NEEDED — averaging rule for PROMPT scores. PromptScores carries a proof field, overall_correct : overall.val = (sum)/6, so the arithmetic mean is welded into the TYPE. Changing it is a proof-obligation change on every value, in Lean and Zig simultaneously. Gates proof-debt D3.", + "DECISION NEEDED — flake.nix vs guix.scm. Estate policy: Guix primary, Nix fallback, satisfying NEITHER is the violation. This repo has no guix.scm, so flake.nix is the only artefact satisfying it; removing it without a verified guix.scm turns Governance red.", + "UPSTREAM hyperpolymath/standards#516 — Hypatia setup-beam pin cannot map ImageOS=ubuntu24; scanner never runs for any caller. Only red on gnpl main.", + "UPSTREAM hyperpolymath/standards#486 — governance/Allowlist Preflight cannot resolve allowed-actions.json (the file EXISTS; path resolution after sparse-checkout). standards' own main is red on it too.", + "UPSTREAM hyperpolymath/standards#520 — scorecard.yml template violates the estate SARIF policy as distributed.", + "NO test coverage for the FFI boundary — ffi_test is excluded from lake test because it links liblith_bridge.a; it is covered only by the zig-ffi CI job.", ] [critical-next-actions] actions = [ - "Update Dockerfile for Lean 4 + elan", - "Add CI workflow for lake build", - "Start Milestone 5: Zig FFI Bridge", - "Create bridge/lith_types.zig", - "Complete Milestone 5 (Zig FFI)", - "Begin Milestone 6 (GQL Parser)", - "UNIFIED-ROADMAP.scm", - "Dependently-typed query language - critical path item", - "M5: Zig FFI Bridge (blocks Studio M3, real type checking)", - "M6: GQL Parser (blocks full FQLdt compilation)", - "Complete M5 Zig FFI - highest priority", - "Integrate with Lithoglyph's EBNF grammar", - "Proof blob serialization (CBOR RFC 8949)", + "Discharge proof-debt D1: executePreservesTypes reduces to `... -> True` with body commented `-- Placeholder`. It reads as a soundness theorem and discharges nothing. Deleting it is strictly better than keeping a vacuous placeholder.", + "Settle the averaging rule, then discharge D3 once against the final definition.", + "Add a test driver entry for the FFI boundary once liblith_bridge.a can be assumed present.", +] + +[history-landmines] +notes = [ + "The gnpl extract from nextgen-databases was a SQUASH; granular history survives only in the _split_gnpl branch there. Never prune it.", + "Local branches backup/sweeps-mistral-vibe and fix-ci-estate hold three superseded agent-generated sweep commits. Do not replay them: sweep2 is boilerplate mise.toml, sweep3 is an AGPL clobber into an MPL-2.0 repo.", + "Callers pin standards reusables at @main, not a SHA, so upstream permission/interface changes reach this repo instantly and unannounced. This caused two separate estate-wide outages in July 2026.", ] +[evidence] +# Commands a machine or human can run to reproduce every claim above. +build = "lake build" +test = "lake test" +bridge = "cd bridge && zig build && zig build test" +proof-gate = "lake build 2>&1 | tee lake-build.log && ./scripts/check-lean-proofs.sh --build-log lake-build.log" +trusted-base = "bash /scripts/check-trusted-base.sh ." + [maintenance-status] -last-run-utc = "2026-02-01T00:00:00Z" -last-result = "unknown" # unknown | pass | warn | fail +last-run-utc = "2026-07-28T18:45:00Z" +last-result = "pass" # unknown | pass | warn | fail +last-result-detail = "lake build exit 0; lake test exit 0 with 163 checks across 3 suites; verified from a clean checkout of merged main (9de0713)." diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index b82cfa6..5fd7451 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -6,9 +6,9 @@ (manifest (identity - (name "GQL-DT") - (full-name "Dependently-Typed Glyph Query Language") - (version "0.2.0") + (name "GNPL") + (full-name "Glyph Narration & Projection Language") + (version "0.3.0") (repo "https://github.com/hyperpolymath/gnpl") (license "MPL-2.0") (author "Jonathan D.A. Jewell ") @@ -16,23 +16,64 @@ (monorepo-parent "nextgen-databases")) (purpose - "Compile-time verification of database constraints via dependent types. - Lean 4 implementation with Mathlib integration. Provides type-safe - query language for Lithoglyph with proofs of query correctness, - normalization, and constraint satisfaction.") + "Lithoglyph's narration/projection language. Where a query language answers + 'what is true in the store?', GNPL answers 'what account does this evidence + support, told from whose stance, with what warrant, and what rival accounts + does the same evidence also support?' — for forensic histories, counterfactual + paths, plural meanings, and synchronic/diachronic evidence interpretation. + TWO LAYERS, ONE REPO. GNPL is built on top of GQLdt here and lowers to it: + GNPL (what account) -> GQLdt (what is) -> Zig FFI -> Lithoglyph (the store). + This is why every source file is namespaced GqlDt in a repo named gnpl; that + is expected, not a mistake. GQLdt is the dependently-typed query core — Lean 4 + with Mathlib, compile-time verification of database constraints, provenance + tracking and normalization proofs — and it is GNPL's compilation target. + + STATUS: GQLdt builds and is tested (163 checks). GNPL itself is DESIGN ONLY — + docs/THEORY.adoc and docs/LITHOGLYPH.adoc; there is no src/Gnpl/ yet.") + + (caveat-for-agents + "A green proof gate here means 'nothing is admitted mid-proof'. It does NOT mean + 'nothing is assumed'. Lean's sorry warning does not fire on `axiom`, and this + repo declares 16 axioms — five in EXECUTABLE position (parseToIR, deserializeIR, + many, many1, sepBy), which therefore have no implementation at all. Code calling + them typechecks and cannot run. Do not report this repository as 'verified' on the + strength of a green build. See docs/proof-debt.md.") + + ;; Corrected 2026-07-28: all six of the previous entries pointed at files that do not + ;; exist. The .scm state/meta/ecosystem/roadmap files were converted to .a2ml under + ;; .machine_readable/6a2/ and never repointed; there is no AI.a2ml and no justfile. + ;; Every path below was checked to exist at the time of writing. (canonical-locations - (ai-instructions "AI.a2ml") - (state ".machine_readable/STATE.scm") - (meta ".machine_readable/META.scm") - (ecosystem ".machine_readable/ECOSYSTEM.scm") - (roadmap ".machine_readable/ROADMAP.scm") - (build "justfile") + (agent-instructions ".machine_readable/6a2/AGENTIC.a2ml") + (state ".machine_readable/6a2/STATE.a2ml") + (meta ".machine_readable/6a2/META.a2ml") + (ecosystem ".machine_readable/6a2/ECOSYSTEM.a2ml") + (playbook ".machine_readable/6a2/PLAYBOOK.a2ml") + (neurosym ".machine_readable/6a2/NEUROSYM.a2ml") + (roadmap ".machine_readable/ROADMAP.a2ml") + (proof-debt "docs/proof-debt.md") + (design-theory "docs/THEORY.adoc") + (design-application "docs/LITHOGLYPH.adoc") + (architecture "ARCHITECTURE.md") + (governance "GOVERNANCE.md") + (build "lakefile.lean") + (test "lakefile.lean") ;; @[test_driver] script test + (proof-gate "scripts/check-lean-proofs.sh") (container-build "Containerfile") (container-deploy "selur-compose.yml") (spec "spec/") + (ffi-bridge "bridge/") + (abi "src/GQLdt/ABI/") (lean-entry "src/GqlDt.lean")) + ;; Commands that reproduce every claim this manifest makes. + (evidence + (build "lake build") + (test "lake test") ;; 163 checks across 3 suites + (bridge "cd bridge && zig build && zig build test") + (proof-gate "lake build 2>&1 | tee lake-build.log && ./scripts/check-lean-proofs.sh --build-log lake-build.log")) + (tech-stack (primary "Lean 4") (lean-version "v4.15.0") diff --git a/README.adoc b/README.adoc index 91765d7..d89a6af 100644 --- a/README.adoc +++ b/README.adoc @@ -64,6 +64,15 @@ Lithoglyph-as-a-database is the second. See the design documents below. | link:docs/LITHOGLYPH.adoc[`docs/LITHOGLYPH.adoc`] | What does GNPL concretely give *Lithoglyph*, as a database? + +| link:docs/STATE-OF-PLAY.adoc[`docs/STATE-OF-PLAY.adoc`] +| Where the project actually stands, what is verified and by which command, what is known + missing, and which decisions are open. Machine-readable twin: + `.machine_readable/6a2/STATE.a2ml`. + +| link:docs/proof-debt.md[`docs/proof-debt.md`] +| All 16 outstanding axioms with `file:line` and disposition. **Read before relying on any + verification claim.** |=== == Status diff --git a/docs/STATE-OF-PLAY.adoc b/docs/STATE-OF-PLAY.adoc new file mode 100644 index 0000000..80eaa8c --- /dev/null +++ b/docs/STATE-OF-PLAY.adoc @@ -0,0 +1,155 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += GNPL — state of play +:toc: macro +:toclevels: 2 + +*As at 2026-07-28, `main` = `9de0713`.* The machine-readable counterpart is +`.machine_readable/6a2/STATE.a2ml`; both are regenerated together and should agree. + +This document exists because the repository's own claims about itself were, for a period, +false — a README describing a template, a lexer advertised as supporting operators it could +not lex, and a manifest pointing at six files that did not exist. What follows is written +to be *checkable*: every claim names the command that establishes it. + +toc::[] + +== What this is, in one paragraph + +GNPL is Lithoglyph's *narration/projection* language. A query language answers +"what is true in the store?"; GNPL answers "what account does this evidence support, told +from whose stance, with what warrant — and what rival accounts does the same evidence also +support?". It is built as a layer on top of GQLdt *in this repository* and lowers to it. +That is why every source file is namespaced `GqlDt` in a repo called `gnpl`: GQLdt is not +a leftover, it is the compilation target. + +---- +GNPL ──lowers to──▶ GQLdt ──FFI──▶ Lithoglyph +(what account) (what is) (the data store) +---- + +== Where things actually stand + +[cols="2,1,3",options=header] +|=== +| Component | State | Established by + +| GQLdt core (Lean 4) +| *typechecks* +| `lake build` — 34/35 targets, exit 0 + +| Test suites +| *163 checks, green* +| `lake test` — Lexer, Parser, TypeSafety; exit 0 + +| Zig FFI bridge (`bridge/`) +| *builds, tests pass* +| `cd bridge && zig build && zig build test` — emits `liblith_bridge.a` + +| Incomplete proofs (`sorry`) +| *none* +| `scripts/check-lean-proofs.sh --build-log` + +| Trusted base +| *16 axioms outstanding* +| estate `check-trusted-base.sh`; enumerated in `docs/proof-debt.md` + +| GNPL narration layer +| *design only* +| `docs/THEORY.adoc`, `docs/LITHOGLYPH.adoc`; no `src/Gnpl/` yet +|=== + +=== The caveat that matters most + +[IMPORTANT] +==== +*A green proof gate means "nothing is admitted mid-proof". It does not mean "nothing is +assumed."* + +Lean 4 emits `declaration uses 'sorry'` for `sorry`/`sorryAx` only — **`axiom` produces no +warning at all**. This repository declares *16 axioms*, all stubs, none necessary in the +policy sense. **Five sit in executable position** (`parseToIR`, `deserializeIR`, `many`, +`many1`, `sepBy`) and therefore have *no implementation*: code calling them typechecks and +cannot run. + +So "34/35 targets build" is a statement about **typechecking**, not about a working parser. +Read `docs/proof-debt.md` before relying on any verification claim made here. +==== + +== How to check any of this yourself + +[source,console] +---- +$ lake build # the Lean core typechecks +$ lake test # 163 checks, 3 suites +$ cd bridge && zig build && zig build test # the FFI bridge +$ cd .. && lake build 2>&1 | tee lake-build.log +$ ./scripts/check-lean-proofs.sh --build-log lake-build.log +---- + +Build *order* matters: `lakefile.lean` links `bridge/zig-out/lib/liblith_bridge.a`, so the +Zig archive must exist before the Lean FFI executables link. + +== Gates, and why they are trusted + +Every gate here has been shown to go *red* on a seeded fault and green when it is removed. +That is the standard, because this repository has shipped, and since removed, four gates +that could not fail: + +* a naming check that compared a string to itself, over files that did not exist; +* a `lake test` step whose `|| echo` swallowed genuine failures; +* test suites whose `main : IO Unit` always exited 0 while printing "All tests passed!"; +* a `Containerfile` masking both its build steps with `|| echo`. + +A gate that has never gone red is not evidence of anything. + +== What is known to be missing + +* **No FFI-boundary coverage in `lake test`.** `ffi_test` links `liblith_bridge.a`, so it + is excluded from the driver and covered only by the `zig-ffi` CI job. +* **No property tests.** Nothing in `docs/proof-debt.md` §(b) can cite a refutation budget + yet, so nothing has been promoted there. +* **`src/Gnpl/` does not exist.** The narration layer is specified, not built. + +== Open decisions + +Two questions are recorded here because work is genuinely blocked on them, and guessing +would be worse than waiting. + +*1. The averaging rule for PROMPT scores.* `PromptScores` carries a proof field — +`overall_correct : overall.val = (…sum…) / 6` — so the arithmetic mean is welded into the +*type*. Changing it is a proof-obligation change on every value, in Lean and in Zig +simultaneously, not an edit to one function. An unweighted arithmetic mean also lets a +source with *zero provenance* score 83/100, which is hard to defend for an evidence +database. This gates proof-debt item D3. + +*2. `flake.nix` versus `guix.scm`.* Estate policy is Guix primary, Nix fallback, and +satisfying *neither* is the violation. This repo has no `guix.scm`, so `flake.nix` is the +only artefact satisfying the policy; removing it without a verified replacement turns +Governance red. + +== Sequencing + +Foundation first, breadth before depth — the base layer is whatever makes everything else +*verifiable*. + +. *Done.* Suites can fail; `lake test` runs; gates canary-tested. +. *Next, unblocked:* proof-debt **D1** — `executePreservesTypes` reduces to `… → True` + with its body commented `-- Placeholder`. It reads as a soundness theorem and discharges + nothing. Deleting it is strictly better than keeping it. +. *Next, gated on decision 1:* **D3** — construct the six asserted `PromptScores` examples. + They are the demonstrations of the repo's central claim, and are currently axioms, so + they demonstrate the opposite of what their comments say. +. *Then:* **D2** — implement `many`/`many1`/`sepBy`; the four `parse*` axioms exist only + because these three do. +. *Then:* `src/Gnpl/` — `Fabula`, `Projection`, `Focalization`, `Account`, `Warrant`, + carrying the no-narration-without-warrant constructor discipline. + +== Related + +* `README.adoc` — start here; the two-layer story +* `ARCHITECTURE.md` — layout, build order, verification posture +* `GOVERNANCE.md` — the rules a change must clear, and why each exists +* `docs/proof-debt.md` — all 16 axioms with `file:line` and disposition +* `docs/THEORY.adoc` — what a narration language is, and what gap it fills +* `docs/LITHOGLYPH.adoc` — what GNPL gives Lithoglyph specifically diff --git a/docs/proof-debt.md b/docs/proof-debt.md index b3f1032..4f5993f 100644 --- a/docs/proof-debt.md +++ b/docs/proof-debt.md @@ -45,10 +45,21 @@ GQLdt sources, recorded honestly for the first time. ## (b) Budgeted — tested with refutation budget -- (none — this repo has **no executable test coverage**: `lake test` reports - `no test driver configured`. Nothing here can currently be budgeted, because there is - no refutation budget to cite. Adding a `@[test_driver]` is a prerequisite for moving - any item into this section.) +- (none yet — but the prerequisite is now met.) + +**Updated 2026-07-28.** This section previously read *"this repo has no executable test +coverage: `lake test` reports `no test driver configured` … adding a `@[test_driver]` is a +prerequisite for moving any item into this section."* That prerequisite has been satisfied: +`lake test` now runs three suites and **163 checks**, and the gate is canary-tested in both +directions (a seeded false check turns it red; removing it returns green). + +So items *can* now be moved here — but none has been yet, and none should be moved without +a **stated refutation budget**. Coverage existing is not the same as a given axiom being +covered. The policy's requirement is a citable budget ("property-tested at N inputs by +``, last green on ``"), because without one "covered by tests" is +unfalsifiable — which is the whole reason this section exists. + +The nearest candidate is **D4** (`inferredInsertTypesMatch`); see its entry. ## (c) Necessary axiom @@ -116,11 +127,14 @@ Declared `axiom`, therefore **unimplemented**, not merely unproven: - **Kind**: the one item with a *reasoned* justification in-source — the dynamic schema lookup in `inferInsert` already performs the check, and reconstructing that proof structurally would require reflecting the schema into the type system. - - **Assessment**: plausible, and closest of the 16 to a genuine §(b)/§(c) entry — but it - cannot be promoted to §(b) today because there is no test suite to give it a - refutation budget, and not to §(c) because it *is* derivable in principle. - - **Plan**: promote to §(b) once a test driver exists and this path is property-tested; - or discharge via schema reflection (the source's own "future work"). + - **Assessment**: plausible, and closest of the 16 to a genuine §(b)/§(c) entry. Not + §(c), because it *is* derivable in principle. Not yet §(b) either — but the reason has + changed as of 2026-07-28: a test suite now exists (163 checks), so the blocker is no + longer "no coverage at all", it is that **this specific path is not property-tested** + and has no citable refutation budget. + - **Plan**: property-test `inferInsert` over generated schema/value pairs, then promote + to §(b) quoting the command and the input count; or discharge via schema reflection + (the source's own "future work"). The first is now genuinely reachable. ## (e) Detector false positives — no action