Formal Evidence Cell Anchor Resolver

Component asks whether

This component asks whether a page's proof-language claim can be tied to a named piece of public evidence, resolving each claim to an evidence cell and capping its strength at what the cell allows. formal_evidence_cell_anchor_resolver checks the project's proof-flavoured writing against recorded evidence. When a paper page says a claim is proved or certified, this component asks a narrower question: can the words be tied to a named piece of public evidence, and does that evidence stay below formal-result correctness. It answers by resolving each claim to an evidence cell, checking the cell's source anchors point at files that exist on the public path, and capping the claim's strength at what the cell allows.

Unit of evidence

The unit of evidence is a cell, a stable id bundling source-anchor refs, a machine_anchor_class, and allowed claim strengths, and the resolver reports which claims resolved, overreached, or had no backing. The unit of evidence is a cell. A cell is a stable id that stands for a bundle of recorded evidence: a list of source-anchor refs, a machine_anchor_class naming what kind of machine artifact backs it, and the claim strengths the cell is allowed to support. The resolver reads paper claims, an evidence-cell registry, a claim-boundary policy, and an obligation graph, then writes a result record that reports which claims resolved, which overreached, and which had no backing. Proof bodies, non-public source refs, and model-output data stay out of that record.

Is not theorem

It is not a theorem prover: it runs over already-public inputs, emits metadata-only result records, and states its full proof boundary once under Scope limit. It is not a theorem prover. It runs over already-public inputs and emits metadata-only result records. The full proof boundary is stated once, under Scope limit.

Purpose

Where proof-adjacent prose drifts

Proof-adjacent prose drifts easily, and a loose check that only scanned for the word proof would pass any sentence avoiding it and could not bound how strong a backed claim may be. Proof-adjacent prose is the easiest place for a claim to drift. A page can write "this proves the theorem" and a reader has no cheap way to tell whether the words rest on a checked artifact or on nothing. A loose check that only scanned for the word "proof" would pass any sentence that avoided the word, and would have no way to bound how strong a backed claim is allowed to be.

proof_language_requires_machine_anchor

The key policy is proof_language_requires_machine_anchor: proof-language claims must name a resolving cell whose anchors point at existing files, with strength capped and human approval refused as a substitute. The policy that makes the component useful is proof_language_requires_machine_anchor. A claim that uses proof language must name a cell, the cell must resolve in the registry, and the cell's source anchors must point at files that exist. A claim that uses proof language but names no cell, or names a cell absent from the registry, lowers the run to a blocked status instead of passing as green prose. On top of the resolved cell sit two limits: the claim's strength is capped by the cell's allowed_claim_strengths, and human approval is refused as a substitute for a machine anchor.

How it works

Two entrypoints share one core

run validates a fixture directory with negative cases included and run_anchor_bundle validates an exported bundle with them off, both calling _build_result to run the pipeline. Two entrypoints share one core. run validates a fixture directory with the negative cases included. run_anchor_bundle validates an exported bundle directory with negative cases off and the source-module manifest required. Both call _build_result, which runs the pipeline and returns the result record.

_build_result scans, validates, folds

_build_result loads the five inputs, scans every path for secret-equivalent material, runs six validators, and passes only when all pass, every expected negative case was observed, and no scan hit fired. _build_result loads the five fixture inputs with _load_payloads, scans every input path for secret-equivalent material with scan_paths, then runs six validators and folds their findings into one status. The run passes only when every validator passes, every expected negative case was observed, and no secret scan hit fired.

The validators, in the order _build_result calls them:

validate_claims resolves each claim

validate_claims passes each claim to _inspect_claim_row, which rejects proof bodies, non-public refs, oracle payloads, missing boundary classes, unknown cells, and out-of-range strengths as structured findings. validate_claims is the resolver proper. It builds a cell_by_id map from the registry and passes each claim to _inspect_claim_row. That function rejects a claim when it carries a proof body, a non-public source refs, or a provider or oracle payload; when it omits an oracle-boundary class; when it uses proof language with no cell; when its cell id is unknown; or when its stated strength is not in the cell's allowed list. A theorem-correctness overclaim is caught either from an explicit flag or from the claim text by THEOREM_CORRECTNESS_OVERCLAIM_RE, a regex that matches "proves" or "certifies" near "theorem" and "correctness". Each rejection is a structured finding, not a silent pass.

Resolving source anchors on the public path

_validate_anchor_refs splits each ref, rejects private schemes and escaping paths, resolves the file among public candidates including a source-artifact mirror, and records digest matches without holding file bodies. Source anchors resolve through _validate_anchor_refs. It splits each ref into a path and an optional marker, rejects private schemes and absolute or parent paths through _public_ref_is_forbidden, then looks for the file among the candidates from _public_ref_candidates. A state/runs/... anchor is allowed to resolve through a public source-artifact mirror under examples/*/*/source_artifacts, so the resolver can confirm an anchor exists from an existing public example bundle without copying wider source trees into this component. When a ref carries a digest, _sha256_file recomputes it and the row records whether it matched. The record holds refs, digests, and status, not file bodies.

metadata-only card shaping

result_card, _source_module_summary_card, and _board_from_result shape the result into compact cards, each carrying body_in_receipt: False. The result record is shaped by result_card, _source_module_summary_card, and _board_from_result into compact cards. Every card and finding carries body_in_receipt: False.

flowchart TD Inputs["paper claims, cell registry, boundary policy, obligation graph, projection protocol"] --> Build["_build_result"] Build --> Scan["scan_paths secret-equivalent material"] Build --> Validators["six validators projection, registry, policy, obligations, source modules, claims"] Validators --> Claims["validate_claims _inspect_claim_row"] Claims --> Status["status = pass only if all validators pass and every negative case observed"] Scan --> Status Status --> Record["metadata-only result record refs, digests, findings"]

Negative cases

Thirteen required negative-case classes

EXPECTED_NEGATIVE_CASES declares thirteen negative-case classes the fixture run must observe, and a run fails if any is missing, keeping the refusal coverage from silently eroding. EXPECTED_NEGATIVE_CASES declares thirteen negative-case classes that the fixture run must observe. A run fails if any of them is missing, which keeps the refusal coverage from silently eroding. The classes name the exact rejection each case exercises: unknown_cell_overclaim, missing_source_anchor, proof_language_without_cell, private_source_ref_leakage, proof_body_leakage, theorem_correctness_overclaim, human_approval_as_evidence_cell, oracle_payload_leakage, oracle_boundary_forward_success_overclaim, and four obligation-graph variants for unmet obligations and private-ref, proof-body, or oracle-payload leakage inside an obligation.

Prior Art Grounding

Provenance and proof-certificate lineage

The component follows provenance and proof-certificate work like W3C PROV and Proof-Carrying Code, borrowing anchor resolution so a small checker bounds what cell metadata can assert without granting theorem authority. This component follows provenance and proof-certificate work where a claim must point at checkable evidence rather than untyped narrative. The W3C PROV model links entities, activities, and agents in an evidence graph. Proof-Carrying Code and small-kernel proof assistants motivate keeping a certificate or anchor separate from the trusted checker that bounds its meaning. This resolver borrows the anchor-resolution pattern: proof-language claims must name cell ids, source anchors, and machine-anchor classes, and a small checker bounds what those metadata can assert. It does not turn metadata cells into theorem-correctness authority.

Validation Result record Path

Run from repo

Run these from the repo root. Run these from the repo root. They do not mutate durable result record or generated projection surfaces.

./repo-pytest tests/test_formal_evidence_cell_anchor_resolver.py -q --basetemp=/tmp/microcosm_formal_evidence_cell_anchor_resolver_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

What a pass means here

A pass means the fixture run observed all thirteen negative cases, resolved three claims to three cells across eight anchors, validated six frozen snapshots by digest, and kept everything metadata-only. A pass means the fixture run observed all thirteen negative cases, resolved three paper claims to three evidence cells across eight source anchors and three machine anchors, validated the exported bundle against six frozen source-module snapshots by digest, and kept every card and finding metadata-only. It is bounded validator evidence over that fixture, not a statement about the wider formal-math corpus.