How the Demo Explains Itself ARCHIVE

How the MathLedger Demo Explains Itself

This document accompanies the front-facing demo. It explains what the demo enforces, what it refuses to do, and why those refusals are the point.

How Claims Are Introduced, Tested, and Closed

MathLedger evolves through discrete claim promotion cycles.

This demo represents the current result of such a cycle.

The system does not attempt to implement every idea in its design materials at once. Instead, it advances by introducing narrow claims, subjecting them to hostile review, and closing them only when contradictions are exhausted.

This process is deliberate.

Two Kinds of Pressure

MathLedger development operates under two fundamentally different forms of pressure:

Phase II — Internal Constraint Pressure (Design Grief)

The Field Manual (fm.tex / fm.pdf) is not a roadmap. It is a pressure map.

It encodes mutually incompatible obligations:

• invariants that demand different data structures,
• governance rules that conflict with liveness,
• auditability constraints that fight scalability,
• formal verification assumptions that contradict learning dynamics.

Pressure activates only when a specific obligation is selected for implementation. At that moment, incompatibilities must be confronted, tradeoffs acknowledged, and losses accepted.

This is design grief.

Phase I — External Adversarial Pressure (Truth Discovery)

Once a claim is chosen, it is:

• made executable,
• published,
• and subjected to hostile external review.

• break assumptions,
• find contradictions,
• and attempt replay or misuse.

This is truth discovery.

The Claim Promotion Cycle

MathLedger does not progress linearly. It advances through claim promotion cycles, each with three stages:

• Select one obligation from the Field Manual
• Confront incompatibilities
• Decide what must be sacrificed
• Produce a specific, narrow claim

• Publish the claim
• Subject it to adversarial audit
• Close contradictions or retreat

• The claim is either enforced, scoped, deferred, or abandoned
• Regression guards are added
• The system stabilizes

This alternating structure is intentional. It prevents premature generalization and preserves epistemic honesty.

Promotion Readiness Checklist

A change is not eligible to be treated as a promoted claim unless it passes this checklist. This prevents Phase II (ideas) from bleeding into Phase I (public claims) prematurely.

• The change corresponds to one concrete claim, stated in one sentence.
• It is possible to say what it would mean for that claim to be false.

The claim is labeled as one of:

• Enforced (Tier A): violation becomes mechanically unavoidable to detect
• Visible (Tier B): violation becomes replay-visible but not blocked
• Documented (Tier C): explicitly aspirational / deferred

The change does not silently introduce:

• new trust semantics,
• new cryptographic contracts,
• new "correctness" implications,
• or new threat model assumptions

At least one of the following must exist before release:

• a regression test that fails on reintroduction,
• a build assertion that prevents drift,
• or a hostile audit script check that would catch it.

• A cold evaluator can follow /docs/for-auditors/ without guessing URLs.
• The verifier self-test remains runnable and interpretable.

• The release is versioned, tagged, and pinned.
• /versions/ and /demo/ reflect the same CURRENT version.
• If anything is "out of sync," it must be visibly declared.

• defer the claim,
• narrow the claim,
• or refuse the change.

What This Means for Evaluators

You may notice:

• explicit ABSTAINED outcomes,
• missing features,
• conservative behavior,
• or references to design materials not yet implemented.

The system prefers refusal with explanation over unjustified output. Only claims that have survived hostile review are enforced.

What This Process Does NOT Claim

This process:

• does not claim the system is complete,
• does not claim all obligations are compatible,
• does not guarantee correctness beyond stated enforcement,
• and does not rewrite history when mistakes are found.

• every critique is preserved,
• every fix is versioned,
• and every closed claim remains inspectable.

What the Demo Is Actually Doing

The demo separates exploration from authority.

The boundary is explicit: exploration identifiers never appear in committed data. The random proposal_id from the draft phase is not present in any hash-committed payload. This is not an implementation detail. It is the design.

Exploration is intentionally unconstrained because suggestions are not claims. Authority is explicitly bound because claims have consequences.

Why the System Stops

The demo produces three possible outcomes: VERIFIED, REFUTED, or ABSTAINED.

Validator Coverage (MV Arithmetic Validator)

The MV validator in v0 has limited coverage:

• 2 + 2 = 4 → VERIFIED (covered)
• 2 + 2 = 5 → REFUTED (covered)
• sqrt(2) is irrational → ABSTAINED (not covered: not arithmetic equality)
• 1e308 + 1e308 = inf → ABSTAINED (not covered: float precision)
• 10 / 0 = undefined → ABSTAINED (not covered: division by zero)

The system does not guess. It does not approximate. It does not hedge. When it cannot verify or refute, it stops and says so.

This stopping is correctness, not caution. A system that produces confident outputs when it lacks grounds for confidence is broken. A system that reports the limits of what it can establish is working as intended.

Abstention as a Terminal Outcome

This is not a limitation. It is a design commitment. The system sacrifices:

• Late upgrade: A claim that ABSTAINED cannot later become VERIFIED, even if a verifier is added.
• Institutional override: No human attestation, policy change, or governance decision can retroactively convert ABSTAINED to VERIFIED.
• Optimistic closure: The system cannot record "probably correct" or "likely valid" as a hedge.

1. Replayability requires deterministic outcomes. If the same artifact could produce different outcomes under different regimes, evidence packs would be meaningless.
2. Audit trails must be immutable. A system that allows retroactive upgrades cannot be trusted to preserve its own history.
3. Abstention is information. It records what the system could not establish at the time of evaluation.

• Submitting a new artifact with the same claim text under a different trust class
• Creating a new claim in a later epoch with enhanced verifier coverage
• Documenting that a previously-abstained claim is now known to be valid (externally)

Why ADV Exists

Claims in the demo have trust classes. Three of them (FV, MV, PA) are authority-bearing and can enter the reasoning attestation. One of them (ADV) cannot.

Trust Class Reference (matches UI)

The system is allowed to produce ADV content. It can speculate. It can offer best guesses. It can generate plausible-sounding statements. All of this is permitted in the exploration phase.

But ADV content is explicitly inert. It does not enter the reasoning root (R_t). It does not contribute to the attestation. It is recorded, but it has no authority.

This is not humility theater. The system is not pretending to be modest. It is making a structural distinction: suggestions exist, but they are not claims. The demo enforces this distinction at the data model level. ADV content cannot leak into authority-bearing paths because the code rejects it.

What the Hashes Mean

The demo produces three values: U_t, R_t, and H_t.

These values are deterministic. Given the same inputs, the system produces the same hashes. If you run the demo twice with identical actions, you get identical values.

This enables two properties:

1. Replayability: Anyone with the inputs can verify the outputs.
2. Non-silent drift: If the system's behavior changes, the hashes change. There is no way for the system to produce different outputs while claiming nothing changed.

Evidence Pack + Replay Verification

The demo provides audit-grade closure through evidence packs.

An evidence pack is a self-contained JSON file containing:

• The committed partition snapshot (all claims and their trust classes)
• UVIL events (what the human did)
• Reasoning artifacts (what the system established)
• The attestation hashes (U_t, R_t, H_t)
• The formula note explaining how H_t is computed
• Replay instructions for independent verification

Evidence packs enable independent verification. An auditor with the evidence pack can:

1. Recompute U_t from the UVIL events
2. Recompute R_t from the reasoning artifacts
3. Recompute H_t = SHA256(R_t || U_t)
4. Compare the computed values to the recorded values

Replay verification is fully local. The evidence pack contains everything needed. No API calls, no network access, no external dependencies. The computation is deterministic and reproducible.

If anyone modifies the evidence pack—changing a claim, altering a trust class, editing an artifact—the replay verification fails. The hashes will not match. There is no way to tamper with the evidence without detection.

1. After verification, click "Download Evidence Pack" to save the JSON file
2. Click "Replay & Verify" to recompute and compare hashes locally
3. A PASS result confirms the attestation is intact
4. A FAIL result shows which hashes diverged

Replay verification proves structural integrity, not truth. A PASS result means: the recorded hashes match what the inputs produce. It does not mean: the claims are correct, the verification was sound, or the system behaved safely. The evidence pack proves the audit trail is intact. It proves nothing about what that trail represents.

What This Demo Refuses to Claim

This demo does not claim the system is aligned with human values.

This demo does not claim the system is intelligent.

This demo does not claim the system is safe.

This demo does not claim the system will behave well in novel situations.

This demo claims one thing: the system's governance is legible. You can see what the human committed. You can see what the system established. You can see where the boundary is. You can verify that the boundary was not crossed.

That is all. Governance and epistemic legibility. Nothing else.

How to Read the Demo as Evidence

• The system separates exploration from authority at the data model level.
• The system produces deterministic attestations for committed content.
• The system refuses to include ADV content in authority-bearing paths.
• The system stops and reports ABSTAINED when it cannot verify or refute.
• The human's actions and the system's reasoning are recorded in separate, verifiable structures.

• The system will behave correctly in all cases.
• The system's verification is complete or sound in any formal sense.
• The system's abstention is always appropriate.
• The governance structure prevents all possible failures.
• The demo generalizes to production systems.

If This Feels Restrictive, That Is the Point

The demo does less than you might expect. It stops when it could guess. It refuses to promote ADV content. It separates phases that could be merged. It records hashes that could be omitted.

These restrictions are not limitations to be overcome. They are the design.

A system that does more than it can justify is not more capable. It is less trustworthy. A system that clearly reports its boundaries is not weaker. It is legible.

The demo is shaped this way because the alternative—a system that blurs the line between suggestion and claim, between exploration and authority, between what it knows and what it guesses—is worse. Not harder to build. Worse.

This demo is boring. That is also the point.

Where the Demo Explains Itself in the UI

As of v0.2.0, the demo includes integrated self-explanation that appears directly in the interface. This is not decorative. These explanations are structurally enforced via regression tests.

UI Self-Explanation Integration Points

UI Doc Sources

Auditors reviewing the demo UI should reference:

1. DEMO_SELF_EXPLANATION_UI_PLAN.md - Full specification of all 9 integration points
2. demo/app.py:UI_COPY - Canonical copy strings (line ~83)
3. tests/governance/test_ui_copy_drift.py - Regression tests for copy integrity
4. tools/run_demo_cases.py --ui-tests - Runtime self-explanation verification

Enforcement

Self-explanation content is enforced through:

1. UI_COPY dictionary: All explanation strings are canonical and versioned
2. Copy drift tests: test_ui_copy_drift.py verifies required phrases are present
3. Regression harness: run_demo_cases.py --ui-tests checks endpoint availability
4. No capability claims: Tests verify absence of "safe", "aligned", "intelligent"

What the UI Copy Does NOT Say

The UI self-explanation follows strict constraints:

• Does NOT say "the system believes" (anthropomorphizing)
• Does NOT say "verified correct" (overclaiming validator capability)
• Does NOT say "safe" or "aligned" (capability claims)
• Does NOT use emojis or exclamation marks (false enthusiasm)
• Does NOT promise future capabilities (scope creep)

Two-Lane Architecture

MathLedger operates on a two-lane architecture that separates certified authority from exploratory reasoning.

Lane A: MathLedger Core (Authority Lane)

Lane A is the certification authority. It contains:

• Committed claim artifacts with immutable identifiers
• Attestation hashes (U_t, R_t, H_t)
• Verification outcomes (VERIFIED, REFUTED, ABSTAINED)
• Evidence packs with replay instructions

Lane B: Exploratory / Agent Audit (Discovery Lane)

Lane B is the exploration space. It is a design pattern and planned product lane, not a fully shipped capability.

• Draft proposals with random identifiers
• Suggested trust class assignments
• ADV (Advisory) claims
• Limited sandbox artifacts and advisory notes

• Agent Audit Kit for systematic exploration
• Structured hypothesis testing pipelines
• Multi-agent coordination artifacts

Architectural Invariant: Unidirectional Flow

The only mechanism for Lane B content to influence Lane A is through explicit human commitment via the UVIL (User-Verified Input Loop). At commitment:

1. The random proposal identifier is discarded
2. A new content-derived identifier is computed
3. The exploratory artifact is transformed into an authority-bearing artifact

ACE Methodology + Ordered-Pairs

MathLedger evaluates claims through the ACE (Admissible Claim Engine) using ordered-pair structures.

The ACE operates in three phases:

• A — Admissibility: Is the claim eligible for authority?
• C — Commitment: Has the claim been explicitly committed by a human?
• E — Evaluation: What did the declared verification route produce?

Ordered-Pair Structure: (Claim Artifact, Verification Route)

Every authority-bearing claim in MathLedger is represented as an ordered pair:

(Claim Artifact, Verification Route)

Where:

• Claim Artifact: The specific textual or formal content being asserted
• Verification Route: The declared method by which the claim will be evaluated (FV, MV, PA)

Claim Identity Computation

The claim_id commits to all identity-bearing components:

claim_id = Hash(domain || normalized_claim || verification_route_id || schema_version)

The verification route is part of identity to prevent retroactive route laundering — an attack where an adversary could claim a different verification path was used after observing the outcome.

ACE Phase Details

• FV: Formal proof required (ABSTAINED in v0; no prover implemented)
• MV: Mechanical validation (arithmetic only in v0)
• PA: Procedural attestation (human attests; ABSTAINED for mechanical verification)

Why No Claim Becomes Authoritative Without a Declared Route

This constraint prevents silent authority inflation. Without explicit route declaration:

• The system cannot know how to evaluate the claim
• Auditors cannot verify the evaluation was appropriate
• Retroactive route assignment would enable outcome manipulation

Epistemic Invariants

The following invariants govern authority, abstention, and replay in MathLedger.

Terminal Abstention

• Changing the verification route, or
• Submitting in a new epoch, or
• Using a new schema version

• Re-asserting the same claim text under a different route (new claim_id)
• Creating new claims in later epochs with enhanced coverage
• External documentation that a previously-abstained claim is now known to be valid

ADV Class Quarantine

• The evidence bundle (for transparency)
• The UI root U_t (as user interaction records)

Monotonic Epistemic Time

Invariant Conflict Preservation (Design Grief)

Bidirectional Accountability

Demo Scope Justification

Why the Demo Is Intentionally Minimal

This demo demonstrates governance substrate, not capability. It is designed to be boring.

• Separation of exploration from authority
• Trust class routing
• Deterministic attestation
• Replay verification
• Explicit abstention

• Formal proof verification (no Lean/Z3 integration)
• Comprehensive mechanical validation (arithmetic only)
• Production-scale throughput
• Novel reasoning capabilities

Prevention of Authority Inflation

Authority inflation occurs when a system's claimed capabilities exceed its actual verification coverage. This demo prevents authority inflation through:

1. Explicit validator coverage: The MV validator handles a op b = c patterns only. All other patterns yield ABSTAINED.
2. No implicit promotion: ADV content cannot silently become authority-bearing.
3. Terminal abstention: Claims that cannot be verified remain permanently marked as such (for that claim_id).
4. Forbidden claims list: The demo includes regression tests that detect capability overclaims.

Auditability Over Impressiveness

The demo prioritizes auditability over impressiveness:

• Every outcome is deterministic and reproducible
• Every attestation is independently verifiable
• Every boundary is explicit and documented
• Every refusal is explained

What This Scope Implies for Evaluators

If you are evaluating this demo for:

• Capability: You will be disappointed. The demo does very little.
• Auditability: You should be able to verify every claim the demo makes about itself.
• Governance: You should be able to trace every authority-bearing artifact to its commitment point and verification route.

External Verifier Checklist

For external reviewers verifying the demo independently:

Step 1: Run the drop-in demo

uv run python scripts/run_dropin_demo.py --seed 42 --output demo_output/

Step 2: Run verification

cd demo_output && python verify.py

Step 3: Expected output

[PASS] Composite root verified: H_t == SHA256(R_t || U_t)

Step 4: Artifacts produced

Confirm the following files exist in demo_output/:

• verify.py — Self-contained verifier
• evidence_pack.json — Complete audit artifact
• manifest.json — Execution metadata
• u_t.txt — UI Merkle root
• r_t.txt — Reasoning Merkle root
• h_t.txt — Composite root

Step 5: Verify claim outcomes

In the evidence pack, confirm:

• Claim outcomes include VERIFIED, REFUTED, and/or ABSTAINED as appropriate
• ADV claims (if any) are present in the bundle but excluded from R_t computation
• All authority-bearing claims have a declared verification route

Step 6: Replay with different seed

uv run python scripts/run_dropin_demo.py --seed 43 --output demo_output_43/
cd demo_output_43 && python verify.py

Confirm: different seed produces different hashes, but verification still passes.

Related Work / Canonical Reference

This demo implements a subset of the governance substrate described in the following paper:

• arXiv: https://arxiv.org/abs/2601.00816
• DOI: https://doi.org/10.48550/arXiv.2601.00816
• Subjects: cs.AI, cs.CR, cs.LG

@misc{mathledger2025,
  title={MathLedger: A Verifiable Learning Substrate with Ledger-Attested Feedback},
  author={MathLedger Contributors},
  year={2025},
  eprint={2601.00816},
  archivePrefix={arXiv},
  primaryClass={cs.AI},
  url={https://arxiv.org/abs/2601.00816}
}

What This Section Does and Does Not Claim

• The two-lane architecture separates exploration from authority at the data model level
• The ACE methodology requires explicit route declaration before authority
• The epistemic invariants are enforced in the current implementation
• The demo is intentionally minimal to prevent authority inflation

• Lane B (Agent Audit) is fully shipped as a product
• The system will behave correctly in all cases
• The invariants are complete or cover all failure modes
• The demo generalizes to production systems