Ring2 Premise Retrieval Precision Recall Harness
Scores how much proof support a premise search found, problem by problem.
Contract
Does When a math-proving system searches for the supporting facts ("premises") a proof will need, this component replays saved records of that search and reports, problem by problem, how much of the needed support the search actually turned up. Per problem it labels one of four outcomes: the search found everything needed and the proof went through; it found everything needed but the proof still failed; it found only some of the needed support; or it found none of it. Separating "the proof failed even though every needed premise was found" from "the proof failed because the search missed a needed premise" shows which part to fix. It also runs as a regression guard that refuses inputs which try to slip the answer into the search itself (the known-correct premises planted in the ranked results), leak proof text, tune on the test answers, or claim more than retrieval-quality numbers.
Scope limit These are after-the-fact retrieval-attribution labels and precision/recall counts over copied run records only. The component does not run Lean or Lake, call any provider, expose proof bodies, tune on test answers, claim benchmark performance, prove formal-result correctness, or include launch operations, and its labels are explicitly forbidden from flowing into provider context. The aggregate numbers describe only the copied fixture/bundle replayed, not any benchmark claims.
Run
PYTHONPATH=src python3 -m microcosm_core.organs.ring2_premise_retrieval_precision_recall_harness run --input fixtures/first_wave/ring2_premise_retrieval_precision_recall_harness/input --out receipts/first_wave/ring2_premise_retrieval_precision_recall_harnessEvidence
ClassComputed projectionevidence 3/5Source-faithful refactor
Links to Mathematical Strategy Atlas Hypothesis Scorer, Verifier Lab Kernel
Source
Paper module
Paper module Ring-2 Premise Precision Recall