Support is reclosed locally.
Withdrawing a receipt affects its admitted descendants, not every claim in the catalogue.
MathGraph Resolve
Evidence can change without truth becoming false.
Resolve recomputes what remains justified under declared evidence, dependencies, scopes, and withdrawals. It preserves alternative support, localizes change, and leaves unsupported conclusions UNKNOWN.
Resolution rules
Change only what the evidence requires.
Independent support remains.
A surviving qualified route can continue to justify a claim at the route's exact scope.
Cycles cannot create evidence.
A dependency loop without a valid evidence root remains UNKNOWN.
Stale is not refuted.
Loss of documentary support does not establish the negation of a mathematical proposition.
Qualified example
When mathematical evidence changes
Three OpenAI publisher-documented support paths become STALE. The related propositions remain UNKNOWN. An unrelated qualified JPL 48-case observation remains WARRANTED_BOUNDED at its original exact scope. Compare the qualified history with the modeled baseline or one explicit counterfactual below.
Documentary original-support routes were modeled as active before publisher withdrawal; this does not prove their correctness.
Read-only evidence explorer
Inspect a resolution without rerunning it.
The historical default below is server-rendered from the qualified snapshot. Optional controls select only precomputed entries from the exact published scenarios artifact; this browser does not resolve claims.
Selective consequence
What changed — and what did not
Three exact objects. No inferred edge between them.
PUBLISHED_AFTERPublished after publisher withdrawalThe publisher withdrew three original arguments. Their prior documentary support paths are stale; mathematical truth remains UNKNOWN.
Changed · documentary support
The documentary support path changes from SOURCE_DOCUMENTED to STALE.
openai.original_support.1BeforeSOURCE_DOCUMENTEDAfterSTALE
Documentary support status is distinct from mathematical truth. This view does not establish that the mathematical proposition is false.
Unchanged · mathematical proposition
The mathematical proposition remains UNKNOWN.
openai.theorem.1BeforeUNKNOWNAfterUNKNOWN
It is not REFUTED. No qualified documentary-to-theorem proof or refutation relation is admitted.
Unchanged · independently bounded observation
The independently bounded observation remains WARRANTED_BOUNDED.
jpl.l4yaml.finite_parser_acceptanceBeforeWARRANTED_BOUNDEDAfterWARRANTED_BOUNDED
nasa-jpl/L4YAML@62bf7077910e888a0bc8adfc8e08a5f500ff3ca3:yaml/yaml-test-suite@da267a5c4782e7361e82889e76c0dc7df0e1e870:48-cases
Published withdrawal receipts: openai.original_publication_receipt.1openai.original_publication_receipt.2openai.original_publication_receipt.3
Invariant boundary: these exact objects remain distinct. Selecting a view does not infer a relation between them or change any object's declared scope.
This synthetic conformance scenario does not use the OpenAI/JPL comparison objects. Inspect its exact precomputed results below.
Precomputed selection only. This is a simulation/counterfactual interface; the browser neither resolves, qualifies, nor mutates historical evidence.
Display-only. Controls unlock only after the same-origin artifact passes its pinned byte digest and identity checks. Every hypothetical view is a simulation and never mutates the immutable historic snapshot.
Static qualified default: Published after publisher withdrawal.
Interactive scenarios are unavailable. The qualified static default remains shown.
If an interaction failure occurs after activation, the qualified default is restored directly from its trusted server-rendered clone; the browser renderer is not used as a fallback.
Qualified historic snapshot
Published after publisher withdrawal
PUBLISHED_AFTERThe publisher withdrew three original arguments. Their prior documentary support paths are stale; mathematical truth remains UNKNOWN.
| Claim at exact scope | Before support | After support | Selected scenario state |
|---|---|---|---|
jpl.l4yaml.finite_parser_acceptance | WARRANTED_BOUNDED | WARRANTED_BOUNDED | WARRANTED_BOUNDED |
openai.original_support.1Algebraicity of Weil classes on split abelian eightfolds | SOURCE_DOCUMENTED | STALE | UNKNOWN |
openai.original_support.2Algebraicity of Kuga–Satake Correspondences for K3 Surfaces | SOURCE_DOCUMENTED | STALE | UNKNOWN |
openai.original_support.3The rational Hodge conjecture for products of K3 surfaces | SOURCE_DOCUMENTED | STALE | UNKNOWN |
openai.theorem.1Algebraicity of Weil classes on split abelian eightfolds | UNKNOWN | UNKNOWN | UNKNOWN |
openai.theorem.2Algebraicity of Kuga–Satake Correspondences for K3 Surfaces | UNKNOWN | UNKNOWN | UNKNOWN |
openai.theorem.3The rational Hodge conjecture for products of K3 surfaces | UNKNOWN | UNKNOWN | UNKNOWN |
Support transitions come from resolutions. Raw selected-scenario claim states come from states. STALE means support was withdrawn; it is not a refutation.
Declared evidence receipts
mathgraph.l4yaml.48-case-qualificationformal · nasa-jpl/L4YAML@62bf7077910e888a0bc8adfc8e08a5f500ff3ca3:yaml/yaml-test-suite@da267a5c4782e7361e82889e76c0dc7df0e1e870:48-casesopenai.original_publication_receipt.1documentary · openai/math:Algebraicity of Weil classes on split abelian eightfolds:original-withdrawn-editionopenai.original_publication_receipt.2documentary · openai/math:Algebraicity of Kuga–Satake Correspondences for K3 Surfaces:original-withdrawn-editionopenai.original_publication_receipt.3documentary · openai/math:The rational Hodge conjecture for products of K3 surfaces:original-withdrawn-edition
Exact withdrawn_evidence field
openai.original_publication_receipt.1Listed inwithdrawn_evidenceopenai.original_publication_receipt.2Listed inwithdrawn_evidenceopenai.original_publication_receipt.3Listed inwithdrawn_evidence
Declared graph routes
mathgraph.l4yaml.48-case-qualificationjpl.l4yaml.finite_parser_acceptanceDeclared in the selected scenario graphopenai.original_publication_receipt.1openai.original_support.1Declared in the selected scenario graphopenai.original_publication_receipt.2openai.original_support.2Declared in the selected scenario graphopenai.original_publication_receipt.3openai.original_support.3Declared in the selected scenario graph
Exact active_routes field
mathgraph.l4yaml.48-case-qualificationjpl.l4yaml.finite_parser_acceptanceListed inactive_routes
Claim states
jpl.l4yaml.finite_parser_acceptanceWARRANTED_BOUNDEDnasa-jpl/L4YAML@62bf7077910e888a0bc8adfc8e08a5f500ff3ca3:yaml/yaml-test-suite@da267a5c4782e7361e82889e76c0dc7df0e1e870:48-casesopenai.original_support.1UNKNOWNopenai/math:Algebraicity of Weil classes on split abelian eightfolds:original-withdrawn-editionopenai.original_support.2UNKNOWNopenai/math:Algebraicity of Kuga–Satake Correspondences for K3 Surfaces:original-withdrawn-editionopenai.original_support.3UNKNOWNopenai/math:The rational Hodge conjecture for products of K3 surfaces:original-withdrawn-editionopenai.theorem.1UNKNOWNNo qualified support route in this snapshotopenai.theorem.2UNKNOWNNo qualified support route in this snapshotopenai.theorem.3UNKNOWNNo qualified support route in this snapshot
Historic graph boundary — unchanged by simulations. No documentary-to-theorem edge is admitted. The withdrawn publication paths and the three mathematical propositions are distinct objects. Each proposition remains UNKNOWN.
Inspect canonical source objects and exact declared relations →
Authority and limits
The interface is not the trust root.
The immutable bundle can be replayed without MathGraph.org. Pinned hashes detect substitution relative to a separately trusted digest; they do not authenticate a publisher or establish truth by themselves.
Producer qualification ↗Same-owner RealityGraph replay ↗Isolated offline replay ↗
The RealityGraph consumer is implementation-independent under the same owner. It is not independent outside-organization adoption and did not rerun the original JPL Lean proof.