Consume the records. Keep their boundaries.

Replay the exact source-check record

The importer is available on main, but this historical replay deliberately detaches at exact implementation commit 1204a1d267b6217c45c9b17f093cc3587450cf78. The release checkout exercises its current local import consumer and policy in CI; the command below preserves the original implementation boundary. No hosted resolver or MCP service is involved.

git clone https://github.com/metalogiclabs/mathgraph.git mathgraph-import-v1
cd mathgraph-import-v1
git checkout --detach 1204a1d267b6217c45c9b17f093cc3587450cf78

python3 -I -S scripts/mathgraph_import_v1.py \
  --record conformance/import_v1/fixtures/record.json \
  --policy conformance/import_v1/fixtures/trust-policy.json \
  --policy-sha256 944231afaf9d89e6f7dc77d9efbe80dcbd3fc76f8e8f260b32637a0f261faf65 \
  --goal finite_parser_acceptance

Inspect the pinned independent consumer ↗ · Inspect the separately reviewed pinned policy ↗

The trust-policy digest in the command must be obtained through a channel trusted separately from the evidence and policy bytes. This historical replay does not run the original proof, kernel, or source suite; current applicability remains UNKNOWN.

Fetch the public evidence bytes separately

curl --fail --silent \
  https://mathgraph.org/evidence/mg-l4yaml-source-check-20261010/record.json \
  -o record.json

sha256sum record.json

The transport-file hash is distinct from the record’s canonical content digest. Consumers should validate the schema, exact record ID, content_sha256, source commits, and requested scope before using the result.

Replay the pinned Mathlib source index offline.

At exact retrieval snapshot 8e8f5f529b44852815627206dc5b45062f0c96d6, this standard-library consumer validates the canonical manifest, manifest-listed shards, search derivation, source identities, structural relation meanings, endpoint closure, counts, and publication budgets. The exact public trust policy identifies producer e6643d8e3d207893713da94041ff3822c1190457 and qualification wrapper eb3149b70f0cdf39109c775898b19a26574c27e6; its same-owner independent qualification run is public on GitHub Actions ↗.

The bundle was committed at 7519de6a51e524caf70df51d37389ff42d430d43. A later catalogue regeneration run ↗ at 8e8f5f529b44852815627206dc5b45062f0c96d6 reproduced the catalogue with a run-specific policy. It did not replay the exact public trust-policy bytes; these are distinct provenance scopes.

git checkout --detach 8e8f5f529b44852815627206dc5b45062f0c96d6

python3 -I -S -B conformance/source_catalogue_v1/consumer.py \
  --catalogue-root website/public/catalogues/mathlib/v4.34.1 \
  --policy conformance/source_catalogue_v1/trust-policy.json \
  --policy-sha256 c3cdec2b2c784728621bb8c25a055a1e73d67d3c1c922b7ab62b09003399e1c9 \
  --audit-imports

{"source_status":"SOURCE_INDEXED","independent_verification":"NOT_CHECKED","current_applicability":"NOT_CHECKED","freshness":"PINNED_HISTORICAL_SOURCE","authority":"NONE","authorization":"NONE"}

Manifest SHA-256: 5974ac4d68b1e090d511964cd61237565b80d39b5e47e9966171d4d8bcd2fe68. Consumer SHA-256: 583dcfca46854f56469cdda865b5da62b1068e985bdce411dac9c587e556ca5d.

The consumer imports neither the producer implementation nor the MathGraph protocol package. It does not fetch upstream source, run Lean, prove declarations, check current applicability, or authorize action. SOURCE_INDEXED means the pinned source structure passed this finite publication contract; independent proof verification remains NOT_CHECKED.

A same-origin digest detects changed bytes only relative to a trusted pin. Obtain the manifest and policy pins through an independently chosen channel; a Git repository identity is itself a trust-policy choice and is not mathematical truth.

Use the modular contracts locally.

Discover exposes a deterministic advisory request/result contract. Develop publishes one exact finite replay. The Capabilities registry separates the qualified finite entry from experimental candidates. Hosted services remain NOT_DEPLOYED; these commands run from a repository checkout.

python3 -I -S scripts/mathgraph_discover_v1.py --request conformance/discover_v1/fixtures/request.json

python3 -I -S scripts/mathgraph_capability_v1.py --contract conformance/capability_v1/fixtures/capability-contract.json

python3 -I -S conformance/capability_v1/consumer.py \
  --fixture conformance/capability_v1/fixtures/finite-representation-refinement-v1.json \
  --contract conformance/capability_v1/fixtures/capability-contract.json \
  --policy conformance/capability_v1/trust-policy.json \
  --policy-sha256 7069c764579d933679f6bfd9b922a724ad9bcb250e4060c660cb4fd099c60e89

The Discover example is PARTIAL, advisory-only, with verification NOT_CHECKED and FULL_REPLAY_UNAVAILABLE. Attention allocates work; it is not truth confidence.

The general descriptor evaluator returns UNKNOWN, including when its process exits 0. Only the separate exact finite replay produces QUALIFIED_BOUNDED. Obtain the consumer and policy pins through a separately trusted channel before executing; same-origin hashes do not authenticate their publisher.

Discover request · Discover result · Capability descriptor · Evaluation · Registry schema

Finite consumer and isolated replay instructions ↗

Unsigned external correspondence.

The local in-toto adapter provides unsigned correspondence only while binding the exact capability artifact bytes, claim, assumptions, and evidence. Its checked result is correspondence only: signature UNSIGNED; authenticity, signer policy, transparency, and freshness NOT_CHECKED; qualification and current applicability UNKNOWN; action authorization NONE.

The caller selects the expected artifact pin independently. A wrapper never imports the finite contract’s qualification. Sigstore, SCITT, and RATS integrations remain deferred; no signing or transparency verification is implemented here.

Exact in-toto statement · Binding schema · Local correspondence contract ↗

Replay record 002 without MathGraph.org

Acquire these three static inputs first. The replay itself imports only the Python standard library and needs no MathGraph package, service, LLM, or network connection. The trust-policy digest must come from a channel you trust separately from the downloaded policy.

The Resolve bundle schema and Resolve trust-policy schema describe the published transport structure. These schemas do not authenticate records or replace the separately pinned trust policy and semantic replay.

mkdir mathgraph-resolve-v1
cd mathgraph-resolve-v1
curl --fail --remote-name https://mathgraph.org/evidence/mg-living-warrant-openai-jpl-20261010/offline/consumer.py
curl --fail --remote-name https://mathgraph.org/evidence/mg-living-warrant-openai-jpl-20261010/offline/bundle.json
curl --fail --remote-name https://mathgraph.org/evidence/mg-living-warrant-openai-jpl-20261010/offline/trust-policy.json

python3 -I -S -c 'import sys; from hashlib import sha256; from pathlib import Path; expected="27a9be606040cc94a47c9b903dfc1cb24a86cbbc4e05ce71040c6c3d6e8d527b"; actual=sha256(Path("consumer.py").read_bytes()).hexdigest(); sys.exit(None if actual == expected else "consumer.py SHA-256 mismatch: "+actual)'
python3 -I -S -c 'import sys; from hashlib import sha256; from pathlib import Path; expected="09e8d5ba97bca126a81dfe0fcbd5d57f3915ffe71402a497ece4d5e6117f2b4a"; actual=sha256(Path("trust-policy.json").read_bytes()).hexdigest(); sys.exit(None if actual == expected else "trust-policy.json SHA-256 mismatch: "+actual)'

python3 -I -S consumer.py \
  --bundle bundle.json \
  --policy trust-policy.json \
  --policy-sha256 09e8d5ba97bca126a81dfe0fcbd5d57f3915ffe71402a497ece4d5e6117f2b4a

Trust the executable first. Verify the independently obtained consumer and policy pins before execution. Hashes copied only from the same origin as the files provide integrity comparison, not publisher authenticity.

The deterministic report recomputes the seven historical results. It does not accept the snapshot’s reported statuses as resolution authority, rerun the original JPL Lean proof, establish current applicability, or authorize an action.

Check the published static interface over HTTP

curl --fail \
  https://mathgraph.org/examples/resolve-consumer-v1.ts \
  -o resolve-consumer-v1.ts

python3 -I -S -c 'import sys; from hashlib import sha256; from pathlib import Path; expected="e7360df24b2fd0900c8ea88ccb1689163cec73a6c2e2347e4ab2b23b4d01bc2e"; actual=sha256(Path("resolve-consumer-v1.ts").read_bytes()).hexdigest(); sys.exit(None if actual == expected else "resolve-consumer-v1.ts SHA-256 mismatch: "+actual)'

node resolve-consumer-v1.ts https://mathgraph.org

The TypeScript reference is an HTTP client, not an offline replay. It accepts one origin, fetches only fixed documented paths, validates independently compiled-in authority pins, and recomputes the bounded historical closure. It does not provide a public execution endpoint.

The exact static path is declared as text/plain; charset=utf-8 for direct inspection while the global nosniff protection remains enabled. The source stays Node-oriented TypeScript; it is not browser JavaScript, proof code, or a resolver endpoint.

Current public record format

mathgraph.public-consequence-record.v1 separates admission state from finite observations, formal proof replay, fidelity, generalization, current requalification, and source-specific discrepancies.

Machine discovery and permanent versions

Agents begin with /llms.txt or the versioned /.well-known/mathgraph.json discovery manifest, then fetch the short-lived record index. Record a local fetched_at time and re-fetch before max_age_seconds elapse; generated_at is the publication time, not a live response timestamp.

The stable human route for this snapshot is /records/mg-l4yaml-source-check-20261010/v1/. Its qualified evidence JSON stays immutable. Citation, lifecycle presentation, and discovery metadata live in a separately versioned presentation sidecar with visible history; changing that sidecar does not requalify the evidence.

The Lean evidence profile is a proposed draft, not a currently implemented record type.

Scoped badge embed

The existing badge describes only the pinned finite observation and links to the permanent V1 boundary. It is not a universal truth badge, a statement-fidelity certificate, or an endorsement mark.

[![MathGraph: warranted — bounded](https://mathgraph.org/v1/badges/mg-l4yaml-source-check-20261010.svg)](https://mathgraph.org/records/mg-l4yaml-source-check-20261010/v1/)

<a href="https://mathgraph.org/records/mg-l4yaml-source-check-20261010/v1/"><img src="https://mathgraph.org/v1/badges/mg-l4yaml-source-check-20261010.svg" alt="MathGraph: warranted — bounded"></a>

Open the scoped status SVG →

Exact source-bound resolver

The qualified release defines POST /v1/resolve as a localhost read-only preview. It accepts only exact pins and a supported goal. It has strict JSON, content-type, method, and request-size checks. The OpenAPI file is a reproducible contract, not evidence of a hosted service.

{
  "record_id": "mg-l4yaml-source-check-20261010",
  "source_commit": "62bf7077910e888a0bc8adfc8e08a5f500ff3ca3",
  "external_suite_commit": "da267a5c4782e7361e82889e76c0dc7df0e1e870",
  "goal": "finite_parser_acceptance"
}

{
  "authority": "PINNED_SOURCE_LEAN_GUARDS",
  "evidence": [
    "https://github.com/metalogiclabs/mathgraph/actions/runs/38020008793"
  ],
  "record_id": "mg-l4yaml-source-check-20261010",
  "record_sha256": "f0d092974d5d710fe9e17fb6759a894f2c28f2d3f5456439c071bd0a71c8d3cb",
  "scope": "48 pinned external YAML cases plus 4 Lean guard controls",
  "status": "WARRANTED_BOUNDED",
  "truth_promotion": false,
  "verified": {
    "extra_controls": 4,
    "matched": 48,
    "total": 48
  },
  "whole_language_validity": "UNKNOWN"
}

WARRANTED_BOUNDED is returned only for the exact record, both exact source pins, and the supported finite agreement goal. An incorrect pin, unsupported goal, or unknown version returns UNKNOWN or an explicit request error; it never inherits a warrant.

Reproduce the qualification

export MATHGRAPH_V1_EVIDENCE_ZIP=/path/to/l4yaml-v1.zip
export MATHGRAPH_V2_EVIDENCE_ZIP=/path/to/l4yaml-v2.zip
python3 -m unittest discover \
  -s tests -p test_mathgraph_public_evidence_v1.py -v

The 13-test gate validates archive digests, source pins, the publication integrity gate, tamper rejection, negative lineage, resolver method and input limits, fail-closed unknowns, and agreement between human and machine-readable outputs.

Versioning and compatibility

Consumers should treat schema names, record IDs, content digests, and source pins as exact. Unknown versions or fields must be retained where possible and must not be interpreted as known types. No endpoint currently promises automatic requalification, arbitrary proof execution, URL fetching, or a universal truth verdict.