Evidence-platform prototype report
Source revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. This concrete offline report joins source fingerprints, static checker metadata, explicit withdrawal dependencies and one illustrative operational claim. It is not an independently checked proof or a completed ten-claim buyer pilot.
Source and checker evidence
- 372 families and 719 unique manuscripts inventoried.
- 242 selected family-scope documents located; existence is not proof verification.
- 2933 source files fingerprinted in manifest.json.
- 416 checker configurations scanned in the preserved preflight; no trusted checker executed.
- 2 configurations enable an external kernel: lean/ComparatorChallenges/ArtinParabolicIntersections.json, lean/ComparatorChallenges/TraceIdealTransportSupport.json.
- Independent proof verification: not run.
Explicit corrections and dependencies
The preserved withdrawal scan found 3 proof-withdrawal notices and 2 explicitly named dependency edges. A withdrawn proof does not establish that its mathematical statement is false. Notice dates and the repository history heading differ and must remain separate.
- Algebraicity of Kuga-Satake Correspondences for K3 Surfaces: notice says October 6, 2026; proof withdrawn.
- Algebraicity of Weil classes on split abelian eightfolds: notice says October 6, 2026; proof withdrawn.
- The rational Hodge conjecture for products of K3 surfaces: notice says October 6, 2026; proof withdrawn.
Illustrative software claim
Claim illustrative_host_restricted_chain_bound_misuse uses contract 131-lazy-switch-chain. The linter reports 9 documentary gaps. Full claim audit. Supplied references and statuses are unverified.
- MODEL_SCOPE_MISMATCH: The declared host_model differs from the reviewed theorem model; a separate bridge is needed.
- ADDITIONAL_RESULT_REQUIRED: The reviewed statement does not supply the claimed use: host_restricted_switch_mixing.
- OBLIGATION_UNKNOWN: A material theorem or engineering obligation remains undocumented or unknown.
- OBLIGATION_UNKNOWN: A material theorem or engineering obligation remains undocumented or unknown.
- OBLIGATION_UNKNOWN: A material theorem or engineering obligation remains undocumented or unknown.
- OBLIGATION_UNKNOWN: A material theorem or engineering obligation remains undocumented or unknown.
- OBLIGATION_UNKNOWN: A material theorem or engineering obligation remains undocumented or unknown.
- OBLIGATION_CONTRADICTED: The manifest explicitly reports a failed obligation.
- OBLIGATION_UNKNOWN: A material theorem or engineering obligation remains undocumented or unknown.
The registry currently has 10 curated source/model contracts. Complete documentation is not mathematical applicability certification. The next implementation work is source-location enrichment and an independently executed proof-run adapter; the next business test is a measured expert workflow comparison.