Skip to main content

40  Proof-Carrying Claims and Adversarial Review

40.1 Chapter status

Field	Value
Chapter ID	spinoza-verification-and-proof-carrying-claims
Part	Part II - Planning, Memory, Reasoning, and Execution
Status	conceptual
Manuscript maturity	v0.3 manuscript draft
Last updated	2026-08-02
Primary source records	spinoza, genesiscode, coherence_exchange, verification_bandwidth, treellm, uat, talos, ext_proof_carrying_code_1997, ext_lean4_theorem_proving, ext_autoformalization_llms_2022, ext_ai_safety_debate_2018, ext_llm_as_judge_mt_bench_2023, ext_contestable_ai_design_2022, cca_project, moecot_manifest_project, beastbrain_project, bugbrain_project, corbens_best_model_possible_project
Claim label	Design rationale
Evidence level	argument
Source queue	primary: spinoza; supporting: genesiscode, coherence_exchange, verification_bandwidth, treellm, uat, talos, cca_project, moecot_manifest_project, beastbrain_project, bugbrain_project, corbens_best_model_possible_project; external comparators: ext_proof_carrying_code_1997, ext_lean4_theorem_proving, ext_autoformalization_llms_2022, ext_ai_safety_debate_2018, ext_llm_as_judge_mt_bench_2023, ext_contestable_ai_design_2022
Source loading state	source notes: spinoza, deterministic_capability_compilation, platonic_world_model, genesiscode, coherence_exchange, verification_bandwidth, treellm, uat, talos, ext_proof_carrying_code_1997, ext_lean4_theorem_proving, ext_autoformalization_llms_2022, ext_ai_safety_debate_2018, ext_llm_as_judge_mt_bench_2023, ext_contestable_ai_design_2022, cca_project, moecot_manifest_project, beastbrain_project, bugbrain_project, corbens_best_model_possible_project; raw cache: spinoza, genesiscode, verification_bandwidth, treellm, uat, talos; connector/recovery: coherence_exchange
Test state	Exact authored refinements: 3 valid/5 rejecting proof-carrying fixtures, 2 valid/7 rejecting dossier cases, 6 stages, 23 routes, and 36/36 rejected target-to-writeback mutations; plus 3 valid/5 rejecting Tribunal reviews, 1 valid/11 rejecting method/independence records, 7 stages, 28 routes, and 45/45 rejected versioned-verdict/appeal mutations. The family has 44 live declarations across four modules and five public targets: 18 Proof-Carrying Claims refinement, 4 retained Proof-Carrying Claims legacy, 19 Tribunal refinement, and 3 retained Tribunal countermodels. No natural target corpus, verifier-soundness or citation-validity campaign, semantic-equivalence evaluator, model judge, debate, competence audit, verdict-correctness result, useful advantage, reproduction, transfer, or core support effect.

The executed merge combines two verification-event families:

• proof-carrying claim records, which ask whether selected claims have an explicit tier, justification type, interpretation mapping, verifier artifact, failed-attempt route, formal scope, support-state effect, residual route, and non-claim boundary;
• tribunal review records, which ask whether contested or high-risk claims and artifacts have bounded dossiers, reviewer roles, adversarial probes, evidence-linked findings, dissent, cycle caps, unchanged-evidence guards, verdicts, required actions, and constraint effects.

40.2 Drafting guardrail

This layer owns prospective selection, execution, and custody of claim-specific verification or adversarial-review routes plus their bounded verdict contracts. It binds a frozen target to its interpretation mapping, route, artifacts, trusted verifier boundary, attempt history, dossier, reviewer-dependence graph, attacks, dissent, verdict, constraints, residuals, and exact writeback request.

It does not own claim identity, obligation adequacy, source truth, theorem meaning, proof-kernel validity, empirical correspondence, reviewer competence, support movement, action authority, contestability legitimacy, rights, cost, or release. A formally valid artifact can target the wrong proposition. A complete tribunal record can reach a wrong verdict. A correct narrow verdict can still be unsafe to generalize. The honest result is a reconstructable bounded verification event, not a truth machine.

40.3 Human Reading Path

Concrete lens. The status-label baseline copies “accepted” forward. The proof-carrying envelope binds verdict to artifact, evidence, interpretation, probes, dissent, and expiry.

Some claims are cheap enough to remain drafts while evidence matures. Other claims shape plans, permissions, releases, or safety boundaries. Those claims need more than a well-written paragraph.

The first upgrade is a proof-carrying or justification-carrying envelope. The system chooses a tier: formal proof, citation dossier, executable procedure, replay log, benchmark artifact, tribunal review, or downgrade route. It records the mapping from the human-language claim to the artifact that was checked, and it records the limits of that check.

When the claim is contested, high-risk, or mismatched, adversarial review is the next escalation. A tribunal-style record defines a dossier, assigns roles, runs probes, preserves dissent, and issues scoped actions. The result goes back to the claim ledger as a bounded effect: no change, downgrade, block, revise, accept within scope, or escalate.

The reader-level point is simple: stronger claims should leave stronger evidence trails, and failed review should be remembered. A proof, citation, benchmark, replay, or tribunal verdict earns its place when later readers can see what it covered, what it missed, who challenged it, and what changed.

40.4 Problem

High-value claims and high-risk artifacts need a governed verification path that can choose proof, citation, procedure, replay, benchmark, or adversarial-review treatment without laundering failed, mismatched, or contested evidence into support.

The claim ledger gives claims durable identity and history. That is necessary but not enough. Some claims need evidence stronger than ordinary prose. Some need a formal proof. Some need citations. Some need an executable procedure or replay. Some need a tribunal because the mapping is contested, the stakes are high, or the evidence points in different directions.

This verification-event layer defines how a claim or artifact receives a justification envelope, how failure is preserved, how adversarial review operates, and how bounded results write back to the ledger without overclaiming. The same path also protects readers and downstream systems from treating fluent certainty as verified standing.

40.5 Why existing approaches are insufficient

Neural generation, one-pass self-critique, and informal review can produce plausible justification language without preserving proof scope, verifier result, evidence dossier, dissent, failed attempts, verdict constraints, or downgrade routes.

A model can explain why a claim sounds right without checking it. A proof can verify the wrong formalization. A citation can support a nearby statement but not the target inference. A reviewer can agree without independent evidence. A tribunal can be rerun until it accepts unchanged evidence. If the record does not preserve those failures, review becomes a confidence-laundering machine.

External comparators help position the boundary but do not prove it. Proof-carrying-code literature, Lean theorem-proving materials, autoformalization work, debate, LLM-as-judge evaluation, and contestable-AI design all illuminate adjacent parts of the problem. Proof-carrying code shows why evidence should travel with an artifact and remain scoped to a consumer policy. Lean grounds the proof-assistant vocabulary. Autoformalization sharpens the interpretation risk between prose and formal target. Debate and LLM-as-judge work show why scalable review needs judge limits, adversarial pressure, bias controls, and human-calibration records. Contestable-AI design grounds the challenge, appeal, audit, and dissent surface. The ASI Stack uses them as comparators while asking a systems question: what record should exist before a claim receives stronger standing?

40.6 Core Claim

[spinoza-verification-and-proof-carrying-claims.core, label: Design rationale, support: argument] Selected claims and artifacts should move through proof-carrying, justification-carrying, or adversarial-review envelopes that record tier, interpretation mapping, evidence dossier, verifier or tribunal result, dissent, limitations, failed attempts, required actions, residuals, and ledger effects.

Reader claim. A passing verifier result belongs to one interpretation, evidence set, artifact version, and claim scope; changed evidence or unresolved dissent prevents silent reuse.

Operational rule. Bind every verdict to exact claim semantics, evidence digest, verifier and reviewer identities, probes, failed attempts, dissent, constraints, required actions, expiry, and ledger effect. Negative results cannot promote, and changed evidence requires a new review rather than editing the old verdict.

40.6.1 Worked tribunal reuse: the evidence changed after acceptance

A high-risk artifact receives an accepted tribunal verdict after independent review and adversarial probes. The verdict records one unresolved dissent but constrains use to a narrow read-only environment. A later artifact version changes its tool interface and adds new evidence. A status-only system reuses the old “accepted” label. The proof-carrying envelope instead detects the artifact and evidence digest changes, preserves the prior verdict, and routes the successor to new probes and review.

If the dissent was never recorded, the route cannot call the earlier review complete. If the new verdict requires actions, those actions need explicit constraints and owners before any downstream ledger change. The finite record model rejects passed verifiers without artifacts, negative results with promotion, high-risk acceptance without probes or independence, changed-evidence reuse, missing dissent, and unconstrained action verdicts. It does not prove verifier correctness, reviewer independence, semantic mapping, evidence truth, or artifact safety.

The claim remains at argument support. Spinoza supplies the central discipline: neural systems may propose, but structured verifiers decide; formal scope is explicit; outward claims carry tiers; unknown, failed, timed-out, or mismatched verification cannot be narrated as success. GenesisCode supplies the obligation-envelope pattern for software artifacts: obligations, evidence hashes, replay logs, semantic patches, provenance, and small trusted-core boundaries. UAT supplies retrieval-bounded proposition review, adversarial siege, cycle caps, and human checkpoints. Talos supplies execution/audit pressure for review artifacts: claim graphs, evidence sets, proof bundles, logs, replay, residual risk, and human adjudication. Verification Bandwidth explains why some claims need stronger verification rather than more context. TreeLLM supplies a possible semantic representation substrate for interpretation mappings and traces. Coherence Exchange remains a speculative synthesis context rather than verifier evidence.

40.6.2 Claim-source mapping status

Appendix C maps the core claim to all eighteen assigned sources. Six local raw caches are passage-reviewed; coherence_exchange remains source-note/connector bounded; the five historical projects have public-safe pinned notes; and all six external comparators have bounded source notes, with the debate paper reviewed in full. The mappings support route and record design, not local theorem or source validity, semantic equivalence, judge calibration, reviewer competence, verdict correctness, institutional redress, or deployed behavior.

Lineage	Source IDs	What the sources contribute	Limit
Proof-carrying claims	spinoza, genesiscode, verification_bandwidth, treellm, coherence_exchange	Proposer/verifier separation, tiered claims, proof/citation/procedure envelopes, obligation artifacts, downgrade behavior, verification-workspace limits, and possible semantic traces.	No open-domain autoformalizer, arbitrary theorem-validity result, citation validator, semantic-equivalence checker, or verifier-quality result exists here.
Tribunal review	uat, spinoza, talos, verification_bandwidth, coherence_exchange	Retrieval-bounded dossiers, atomic proposition states, adversarial probes, reviewer roles, dissent, cycle caps, SME checkpoints, constraint effects, action-linked review artifacts, and Talos’s final correction that capped termination, state stability, epistemic revision, and correctness are different properties.	No multi-reviewer tribunal run, reviewer-independence audit, adversarial-probe-quality result, consensus-quality result, density/coverage validity result, cost-certainty result, or verdict-correctness result exists here.
External comparators	ext_proof_carrying_code_1997, ext_lean4_theorem_proving, ext_autoformalization_llms_2022, ext_ai_safety_debate_2018, ext_llm_as_judge_mt_bench_2023, ext_contestable_ai_design_2022	Position machine-checkable evidence, dependent-type proof practice, informal-to-formal translation, adversarial debate, model-graded review, and contestable review surfaces.	Comparator status only; no local reproduction, autoformalizer, debate run, judge-calibration result, tribunal-quality result, or support-state promotion.

40.6.3 Strongest objection

Method diversity can be theater. Differently named checks may share evidence, models, prompts, implementations, organizations, incentives, or blind spots. Even genuinely different methods can all target the wrong proposition or reward the same persuasive proxy. Formal proof, debate, model judging, human review, and contestability also impose latency, privacy, expertise, and appeal costs; a simpler source check or accountable editor may perform as well. The design case therefore needs semantic, competence, outcome, safety, and total cost comparisons rather than method labels, agreement, or internal consistency.

40.7 Mechanism

The verification event begins only after an exact target and adequacy request exist. Its first half fixes the target, declares eligible modes, chooses the route prospectively, preserves interpretation uncertainty, binds artifacts and trusted verifiers, and records every attempt. That structure separates the thing a consumer cares about from the formal, textual, procedural, replay, or review object that a particular method actually inspects.

The second half governs contested review and bounded consequences. It defines the dossier world, maps dependence among reviewers, runs named attacks, retains ignorance and dissent, constrains reuse, and issues a typed verdict. Writeback then becomes an explicit request to the proper owner rather than an automatic promotion. The full contract has eighteen mechanisms:

1. Freeze target claim or artifact identity, exact natural and formal scope, definitions, assumptions, consumer, consequence, risk, requested standing or action effect, authority, rights, budget, horizon, and change triggers before route outcomes.
2. Classify the target and declare eligible, ineligible, required, and unavailable verification modes: source inspection, citation dossier, formal proof, executable procedure, replay, benchmark, adversarial review, accountable-human adjudication, downgrade, block, or abstention.
3. Select a prospectively justified route or route portfolio under an explicit adequacy request, trusted-core boundary, resource envelope, and refusal rule rather than choosing the route after seeing a favorable result.
4. Bind source prose, normalized claim, formal target, interpretation mapping, ambiguity, scope delta, semantic-adequacy state, mapper identity, independent review, and unresolved mismatch without treating formal syntax as semantic equivalence.
5. Bind every justification artifact to content identity, environment and policy version, producer, consumer checker, verifier implementation, trust root, dependencies, expiry, replay boundary, and exact property checked.
6. Execute the declared route and retain every proof search, source check, procedure, replay, benchmark, counterexample, timeout, parse failure, retry, intervention, failed attempt, and discarded candidate.
7. Enforce route-specific evidence contracts: formal routes carry checkable proof or countermodel artifacts; citation routes carry versioned spans and entailment review; procedures, replay, and benchmarks carry pinned inputs, code, environment, logs, metrics, and residuals.
8. Keep artifact shape, checker acceptance, interpretation adequacy, premise truth, source validity, empirical correspondence, outcome relevance, support movement, authority, and release as distinct states with distinct owners.
9. Declare an epistemic trusted computing base with named roots, bounded delegation, verifier and policy versions, recursion stop, outside-TCB residuals, compromise response, and no ambient self-verifier trust.
10. Construct bounded review dossiers with exact target, evidence world, omitted frontier, evidence and attack refs, prior attempts, known conflicts, affected parties, decision options, and disclosure limits.
11. Assign reviewer, proposer, critic, judge, subject-matter, red-team, appeal, and accountable-human roles while recording model, data, prompt, code, infrastructure, organization, incentive, and temporal dependence.
12. Run prospectively declared adversarial probes for contradiction, counterexample, omission, source challenge, interpretation mismatch, policy mismatch, judge bias, persuasion, collusion, and strategic abstention.
13. Bound turns, retrieval expansion, compute, latency, human work, privacy exposure, appeal, and stop rules while preserving unresolved questions instead of narrating convergence or budget exhaustion as truth.
14. Preserve dissent, veto, justified ignorance, abstention, minority findings, reviewer disagreement, appeal grounds, confidence limits, and reasons; forbid empty-case, consensus-only, or default approval.
15. Reuse prior review only when target, evidence, mapping, model, verifier, policy, threat, environment, authority, rights, and outcome boundary are unchanged and the reuse guard is independently checkable.
16. Issue a typed verdict with exact scope, evidence basis, method and independence limits, required actions, constraint effects, expiry, residuals, appeal route, human decision, and explicit non-claims.
17. Write only bounded proposals or effects to Claim Ledgers, Evidence States, Planning, Execution, Readiness, and Release owners: no change, narrow, split, downgrade, block, revise, scoped acceptance, escalation, dispatch constraint, authority narrowing, or residual work.
18. Compare governed routing against direct answer, self-critique, citation-only, proof-only, replay-only, benchmark-only, model-judge, debate, human-review, and abstention baselines under matched targets, information, resources, authority, complete failures, delayed outcomes, and total cost.

flowchart LR
  A["Frozen target + adequacy request"] --> B["Eligible modes + prospective route"]
  B --> C["Interpretation mapping + artifact contract"]
  C --> D["Trusted verifier + complete attempts"]
  D --> E{"Contested / high risk / mismatch?"}
  E -- "no" --> F["Mode-scoped result"]
  E -- "yes" --> G["Dossier + roles + attacks"]
  G --> H["Dissent + bounded verdict"]
  F --> I["Typed consequence proposal"]
  H --> I
  I --> J["Owning ledger / evidence / action gate"]
  J --> K["Accepted bounded effect"]
  J --> L["Reject / narrow / residual / appeal"]

How to read the verification-event flow: The path begins with a frozen consumer question, not a favored method. Interpretation and artifact contracts precede execution. High-risk, contested, or mismatched cases add dossier, attack, dependence, and dissent records. The resulting verdict remains a scoped consequence proposal until the separate ledger, evidence, action, readiness, or release owner accepts it.

The central distinction is between custody and authority. This layer keeps the route, artifacts, failures, review history, and verdict reconstructable. Formal kernels, source reviewers, empirical evaluators, accountable humans, Evidence States, and downstream control layers retain authority over their respective questions. A complete record therefore exposes where confidence came from without turning record completeness into confidence.

40.7.1 Commitment classes, interpretation custody, and semantic escape

The complete Spinoza lineage makes an important correction to a simple “certified / probable / speculative” ladder. A formal proof, a mapping to a norm, a reproducible procedure, and a heuristic synthesis are different justification classes, not interchangeable amounts of confidence:

Class	Required artifact	What it can establish	What remains outside it
deductive	exact formal target, proof term or certificate, dependencies, theory and kernel pins	checker acceptance for that target in that theory	intended meaning, premise truth, world fit, safety, and authority
norm-anchored	exact versioned spans plus a Formal Interpretation Mapping Object	one documented reading under declared applicability and conflict rules	unique interpretation, legal correctness, legitimacy, or compliance approval
procedural	pinned inputs, toolchain, run, output, log, and replay checksum	that the declared procedure produced the result under those pins	that the procedure encodes the right standard or predicts the world
speculative	labeled synthesis plus sources, assumptions, uncertainty, and verification route	a proposal that may be examined	commitment, support, action authority, or release
metacognitive	named metric, detector, window, threshold, log, and escalation owner	a bounded observation about the verification system	permission to rewrite its own policy, bridge, axiom, or support state

No class automatically dominates another. A procedure can reveal that a formal model omitted a physical condition. A proof and a norm mapping can both be valid inside different scopes while disagreeing at their interface. A monitoring alert can require review without becoming a self-authenticating truth. Each class therefore keeps its own scope, allowed consumers, expiry, downgrade rule, and non-claims.

A Formal Interpretation Mapping Object makes the norm route concrete. It pins corpus identity and version, exact span and hash, jurisdiction and effective time, subject and applicability predicates, exceptions, imported definitions, term bindings, interpretation mode, competing-norm set, conflict policy, assumption ledger, creator and reviewer, and canonical object hash. Anchor-only, explicitly mapped, and conflict-checked states remain distinct. Even the strongest state means “this documented reading was checked against this declared conflict set,” not “the organization is compliant.” A disputed mapping forks or downgrades the result instead of disappearing behind a green badge.

Formalization then needs two complementary meaning checks. First, a deterministic renderer exposes every quantifier, negation, condition, scope, and exception rather than asking another language model for a persuasive paraphrase. Ambiguous inputs produce several side-by-side candidates and a semantic diff. Second, counterexample-driven intent testing supplies positive, negative, boundary, and quantifier/exception-confuser scenarios. If the selected statement classifies those cases differently from the intended meaning, it is rejected or quarantined before proof can raise its standing.

These checks reduce one failure path; they do not prove equivalence. The formalizer, renderer, scenario generator, schema author, and reviewer may share the same missing concept. The record therefore retains the original prose, formal candidate, deterministic rendering, scenario suite, reviewer role, uncovered frontier, and later semantic escapes—cases in which an accepted mapping fails independently labeled scenarios after deployment.

Routine mappings also cannot require a confirmation click forever. A trusted template registry may automate restricted formalization, norm-mapping, or procedure templates only through a multi-factor record: diverse slot and boundary coverage, scenario-test history, rollback and escape rate, approved compartments and versions, reviewer quality and dependence, time and drift, centrality, and adversarial signals. Audit sampling emphasizes rare buckets, boundaries, changed distributions, and high-impact templates. Bursts, repeated easy values, and implausibly fast approvals are grinding signals. Trust decays when schema, source, policy, conflict incidence, or use distribution changes; the source’s suggested counts and thresholds remain unvalidated parameters.

Finally, proof validity is compartment-relative. A least-privilege bridge names the exact imported symbols and permitted lemma shapes, explicitly forbids other imports, binds proof or regression duties, records the background assumptions on both sides, and carries rate and centrality budgets. Cross-class or cross-compartment contradictions end in typed routes—quarantine, downgrade, fork, replay, supersession, governance escalation, or persistent conflict—not an implicit priority rule. This turns proof laundering, hidden definition imports, and background-assumption drift into reviewable artifacts.

The corresponding evaluation is not proof count alone. It jointly measures semantic escape, contradiction persistence, silence or paralysis, confirmation fatigue, proof-laundering resistance, useful outcomes, error cost, latency, privacy exposure, maintenance, and human governance burden against direct, citation-only, stateless-prover, checklist, and accountable-editor baselines.

TreeLLM adds a specific anti-laundering case: a traversal path is an execution trace, not a proof-carrying claim. It may show which graph objects and edge types a navigator visited, but it does not establish stable referent resolution, edge truth, source authority, entailment, completeness, causal use by the model, or answer correctness. The claim packet therefore binds path and graph epochs, exact object and sense identities, relation provenance, contradictions, approximate or speculative hops, omitted frontier, retrieved context, cited context, and evidence actually used. Soft links and Scout bridges remain proposals; repeated traversal cannot harden them into belief. The source’s perfect-grounding and native-explainability language is explicitly rejected, and no TreeLLM implementation or result is imported.

40.7.2 Proof-carrying training and semantic-basis validity

Deterministic Capability Compilation proposes a proof-carrying training receipt that binds exact source charter and scaffold, base model, corpus and counterexamples, code, optimizer, seeds, budgets, parameter changes, denominators, failures, authority, rollback, evaluator dependencies, support effect, and non-claims. The receipt does not prove equivalence; it makes candidate-specific translation validation and later challenge reproducible. pass, fail, and unknown remain distinct verdicts.

The Platonic World Model adds the semantic validity conditions for a proof. A proof or justification names immutable Form and relation versions, context, world branch, assumptions, inference rules, attestations, tools, calibration, defeaters, and replay environment. A proof can remain historically replayable while becoming invalid under the current preferred basis or unauthorized for a present action. Formal deduction, statistical synthesis, measurement procedure, and review dossier are different proof-object types and cannot borrow one another’s certainty.

40.7.3 What a bounded verification loop converges to

The Talos lineage usefully corrects its own early “truth by siege” language. Its final form says adversarial review converges because time, tokens, and cycles are capped—not because the process reaches truth. That distinction separates four properties that a verifier record must not merge:

1. Termination means every attempt reaches a typed terminal route before its budget expires.
2. Within-run state discipline means one frozen claim, evidence set, policy, and evaluator cannot change state without a recorded transition.
3. Cross-run epistemic revision means new evidence, definitions, policy, ontology, attacks, or evaluator findings may downgrade or split an earlier result.
4. Correctness means the scoped proposition actually satisfies an external target; termination, stability, and a clean transition history do not establish it.

A three-state vocabulary such as supported, uncertain, and refuted is useful only when each state binds claim version, scope, evidence set, verifier, policy, time, environment, and defeaters. “Supported” is not an absorbing state. It may remain stable inside a frozen run while being superseded or downgraded later. The ledger must preserve both the historical verdict and the current materialized view.

Likewise, draft stability and information density are control signals rather than truth metrics. Low edit distance can mean that reviewers share the same blind spot. High claim density can reward duplicated or atomized nonsense. Domain coverage is undefined without a declared denominator and omission evaluator. These measures may trigger more retrieval, another method, human review, abstention, or a residual; none may promote the claim by itself.

The same caution applies to cost-versus-certainty. More retrieval and review can reduce some uncertainty, but can also introduce contradictory evidence, correlated judges, fatigue, privacy exposure, delay, or new unknowns. The useful object is an empirical, task-specific frontier over accepted utility, calibration, omission, unsafe release, cost, latency, and human burden—not a strict law that spending more monotonically buys truth.

40.8 Interfaces

Ownership stays explicit across twelve interfaces:

1. Claim Ledgers supply durable target identity and version history and receive bounded verdict events; they do not judge route adequacy or verdict correctness.
2. Verification Bandwidth supplies the frozen obligation and adequacy request; this layer executes selected verification and review routes rather than declaring total claim adequacy.
3. Evidence States owns accepted support transitions; a verifier or tribunal may propose, constrain, or block a transition but cannot promote itself.
4. VCM and Context Transactions supply exact source, evidence, and dossier views with provenance, policy, taint, rights, and expiry; availability is not verification success.
5. Formal kernels, proof checkers, solvers, procedure runners, replay engines, benchmark harnesses, citation reviewers, and empirical evaluators own the validity of their exact mode-specific result.
6. Artifact Graphs owns general artifact identity, lineage, receipt faithfulness, replay grade, and audit reconstruction; this layer binds those artifacts to verification attempts and verdict scope.

7. Scalable Oversight and accountable-human governance own reviewer competence, contestability, appeal, adjudication, and affected-party legitimacy beyond the finite tribunal record.
8. Security, Privacy, Rights, and Licensing owners constrain dossier access, evaluator exposure, source use, disclosure, retention, and redress.
9. Planning, Labor OS, runtime adapters, and tool-permission owners consume explicit constraints and required actions without interpreting review rhetoric as execution authority.
10. Resource Economics owns model, tool, compute, latency, human-work, privacy, recovery, and opportunity-cost accounting across all routes and failed attempts.
11. Readiness and publication owners decide release and public wording from accepted evidence and bounded verdicts; tribunal acceptance is not release approval.
12. Historical Spinoza, GenesisCode, UAT, Talos, and project records plus external PCC, Lean, autoformalization, debate, model-judge, and contestability sources supply design lineage and comparators, not local verifier-quality evidence.

Minimum proof-carrying and tribunal fields include:

Record family	Representative fields
Proof-carrying claim	proof_claim_id, claim_id, claim_scope, required_tier, justification_type, interpretation_mapping, interpretation_confidence, justification_artifact, artifact_validity_state, semantic_adequacy, verifier, verifier_result, verifier_artifact_refs, failed_attempt_refs, formal_scope, limitations, consumer_requirements, downgrade_rule, claim_validity_effect, residual_route, tribunal_ref, ledger_update, source_refs, support_state_effect, non_claims
Tribunal review record	review_id, target_ref, review_state, risk_class, dossier_boundary, dossier_refs, reviewer_independence, reviewer_roles, adversarial_probes, cycle_cap, prior_review_refs, unchanged_evidence_guard, retrieval_expansion_policy, findings, evidence_refs, dissent, unresolved_issues, verdict, required_actions, constraint_effects, human_adjudication, non_claims

The current public schemas do not yet represent every field in the expanded contract, including prospective route portfolios, exact dependency dimensions, appeal state, judge-bias probes, changed-boundary reuse checks, and total cost. Those gaps are implementation residuals rather than fields silently inferred from the existing records.

40.9 Invariants

The invariants preserve target, method, artifact, evaluator, verdict, and consequence boundaries through the whole event. They turn a favorable result into a scoped fact about one attempted route rather than a general license to claim truth, support, authority, or release.

1. Every route binds one exact target version, natural and formal scope, definitions, assumptions, consumer, consequence, risk, requested effect, authority, rights, budget, horizon, and expiry boundary.
2. Route selection, obligation adequacy, artifact validity, interpretation adequacy, premise or source validity, empirical correspondence, verdict correctness, support, action authority, and release remain distinct.
3. Every formal, citation, procedure, replay, benchmark, adversarial, and human-review route carries its exact required artifact and mode-specific validity state.
4. A narrow theorem, citation, procedure, replay, benchmark, or verdict never widens to a broader proposition, population, environment, policy, threat, outcome, or time without separate accepted mapping and evidence.
5. Passed, failed, refuted, timed-out, mismatched, unknown, infeasible, disputed, abstained, blocked, and not-run outcomes remain distinct and inspectable.
6. Failed, timed-out, mismatched, unknown, or missing required routes cannot create an upward support, authority, readiness, or release effect.
7. Every artifact binds exact bytes or content identity, producer, checker, environment, policy, dependencies, trust root, replay boundary, property, expiry, and residuals.
8. The trusted verifier boundary names roots, delegation, recursion stop, versions, outside-TCB residuals, compromise response, and independent observation; a component cannot establish its own trust by declaration.
9. Dossiers expose their evidence world, omitted frontier, source transformations, prior attempts, conflicts, affected parties, decision options, and disclosure limits.
10. Reviewer independence remains graded across model, data, prompt, code, infrastructure, organization, incentives, time, evidence access, and communication paths; labels and group counts are not competence evidence.
11. High-risk, contested, authority-changing, or interpretation-mismatched targets cannot bypass their prospectively required adversarial or accountable-human route.
12. Falsification, counterexample search, omission search, judge-bias probes, justified ignorance, abstention, veto, dissent, minority findings, and appeal grounds remain first-class results.
13. Cycle caps and convergence describe resource termination only; they do not establish truth, completeness, consensus quality, or absence of undiscovered attacks.
14. Prior review reuse requires exact unchanged-boundary evidence across target, mapping, sources, artifacts, models, verifiers, policies, threats, environment, authority, rights, and outcomes.
15. Every verdict binds exact evidence and attack refs, method and independence limits, scope, required actions, constraints, expiry, residuals, appeal, accountable human state, and non-claims.
16. No verifier, tribunal, judge, proof bridge, fixture, route function, artifact receipt, or reviewer may authorize its own support promotion, action, disclosure, training, or release.
17. Every attempt, failure, timeout, retry, intervention, rejected route, dissent, appeal, privacy exposure, human burden, latency, cost, missed help, unsafe acceptance, and delayed residual remains in the denominator.
18. Schemas, authored fixtures, finite route theorems, source-reported results, and local green checks establish only their exact formal, record, source, and environment boundaries.

40.10 Failure modes

The most dangerous failures combine a valid local artifact with an invalid global inference. Others hide method selection, dependence, omitted evidence, uncertainty, or cost until the resulting verdict appears cleaner than the work that produced it. The taxonomy covers both classes:

1. Certified delusion pairs a false, unsupported, or irrelevant natural claim with a valid-looking artifact or verdict.
2. Invalid formalization proves or refutes a target that differs materially from the prose, assumptions, scope, population, environment, policy, or consumer question.
3. Theorem, citation, replay, benchmark, or procedure laundering widens a mode-specific result beyond the property and boundary actually checked.
4. Artifact theater supplies a missing, stale, unverifiable, policy-mismatched, environment-mismatched, self-reported, or reality-false justification object.
5. Verifier-trust recursion treats named checkers, signatures, green builds, consensus, or an internally declared trusted core as self-authenticating competence.
6. Route shopping reruns, switches, combines, or selectively reports methods after outcomes until one produces the desired standing.
7. Dossier capture hides decisive sources, attacks, transformations, affected parties, prior failures, or omitted frontiers behind a bounded evidence world.
8. Reviewer collusion or correlated error presents shared models, data, prompts, code, infrastructure, organizations, incentives, or communication as independent challenge.
9. Judge and persuasion laundering rewards position, verbosity, style, confidence, familiarity, rhetoric, or strategic evidence selection rather than target correctness.
10. Consensus theater averages disagreement, treats majority vote as evidence, or removes dissent, veto, minority findings, and appeal grounds from the verdict.
11. Vacuous-pass and default-approval laundering accept empty dossiers, missing review, absent attacks, unexercised falsification, or reviewer silence.
12. Abstention and ignorance erasure converts unknown, infeasible, disputed, budget-exhausted, or justified-ignorance results into agreement or rejection.
13. Convergence and cycle-cap laundering narrates edit stability, repeated agreement, or budget termination as truth, adequacy, or exhausted attack space.
14. Repeated-review laundering reuses changed evidence or reruns unchanged evidence without a prospective guard until rejection becomes acceptance.
15. Critique-without-consequence records findings or dissent without required actions, constraints, downgrade, blocker, repair, expiry, appeal, or residual ownership.
16. Self-promotion laundering lets a verifier, tribunal, model judge, proof bridge, schema, fixture, or green check move support, authority, readiness, or release.
17. Failure and cost survivorship removes failed routes, timeouts, retries, human work, privacy exposure, appeals, false refusal, missed help, unsafe acceptance, delay, and residuals.
18. Portability theater treats one formal system, claim family, dossier, model, judge, domain, language, organization, threat, or horizon as general verifier or tribunal evidence.

40.11 Minimum Viable Implementation

The current minimum is an authored record-and-route scaffold:

• three public schemas for proof-carrying claims, tribunal reviews, and tribunal method/independence records;
• three valid and five rejecting proof-carrying-claim fixtures;
• three valid and five rejecting tribunal-review fixtures;
• two valid and seven rejecting adversarial-dossier cases;
• one bounded five-project method/independence record and eleven rejecting mutations;
• a related three-valid/six-rejecting epistemic trusted-computing-base fixture owned by Artifact Graphs; and
• a six-stage AsiStackProofs.ProofCarryingClaimsRefinement lifecycle with twenty-three routes, eighteen declarations, and an independent consumer that recompiles the exact surface and rejects 36/36 mutations;
• four retained small legacy artifact-reference and negative-result lemmas, with four weak baseline projections physically retired; and
• a seven-stage AsiStackProofs.TribunalRefinement versioned request, dossier, panel, verdict, acknowledgment, and appeal lifecycle with twenty-eight routes, nineteen declarations, and an independent consumer that recompiles the exact surface and preserves the exact 3/5 and 1/11 suites while rejecting 45/45 mutations; and
• three retained Tribunal countermodels, with ten assumption-restating or literal-route declarations physically retired, for 44 live declarations across four modules and five public targets total.

The Adversarial review dossier and verdict-quality probe is recorded at experiments/adversarial_review_dossier/results/2026-07-02-local.json; its two accepted synthetic dossiers and seven rejecting controls remain part of the authored scaffold, not a natural verdict-quality result.

The related epistemic-TCB fixture treats verifier-trust laundering as an explicit rejecting case: naming a checker or trusted core does not supply the root, delegation, recursion stop, independence, compromise, and residual evidence that the broader trust claim would need.

The proof-carrying refinement proves exact represented target custody, zero support and external-effect authority over arbitrary finite event lists, rejection noninterference, exact batch composition, absorbing writeback, accepted-step receipt accounting, negative and mismatch routing, dossier/dissent/residual requirements, and a full reachable witness. The Tribunal refinement proves exact represented case, target, evidence, dossier, panel, policy, consumer, and verdict-version custody over arbitrary finite event lists, rejection noninterference, exact batch composition, absorbing appeal resolution, and zero support/effect authority, but not competence, independence in fact, or correctness. The retained legacy declarations remain finite countermodels or small record consequences. The Python records reject missing or wrong artifacts, promotional negative results, missing dossiers and probes, erased dissent, unguarded review reuse, action verdicts without actions, dependence laundering, vacuity, falsification omission, abstention erasure, silent veto, default approval, and fixture-driven support promotion.

No current artifact executes a natural target corpus, actual theorem or citation-validity campaign, autoformalizer, semantic-equivalence evaluator, model judge, debate protocol, multi-model tribunal, independent reviewer competence audit, contestability or redress outcome, usefulness comparison, causal ablation, clean reproduction, or transfer. The schemas also lack parts of the expanded contract. Green local checks establish finite record discipline and route behavior only.

The next honest minimum must prospectively freeze natural high-value claims and high-risk artifacts across mathematical, software, scientific, policy, and mixed-evidence tasks. It must include accepted natural/formal mappings, source truth and entailment labels, actual proof or countermodel checking, executable procedures and replay, benchmark outputs, adversarial dossiers, reviewer and judge dependence, affected-party and appeal cases, and delayed outcomes. Strong direct, self-critique, citation-only, proof-only, replay-only, benchmark-only, model-judge, debate, accountable-human, and abstention routes must receive matched information, resources, authority, and time.

Independent evaluators must score interpretation error, artifact and source validity, theorem-target fidelity, false acceptance, false refusal, missed help, attack discovery, calibrated ignorance, dissent and appeal preservation, action follow-through, delayed harm and usefulness, latency, privacy, human burden, and total cost. Reproduction from locks and transfer to a second model, domain, language, formal system, evaluator implementation, organization, threat, and time period precede any promotion.

40.12 Mature Research Target

A mature verification operating system prospectively routes natural high-value claims and high-risk artifacts to the cheapest adequate combination of formal proof, citation review, procedure, replay, benchmark, model judging, adversarial debate, accountable-human adjudication, appeal, or abstention. It preserves interpretation mappings, trusted verifier boundaries, every attempt, dossier limits, dependence, attacks, ignorance, dissent, verdict scope, required actions, and bounded writeback without claiming that one method fits every proposition.

The decisive comparison is joint. Useful accepted work, claim-specific false acceptance, unnecessary refusal, missed help, interpretation error, source and theorem validity, attack discovery, calibrated abstention, dissent and appeal preservation, delayed outcomes, latency, privacy exposure, human burden, and total cost all remain visible. Direct answers, self-critique, citations, proof, replay, benchmarks, model judges, debate, human review, and abstention form strong matched baselines rather than decorative references.

Each claimed mechanism needs a prospectively predicted signature under matched ablation. A routing benefit disappears when route selection is removed; a mapping benefit disappears when semantic mapping is hidden or corrupted; an adversarial-review benefit disappears when attacks, independence, or dissent are removed. Clean replay from locks and independent transfer across models, domains, languages, formal systems, evaluators, organizations, threats, and time are separate gates.

Any missed gate narrows the claim or produces a null, negative, refuted, deprecated, cost-dominated, or blocked-after-full-attempt result. That outcome is still useful evidence. It is more informative than a schema-valid claim that the stack has built a truth machine.

No current result meets this proof-carrying adjudication endpoint; support remains argument until natural claims, independent evaluators, adversarial verifier tests, causal ablations, reproduction, and transfer pass.

40.13 Codex test plan

Test	Purpose	Status
Proof-carrying claim fixture validation	Check that the proof-carrying claim fixture records claim scope, tier, justification type, interpretation mapping/confidence, artifact ref, verifier, result field, verifier artifacts, failed attempts, formal scope, limitations, downgrade rule, tribunal ref, ledger update, source refs, support-state effect, and non-claims.	implemented by protocol validation; validated locally
Proof artifact presence predicate	Check that modeled formal or verified claims carry an appropriate artifact reference, and that passed verifier records carry verifier artifact refs.	implemented in AsiStackProofs.ProofCarryingClaims; builds locally
Failed verification route predicate	Check that failed, timed-out, or mismatched verifier results produce non-promotional effects.	implemented in AsiStackProofs.ProofCarryingClaims; builds locally
Proof-Carrying Claims target-to-writeback refinement	Check exact target, interpretation, artifact, verifier, trusted-base, attempt, dossier, dissent, limitation, residual, and owner custody while separating verifier pass, semantic review, bounded proposal, support assignment, and external effects.	implemented by python3 scripts/validate_proof_carrying_claims_refinement.py: exact eighteen-theorem surface, arbitrary-run custody and non-authority, rejection noninterference, batch composition, absorbing writeback, exact 3/5 proof and 2/7 dossier suites, six stages, twenty-three routes, and 36/36 rejected mutations; support-state effect none
Tribunal review fixture validation	Check that the tribunal fixture records target, risk class, dossier, reviewer roles, probes, findings, evidence refs, dissent, unresolved issues, verdict, required actions, and human adjudication.	implemented by protocol validation; validated locally
High-risk accepted-verdict negative case	Check that a finite high-risk accepted verdict without adversarial probes or reviewer-independence records rejects the probe-discipline predicate.	implemented in AsiStackProofs.Tribunal.high_risk_accepted_verdict_without_probes_or_independence_rejected; no reviewer-independence or probe-quality claim
Prior-review reuse negative case	Check that finite accepted reuse of prior review over unchanged evidence rejects the guard predicate when the unchanged-evidence guard is absent.	implemented in AsiStackProofs.Tribunal.accepted_prior_review_reuse_without_unchanged_evidence_guard_rejected; no prior-review adequacy or semantic-equivalence claim
Action verdict negative case	Check that a finite action-requiring verdict rejects the action/constraint predicate when required actions or constraint effects are missing.	implemented in AsiStackProofs.Tribunal.action_verdict_without_actions_or_constraints_rejected; no deployed enforcement or verdict-correctness claim
Tribunal versioned-verdict and appeal refinement	Check exact case/evidence bindings and request, dossier, panel, verdict, acknowledgment, and appeal custody while rejecting missing high-risk, independence, falsification, abstention, veto, dissent, action, residual, appeal, owner, and consumer obligations; changed-evidence reuse; default approval; replay; substitution; and authority leakage.	implemented by python3 scripts/validate_tribunal_refinement.py: exact nineteen-theorem surface, arbitrary-run custody and non-authority, rejection noninterference, batch composition, absorbing appeal resolution, exact 3/5 review and 1/11 method/independence suites, seven stages, twenty-eight routes, and 45/45 rejected mutations; support-state effect none
Adversarial review dossier and verdict-quality probe	Check that a deterministic synthetic review-dossier fixture includes scoped acceptance with dissent preserved, semantic-mismatch rejection, rejected negative controls, rejected LLM-judge-only acceptance, no support-state effect, and explicit non-claim boundaries.	implemented by python3 scripts/validate_adversarial_review_dossier_probe.py; two valid synthetic review dossiers and seven expected-invalid controls; no semantic-equivalence, reviewer-independence, adversarial-probe-quality, verdict-correctness, LLM-judge, debate-system, or support-state-promotion claim
Historical-project tribunal method/independence fixture	Check six method labels, distinct independence groups, bounded dependencies, vacuous-case refusal, substantive falsification, explicit abstention, visible veto/dissent, no default approval, and no fixture promotion.	implemented by python3 scripts/validate_tribunal_method_independence.py with one bounded five-project record and eleven expected-invalid mutations; no reviewer-independence, method-adequacy, verdict-correctness, deployed-tribunal, or support claim
Tier assignment over real verifier outputs	Check that support tiers match verifier result and limitations over actual verifier outputs and interpretation examples.	planned; not run
Real adversarial review quality test	Check reviewer routing, probe coverage, consensus quality, and action-linked verdict traces over reproducible dossiers.	planned; not run

The implemented checks are bounded record-discipline gates. They are not open-domain verifier tests, theorem-validity results, citation-accuracy audits, reviewer-independence audits, verdict-correctness results, runtime traces, or deployed review systems.

40.13.1 Formalization hooks

Tag	Module	Target	Status
lean:spinoza.proof_carrying.operational_invariant	AsiStackProofs.ProofCarryingClaimsRefinement	Every finite target-specific verification run preserves exact claim, interpretation, scope, assumption, artifact, verifier, and trusted-base custody; rejected events preserve exact state, batches compose, owner writeback is absorbing, and support or external effects remain unassigned.	implemented
lean:spinoza.proof_carrying.failure_blocks_promotion	AsiStackProofs.ProofCarryingClaimsRefinement	Passed results require artifacts and semantic review; negative results cannot request scoped promotion; mismatch requires tribunal; high-risk adjudication requires an independent dossier.	implemented
lean:tribunal.review.operational_invariant	AsiStackProofs.TribunalRefinement	Every finite versioned Tribunal run preserves exact case, target, evidence, dossier, panel, policy, consumer, and verdict-version custody; rejected events preserve exact state, batches compose, appeal resolution is absorbing, and support or external effects remain unassigned.	implemented
lean:tribunal.review.failure_blocks_promotion	AsiStackProofs.TribunalRefinement	Missing high-risk probes, panel or independence records, falsification, preserved dissent, actions, constraints, residuals, appeal, owner handoff, or consumer acknowledgment; changed-evidence reuse; default approval; replay; substitution; and authority leakage all block lifecycle progress without mutating exact state.	implemented
lean:spinoza.adversarial_review.dossier_probe_bridge	AsiStackProofs.ProofCarryingClaimsRefinement	An independent consumer recompiles the exact eighteen-theorem surface, covers twenty-three lifecycle routes, consumes the exact 3/5 proof-carrying and 2/7 adversarial-dossier suites, and rejects 36 mutations without assigning support.	implemented

The family now contains 44 live declarations across four modules: eighteen Proof-Carrying Claims refinement declarations, four retained small legacy lemmas, nineteen Tribunal refinement declarations, and three retained Tribunal countermodels. Four Proof-Carrying Claims and ten Tribunal assumption- restating, broad-summary, or literal-route declarations are absent from the live corpus with frozen rationalization lineage. The Proof-Carrying Claims subfamily now establishes arbitrary-run authored lifecycle custody, rejection noninterference, composition, and terminal closure; the Tribunal subfamily now establishes the same finite-run properties through appeal resolution. All five public targets remain narrower than the chapter core claim and do not convert fields, route order, panel labels, or a bounded verdict into competence, correctness, semantic evidence, empirical evidence, support, or effect authority.

The formal layer establishes only exact finite consequences about artifact references, non-promotional negative results, missing review, probes and dependence records, changed-evidence reuse, dissent preservation, action constraints, evidence-transition requests, and bounded acceptance. It does not prove natural/formal equivalence, theorem or source truth, artifact-reality correspondence, verifier competence, reviewer independence, probe quality, judge calibration, verdict correctness, contestability, action enforcement, usefulness, safety, or transfer.

40.14 Source crosswalk

Source ID	Title	Layer	Planned use	Readiness
spinoza	Proof of Belief / The Spinoza Architecture	reasoning_epistemology	Twelve-tab lineage fully section-family reviewed: artifact-class commitments, proof/norm/procedure/speculation boundaries, FIMO, deterministic rendering and counterexample intent tests, template trust and decay, bounded revision, theory bridges, contradiction arbitration, threats, metrics, and explicit nonclaims.	source note available; local raw cache available
genesiscode	GenesisCode	executable_specification	Obligation-carrying artifacts, tests/proofs/provenance, capability boundaries, semantic patch validation, and small trusted-core discipline.	source note available; local raw cache available
coherence_exchange	The Coherence Exchange	epistemic_market_synthesis	Connector/source-note synthesis for verification supply chains, contestability, fork/exit/audit, and review-market framing.	source note available; connector or recovery required
verification_bandwidth	Verification Bandwidth in Bounded Contexts	context_verification_theory	Generation/verification separation, verification workspace limits, pairwise checking cost, and context-adequacy pressure.	source note available; local raw cache available
treellm	TreeLLM correction lineage	semantic_representation	Graph/path traces as versioned route artifacts, with exact/approximate/speculative hops and stable identity/provenance required before any claim use. A route is neither truth, entailment, causal explanation, nor proof.	source note available; local raw cache available
uat	Unified Adaptive Tribunal	evaluation_refinement	Retrieval-bounded dossiers, atomic proposition states, adversarial review, hard cycle caps, SME checkpoints, and dissent preservation.	source note available; local raw cache available
talos	Talos Protocol	labor_execution_os	Typed review artifacts, claim graphs, evidence sets, logs, replay, residual risk, and human adjudication pressure.	source note available; local raw cache available
ext_proof_carrying_code_1997	Proof-Carrying Code	external_literature	Comparator for machine-checkable artifact evidence and host-side policy verification.	source note available
ext_lean4_theorem_proving	Theorem Proving in Lean 4	external_literature	Comparator for proof-term and dependent-type practice around formal artifacts.	source note available
ext_autoformalization_llms_2022	Autoformalization with Large Language Models	autoformalization	Comparator for informal-to-formal translation and semantic-adequacy risks around proof targets.	source note available
ext_ai_safety_debate_2018	AI safety via debate	adversarial_review	Comparator for adversarial agents plus human judge review when direct human judgment is difficult.	source note available
ext_llm_as_judge_mt_bench_2023	Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena	model_evaluation	Comparator for model-graded evaluation, human-preference agreement, and judge bias limits.	source note available
ext_contestable_ai_design_2022	Contestable AI design literature	external_literature	Comparator for challenge, review, appeal, dissent, and contestable decision surfaces.	source note available
cca_project, moecot_manifest_project, beastbrain_project, bugbrain_project, corbens_best_model_possible_project	Historical project lineage	local_verification_and_tribunal_lineage	Method labeling, verifier/tribunal boundaries, dependence disclosure, dissent, falsification, abstention, vacuous-pass detection, replay limits, and negative cases for nominal review.	public-safe pinned notes reviewed; one hand-authored tribunal fixture only, no historical runtime replay or independent replication

No listed external source is local reproduction evidence. The records orient readers around proof-carrying code, theorem-proving practice, autoformalization, adversarial debate, model-graded review, and contestable review surfaces while preserving the claim-support boundary.

40.14.1 Manifest source assignment reconciliation

These rows keep Proof-Carrying Claims and Adversarial Review’s manifest assignments visible at their recorded review boundary. Passage review does not establish local reproduction, performance, safety, deployment, or support-state movement.

Source	Intake role	Boundary
deterministic_capability_compilation	Passage-reviewed Corben architecture source: Deterministic Capability Compilation: A Capability-Preserving Ladder from Executable Scaffolds to Governed Adaptive Agents. Corben-authored July 2026 architecture and research program for compiling executable scaffolds into contract-bound experts and linked Neural Capability Objects while retaining semantic obligation mass balance, candidate-specific translation validation, fallback, residual escrow, authority ceilings, reification, and effect-complete recovery. Existing chapters are upgraded first; no foundry implementation, learned-capability result, preservation result, safety result, SOTA result, AGI, ASI, or support-state promotion is inferred.	No local implementation, reproduction, performance, safety, deployment, support-state, or ASI result is established by this reconciliation row.
platonic_world_model	Metadata-first comparator: The Platonic World Model: A Semantic Constitution for Grounded, Proof-Carrying, Self-Editing Artificial Intelligence. Corben-authored July 2026 conceptual architecture and falsifiable research program for semantic continuity through stable Form lineages, immutable semantic versions, typed Essence Contracts, six mutually constraining planes, explicit proposition-attestation-commitment-proof separation, branch-protected world dynamics, qualified grounding, semantic transactions, runtime packet compilation, and federated mappings. Existing chapters are upgraded first; no implemented substrate, benchmark result, philosophical solution to grounding, safety result, SOTA result, AGI, ASI, or support-state promotion is inferred.	No passage-level source claim, local implementation, reproduction, safety, performance, deployment, support-state, or ASI result is established by this reconciliation row.

40.15 Summary

Proof-Carrying Claims and Adversarial Review owns the route from a frozen target to a reconstructable bounded verification event. It records prospective mode selection, interpretation mapping, artifacts, verifier trust, attempts, dossiers, dependence, attacks, ignorance, dissent, verdicts, constraints, appeals, residuals, and writeback requests.

The boundary remains narrow. Verification Bandwidth owns adequacy; formal and empirical evaluators own their exact mode results; Claim Ledgers own identity and history; Evidence States owns support; accountable humans own adjudication and redress; execution layers own action; readiness owners own release. A proof or verdict crosses those boundaries only through an accepted scoped record.

The present evidence is an authored zero-model scaffold: finite schemas, fixtures, route consequences, and negative controls. Its value is exact anti-laundering discipline, not demonstrated verifier quality. Natural matched campaigns, causal ablations, reproduction, and transfer remain the gates between that discipline and any stronger claim.

40.16 Provenance and consolidation history

Both families remain visible in this chapter’s implementation horizon, test plan, source crosswalk, and formal proof records. The former standalone tribunal chapter is retired from the active spine, archived under archive/retired_chapters/, and preserved through the public slug chapters/unified-adaptive-tribunal-and-adversarial-review.html.

40.17 Evidence reconciliation (2026-07-16)

The invariant protocol, field meanings, and inference limits are stated once in Living Book Methodology. This packet contains only the chapter-specific projection; its authoritative per-atom rows are the spinoza-verification-and-proof-carrying-claims slice of experiments/claim_family_terminal_coverage/results/result.json.

The core remains narrowed after full attempt at argument support. The strongest family attempt was Situated world-model acquisition and consolidation campaign. Its exact boundary is: Bounded finite POMDP result only; no open-world truth, general memory transfer, deployment, or chapter-core promotion. Across 76 atoms, the terminal ledger records 75 blocked_after_full_attempt; 1 narrowed_after_full_attempt.

Chapter-specific field	Value
Family / atom denominator	CF-04 / 76 atoms
Terminal dispositions	75 blocked_after_full_attempt; 1 narrowed_after_full_attempt
Core	spinoza-verification-and-proof-carrying-claims.core: narrowed_after_full_attempt at argument
Core attempted / missing lanes	source-synthesis / causal, empirical, executable, formal, normative, transfer
Attempted local lanes	source-synthesis
Missing or unproved lanes	causal, empirical, executable, formal, normative, transfer
Strongest family bundle	Situated world-model acquisition and consolidation campaign (natural_work_and_end_to_end): Two partially observed environments, 11,250 episodes, 6,000 held-out episodes, six directional ablation signatures, and governed replacement/rollback.
Negative controls	ten arms; six matched ablations; ten laundering mutations; replacement and rollback checks.
Accepted transitions	v1_0_pilot.spinoza.no_change
Maximum inference	Bounded finite POMDP result only; no open-world truth, general memory transfer, deployment, or chapter-core promotion.
Reproduction / next burden	Replay scripts/validate_p4_m8_world_model_campaign.py and scripts/validate_claim_family_terminal_program.py; fill the named atom-specific lanes under a new prospective protocol.

40.18 Handoff

The next layer turns accepted constraints, blocked states, and required actions into work. Once a verification event narrows a claim, blocks a route, requires source fetch, demands human sign-off, or creates residual work, the execution system needs typed jobs that preserve those constraints.

That is the job of Labor OS and Typed Jobs.