docs: two-strand work-up — the consonance claim and the VeriSimDB application

The strategic deliverable. Two strands kept deliberately separate because they
have different success conditions: Strand A succeeds if the theoretical claim
is novel and defensible; Strand B succeeds if VeriSimDB is measurably safer.
Neither implies the other.

STRAND A — the theoretical claim

Argues that consonance languages are a distinct class, not query languages
with extra types, on three grounds: statements are propositions and epistemic
requests rather than read requests; retraction is not deletion and drift is a
typed condition rather than an error; and well-typedness stops being
sufficient once several modal witnesses can disagree.

The gap in the world is stated honestly. Type-safe query languages are a
crowded, mature field — LINQ, Quill, Diesel, jOOQ, TypeQL, EdgeQL for L0-L5,
and substantial literature for effects, temporal, linear and cardinality. A
"ten levels of query safety" paper enters that field as a thorough synthesis
and will be read as one. What none of them do is type WARRANT: every one
assumes a single source of truth that cannot disagree with itself. Epistemic
logic, provenance and truth-maintenance all exist, but beside the query path —
never as a type that can refuse a statement.

The decisive evidence came from the code rather than from taste. The ladder
has eleven levels; the eleventh is not a query-safety property; and it is the
one level NOT inherited from TypeLL, because a UI panel has no federation and
so no warrant question. A framework whose eleventh member does not fit its own
name is telling you the name is wrong.

WHITEPAPER REFRAME IS A PROPOSAL, NOT AN EXECUTED REWRITE

Deliberate. The direction is settled, but how a paper argues its claim is the
author's call and is the least testable, highest-blast-radius change available
here. The 1,909-line .tex is untouched. What is offered is a section-by-section
structure and a complete draft abstract, for approval first.

STRAND B — the VeriSimDB application

Opens with the uncomfortable fact: VCL-UT delivers nothing to VeriSimDB at
runtime today. The proof corpus is real, the parser is real and gated, the
gate binary exists and Contract v1 is frozen — but the seam is built on one
side only. The producer is finished and the consumer was never written.

Defends the subprocess/JSON-line seam against the obvious objection that it
looks unfashionable, using evidence from this repository: src/interface's
external path-dep on an echidna sibling is exactly the build coupling the
CLI seam avoids, and it is why echidna-client cannot even be covered by
Dependabot.

Sets out what VeriSimDB actually gets — a fail-closed admissibility check
before statements touch consonance state; one level ladder instead of two
divergent ones; independently-verifiable attestation; and vocabulary
discipline — and gives a migration path that keeps VeriSimDB's genuinely good
ReScript surface parser and diagnostics while replacing only the verdict.

Two concrete defects, both located precisely:
  - VCLTypeChecker.res:60 builds the default context with six modalities
    though the type admits eight. Provenance and Spatial are silently absent
    from every default type-check. The hexad-to-octad migration reached the
    variants and stopped before the defaults and the names — HexadType is
    still the type name in four places.
  - The seam is unwired (zero vclt-gate references in verisim-api/src/vcl.rs).

Sequenced plan, ordered by value per unit of risk, with the repository each
item belongs to marked — items 3-5 are VeriSimDB changes and cannot be
committed from this repository.

Closes with a falsification section, so the plan can be argued with rather
than assumed: if VeriSimDB's ReScript checker is materially more capable than
the corpus, "vcl-ut is source of truth" costs capability; if subprocess
latency is material on the hot path, the CLI seam is wrong and should be
measured BEFORE the wiring work rather than after; and if the consonance claim
has prior art under another name, Strand A weakens to a synthesis claim. The
prior-art search behind the gap argument was not exhaustive and says so.

Verification:
  reuse lint -> compliant, 460/460
  every factual claim in the Ground Truth table measured against the working
  tree on 2026-07-21, including the two VeriSimDB defects

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: hyperpolymath