Add Lean-backed logical evaluation and harden NICE scraping

[buley]

Why this is worth caring about

AMFV will only be as trustworthy as the boundaries that feed and evaluate it. The NICE scraper had several ways to produce output that looked reasonable while changing what evidence entered the system:

• chapter links were accepted from path text before normalized host and guidance scope were checked;
• a link could begin under one guidance document and normalize into another;
• the reported listing total remained NICE's raw total after local filtering;
• extraction steps could silently omit or duplicate sections without an accounting witness.

Those are not cosmetic scraper defects. They are provenance defects: downstream evaluation can be internally consistent and still be evaluating the wrong corpus.

Why Lean, and why now

This PR does not add Lean because medical software sounds mathematical. It adds Lean because the risky rules here are small, finite logical gates with expensive failure modes.

Lean gives us a place to state those gates precisely, try adversarial cases against them, and require future changes to preserve them. Adding that layer now is comparatively cheap: the interfaces are still taking shape, the models are dependency-free, and the proof surface can remain smaller than the Python it constrains. Waiting until these assumptions are spread across a mature ingestion and evaluation pipeline would make the same work both harder and less useful.

The practical payoff is immediate rather than aspirational: formalizing the intended rules exposed concrete URL-scope and accounting bugs in the existing scraper, and this PR fixes them.

Lean is a development and CI dependency only. It is not added to the production runtime, and the formal project has no Mathlib or other external Lean dependencies.

What changes

• pins Lean 4.32.0 and adds a small lake project under formal/;
• models adversarial gates, source URL policy, listing and extraction accounting, verifier receipts, cache admission, evaluation, and verdict construction;
• adds an executable JSONL oracle for shared conformance fixtures;
• rejects off-domain and cross-guidance NICE traversal after URL normalization;
• validates overview authority and reports honest source totals;
• records extraction receipts and provenance instead of relying on silent cardinality changes;
• links Python symbols and paired tests to their Lean specifications with lean-spec tags;
• adds a dedicated GitHub Actions workflow for pull requests, pushes, weekly drift checks, and manual runs.

How the bridge stays maintainable

The source tags are deliberately reviewable rather than magical. A repository checker verifies that every tag names a real theorem, that the theorem has an empty axiom footprint, that a paired Python test exists, and that the formal project has not acquired undeclared dependencies. Reviewers can move from a Python boundary to the corresponding statement without needing to infer which proof was intended.

The shared fixtures provide the other half of the bridge: Lean and Python must emit the same stable accept/reject result and violation code for the cases we use as regression tests.

Proof boundary

These proofs establish properties of the finite models in formal/. They do not prove arbitrary Python bytecode correct, parse arbitrary HTML, establish the medical truth of evidence, or prove a source corpus complete. The Python tests and conformance checks are what connect the model to the implementation.

That boundary is intentional. The goal is a useful logical evaluation layer, not a claim that formal methods have certified the whole application.

Review map

Failure mode	Formal statement	Runtime evidence
Off-domain or cross-guidance traversal	accepted chapters respect the normalized source boundary	paired NICE URL-policy tests
Misleading filtered totals	source totals remain distinct from accepted counts	listing-accounting tests
Silent extraction omission or duplication	extraction receipts account for every accepted section	receipt and provenance tests
Proof/runtime drift	theorem tags resolve and fixtures agree	proof-link checker and JSONL conformance suite

Verification

• lake build --wfail
• proof-link, dependency, and axiom-footprint checks
• shared Lean/Python fixture conformance
• full Python test suite
• Ruff and formatting checks