Component · spec & evidence

Formal Evidence Cell Anchor Resolver

Resolves each proof-flavored math claim to named evidence and flags ones that overreach or lack backing.

Contract

Does When the project's writeups make proof-flavored claims about its formal-math work, this component checks each claim against a named piece of recorded evidence and the public reference files in the repo, confirms the claim is no stronger than that evidence allows, and flags claims that have no backing or that overreach. The record shows which claims are anchored to evidence and which are just words, while proof contents and any private file references are kept out of the output.

Scope limit It validates claim-to-evidence anchoring mechanics only: claim-to-cell resolution, source-anchor presence, permitted claim strength, copied-source-module digest checks, and leakage refusals. It does not run Lean/Lake, certify theorem or mathematical correctness, expose proof bodies or non-public source refs, use external model services, or include launch operations/public sharing.

Run

microcosm formal-evidence-cell-anchor-resolver run-anchor-bundle --input examples/formal_evidence_cell_anchor_resolver/exported_evidence_cell_anchor_bundle --out receipts/runtime_shell/demo_project/organs/formal_evidence_cell_anchor_resolver

Evidence

ClassComputed projectionevidence 3/5Source-faithful refactor

Links to Formal Math Verifier Trace Repair Loop, Proof Diagnostic Evidence Spine, Target Shape Tactic Routing Gate

formal-methodstheorem-provinglean

Source

Source Design note · Source

Map Show on the map

Index Open compact index card

Paper module