On this page
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 self_authored_zero_startup_uniform_kserver_claim uses contract 110-uniform-kserver. The linter reports 11 documentary gaps. Full claim audit. Supplied references and statuses are unverified.
- MODEL_SCOPE_MISMATCH: The declared additive_cost_model differs from the reviewed theorem model; a separate bridge is needed.
- ADDITIONAL_RESULT_REQUIRED: The reviewed statement does not supply the claimed use: zero_additive_loss_for_uniform_implementation.
- ADDITIONAL_RESULT_REQUIRED: The reviewed statement does not supply the claimed use: polynomial_activation_delay.
- 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.
- OBLIGATION_UNKNOWN: A material theorem or engineering obligation remains undocumented or unknown.
The registry currently has 13 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.
Preserved report inputs
All six research inputs, including the exact linter and bundle generator, are copied into input-archive. Their byte hashes and original paths are retained in the manifest. These snapshots remain inert reference material; no archived source or proof code is executed. Later tool edits do not replace this report's inputs.