Validity cartography for informal mathematics — per-claim maps of where a result is proven, refuted, empirically supported, marginal, vacuous, or unprobed, with provenance, margins, and coverage accounting.
House rule: a
VERIFIEDbadge may not assert what the harness cannot rerun.
proof-radar is the middle rung of mathematical validation: adversarial
verification at the rigor level papers are actually written — above unaided peer
review (uninstrumented, unlogged), below full formalization (months per theorem).
It is cartography, not policing: errors are found because boundaries are mapped,
and the boundaries are the publishable object.
It is not formal verification, not a substitute for peer review or Lean/mathlib, and not a certainty machine. It emits graded confidence with documented failure modes, or it emits nothing.
Full specification: CHARTER.md.
| Deliverable | File | What it is |
|---|---|---|
| The radar | RADAR.md + radar.json |
the validity map — regions of hypothesis space graded {proven, refuted, empirical, marginal, vacuous, open}, each with provenance, boundary sharpness, margin gauges, coverage |
| The ledger | VERIFICATION.md |
the audit trail — every check that produced a region, logged, graded, rerunnable |
No radar region may exist without ledger rows behind it (Rule 5.1: provenance or
nothing). Unprobed space renders as unprobed (Rule 5.2) — the verifier's own
blind spots are a first-class layer, the verifier's ker P_C.
In review round three of Keep the Angle, an AI verifier certified a Corollary-1 summation argument as sound. It was not — the argument silently required the multiplicative-uniform form of a limit and a bounded degree ratio. The conclusion was true; the derivation was incomplete; the pass was a false pass on the derivation while correct on the conclusion. Two structural lessons follow, and they are load-bearing:
- Conclusion-checks and derivation-checks are different objects — graded on separate axes, always (Rule 4.1). A numerical confirmation of a true conclusion says nothing about the proof.
- An embedded verifier is not independent — same model, same context, co-author of the derivation ⇒ correlated errors. Grading runs fresh-context (§6).
That false pass is Baseline Datum #1 of the benchmark (benchmark/).
Recomputation · special-case instantiation · numerical falsification harness ·
type/dimension/units lint · statement↔proof diff · cross-artifact consistency ·
citation verification · formalization escalation. See checks/.
Every ledgered claim gets C1 + C5 at minimum.
| Path | What |
|---|---|
CHARTER.md |
full charter (mission, scope, checks, gates, governance) |
checks/ |
the C1–C8 check taxonomy as an operational checklist |
schema/radar.schema.json |
JSON Schema for radar.json |
templates/ |
RADAR.template.md, VERIFICATION.template.md |
ledgers/ |
per-paper VERIFICATION.md ledgers (v0 scope: the trilogy) |
benchmark/ |
the seeded-error benchmark (§8) |
nrp/ |
NRP/Nautilus manifest conventions (§7) |
In scope (v0): the Geometric Observation trilogy — Keep the Angle,
TurboQuant-Pro, Observation Theory — and their companion artifacts. One
VERIFICATION.md per paper. Expansion beyond the trilogy is gated on G2
(Rule 2.1: the project that verifies everything verifies nothing reproducibly).
Status: draft v0.1 — for adoption at G0. Open G0 parameters: final name;
benchmark numeric bars; radar.json schema freeze; human-auditor roster; the
LLM-verification prior-art scan.
The embedded assistant may draft radars and run harnesses; it may not be the sole grader of anything it helped derive (R-IND-5). Grading passes run in fresh context (R-IND-2), cross-model where available (R-IND-3), with ≥10% human spot-audit (R-IND-4). Every ledger row names its verifier (model, version, context freshness).
PI: A. H. Bond. Stand-down clause: if the gate (G2) fails twice, the project stands down and the postmortem is published — the value was in the adversarial relationship, not the artifact. This clause is the project's own falsifiability.
Code Apache-2.0 (LICENSE); documents CC-BY-4.0
(LICENSE-docs); benchmark ground-truth labels sealed until G3.