38 Verification Bandwidth and Context Adequacy

38.1 Chapter status

Field	Value
Chapter ID	`verification-bandwidth-and-context-adequacy`
Part	Part II - Planning, Memory, Reasoning, and Execution
Status	conceptual
Manuscript maturity	v0.3 manuscript draft
Last updated	2026-07-15
Primary source records	`verification_bandwidth`, `vcm_public`, `spinoza`, `treellm`, `vcm_editable`, `ext_graphrag_2024`, `ext_hipporag_2024`, `ext_raptor_2024`, `ext_dont_hallucinate_abstain_2024`, `ext_alce_2023`, `ext_checklist_2020`, `ext_gpqa_2023`, `ext_longbench_2023`, `ext_ruler_2024`, `ext_longllmlingua_2023`, `ext_reluplex_2017`
Claim label	Design rationale
Evidence level	argument
Source queue	primary: `verification_bandwidth`, `vcm_public`; supporting: `spinoza`, `treellm`, ALCE, CheckList, GPQA, abstention, Reluplex; variants: GraphRAG, HippoRAG, RAPTOR, LongBench, RULER, LongLLMLingua; connector/recovery: `vcm_editable`
Source loading state	source notes: `verification_bandwidth`, `vcm_public`, `spinoza`, `treellm`, `vcm_editable`, `ext_graphrag_2024`, `ext_hipporag_2024`, `ext_raptor_2024`, `ext_dont_hallucinate_abstain_2024`, `ext_alce_2023`, `ext_checklist_2020`, `ext_gpqa_2023`, `ext_longbench_2023`, `ext_ruler_2024`, `ext_longllmlingua_2023`, `ext_reluplex_2017`, `kernel_english_residual_compiler`; raw cache: `verification_bandwidth`, `vcm_public`, `spinoza`, `treellm`; connector/recovery: `vcm_editable`
Test state	Exact authored scaffold: 3 valid/5 rejecting admission records; 2 valid/7 rejecting contradiction traces; 3 valid/5 rejecting capacity traces; one 12-unit/66-obligation/18-checked/48-residual record; one 24-obligation decomposition including 6 boundary checks; a five-stage/twelve-route refinement; and 31/31 rejected evidence-handoff mutations. Four baseline declarations are retired and eight stronger lifecycle declarations added. M8 Campaign 4 added 18 sacrificial tasks and 36 local Qwen3-8B calls across three versioned instruments; its terminal path reached 6/6 eligibility accuracy and perfect required-residual recall but admitted only 3/6 extraction interfaces, so heldout stayed sealed and support did not move. No natural heldout claim, externally independent evaluator, deployed ledger or escalation service, useful advantage, or chapter-core support effect.

38.2 Drafting guardrail

Verification Bandwidth is a claim-specific adequacy contract, not a measured law of model cognition. The repository has three valid and five rejecting admission records, two valid and seven rejecting contradiction traces, three valid and five rejecting capacity traces, and a reachable five-stage, twelve-route refinement with thirty-one rejected mutations. Those artifacts test authored record, lifecycle, authority-separation, and route consequences. They do not run a model, natural claim, independent evaluator, citation or behavior audit, property verifier, deployed ledger, calibrated adequacy classifier, usefulness comparison, or transfer study.

Campaign 4 now supplies a concrete negative interface result. A model may identify the right residual set and still fail to request the checks or emit the route vocabulary that a verifier-capacity allocator accepts. In the terminal sacrificial instrument, all three defect cases used undeclared route retain and omitted requested-check IDs. Verification bandwidth must therefore be measured at the consumer boundary—admissible check requests per available capacity—not inferred from defect mention or conservative refusal. Because the heldout workload never opened, this sharpens the contract but does not establish verifier adequacy or a natural-task effect.

It follows transactions because a coherent, authorized context view can still be inadequate for the claim at hand. Memory correctness and verification adequacy are different gates.

38.3 Human Reading Path

Concrete lens. The context-size baseline calls a large packet adequate. The verification contract requires the exact negative, contradiction, boundary, counterexample, and transfer checks for the claim.

A coherent memory view can still be insufficient for verification work. The stack has to separate having context from being able to verify with it. It needs to know when the available context, attention, time, tools, comparison method, and reviewer capacity are adequate for the claim being made.

This is a warning against long-context theater. More text in the window does not automatically mean better reasoning. A governed system should record when verification bandwidth is too narrow and downgrade, defer, split, or escalate instead of sounding certain. The honest output may be an adequacy label, not a more confident answer. Adequacy is a budgeted property, not a mood.

Knowing that verification is underpowered is itself valuable evidence for the next decision.

Adequacy labels keep uncertainty actionable instead of merely uncomfortable. They tell the system when more text would not actually create more checkable understanding.

Verification improves when the system knows what it cannot afford to check, and adequacy becomes the honest substitute for impossible total review. Honesty beats impossible certainty because context limits are part of truth.

38.4 Problem

A system can possess relevant context, tools, formal checks, citations, reviewers, and compute yet still lack enough independent, claim-specific work to justify the requested conclusion or support transition. Context length, retrieval coverage, citation count, benchmark success, proof-checker output, model agreement, and review activity are all compatible with missed obligations, weak checks, correlated evaluators, undiscovered contradictions, or unaffordable verification.

The inquiry is therefore prospective: for this exact proposition, scope, population, environment, risk, consequence, and requested support effect, which positive, negative, boundary, contradiction, counterexample, causal, outcome, cost, reproduction, and transfer obligations must be checked; which sources, modes, tools, and evaluators are eligible; and which work can be completed within the declared authority, rights, budget, and horizon?

The answer is not a confidence score. It is an obligation-to-capacity record that distinguishes work attempted from work passed, work passed from work valid, and local verification from claim-level adequacy. A packet can support orientation while remaining inadequate for a safety claim. A formal proof can settle one modeled property while leaving implementation refinement and deployment outcomes open. Adequacy is purpose-relative and expiring.

38.5 Why existing approaches are insufficient

Long context, direct and graph RAG, hierarchical retrieval, and prompt compression can improve availability or bounded task performance. They do not establish that the target claim’s obligations were identified, jointly checked, or checked by valid and independent-enough methods. More context can also add distractors and unverified summary burden.

Citation systems such as ALCE sharpen the distinction between answer quality and citation quality, but citation presence is not entailment or source truth. CheckList-style behavioral matrices and GPQA-style hard expert questions expose important failures, but benchmark success does not certify a particular live claim, evaluator, population, or deployment. LongBench and RULER stress nominal context claims; LongLLMLingua exposes compression trade-offs; GraphRAG, HippoRAG, and RAPTOR expose graph and abstraction choices. None is reproduced here, and none alone is a general adequacy certificate.

Formal tools such as Reluplex can verify a declared property inside a modeled scope and produce counterexamples. That authority does not automatically extend to semantic-model fidelity, implementation refinement, distribution shift, tool use, or whole-system safety. Abstention and model panels can reduce some errors, but shared data, prompts, code, model families, incentives, and blind spots limit independence. Verification adequacy requires an explicit obligation denominator and mode-specific ceilings across all of these routes.

38.6 Core Claim

[verification-bandwidth-and-context-adequacy.core, label: Design rationale, support: argument] Verification Bandwidth should own the prospective, claim-specific adequacy contract for a verification attempt. Before outcomes, it binds target proposition and scope, population and environment, risk and consequence, requested support effect, required positive, negative, boundary, contradiction, counterexample, and transfer obligations, available source units, verification modes, tools, evaluator-dependency graph, authority and rights, budget, horizon, stop rule, and escalation path. After execution, it records every attempted, passed, failed, disputed, unknown, infeasible, and unattempted obligation plus actual artifacts, costs, disagreement, residuals, expiry, and causal-use observations. Adequacy means only that the declared verification program was sufficient for its exact purpose under stated premises; it does not establish claim truth, model cognition, source correctness, formal-model fidelity, useful outcomes, safety, support promotion, or release.

Reader claim. More context does not guarantee adequate verification; adequacy depends on whether the available evidence and checking capacity cover the exact claim and its most dangerous failure modes.

Operational rule. Before outcomes, freeze the proposition, scope, risk, positive, negative, contradiction, counterexample, and transfer obligations, source units, evaluator dependencies, budget, stop rule, and escalation path. Record unattempted and infeasible checks alongside passes; one contradiction blocks verified support.

38.6.1 Worked adequacy decision: abundant context, one missing contradiction check

A high-risk claim arrives with a large context packet, several supporting sources, and a passing formal check. Its adequacy contract also requires an independent contradiction search against a named negative source unit. The budget expires before that obligation is attempted. The packet is context-rich but verification-inadequate, so it may remain a draft or disputed claim; it cannot receive the requested verified-support route.

If the contradiction search later finds a conflict, adding more positive sources does not cancel it. The five-stage refinement checks twelve routes, including three of five admission cases, two of seven contradiction cases, and three of five capacity cases, and rejects 87 mutations. This finite behavior preserves attempt denominators and escalation. It does not establish claim truth, source correctness, evaluator competence, formal-model fidelity, useful outcomes, or safety.

The claim remains at argument. Current evidence establishes authored record checks, finite route behavior, a conservative obligation-count example, and explicit non-claim boundaries. It does not establish a general capacity law, natural adequacy classification, evaluator competence, useful error reduction, or transfer.

38.6.2 Claim-source mapping status

Appendix C maps all sixteen assigned sources. Four local raw-cache mappings are passage-reviewed; editable VCM remains bounded to its connector/source note; and eleven external records remain primary-record or primary-paper-note comparators. None is imported as a local model, benchmark, citation, behavioral, formal-verification, abstention, adequacy, or usefulness result.

Source	What it supports	Limit
`verification_bandwidth`	Passage-reviewed: generation-versus-verification distinction, semantic units, effective verification workspace, coherence as constraint satisfaction, pairwise grinding, two-body verification limit, dominant-component suppression, transitive decay, interface-verification tradeoff, hierarchical summary fidelity tradeoff, proposed constraint-satisfaction/LCR test, and context window as verification bound.	Contradiction-rate, distractor-resistance, and adequacy-labeling experiments have not been run or mechanized here.
`vcm_public`	Passage-reviewed: object/version/representation/validation/packet/materialization identities, role-indexed operation contracts, adequacy/admission separation, strict SATISFIED/UNKNOWN/UNSATISFIED mapping, protected joint compilation, feasibility and semantic-fault outcomes, conservative recovery options, use-relative representation certificates, no-universal-strict-summary limitation, authority non-escalation, and evidence/authority separation.	No end-to-end model superiority, adequacy-classifier correctness, resolver, VCM-Bench result, or model-facing packet result exists.
`spinoza`	Passage-reviewed: proposer/verifier/maintainer separation, explicit formal-scope limits, structured unsupported states, verifier proof/refute/unknown outcomes, tier labels, proof budgets, solver status and counterexample/unsat-core reporting, contradiction-triggered belief revision, dependency tracing, entrenchment, retraction and re-verification, proof-carrying graph metadata, object-level tiering, proof invalidation, and reproducible-procedure support tiers.	Does not solve open-domain autoformalization, arbitrary theorem validity, verifier quality, or whole-system epistemic correctness.
`treellm`	Passage-reviewed: explicit traversable probabilistic graph/DAG proposal, concept/question/relation nodes, weighted edges, multi-entry roots, convergent paths, fixed semantic-token formats, path IDs, residual attributes, self-tokenizing bootstrap, reconstruction/alignment objectives, shared external DAG, incremental updates, explicit knowledge storage, memory-mapped lattice variants, and residual fingerprints.	No implementation, reasoning benchmark, fixed-token adequacy validation, graph coverage result, perfect-grounding claim, or model-size/performance claim exists here.
`vcm_editable`	Evidence-carrying planner-guided context compilation with virtual context ABI, representation graphs, certificates, authority non-escalation, transactional memory, and benchmark agenda.	Connector-readable refinement only; no VCM-Bench, contradiction benchmark, or citation-normalized external-literature support is recorded.
`ext_graphrag_2024`, `ext_hipporag_2024`, `ext_raptor_2024`	Graph, associative, and hierarchical retrieval comparators for source-unit availability, decomposition, abstraction, multi-hop navigation, and fidelity residuals.	Metadata-first notes; no graph build, QA run, contradiction audit, adequacy result, or reproduction.
`ext_alce_2023`	Citation-backed generation comparator separating fluency, correctness, and citation quality.	No corpus, output, entailment audit, evaluator reproduction, or local result.
`ext_checklist_2020`	Behavioral verification comparator using minimum-functionality, invariance, and directional-expectation tests.	No software, templates, model run, coverage audit, or reproduced failure.
`ext_gpqa_2023`	Hard expert-question and weaker-supervisor comparator for evaluator competence and scalable oversight pressure.	No dataset run, score, expert-review reproduction, contamination audit, or disagreement record.
`ext_longbench_2023`, `ext_ruler_2024`, `ext_longllmlingua_2023`	Long-context task diversity, complexity stress, and compression trade-off comparators.	No task, adapter, model, compressor, fidelity, latency, or adequacy result.
`ext_reluplex_2017`	Property-specific formal verification and counterexample comparator.	No Reluplex run, ACAS Xu reproduction, local model verification, refinement result, or broad safety proof.
`ext_dont_hallucinate_abstain_2024`	Abstention, coverage, calibration, and model-collaboration comparator.	No reproduced models, domains, collaboration schemes, independent panel, or useful-throughput result.

38.7 Mechanism

Verification Bandwidth begins after packet conformance and transaction validity. It turns a proposed claim and a finite verification budget into an explicit obligation program rather than treating loaded context or reviewer activity as proof.

The contract has eighteen mechanisms:

The opening mechanisms turn a proposition into a bounded work program. They freeze its consequence, enumerate distinct obligations, expose decomposition assumptions, bind available source units, and assign verification modes and resources before results arrive. This creates a trace from the claim that was asked to the work that was attempted, including missing units and deliberately unattempted obligations.

Freeze the proposition, definitions, scope, population, environment, time, consumer, risk, affected parties, consequence, requested support effect, authority, rights, budget, horizon, and change triggers before outcomes.
Decompose the target into premise, definition, source, entailment, contradiction, boundary, counterexample, threat, causal, outcome, cost, reproduction, and transfer obligations with owners and falsifiers.
Build an obligation dependency and interaction graph. Use all-pairwise or higher-order checks only when warranted; every reduction names clusters, boundary obligations, omitted interactions, assumptions, and residuals.
Map the actual source units and consumer-visible packet to each obligation, including missing, omitted, compressed, transformed, inaccessible, conflicting, stale, or rights-blocked material.
Assign an authorized mode to every obligation: direct source inspection, citation entailment, behavioral probe, executable test, formal property check, adversarial review, independent replication, or outcome observation.
Allocate model calls, context, tools, solvers, compute, latency, human work, privacy exposure, and opportunity cost prospectively; infeasible and deliberately unattempted work remains visible.
Record evaluator identity, implementation, model family, training-data and prompt overlap, shared code and infrastructure, incentives, conflicts, calibration history, and disagreement as an independence graph.
Execute the declared attempts against actual artifacts and retain every parse, query, retrieval, comparison, test, proof attempt, counterexample, timeout, retry, intervention, failure, and discard.
Maintain an obligation matrix separating attempted, passed, failed, contradicted, disputed, unknown, infeasible, blocked, and unattempted states.
Search prospectively for negative evidence, omitted alternatives, contradictory sources, adversarial examples, distribution shift, evaluator failure, and disconfirming outcomes.
Separate source availability, packet admission, fidelity, local-check validity, obligation coverage, evaluator competence, claim adequacy, usefulness, safety, and support.
Calibrate adequacy and abstention against held-out false acceptance, false refusal, missed contradiction, missed help, disagreement, usefulness, and delayed residuals rather than confidence or agreement alone.
Use risk- and consequence-relative stop rules that may allow drafting, request another source or mode, split or narrow the claim, abstain, quarantine, or block while preserving false-denial costs.
Issue escalation requests naming missing obligations, eligible modes, evaluator constraints, resources, authority, deadline, and return contract.
Expire and rerun affected adequacy decisions after material changes to the claim, source, packet, model, tool, verifier, property, environment, authority, rights, budget, threat, outcome, or support target.
Test causal use by removing, replacing, corrupting, or hiding required units, modes, evaluator separation, negative-evidence search, and residual handling while holding resources and candidate answers fixed.
Preserve every candidate, attempt, failure, escalation, abstention, retry, intervention, cost, privacy exposure, delay, discard, missed-help case, and residual in the denominator.
Compare answer-only, long-context, direct and graph RAG, hierarchical retrieval, compression, citation-first, self-critique, model-consensus, behavioral-test, formal-property, human-review, abstention, and governed routes on natural claims under matched conditions.

flowchart LR
  A["Frozen claim + requested effect"] --> B["Obligation graph"]
  B --> C["Actual units + modes"]
  C --> D["Prospective capacity allocation"]
  D --> E["Independent-enough attempts"]
  E --> F["Attempt and result matrix"]
  F --> G{"Adequate for exact purpose?"}
  G -- "yes" --> H["Adequacy receipt"]
  G -- "narrow" --> I["Split / narrow / draft"]
  G -- "no" --> J["Abstain / block / escalate"]
  H --> K["Claim-ledger review"]
  I --> K
  J --> K
  K --> L["Residuals + expiry"]

Reading the verification adequacy flow: Adequacy begins with a frozen claim and requested consequence, not with an answer. Obligations, actual units, modes, resources, and evaluator dependencies are declared before attempts. Adequacy routes the completed matrix to a separate claim-ledger decision; it does not promote support itself.

The later mechanisms govern interpretation of that trace. They retain negative search, evaluator dependence, abstention, expiry, ablation, costs, and failed attempts beside positive results. Adequacy then appears as a scoped routing decision over a complete attempt matrix, while evidence acceptance, support movement, authority, and release remain decisions of their respective owners.

38.7.1 Adequacy states

Adequacy state	Meaning	Allowed use
`absent`	Required source units are not loaded or not identified.	No source-derived claim.
`drafting_only`	Enough context exists to write or orient, but not to verify the target claim.	Prose draft, source queue, residual.
`local_check`	A narrow fact, citation, schema, or local consistency relation was checked.	Bounded claim with narrow support note.
`joint_check`	Required semantic units were compared in the declared mode.	Candidate for support promotion if other gates pass.
`summary_derived`	The claim rests on summaries or compressed packets with known loss.	Cannot exceed the summary’s evidence ceiling.
`escalated`	The context is inadequate for the claim and has been routed to retrieval, split review, tribunal, proof, or human review.	No promotion until the escalation returns evidence.
`contradicted`	The adequacy pass found a conflict that matters to the target claim.	Revision, downgrade, or refutation path.

This table does not measure a model’s true attention. It gives the stack a public vocabulary for refusing overconfident prose.

38.7.2 Verify the semantic contract without trusting the compression loop

KERC turns compressed context adequacy into a paired question. First, does the Kernel packet preserve the distinctions required by this consumer—entities, values, scope, modality, time, attribution, uncertainty, authority, and exact objects? Second, does the rendered output preserve the intended answer packet? A consumer can pass one and fail the other. A semantically adequate planning view may be inadequate for quotation; a perfect surface reconstruction may carry a wrong canonical proposition.

Round-trip recompilation is useful as a high-throughput local check for dropped negation, swapped entities, changed units, strengthened certainty, reversed causality, lost attribution, altered quotation, or omitted caveats. Its ceiling is determined by evaluator dependence. When compiler and recompiler share architecture, training data, concept registry, codebook, prompts, or organization, agreement can reproduce the same mistake. Symbolic exact checks, alternative parsers, source-grounded questions, task outcomes, and independent adjudication remain separate lanes.

Verification can request selective source expansion rather than loading every exact byte into every reasoning step. The request names the disputed Kernel unit, protected object, source span, fidelity mode, consumer, authority, and purpose. The returned view may resolve the issue, preserve several candidate parses, or show that the representation is inadequate. Expansion cost, privacy, latency, evaluator capacity, and residual uncertainty stay visible; fallback to source is a normal adequacy outcome, not a defeat to hide.

No architecture may claim adequate compressed context solely from a short sequence, valid packet, or successful cycle. The paper proposes the test surface but supplies no independent evaluator, measured error-detection rate, or evidence that verification cost leaves a net benefit.

38.7.3 Verify graph packets without treating traversal as truth

TreeLLM’s later snapshot interface suggests a useful verification unit: entry objects, graph epoch, maximum hops and nodes, allowed relation types, minimum weights, and a bounded neighborhood. Verification Bandwidth adds what the snapshot omits. The packet records the retrieval plan, exact and approximate routes, denied candidates, source and rights references, contradictions, unresolved senses, token/coordinate codec, cache epoch, omitted frontier, expiry, and the objects actually delivered to and used by the verifier.

The adequacy campaign varies polysemy, aliases, sarcasm, multilingual terms, temporal change, contradictory sources, near-neighbor but distinct entities, ontology migration, stale tokens, poisoned popular edges, overlay/global conflict, and deletion after snapshot. It compares exact database lookup, ordinary graph retrieval, vector and hybrid retrieval, GraphRAG-style assembly, path/coordinate tokens, bounded snapshots, and full-source context under matched information and total cost. HLSH neighborhood recall, false neighbors, collision, stability under update, residual ablations, cache hit/miss/tail behavior, route calibration, provenance survival, contradiction survival, rights violations, downstream utility, and source-fallback rate stay separate axes.

A graph path can pass structural replay and still fail epistemic adequacy: the edge may be false, the wrong sense may have been resolved, material evidence may sit outside the hop bound, or the model may not have used the returned object. “O(1)” node writes are evaluated separately from identity resolution, edge repair, token and index migration, cache invalidation, descendant notices, backups, and deletion closure. The TreeLLM source reports no local graph, token, cache, benchmark, or independent evaluator, so this remains an argument-level falsification program.

38.8 Interfaces

Context adequacy travels with the packet and claim, but ownership remains separated:

The Virtual Context ABI supplies the request, candidate inventory, actual packet, omissions, and conformance state. It may carry a requested adequacy target but cannot declare verification adequacy.
Context Transactions supplies exact committed source and snapshot state; consistency, durability, and authorization do not establish adequacy.
Intent, Cognitive Compilation, and Planning own accepted purpose, claim demand, non-goals, risk request, and scheduling. Verification Bandwidth may narrow, fault, abstain, or escalate but cannot reinterpret intent.
Scalable Oversight owns reviewer competence, adversarial control, oversight policy, and evaluator-system governance; this layer records capacity and dependencies for the exact attempt.
Spinoza and Claim Ledgers own proposition identity, contradiction, belief, evidence, and support transitions. Adequacy cannot promote a claim.
Executable Specifications and formal tools own property semantics and proof checking; a valid result remains bounded to its modeled property.
Security, Privacy, Authority, Rights, and Licensing owners decide source access, processing, disclosure, retention, reviewer eligibility, and modes.
Artifact Graphs preserve source, packet, obligation, attempt, evaluator, artifact, disagreement, cost, outcome, and residual lineage without certifying adequacy or truth.
Runtime Adapters own tools, approvals, and effects. Verification work grants no execution authority, and a checked prediction is not an observed outcome.
Resource Economics owns compute, tokens, storage, solver, retrieval, model, human, privacy, latency, recovery, and opportunity cost.
Evidence States and Readiness Gates own support, quarantine, promotion, and release. Adequacy, coverage, citation, consensus, proof, or abstention has no direct support-state effect.

Minimum fields:

adequacy_id
target_claim_id
target_definition_refs
population_scope
environment_scope
consumer_ref
decision_consequence
requested_support_effect
claim_scope
context_packet_ref
context_scope
risk_tier
semantic_units
obligation_graph
obligation_matrix
boundary_obligations
unattempted_obligations
compression_path
verification_mode
evaluator_dependency_graph
capacity_allocation
attempt_refs
disagreement_state
calibration_ref
adequacy_state
residual_risks
negative_evidence
required_escalation
stop_rule
expiry_and_revalidation
verification_artifact_refs
audit_refs
support_state_effect
non_claims

Planning consumes missing-obligation and escalation requests. The ABI may materialize a revised packet. Oversight may qualify a different evaluator. Claim Ledgers decide whether any returned artifacts justify a support transition. No component can substitute its own success state for another owner’s decision.

An adequacy record also names the comparison mode:

direct source lookup
pairwise semantic-unit comparison
schema or fixture validation
proof-checker result
tribunal/adversarial review
human review
summary-only review

Naming the mode prevents an adequacy state from becoming vague confidence. A claim may be locally checked by schema validation and still be unverified as an empirical claim. A proof-checker result may verify a finite predicate and still leave open whether the predicate models the real system. Mode-tagged adequacy preserves that difference.

38.8.1 Capacity model

The Verification bandwidth capacity model turns the “long-context theater” warning into a bounded record-level obligation count. python3 scripts/validate_verification_bandwidth_capacity_model.py writes experiments/verification_bandwidth_capacity/results/2026-07-03-local.json and checks three valid synthetic capacity traces plus five expected-invalid controls. In the worst-case all-pairwise trace, 12 semantic units create 66 all-pairwise obligations. A verifier that checks only 18 obligations records 48 residual obligations and must split, escalate, or keep the claim below verified support.

The model also records a valid named-decomposition trace: three clusters of four semantic units plus six boundary checks reduce the modeled obligation set to 24 checks. That reduction is allowed only because the decomposition names the boundary obligations; a control that hides those boundary checks is rejected. Other controls reject treating linear context slots as pairwise verification capacity, hiding residual obligations, declaring adequacy without identified semantic units, and promoting a core support state from the fixture.

This is still a synthetic record model. It does not prove a model verification bandwidth law, does not measure contradiction-rate performance, does not validate an adequacy classifier, does not prove long-context failure in deployed systems, and does not promote any core support state.

38.9 Invariants

These invariants protect the distinction between available information and completed verification. They preserve scope, obligation state, evaluator dependence, negative evidence, calibration, and denominator completeness as separate coordinates. A favorable result on one coordinate leaves the others unchanged, giving downstream reviewers an explicit account of what was checked, what remained open, and which consequence the adequacy decision addressed.

Every decision binds one exact proposition, definitions, scope, population, environment, time, consumer, risk, consequence, requested support effect, authority, rights, budget, horizon, and stop rule.
Every positive, negative, boundary, contradiction, counterexample, threat, causal, outcome, cost, reproduction, and transfer obligation is satisfied, failed, disputed, unknown, infeasible, blocked, or residualized.
Availability, retrieval, context length, packet admission, fidelity, attention, citation, local validity, coverage, claim adequacy, usefulness, safety, and support remain distinct.
Actual units, transformations, omissions, conflicts, packet placement, attempts, artifacts, evaluator observations, and outcomes remain inspectable.
All-pairwise counts are declared worst-case models, not universal laws; decomposition exposes clusters, boundary checks, higher-order interactions, omitted edges, assumptions, and completeness residuals.
More passed checks or covered obligations do not establish correctness when checks are invalid, dependent, weak, mis-scoped, contaminated, or selected after outcomes.
Evaluator independence remains graded across model, data, prompt, code, infrastructure, organization, incentives, and time.
Each mode retains its property, model, source, population, environment, authority, rights, and outcome ceiling.
Citations, retrieval recall, benchmark scores, agreement, self-critique, confidence, and green validators cannot promote claims without accepted claim-specific evidence.
Negative evidence, contradictions, disagreement, timeouts, infeasibility, unattempted obligations, and evaluator failures remain first-class.
High-risk claims require stronger independent modes, lower false-acceptance tolerance, explicit false-refusal and missed-help accounting, and no silent best effort.
Adequacy is calibrated against held-out acceptance, rejection, contradiction, abstention, usefulness, and delayed outcomes.
Escalation, abstention, narrowing, quarantine, and blocking name exact missing obligations, owners, resources, return conditions, and residuals.
Material changes to claim, source, packet, model, tool, verifier, property, environment, authority, rights, budget, threat, outcome, or support target expire affected receipts.
Every candidate, attempt, failure, escalation, abstention, retry, intervention, cost, privacy exposure, delay, discard, missed-help case, and residual remains in the denominator.
Lower tokens, faster review, more citations, higher coverage, more agreement, fewer releases, or fewer observed errors do not establish a superior frontier without joint usefulness, safety, calibration, and cost.
Schemas, synthetic traces, authored counts, finite theorems, and local reversible checks establish only their exact scopes.

38.10 Failure modes

The failure taxonomy centers on substitution, omission, and selection after the outcome. Substitution turns context length, citations, agreement, or formal syntax into broader verification than the artifact contains. Omission drops hard obligations, correlated evaluators, failures, or costs. Outcome-dependent selection then makes the retained record look stronger than the prospective program that actually ran.

Verification theater records plans, role labels, artifacts, or green status without competent claim-specific work and consequences.
Context-length laundering treats more tokens, units, or nominal window size as joint verification capacity.
Obligation deletion omits negative, boundary, contradiction, threat, causal, outcome, cost, reproduction, or transfer checks after seeing results.
Decomposition laundering removes pairwise or higher-order work without boundary obligations, completeness assumptions, or residuals.
Capacity-law laundering presents one conservative authored count as a universal theorem about cognition or every verification strategy.
Citation laundering treats links, counts, or plausible entailment judgments as source truth or complete support.
Benchmark laundering transports aggregate scores into a live claim, population, environment, threat, or support state not evaluated.
Formal-scope laundering treats a modeled property as semantic-model fidelity, implementation refinement, deployment safety, or whole-system correctness.
Evaluator-independence laundering relabels correlated models, prompts, datasets, code, infrastructure, organizations, or incentives.
Self-judge and consensus laundering treats reflection, confidence, majority agreement, or repeated sampling as independent verification.
Negative-evidence starvation spends the budget on confirmation while contradictions, counterexamples, alternatives, and outcomes remain unsearched.
Contradiction averaging hides material conflict inside aggregate adequacy, confidence, coverage, or usefulness scores.
Escalation theater records tribunal, proof, model-panel, or human referral without attempted work, returned artifacts, deadlines, or closure.
Over-refusal laundering lowers errors by omitting missed help, delay, opportunity cost, and false-denial burden.
Under-refusal laundering maximizes throughput by accepting unknown, infeasible, weakly checked, or contradicted claims.
Failure and cost survivorship removes failed checks, timeouts, retries, human work, privacy exposure, abstentions, slow cases, and residuals.
Stale-adequacy laundering reuses a receipt after claim, source, packet, model, verifier, property, environment, threat, authority, rights, or outcome changed.
Portability theater treats one fixture, model, domain, language, evaluator, mode, or horizon as general adequacy evidence.

38.11 Minimum Viable Implementation

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

one context-adequacy schema and fixture;
three valid and five rejecting admission/adequacy records;
two valid contradiction/adequacy traces and seven rejecting controls;
three valid capacity traces and five rejecting controls;
one conservative twelve-unit record with sixty-six all-pairwise obligations, eighteen checked, and forty-eight residual;
one named decomposition with twenty-four modeled obligations including six boundary checks; and
fourteen Lean declarations grouped under four public targets.

Three theorem declarations restate modeled predicates or summary validity and eleven construct a finite witness or prove finite route consequences. The scaffold does not run a model, natural claim, contradiction-rate study, distractor test, citation audit, behavioral suite, neural-network property check, independent evaluator, deployed ledger or escalation service, adequacy classifier, usefulness comparison, or transfer.

The next honest minimum must prospectively sample natural claims with nonzero verification opportunity across domains and stakes. It must compare answer-only, long-context, retrieval, graph and hierarchical retrieval, compression, citation, self-critique, model-panel, behavioral-test, formal-property, human, abstention, and governed routes under matched sources, models, tools, authority, budgets, and horizons. Independent evaluators must label obligations, actual attempts, contradictions, outcomes, usefulness, safety, false acceptance, false refusal, missed help, calibration, and total cost. Reproduction from locks and transfer to a second model, domain, and evaluator implementation are required before promotion.

38.12 Mature Research Target

A mature Verification Bandwidth layer is an independently testable claim-specific capacity and adequacy control plane. Natural claims are frozen and decomposed into falsifiable positive, negative, boundary, contradiction, counterexample, causal, outcome, cost, reproduction, and transfer obligations. Actual units and resources are allocated before outcomes, and complete ledgers distinguish availability, work performed, check validity, coverage, evaluator dependence, adequacy, usefulness, safety, support, and release.

Strong matched baselines span answer-only, long-context, direct and graph RAG, hierarchical retrieval, compression, citation-first generation, self-critique, model panels, behavioral tests, formal property checks, human review, and calibrated abstention. Promotion requires useful opportunity, lower claim-specific false acceptance without unacceptable false refusal or missed help, calibrated residuals, negative-evidence discovery, causal signatures under ablation, complete total cost, clean reproduction, and cross-model, cross-domain, and cross-evaluator transfer. Otherwise exact claims narrow, remain null or negative, become refuted, or are blocked after a full attempt.

The decisive comparison is a frontier rather than a single score. Every point on that frontier carries the same frozen claims, information access, resource budget, evaluator accounting, and delayed-outcome window. The resulting record places accepted help, unsafe acceptance, unnecessary refusal, missed contradiction, latency, privacy exposure, human effort, and residual uncertainty in one inspectable comparison instead of allowing any favorable metric to stand in for the whole decision.

No current result meets this adequacy-allocation endpoint; support remains argument until natural claims, matched information and resource budgets, independent outcomes, causal ablations, reproduction, and transfer pass.

38.13 Codex test plan

Test	Purpose	Status
Context adequacy fixture validation	Check that the adequacy fixture matches the public schema and declares target claim, claim scope, context packet, context scope, risk tier, semantic units, compression path, verification mode, adequacy state, residual risks, negative evidence, escalation requirements, verification artifact refs, audit refs, support-state effect, and non-claims.	implemented by protocol validation; validated locally
Distractor resistance test	Compare contradiction detection when a decisive small unit is paired with a dominant distractor unit.	planned; not run
Adequacy labeling test	Check that drafting-adequate context is blocked from verification-backed support when pairwise checking is absent.	implemented in `python3 scripts/validate_context_admission_adequacy.py`; no model verification-bandwidth claim
Verification escalation test	Check that high-risk claims with inadequate context route to tribunal, proof, retrieval, split-context, or human review instead of promotion.	implemented in `python3 scripts/validate_context_admission_adequacy.py`; no deployed escalation claim
Verification adequacy route proof	Check that a finite verification lifecycle separates malformed plans, unadmitted context, missing obligations, unauthorized promotion, inconsistent counts, contradictions, residuals, evaluator dependence, missing negative search, missing artifacts, drafting, and evidence-gate handoff.	implemented by Lean build; finite authored lifecycle only
Verification bandwidth contradiction probe	Check a synthetic adequacy fixture covering pairwise contradiction blocking, drafting-only inadequacy, summary-derived promotion rejection, dominant-distractor miss rejection, high-risk inadequate context without escalation, schema-mode empirical support rejection, ignored negative evidence, unidentified semantic units, and support promotion from the fixture.	implemented in `python3 scripts/validate_verification_bandwidth_probe.py` with two valid synthetic adequacy traces and seven expected-invalid controls at `experiments/verification_bandwidth/results/2026-07-02-local.json`; no model-verification-bandwidth, contradiction-rate-performance, distractor-resistance, adequacy-classifier, deployed-claim-ledger, escalation-service, support-state-promotion, or evidence-transition claim
Verification bandwidth capacity model	Check a bounded synthetic verification-workload model where 12 semantic units create 66 all-pairwise obligations, 18 checked obligations leave 48 residual obligations, named decomposition reduces modeled obligations only when boundary checks are explicit, and negative controls reject linear-context overclaim, hidden residuals, unidentified units, and support promotion.	implemented in `python3 scripts/validate_verification_bandwidth_capacity_model.py` with three valid capacity traces and five expected-invalid controls at `experiments/verification_bandwidth_capacity/results/2026-07-03-local.json`; no model-verification-bandwidth law, contradiction-rate-performance, adequacy-classifier, deployed-long-context-failure, support-state-promotion, or evidence-transition claim
Reachable verification-plan and evidence-gate refinement	Bind the exact prospective plan to exhaustive execution dispositions, preserve identity and receipt custody across arbitrary successful runs, compute all twelve routes independently, and prevent adequacy from assigning support or external effects.	implemented in `AsiStackProofs.VerificationBandwidthRefinement` and `python3 scripts/validate_verification_bandwidth_refinement.py`; exact 35-theorem compilation, four-event transaction, three consumed suites, twelve routes, and 87/87 rejected route/lifecycle mutations; support effect `none`
Mode-confusion audit	Check that schema, proof, summary, human-review, and empirical modes are not used to support broader claims than they actually verify.	planned; not run

The fixture-shape check, finite-record proof predicates, synthetic context admission/adequacy harness, and deterministic contradiction-probe fixture are implemented. The finite route proof records how modeled adequacy reviews should route, and the contradiction probe checks local fixture boundaries, not whether a model actually has enough verification bandwidth. Distractor resistance, contradiction-rate measurement, semantic adequacy classification, and deployed claim-ledger outcomes still require logged prompts or deterministic checkers, real or replayed model traces, and reviewable claim-ledger results.

38.13.1 Formalization hooks

Tag	Module	Target	Status
`lean:verification_bandwidth.adequacy.operational_invariant`	`AsiStackProofs.VerificationBandwidthRefinement`	Context admission is separated from a frozen claim-specific obligation plan; only an exactly bound execution can advance, while arbitrary successful runs preserve identity, valid traces, composition, and receipt custody.	implemented
`lean:verification_bandwidth.adequacy.failure_blocks_promotion`	`AsiStackProofs.VerificationBandwidthRefinement`	Direct chapter-core promotion requests and represented contradictions block evidence-gate handoff; high-risk correlated evaluation requires escalation.	implemented
`lean:verification_bandwidth.adequacy.route_envelope`	`AsiStackProofs.VerificationBandwidthRefinement`	A five-stage lifecycle and four-event transaction cover twelve explicit routes; arbitrary successful runs preserve zero support and external-effect authority, so the strongest positive effect is evidence-gate handoff.	implemented
`lean:verification_bandwidth.contradiction_probe_fixture_bridge`	`AsiStackProofs.VerificationBandwidthRefinement`	An independent consumer recompiles the exact 35-theorem surface, recomputes all twelve routes, consumes the exact 3/5 admission, 2/7 contradiction, and 3/5 capacity suites, reconstructs the transaction, and rejects 87 route/lifecycle mutations.	implemented

Four of the fourteen activation-baseline declarations are physically retired: the direct high-risk assumption projection, both copied validator-summary projections, and the theorem naming an adequacy route as permission to assign verified support. Frozen lineage remains in the proof-rationalization registry. The eight new declarations provide a reachable lifecycle, general blocking consequences, a complete witness, and an independently recomputed consumer boundary. This is finite authored verification-control semantics, not a model of verification cognition.

The declarations do not prove obligation completeness, evaluator competence or independence, source truth, citation entailment, behavioral coverage, formal-model fidelity, model attention, a general capacity law, calibrated adequacy, useful error reduction, safety, or transfer. Stronger claims require typed obligation and evaluator semantics, executable natural attempts, countermodels, actual artifacts, held-out outcomes, causal ablations, independent implementations, reproduction, and accepted evidence transitions.

38.14 Source crosswalk

Source ID	Title	Layer	Planned use	Readiness
`verification_bandwidth`	Verification Bandwidth in Bounded Contexts	context_verification_theory	Generation vs verification; long context is not automatically long-range reasoning.	source note available; local raw cache available
`vcm_public`	Virtual_Context_Memory_v1	memory_context	Public VCM release. Governed protocol for compiled working context.	source note available; local raw cache available
`spinoza`	Proof of Belief / The Spinoza Architecture	reasoning_epistemology	Neurosymbolic belief, transparent axiomatic AI belief systems, verification, belief revision.	source note available; local raw cache available
`treellm`	TreeLLM correction lineage	semantic_representation	Bounded graph snapshots, structured token contracts, exact/approximate/exploratory routes, residuals, caching, migration, and an adversarial adequacy matrix after rejecting route-as-proof and fixed-width-as-sufficiency.	source note available; local raw cache available
`vcm_editable`	Virtual_Context_Memory_v1.0_Editable	memory_context	Editable version with evidence-carrying planner-guided context compiler framing.	source note available; connector or recovery required
`ext_graphrag_2024`, `ext_hipporag_2024`, `ext_raptor_2024`	GraphRAG, HippoRAG, and RAPTOR	retrieval_and_memory	Comparators for global summaries, associative navigation, and multi-resolution retrieval while keeping retrieval quality separate from evidential adequacy.	source notes available; no local QA, adequacy, or verification result
`ext_alce_2023`	ALCE	citation_evaluation	Comparator separating answer fluency, correctness, citation presence, and citation quality.	source note available
`ext_checklist_2020`, `ext_gpqa_2023`	CheckList and GPQA	behavioral_and_expert_evaluation	Comparators for targeted behavioral probes, hard expert questions, and evaluator-competence pressure.	primary-record notes reviewed; no local suites or expert-review reproduction
`ext_longbench_2023`, `ext_ruler_2024`, `ext_longllmlingua_2023`	LongBench, RULER, and LongLLMLingua	long_context_and_compression	Comparators for task diversity, context complexity, and compression loss/cost.	primary-record notes reviewed; no local model or adequacy run
`ext_reluplex_2017`	Reluplex	property_specific_verification	Comparator for modeled property checks and counterexample scope.	source note available
`ext_dont_hallucinate_abstain_2024`	Don’t Hallucinate, Abstain	abstention_and_model_panels	Comparator for coverage, calibration, collaboration, shared blind spots, and refusal cost.	source note available

All sixteen assigned sources have bounded mappings. They position the claim against retrieval, abstraction, citation, behavioral, expert, long-context, compression, formal-property, abstention, and model-panel comparators without importing source-reported performance or local support.

38.14.1 Manifest source assignment reconciliation

These rows keep Verification Bandwidth and Context Adequacy’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
`kernel_english_residual_compiler`	Metadata-first comparator: Kernel English with Hierarchical, Interaction-Amortized Residuals: A Dual-Vocabulary Cognitive Compiler for Efficient Language-Model Reasoning. Corben-authored July 2026 architecture proposal for KERC: protected-object capture, uncertainty-aware normalization, sense-aware Kernel IR, dual surface/core vocabularies, a four-level interaction-amortized residual ledger, exact object storage, grammar-aware macro fusion, structured answer packets, rendering, round-trip verification, versioned migration, and complete rate-compute-fidelity evaluation. Existing chapters are upgraded first; no implementation, benchmark, novelty, efficiency, fidelity, safety, transfer, SOTA, AGI, ASI, or support-state result is inferred.	No passage-level source claim, local implementation, reproduction, safety, performance, deployment, support-state, or ASI result is established by this reconciliation row.

38.15 Post-v2.1 evaluator adequacy result

The routing/deliberation evaluator receives only the request, public candidate, and answer criterion; it sees neither gold route nor router score. That implementation boundary is useful, but its outcome is stark: zero of 360 substantive candidates satisfy the criterion, while route-level policy actions can still score as correct. The result separates evaluator bandwidth from candidate adequacy and from route adequacy. It does not independently validate the criterion, establish that a richer context would repair the answers, or show that five low-quality candidates provide more verifiable information than one. RD-03 therefore narrows rather than closes.

38.16 Summary

Verification Bandwidth owns the prospective obligation-to-capacity contract for an exact claim. It records what had to be checked, what sources and modes were available, what work actually happened, how evaluators were related, what failed or remained unattempted, what it cost, and why the result is adequate, narrowed, escalated, abstained, blocked, disputed, or expired.

The current repository proves only authored record, lifecycle, and route consequences. It does not measure model cognition or natural verification quality. The next proof step is a matched natural campaign with independent-enough evaluators, real artifacts, useful and unsafe outcomes, calibrated acceptance and refusal, causal ablations, complete costs, reproduction, and transfer.

Even a claim-specific adequate program cannot move support by itself. The completed record becomes an input to Claim Ledgers and Belief Revision, which owns the separate evidence and support decision.

38.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 verification-bandwidth-and-context-adequacy slice of experiments/claim_family_terminal_coverage/results/result.json.

The core remains blocked 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 73 atoms, the terminal ledger records 73 blocked_after_full_attempt.

Chapter-specific field	Value
Family / atom denominator	`CF-04` / 73 atoms
Terminal dispositions	73 `blocked_after_full_attempt`
Core	`verification-bandwidth-and-context-adequacy.core`: `blocked_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	none
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.

38.18 Handoff

Adequacy records need somewhere durable to land, otherwise verification limits remain comments around the work rather than part of the work. Claim Ledgers and Belief Revision turns those limits into claim identity, evidence state, contradiction links, revision history, uncertainty, and required promotion conditions. The stack can then change belief without erasing why the earlier belief was weaker.