docs(V4): design proof_attempts ↔ VQL-DT certificate integration

Proposes auto-minting PROVEN certificates (τ=0.80, n≥20) and SANCTIFY
certificates (k≥2 provers, n≥50 combined) via materialized views over
mv_prover_success_by_class, with evidence cursors back to attempt_ids.

Uses current real-data snapshot (2026-04-05) as baseline: safety z3:0.5×4,
equiv agda:1.0×5, totality idris2:0.0×5 — all below threshold, showing
the loop needs to converge before certification is meaningful.

Closes pending design question #22.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/design/DESIGN-2026-04-05-V4-proof-attempts-vqldt.adoc

@@ -0,0 +1,239 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+= V4: proof_attempts ↔ VQL-DT Certificate Integration
+:toc: left
+:toclevels: 2
+:date: 2026-04-05
+:status: draft
+
+== Context
+
+VeriSimDB's `proof_attempts` table (ClickHouse) records every prover invocation
+across the hyperpolymath estate, aggregated via `mv_prover_success_by_class`
+into a recommendation source for `/api/v1/proof_attempts/strategy`.
+
+VQL-DT has 11 proof types. Two of them — *PROVEN* and *SANCTIFY* — are
+currently certificate-shaped (proven_bridge parses external JSON/CBOR blobs)
+but have no live connection to actual prover outcomes accumulating in
+ClickHouse.
+
+The question: how should VQL-DT `PROOF PROVEN(...)` and `PROOF SANCTIFY(...)`
+relate to the evidence in `proof_attempts`?
+
+== Decision (proposed)
+
+*Option (iii): both auto-mint certificates AND require evidence rows.*
+
+Certificates are minted by a materialized view policy, not hand-authored.
+Every certificate references the specific `attempt_id`s that back it.
+
+=== PROVEN certificate
+
+A *PROVEN* certificate asserts:
+
+[quote]
+____
+For obligation class `C`, prover `P` succeeds at rate ≥ `τ_proven`
+given ≥ `N_proven` attempts.
+____
+
+Minting rule (computed nightly from `mv_prover_success_by_class`):
+
+[source]
+----
+PROVEN(class=C, prover=P) ⟺
+  success_count(C,P) / total_attempts(C,P) ≥ τ_proven
+  ∧ total_attempts(C,P)                    ≥ N_proven
+----
+
+Defaults: `τ_proven = 0.80`, `N_proven = 20`.
+
+=== SANCTIFY certificate
+
+A *SANCTIFY* certificate is a higher-tier attestation requiring
+*portfolio agreement*:
+
+[quote]
+____
+For obligation class `C`, at least `k_sanctify` distinct provers
+each hold a PROVEN certificate, covering ≥ `N_sanctify` combined attempts.
+____
+
+Minting rule:
+
+[source]
+----
+SANCTIFY(class=C) ⟺
+  |{ P : PROVEN(C,P) holds }|            ≥ k_sanctify
+  ∧ Σ_P total_attempts(C,P)              ≥ N_sanctify
+----
+
+Defaults: `k_sanctify = 2`, `N_sanctify = 50`.
+
+== Schema
+
+Add two new ClickHouse views on top of `mv_prover_success_by_class`:
+
+[source,sql]
+----
+CREATE MATERIALIZED VIEW mv_proven_certificates
+ENGINE = ReplacingMergeTree()
+ORDER BY (obligation_class, prover_used)
+AS
+SELECT
+  obligation_class,
+  prover_used,
+  sum(success_count) AS success_count,
+  sum(total_attempts) AS total_attempts,
+  sum(success_count) / sum(total_attempts) AS success_rate,
+  now() AS minted_at,
+  if(sum(success_count) / sum(total_attempts) >= 0.80
+     AND sum(total_attempts) >= 20, 'proven', 'pending') AS status
+FROM mv_prover_success_by_class
+GROUP BY obligation_class, prover_used;
+
+CREATE MATERIALIZED VIEW mv_sanctify_certificates
+ENGINE = ReplacingMergeTree()
+ORDER BY obligation_class
+AS
+SELECT
+  obligation_class,
+  count(DISTINCT prover_used) AS proven_provers,
+  sum(total_attempts) AS combined_attempts,
+  now() AS minted_at,
+  if(count(DISTINCT prover_used) >= 2
+     AND sum(total_attempts) >= 50, 'sanctified', 'pending') AS status
+FROM mv_proven_certificates
+WHERE status = 'proven'
+GROUP BY obligation_class;
+----
+
+== Evidence linkage
+
+Certificates must be *falsifiable* — each one carries a cursor back to the
+attempts that established it. Add a `proof_attempts_cert_evidence` table:
+
+[source,sql]
+----
+CREATE TABLE proof_attempts_cert_evidence (
+  cert_id         String,               -- sha256(cert_type|class|prover|minted_at)
+  cert_type       Enum8('proven'=1, 'sanctify'=2),
+  obligation_class String,
+  prover_used     String,
+  attempt_id      String,               -- back-reference to proof_attempts
+  minted_at       DateTime64(3)
+) ENGINE = MergeTree()
+ORDER BY (cert_id, attempt_id);
+----
+
+A nightly job samples up to 100 `attempt_id`s per certificate as evidence
+(oldest + most recent + random middle — so falsifying any sample invalidates
+the claim).
+
+== VQL surface
+
+Add VQL-DT endpoints that resolve against the new MVs:
+
+[source]
+----
+-- Look up whether a (class, prover) pair is certified
+PROOF PROVEN(class='linearity', prover='lean')
+  → consults mv_proven_certificates, returns status + evidence cursor
+
+-- Look up whether a class is portfolio-certified
+PROOF SANCTIFY(class='equiv')
+  → consults mv_sanctify_certificates, returns proven_provers list
+
+-- Query the evidence directly
+SELECT * FROM REFLECT
+  WHERE cert_id = 'abc123...' AND cert_type = 'proven'
+  → walks proof_attempts_cert_evidence, returns attempt rows
+----
+
+== Integration points
+
+[cols="1,3"]
+|===
+| Component | Hook
+
+| verisim-api
+| New `GET /api/v1/proof_attempts/certificates?class=X[&prover=Y]`
+returning certificate status + evidence cursor.
+
+| hypatia proof_strategy_selection rule
+| Already picks top prover by `success_rate`. Augment to prefer
+*PROVEN-certified* pairs over uncertified ones with equal or higher
+success rate. Uncertified pairs fall through to novelty guard.
+
+| echidnabot fleet dispatch
+| When dispatching, attach the (class, prover) certificate ID to the
+GraphQL mutation for audit trail. hypatia's ProofObligationInput already
+carries `prover_hint` — add optional `cert_id`.
+
+| proven-library bridge
+| Existing `proven_bridge.rs` parses external PROVEN blobs. Extend to
+*emit* locally-minted blobs when an attempt crosses a threshold.
+
+| VQL-DT type checker
+| `PROOF PROVEN(class, prover)` becomes a well-typed query against
+`mv_proven_certificates`. No longer requires external contract file.
+|===
+
+== Thresholds are policy
+
+`τ_proven`, `N_proven`, `k_sanctify`, `N_sanctify` live in a config table
+(`proof_attempts_cert_policy`), not hardcoded. One row per certificate tier.
+Policy changes re-compute the MVs on next materialization.
+
+Default policy bootstrapped from current real data (as of 2026-04-05):
+
+[cols="1,1,1,1"]
+|===
+| class | best prover | rate × n | current cert?
+
+| safety       | z3     | 0.5 × 4  | no (needs τ≥0.8, n≥20)
+| linearity    | coq    | 1.0 × 1  | no (needs n≥20)
+| termination  | lean   | 1.0 × 1  | no (needs n≥20)
+| equiv        | agda   | 1.0 × 5  | no (needs n≥20)
+| equiv        | lean   | 1.0 × 5  | no (needs n≥20)
+| totality     | idris2 | 0.0 × 5  | no (fails τ)
+|===
+
+These numbers show the evidence threshold matters: one obligation is not
+enough to certify a prover, but the loop can converge quickly once batch
+runs scale.
+
+== Non-goals
+
+* *Not* replacing external PROVEN contracts from the proven library.
+  VQL-DT `PROVEN` expressions can still reference external JSON/CBOR.
+  The new minting path is additive — it turns the estate's own proof-running
+  behaviour into first-class evidence.
+* *Not* generating machine-checkable proofs from `proof_attempts` alone.
+  A PROVEN certificate is a statistical attestation (N trials, success rate),
+  not a Coq proof term.
+
+== Implementation order
+
+. Add `proof_attempts_cert_policy` config table + seed defaults (V4a)
+. Create `mv_proven_certificates` + `mv_sanctify_certificates` MVs (V4b)
+. Create `proof_attempts_cert_evidence` table + nightly sampling job (V4c)
+. Add `GET /api/v1/proof_attempts/certificates` endpoint (V4d)
+. Extend hypatia `proof_strategy_selection` to prefer certified pairs (V4e)
+. Update VQL-DT parser/typechecker to resolve `PROOF PROVEN(class, prover)`
+  against the MV (V4f)
+. Documentation + VQL-SPEC update (V4g)
+
+V4a–V4d are pure schema/endpoint work, ~1 session. V4e–V4g integrate across
+three repos (hypatia, verisimdb, echidna).
+
+== Open questions
+
+. Should PROVEN certificates *decay* if recent attempts shift the rate below
+  `τ_proven`? Proposed: yes, use a sliding-window variant MV
+  (`last 30 days` rather than all-time).
+. How do we handle certificate *revocation* — if a previously-PROVEN prover
+  suddenly starts failing? Proposed: emit a `revoked` status alongside
+  `proven`/`pending`.
+. Should failures be weighted more heavily than successes for novelty? E.g.
+  2 failures cancel 1 success when `total_attempts < 10`. Proposed: no,
+  keep statistics honest; policy thresholds handle this.