Portable evidence without platform dependence.

One protocol, separately usable functions

Independent producers can publish declared receipts and snapshots; independent consumers can validate and replay them without this website. The website is one static publisher and reader. It is not a required runtime, a certificate authority, or the source of the protocol’s validity.

The conceptual Discover → Check → Resolve → Develop loop is optional, not a compulsory runtime pipeline. No autonomous loop is implemented. Capability qualification adds no mathematical terminal form: accepted claims still end in exactly one VERIFIED_PROOF, FINITE_COUNTERMODEL, or NAMED_OBSTRUCTION.

Proposed The Lean evidence profile remains a draft; native replay and independent statement correspondence are separate admission requirements.

Five responsibilities, not a new universal ontology.

Object responsibility

Preserve the exact identity, type, version, source occurrence, attribution, and history already declared by each supported contract.

Relation responsibility

Carry only typed dependencies, evidence support, provenance, withdrawal, or other relations explicitly declared by a qualified source contract. Names and layout create no relation.

Evidence responsibility

Bind a claim to exact sources, verifier results, assumptions, toolchains, scope, and replay boundaries without promoting signatures or hashes into truth.

Resolution responsibility

Let a receiving consumer apply its own pinned policy and distinguish historic warrant, lifecycle, freshness, applicability, and authorization.

Transition responsibility

Represent a separately evidenced lifecycle or developmental change while preserving the byte-identical historical state that preceded it.

These responsibilities organize the current record, Resolve, Discover, capability, and interoperability contracts. They do not replace those contracts with a new serialized Unit type.

CLOSE, ACT, and REFINE do different work.

CLOSE

Bounded support closure over exact admitted roots and declared routes. Unsupported cycles and scope changes remain UNKNOWN.

ACT

Caller policy, viability, and permission. Action authorization remains NONE in every published static consumer and projection here.

REFINE

A separately qualified evidence or lifecycle change. It emits a new event or state and never rewrites historic bytes.

A proof does not authorize an action. A display projection cannot refine evidence. A new distinction requires its own appropriate qualification.

Objects required by the bounded replay

This is the minimum common model exercised by record 002, not a claim that every proposed MathGraph semantic object has a stable public contract.

Rooted, exact-scope resolution

Each dependency route is conjunctive: every named premise and evidence receipt must be supported. Separate routes to the same conclusion are alternatives, so one route can disappear while another preserves support.

Resolution computes a least fixed point from admitted qualified roots. A dependency cycle without such a root remains UNKNOWN; cycles cannot manufacture support or create circular self-justification.

Claims, receipts, premises, verifier identities, assumptions, source pins, and scopes are exact. An unsupported semantic transport, implication, equivalence, kind change, or scope generalization returns UNKNOWN or an explicit validation error. Similar names, shapes, and hashes establish no correspondence.

Content identity is not claim truth

Canonical content identities make exact objects addressable. Source pins name repositories, commits, files, and toolchains. A content hash proves byte identity relative to an expected digest; it does not authenticate its own publisher or establish that the represented claim is correct.

The historical Crystal/MGSO envelope remains an experimental semantic transport candidate. Its MGSO magic prefix and canonical encoding are not the deployed P0 record format, and unfamiliar object types must be preserved or declined—not coerced into known semantics.

Verification receipts therefore keep native-verifier authority, source identity, assumptions, and result separate. External proof assistants and finite checkers retain their own semantics; MathGraph does not replace them.

Historical qualification is not current applicability

An immutable snapshot can establish what qualified evidence supported at a pinned historical point. Historical qualification and historical support resolution remain distinct from current applicability, freshness, lifecycle, revocation or supersession, and action authorization.

The offline record-002 replay reports current applicability as UNKNOWN, freshness as NOT_CHECKED, revocation or supersession as NOT_CHECKED, and action authorization as NONE. A withdrawal can make documentary support STALE without making a mathematical proposition REFUTED.

Authenticity is not semantic correctness

A signature authenticates a signed statement under a key policy; it does not establish the truth of that statement. A cryptographic commitment likewise binds bytes without proving their mathematical or semantic meaning.

The local in-toto profile implements unsigned correspondence only for one exact capability descriptor. The wrapper does not import qualification: signature is UNSIGNED, authenticity and freshness are NOT_CHECKED, qualification and current applicability are UNKNOWN, and action authorization is NONE. Inspect the exact binding contract.

Sigstore, SCITT, and RATS remain deferred extension boundaries. No signing, transparency verification, partnership, or endorsement is established. Full interoperability boundary ↗

The experiment is evidence that a bounded warrant can be signed and replayed—not a claim of general security, universal verification, production post-quantum security, or semantic truth.