Proof Diagnostic Evidence Spine
Sorts proof-pipeline checks into accepted or rejected without inflating a pass.
Contract
Does An evidence checkpoint that sits in front of formal-proof work. It reads the diagnostic records left by earlier proof-pipeline steps and writes a "diagnostic board" listing which checks were accepted, which were rejected, and why. The board shows exactly what evidence was kept, and refuses to let raw model output, a stale record, or a merely-passing check get inflated into a claim that the math is actually correct. It only arranges and judges existing records; it never runs a proof checker itself.
Scope limit It records proof/evidence diagnostics over existing result record references only. It does not run Lean, use external model services, expose proof bodies, turn a passing check into formal-proof or theorem authority, prove runtime or whole-system correctness, authorize later components, certify public launch, authorize public sharing or recipient work, or establish secret export.
Run
microcosm proof-diagnostic-evidence-spine run --input fixtures/first_wave/proof_diagnostic_evidence_spine/input --out receipts/first_wave/proof_diagnostic_evidence_spine --cardEvidence
ClassComputed projectionevidence 3/5Source-faithful refactor
Links to Formal Math Verifier Trace Repair Loop, Formal Evidence Cell Anchor Resolver, Formal Math Lean Proof Witness, Verifier Lab Kernel, Ring2 Premise Retrieval Precision Recall Harness, Target Shape Tactic Routing Gate
Source
Paper module
Paper module Proof Diagnostic Evidence Spine