feat(verisim): first-class Proof / TacticApplication / ProofVersion / ProofStateRecord

src/rust/verification/proof.rs
  New module (verisim-feature-gated) materialising the four entities the
  E-R audit flagged as missing from the Verisim schema.  Each closes one
  of the FK-discipline gaps identified in the 2026-04-19 audit:

  * Proof{id, goal_hash, theorem_hash, theorem_name, prover, first_seen}
    makes the SHA-256 digest already produced by
    proof_encoding::proof_identity() a first-class row.  theorem_hash
    (new helper theorem_identity) and goal_hash let cross-prover and
    cross-goal joins index on fixed-width columns without re-deriving
    the triple from the primary key.

  * TacticApplication{proof_id, step, tactic, goal_hash, status,
    goals_after, duration_ms, applied_at} persists the proof DAG.
    Success/Closed/Error TacticStatus is kept (not just success) so
    MCTS/agentic search retains failed-branch training signal.

  * ProofVersion{proof_id, version, snapshot_id, goals_remaining,
    is_qed, actor, recorded_at} is the append-only audit log that
    OctadPayload.temporal.versions currently lacks — the latter is
    render-only; this is durable.  `initial()` and `next()` chain
    monotonically so versions never collide.

  * ProofStateRecord{proof_id, step, goal_hash, prover, prover_version,
    state_cbor_b64, features, relevant_premises, label_confidence,
    source} is the typed corpus schema replacing the ad-hoc JSONL dict.
    state_cbor_b64 round-trips the tree structure the JSONL format
    loses; label_confidence separates human-verified ground truth from
    weak heuristics; prover_version attributes MRR deltas to solver
    builds.

  The module adds 8 unit tests (hash-derivation correctness, FK wiring,
  monotonic version chaining, QED marking, round-trip serde).  Existing
  OctadPayload posting continues unchanged — these rows are intended to
  be written alongside, not instead of, the octad, via an incremental
  migration path.

src/rust/verification/mod.rs
  Export the new types behind the existing `verisim` feature gate,
  matching how proof_encoding is gated.

src/rust/proof_encoding.rs + src/rust/verisim_bridge.rs
  Drive-by fix: the `verisim` feature tests referenced
  ProverKind::Lean4 (doesn't exist; the Lean 4 variant is ProverKind::Lean,
  Lean 3 is the sibling ProverKind::Lean3) and a hardcoded "Lean4" Debug
  string.  Restoring the 27 previously-uncompilable verisim-feature
  tests so the new proof.rs tests can share the harness.

Test counts: 613 default, 640 with --features verisim (0 failures).

Author: claude

src/rust/proof_encoding.rs

@@ -154,8 +154,8 @@ mod tests {
             hypotheses: vec![],
         };
 
-        let id1 = proof_identity("my_theorem", &goal, ProverKind::Lean4);
-        let id2 = proof_identity("my_theorem", &goal, ProverKind::Lean4);
+        let id1 = proof_identity("my_theorem", &goal, ProverKind::Lean);
+        let id2 = proof_identity("my_theorem", &goal, ProverKind::Lean);
         assert_eq!(id1, id2, "Same inputs must produce same identity");
     }
 
@@ -167,7 +167,7 @@ mod tests {
             hypotheses: vec![],
         };
 
-        let lean = proof_identity("thm", &goal, ProverKind::Lean4);
+        let lean = proof_identity("thm", &goal, ProverKind::Lean);
         let coq = proof_identity("thm", &goal, ProverKind::Coq);
         assert_ne!(
             lean, coq,

src/rust/verification/mod.rs

@@ -16,6 +16,8 @@ pub mod confidence;
 pub mod mutation;
 pub mod pareto;
 pub mod portfolio;
+#[cfg(feature = "verisim")]
+pub mod proof;
 pub mod statistics;
 
 pub use axiom_tracker::{AxiomPolicy, AxiomTracker, AxiomUsage, DangerLevel};
@@ -24,4 +26,8 @@ pub use confidence::TrustLevel;
 pub use mutation::{MutationKind, MutationResult, MutationTester};
 pub use pareto::{ParetoFrontier, ProofCandidate, ProofObjective};
 pub use portfolio::{PortfolioConfig, PortfolioResult, PortfolioSolver};
+#[cfg(feature = "verisim")]
+pub use proof::{
+    theorem_identity, Proof, ProofStateRecord, ProofVersion, TacticApplication, TacticStatus,
+};
 pub use statistics::StatisticsTracker;