Minimum Third-Mode Interface

Appendix I

31 min read

Text size

A32 states four design requirements. This appendix specifies their ten-operation implementation contract. Compliance with this interface requires demonstrating the stated preconditions, outcomes, retained evidence and completion rules; satisfying a description of the design is not itself that demonstration.

These are proposed operation contracts and schematic records, not a description of a shipped protocol. Compliance below concerns this interface. It does not establish the truth of source observations, legitimate authority, complete capture of consequential actions or access to a remedy. The exact gluing guarantee applies only to the stated sheaf and matching conditions; Appendix L, Problem 8, leaves the extension to approximate agreement open.

I.1 Core Types

Before specifying operations, we define the types that appear in signatures.

I.1.1 Primitive Types

Context       := { name: String, signature: Set⟨Predicate⟩, logic: Logic }
Logic         := { consequence_relation: LogicRef, absence_profile: PredicateScopedProfile }
                 -- classical, intuitionistic, etc. govern derivation; CWA/OWA govern absence
                 -- a three-valued evaluator has its own declared interpretation
Claim         := { subject: EntityRef, predicate: PredicateName, value: Value, context: Context }
EntityRef     := Opaque identifier for an entity
PredicateName := String
Value         := Any (type determined by predicate signature)

I.1.2 Witness Types

Witness       := { class: WitnessClass, content: WitnessContent, provenance: Provenance }
WitnessClass  := DECIDABLE | PROBABILISTIC | ATTESTED
WitnessContent := class-specific evidence (see A2c)
Provenance    := { source: String, timestamp: DateTime, method: String }

I.1.3 Equivalence Types

Scope         := Set⟨Context⟩ (downward-closed under the evidence-preserving refinements of A30)
RelationKind  := EQUALITY | ISOMORPHISM | EQUIVALENCE | ADJUNCTION_DERIVED_APPROXIMATION
Equivalence   := { left: EntityRef, right: EntityRef, relation_kind: RelationKind,
                   scope: Scope, witness: Witness }
TransportCertificate := { equivalence: Equivalence, property: PredicateName, direction: LEFT_TO_RIGHT | RIGHT_TO_LEFT }

The relation kinds are A10's distinctions. relation_kind declares what relationship is claimed; witness.class declares how its evidence is checked. Neither field determines the other. The evidence must supply the maps, laws and property footprint required for that relationship in its declared setting. A label supplies none of them. General certification in A19b may instead concern a recommendation; it does not thereby create an Equivalence under this operation.

I.1.4 Cover Types

Cover         := { components: Set⟨Context⟩, target: Context }
                 -- components must jointly cover target in the site topology
MatchingFamily := { sections: Map⟨Context, Claim⟩, cover: Cover }
                 -- sections must agree on overlaps for the family to be "matching"

I.1.5 Artifact Types

-- Success artifacts
ClaimReceipt        := { claim: Claim, witness: Witness, timestamp: DateTime }
GluingReceipt       := { global_claim: Claim, local_receipts: Set⟨ClaimReceipt⟩, cover: Cover }
TransportReceipt    := { original: Claim, transported: Claim, certificate: TransportCertificate }
AcceptanceReceipt   := { predicate: PredicateName, tests_passed: Int, scope: Scope, version: SemVer }

-- Failure artifacts
ObstructionWitness  := { disagreeing_contexts: Set⟨Context⟩, conflict_set: Set⟨Claim⟩, 
                         resolution_options: Set⟨ResolutionHint⟩ }
ScopeViolation      := { equivalence: Equivalence, attempted_context: Context, 
                         valid_scope: Scope, violation_type: OUTSIDE_SCOPE | SCOPE_LEAK }
UnsatCore           := { constraints: Set⟨Constraint⟩, derivation: DerivationChain }
RejectionWitness    := { reason: RejectionReason, evidence: Any }
RejectionReason     := a diagnostic code identified by the operation below
Inconclusive        := { reason: String, unchecked_obligations: Set⟨String⟩ }
                 -- no certificate of success and no claim that an unproved proposition is false

I.1.6 Incomplete Checks and Pending Uses

An Inconclusive outcome identifies the required obligation that remains unestablished and its cause. Its reason distinguishes unavailable evidence, exhausted resources, authority not established, a method not supplied or another specified impediment. It must state what further work could change the result, or state that no adequate resolving method is known. An honest incomplete outcome does not require a promise that the question can be answered.

When a receiving institution uses that outcome to continue an action, withhold a qualification or postpone a consequential decision, it must also retain a pending-use account. The account identifies:

The affected use: what is being done, withheld or postponed, and which unfinished obligation it depends on.
Responsibility for disposition: the responsible institution or office, the authority under which it proceeds, and any other actor whose cooperation or permission is required. This is not a claim that the responsible party can solve the evidentiary problem alone.
The next decision: the applicable deadline or review point, related to the consequences of delay, and the process that must decide what follows if the underlying question remains unsettled.
The interim course: any restriction, precaution or permitted use, with its separate grounds and bounds, and the evidence of review or referral actually completed.

These requirements govern the use of an outcome, not a new operation or wire format. Existing reason, obligation and receiving-process references may carry the account. If responsibility or a governing process has not been established, that gap must remain explicit; the institution cannot claim to have supplied a managed pending process merely because it issued an incomplete result. A standalone unanswered mathematical query need not invent an administrative deadline when no consequential use is pending.

At the review point: the institution must record the required disposition, any authority for continuation and the next applicable boundary. Reissuing Inconclusive does not establish that continuation is justified. Expiry establishes neither falsity nor permission and does not prescribe one remedy for every use. The governing process may require suspension, independent review, a supported alternative or another authorized response. Any further delay must meet that process's conditions; successive dates cannot substitute for the decision required.

The selected constitutional Articles distinguish timely contestation from an independent human arbiter's review of material adverse action. A recorded deadline does not provide either institution. Where those duties apply, the pending-use account must identify the actual review and relief available before delay defeats their purpose. Separately justified precaution can proceed under its own conditions; it must not be described as completion of the ordinary check.¹

I.2 The Ten Operations

Operation 1: `create_context`

Purpose: Establish a new context with a declared signature and logic regime.

create_context(
  name: String,
  signature: Set⟨PredicateSpec⟩,
  logic: Logic,
  refines?: Set⟨Context⟩    -- optional: contexts this one refines
) → Context | RejectionWitness | Inconclusive

Preconditions:

name is unique within the system
Each PredicateSpec in signature is well-formed
If refines is provided, supply the declared context maps and their composition/restriction obligations. Where preservation of the old theory is claimed, establish the appropriate conservativity condition separately.

Artifacts on success:

Context object with assigned identity

Failure modes:

RejectionWitness with NAME_COLLISION if name exists
RejectionWitness with SIGNATURE_MALFORMED if any predicate spec is invalid
RejectionWitness if a required context-map or conservativity obligation is violated; an unestablished obligation yields Inconclusive.

Invariant: Created contexts are immutable. To modify a context, create a new version.

Operation 2: `register_claim`

Purpose: Assert a claim in a context with supporting witness.

register_claim(
  subject: EntityRef,
  predicate: PredicateName,
  value: Value,
  context: Context,
  witness: Witness
) → ClaimReceipt | RejectionWitness | Inconclusive

Preconditions:

predicate is in context.signature
value conforms to predicate's declared type
Verify the supplied witness for this claim, scope and version under the predicate's policy; a permitted class label alone is insufficient
Establish the required consistency with existing active claims in context; preserve disagreement as attributed evidence where the declared logic permits it

Artifacts on success:

ClaimReceipt with timestamp and witness binding

Failure modes:

RejectionWitness with PREDICATE_NOT_IN_SIGNATURE if predicate unknown in context
RejectionWitness with TYPE_MISMATCH if value type is wrong
RejectionWitness with WITNESS_INSUFFICIENT if a completed check establishes that the witness fails a required evidence or verification condition of the predicate’s policy
RejectionWitness with CONTRADICTION if the required consistency check finds a conflict
Inconclusive if required evidence or consistency cannot be established within the checking regime

Invariant: A registered claim cannot be silently overwritten. Correction requires explicit retraction (Operation 10).

Operation 3: `verify_witness`

Purpose: Check that a witness is valid for a claim under its declared class.

verify_witness(
  claim: Claim,
  witness: Witness
) → VerificationResult

VerificationResult := 
  | { status: OK }
  | { status: OK_WITH_CONFIDENCE, confidence: Float, bounds: (Float, Float) }
  | { status: OK_IF_TRUSTED, authority: String }
  | { status: FAIL, reason: String }
  | { status: INCONCLUSIVE, reason: String }

Preconditions:

witness.class is declared
witness.content is parseable for that class

Artifacts: Returns VerificationResult (no persistent artifact from this operation). A receiving use must retain the result and the further account required by I.1.6 when it uses incomplete checking to maintain a consequential pending state.

Failure modes: FAIL identifies a failed declared check. INCONCLUSIVE identifies unavailable evidence, exhausted resources or an unsupported verification task. Neither the latter nor failure to verify a witness establishes that the underlying claim is false.

Contract by class (per A2c):

Class	Verification	Output on success
`DECIDABLE`	Total, deterministic	`OK`
`PROBABILISTIC`	Evaluates a specified statistical claim under its assumptions	`OK_WITH_CONFIDENCE(p, bounds)` with the estimand, procedure and assumptions recorded
`ATTESTED`	Checks provenance chain	`OK_IF_TRUSTED(authority)`

Operation 4: `declare_equivalence`

Purpose: Assert that two entities are equivalent within a scope, with witness.

declare_equivalence(
  left: EntityRef,
  right: EntityRef,
  relation_kind: RelationKind,
  scope: Scope,
  witness: Witness
) → Equivalence | RejectionWitness | Inconclusive

Preconditions:

left ≠ right (no trivial self-equivalence declarations)
scope is valid under the declared property footprint and evidence-preserving refinement maps of A30
relation_kind is declared. Verify that relationship in its stated setting, including the necessary maps and laws, property footprint, evidence and validity conditions; approximation requires its own error bounds
No verified inequality or incompatible property requirement contradicts the proposed equivalence. Two entities both equivalent to a third are not, for that reason, in conflict.

Artifacts on success:

Equivalence object retaining the checked relation_kind, scope and witness, registered in the system's equivalence graph

Failure modes:

RejectionWitness with MISSING_RELATION_KIND if the declaration omits the required relation; this rejects an incomplete declaration, not the underlying claim
RejectionWitness with TRIVIAL_EQUIVALENCE if left = right
RejectionWitness with INVALID_SCOPE if scope is malformed
RejectionWitness with CONFLICTING_EQUIVALENCE if contradicts existing
Inconclusive if the declared relationship or its required evidence cannot be established within the checking regime

Invariant: Equivalences are persistent within their scope. Retraction requires explicit operation with audit trail.

Operation 5: `transport`

Purpose: Move a property from one entity to an equivalent entity via certificate.

transport(
  claim: Claim,
  equivalence: Equivalence,
  target_context: Context
) → TransportReceipt | ScopeViolation | RejectionWitness | Inconclusive

Preconditions:

claim.subject matches one side of equivalence
target_context ∈ equivalence.scope
The checked certificate supplies the map for the particular property, source and target evaluators and versions, under equivalence.relation_kind; the claim's evidence meets the receiving use's requirements. A transportable flag alone supplies none of these.

Artifacts on success:

TransportReceipt binding the original and transported claims through a certificate whose equivalence retains the relation kind, scope and witness

Failure modes:

ScopeViolation with OUTSIDE_SCOPE if target_context ∉ equivalence.scope
ScopeViolation with SCOPE_LEAK if transport would leak beyond declared scope
RejectionWitness with NOT_TRANSPORTABLE if predicate blocks transport

Invariant: Transport produces a new claim in target context. Original claim remains. Both are linked via receipt. The receiving operation cannot silently promote the retained relation kind: establishing a stronger relation requires its own grounds and declaration.

For example, two declarations can both use a DECIDABLE witness while one establishes an ISOMORPHISM of finite identifier sets and another an ADJUNCTION_DERIVED_APPROXIMATION between ordered classifications. The first must supply its checked inverse maps; the second its adjunction laws and the bounds relevant to the proposed property. Transport follows those different grounds. Sharing a checking class does not make the approximation invertible.

Operation 6: `glue`

Purpose: Check a supplied local family against an exact matching obligation and, where an established sheaf construction applies, return its amalgamation.

glue(
  cover: Cover,
  claims: Map⟨Context, Claim⟩
) → GluingReceipt | ObstructionWitness | RejectionWitness | Inconclusive

Preconditions:

cover belongs to the declared site topology; the necessary overlap maps are supplied.
Each local claim is registered with its evidence and version.
The local data inhabit the stated sheaf, and the implementation supplies its restriction and gluing construction. Matching alone does not establish that an arbitrary presheaf has a unique amalgamation.

Exact matching check: For every required overlap, compare the restricted sections for equality. A finite cover and effective equality permit direct checking; other cases require the corresponding proof procedure. Data with different subjects, predicates or jurisdictional meanings must first be represented as such. A difference between unlike claims is not a failed equality of one claim.

Artifacts on success:

GluingReceipt records the amalgamation, cover, local receipts, versions and checked conditions. Under the established sheaf hypotheses, the amalgamation is unique for this family.

Failure and incomplete outcomes:

A verified unequal pair yields an ObstructionWitness with the actual restricted values. A complete or minimal conflict set may be claimed only if established.
Missing construction, evidence, or completed comparisons yields Inconclusive; it is not a proof of disagreement.
An invalid cover or input yields RejectionWitness.

Tolerance and distribution overlap may support useful approximate reconciliation, but they do not inherit this uniqueness theorem. Such a result must state its own construction, error bounds and checks. Changing a tolerance, a scope or a governing authority creates a new decision to record; it does not retroactively make the old family match. Appendix L, Problem 8, remains open.

Operation 7: `propose_predicate`

Purpose: Submit a new predicate for potential inclusion in the vocabulary.

propose_predicate(
  name: PredicateName,
  signature: PredicateSpec,
  intension: IntensionSpec,      -- definition (rule, model, exemplars)
  scope: Scope,
  invariants: Set⟨Constraint⟩,
  tests: TestSuite
) → ProposalId | RejectionWitness

Preconditions:

name is not already in global vocabulary
signature is well-formed
tests supplies the examples and boundary or abstention treatment required by the declared A29 admission profile, including a justified non-applicability statement where that profile permits one

Artifacts:

ProposalId for tracking through acceptance pipeline

Failure modes: Malformed or out-of-scope submissions receive RejectionWitness. A well-formed proposal is accepted for evaluation, not thereby admitted as a predicate.

Note: This operation does not add the predicate to the vocabulary. It queues the proposal for acceptance testing (Operation 8).

Operation 8: `accept_predicate`

Purpose: Run acceptance tests on a proposed predicate and, if passed, add to vocabulary.

accept_predicate(
  proposal_id: ProposalId
) → AcceptanceReceipt | RejectionWitness | Inconclusive

Preconditions:

proposal_id refers to a valid pending proposal
System has sufficient resources to run test suite

Acceptance criteria (per A29):

Positive exemplars: Meet the declared discrimination requirement under the specified evaluation
Negative exemplars: Meet the declared exclusion and confounder requirements; exact checks and statistical evaluations retain their different warrants
Invariants: All hard invariants must hold
Preservation: Establish any claimed deductive conservativity; check query and version compatibility separately. Passing the exemplar suite does not prove either universal claim.
Scope consistency: Verify the required overlap, receiving-context and authority obligations, including the confounder and abstention checks of A29.
Operationality: Establish the declared latency and cost bounds, pinned dependencies, caching conditions and revalidation requirements of A29.

Artifacts on success:

AcceptanceReceipt with version, scope, and test results summary
Predicate added to vocabulary with declared scope

Failure modes:

RejectionWitness with TEST_FAILURE listing failed cases
RejectionWitness with INVARIANT_VIOLATION with specific constraint
RejectionWitness with NOT_CONSERVATIVE with counterexample
RejectionWitness with SCOPE_UNDEFINED listing demonstrated scope failures
Inconclusive where a required obligation remains unestablished; provisional evaluation does not grant certified use

Invariant: Accepted predicates are versioned. Future modifications create new versions, not overwrites.

Operation 9: `query`

Purpose: Return candidates matching query predicates, with attached obligations.

query(
  pattern: QueryPattern,
  contexts: Set⟨Context⟩,
  constraints: Set⟨Constraint⟩
) → QueryResult | UnsatCore | RejectionWitness | Inconclusive

QueryResult := {
  candidates: Set⟨{ entity: EntityRef, claims: Set⟨ClaimReceipt⟩ }⟩,
  obligations: QueryObligations,
  coverage: CoverageReport
}

QueryObligations := {
  required_witnesses: Set⟨WitnessRequirement⟩,
  contexts_consulted: Set⟨Context⟩,
  invariants_enforced: Set⟨Constraint⟩,
  uncertainty_budget: UncertaintySpec
}

Preconditions:

All predicates in pattern exist in at least one context in contexts
The query declares the supported logic, evidence requirements and checking budget. A preliminary search may establish satisfiability or unsatisfiability in its supported fragment; it need not decide every query.

Artifacts:

QueryResult with candidates, obligations, and coverage report

Failure modes:

UnsatCore if unsatisfiability is established; an empty retrieved set alone does not establish it
RejectionWitness with PREDICATE_UNKNOWN if pattern uses undefined predicate
RejectionWitness with CONTEXT_INACCESSIBLE if context cannot be reached
Inconclusive when a required logical or evidence check remains incomplete

Invariant: Query results include provenance for every claim. No "orphan" results.

Operation 10: `refuse_or_retract`

Purpose: Record established unsatisfiability, or accept a withdrawal or correction and account for its treatment within a declared dependency boundary. These are distinct modes of one operation.

-- Refusal mode; call after unsatisfiability has been established
refuse(
  constraints: Set⟨Constraint⟩,
  grounds: RefusalEvidence
) → UnsatCore

-- Retraction mode; correction identifies the assertion being superseded
retract(
  claim_receipt: ClaimReceipt,
  reason: RetractionReason,
  authority: Witness,
  correction: Option<CorrectedAssertionAndEvidence>,
  dependency_boundary: DeclaredDependencyBoundary
) → RetractionReceipt | RejectionWitness | Inconclusive

Refusal preconditions: The constraints have been determined unsatisfiable. A pending determination is handled as Inconclusive by the requesting query; it does not satisfy this mode's precondition.

Refusal artifacts (per A27): UnsatCore identifies a verified inconsistent subset, the derivation and its premises. Minimality is claimed only if checked. A supported regime may promise a machine-checkable certificate; otherwise the receipt identifies the written proof and its review status.

Retraction preconditions:

The source assertion, evidence and version are identified.
The correction has supporting grounds and is accepted by an authority empowered under the applicable process. That may be the original asserter, its delegate, or another institution with authority to correct this record. The receipt identifies the basis of that authority.
The submitted dependency boundary distinguishes known uses, the records examined and gaps in the recipient or dependency inventory.

A failed authority check returns RejectionWitness; an unfinished required check returns Inconclusive with the missing grounds. Neither changes the claim to retracted. Rejecting an unauthorized instruction does not dispose of the underlying substantive challenge, which may require referral under the applicable process.

Retraction artifacts:

RetractionReceipt contains the accepted source withdrawal or correction, grounds, authority, timestamp, version references and a link to any replacement assertion. Registration and verification of the replacement remain separate operations; acceptance of the correction does not certify the replacement automatically.

The receipt also carries or references A26's DependentReassessment records. A premise reference can identify compound and alternative support routes. If withdrawal defeats one route while another remains adequate, retention records the assessed alternative; an apparent alternative whose dependence has not been checked cannot be declared unaffected. Each identifies the receiving use and policy, the property or premise it consumed, its evidence version, disposition, supporting grounds and remaining obligations. Required support withdrawn, independent support retained, reassessment incomplete and dependency unaffected are distinct dispositions. An action already taken is recorded separately with the authorized review or remedy process and its status.

Completion rule: Acceptance at the source is one completed act. Propagation is reported only for the declared, examined boundary. Known uses cannot keep advertising withdrawn support while reassessment is pending. An independently supported conclusion can survive on identified grounds; a use of an unaffected premise need not be invalidated. Notifications, acknowledgments, completed reassessments and completed remedies are recorded separately. Unknown or unreachable recipients, absent dependency records and outstanding actions preclude claiming completion beyond the work actually established.

Invariant: Retraction remains legible as a correction. Historical audit access is governed by purpose, authority and retention obligations; it does not restore the withdrawn assertion to ordinary results or renew adverse use against its subject. Routine retirement is not falsification. A receipt that traces an affected action supplies neither the authority nor the practical means to reverse it.

I.3 Compliance Criteria

A system is compliant with this Third-Mode interface iff it demonstrates the following requirements within its declared implementation boundary:

All ten operations are implemented with the specified signatures
Preconditions are enforced (operations fail predictably when preconditions are violated)
Artifacts are produced (success, demonstrated failure and incomplete checking retain their distinct grounds and outstanding obligations; consequential pending uses carry the account and disposition evidence required by I.1.6)
Invariants are maintained (immutability, auditability, versioning)
Outcomes remain distinguishable: verified success, demonstrated failure and incomplete checking. Implementations must test failure capture and disclose its operational boundary; listing outcome types does not prove capture through every crash or bypass.

I.3.1 Minimum Test Suite

A compliance test must verify:

Test Case	Operation	Expected
Register valid claim	`register_claim`	`ClaimReceipt`
Register claim with wrong type	`register_claim`	`RejectionWitness(TYPE_MISMATCH)`
Register claim violating the declared consistency requirement	`register_claim`	`RejectionWitness(CONTRADICTION)`
Declare valid equivalence	`declare_equivalence`	`Equivalence`
Transport within scope	`transport`	`TransportReceipt`
Transport outside scope	`transport`	`ScopeViolation(OUTSIDE_SCOPE)`
Glue matching family under established sheaf and effective-construction hypotheses	`glue`	`GluingReceipt`
Glue disagreeing family	`glue`	`ObstructionWitness`
Accept valid predicate	`accept_predicate`	`AcceptanceReceipt`
Accept failing predicate	`accept_predicate`	`RejectionWitness(TEST_FAILURE)`
Query with satisfiable constraints and completed required checks	`query`	`QueryResult`
Query with established unsatisfiability and its grounds	`query`	`UnsatCore`
Retract with authority	`retract`	`RetractionReceipt`
Retract without authority	`retract`	`RejectionWitness`; no accepted source withdrawal
Authority check unfinished	`retract`	`Inconclusive`; challenge remains pending
Required support withdrawn	`retract`	Dependent use stops claiming that support; reassessment status recorded
Independent grounds remain	`retract`	Retention names adequate unaffected support
Different premise consumed	`retract`	Dependency recorded as unaffected on stated grounds
Recipient unknown or unreachable	`retract`	Coverage limit and outstanding recipient recorded
Action already taken	`retract`	Separate authorized review or remedy remains outstanding unless completion is evidenced
No adequate resolving method known	Any incomplete check	`Inconclusive` states the unresolved obligation and method limit; no promised discovery date
Incomplete result used to maintain a consequential pending state	Receiving use of any operation	I.1.6 account identifies cause, responsibility, review point, governing response and interim grounds
Pending use reaches its review point without resolution	Receiving process	Required disposition recorded; repeating the incomplete result is not authority for continuation
Responsible process not established	Receiving use	Gap and referral status explicit; no claim that a managed pending process has been supplied
Separately authorized precaution	Receiving process	Actual grounds and bounds retained; unfinished ordinary certification remains unfinished

I.4 What This Specification Does Not Cover

This interface specifies what a Third-Mode system must do, not how:

Storage implementation: Any backend (graph DB, relational, in-memory) is acceptable
Consistency model: The chosen model must preserve the promised acceptance and reading guarantees; its name alone does not demonstrate compatibility
Computation strategy: Eager or lazy evaluation of gluing is implementation-dependent
Distributed architecture: Single-node or distributed implementations are both valid
Query language: The QueryPattern type is abstract; implementations may use SQL, GraphQL, Datalog, etc.

The specification also does not cover:

Authentication/authorization: The mechanism and institutional allocation of authority are external. Operations must check the authority they require; a field claiming it is insufficient. Their records do not create political authority or determine adequate process.
Performance requirements: No universal latency or throughput guarantees. This does not waive a receiving use's declared budgets or I.1.6 review obligations.
UI/API surface: Operations may be exposed via any interface (REST, gRPC, library API)

I.5 Relationship to Anchors

This interface draws directly from the formal anchors:

Operation	Primary Anchors
`create_context`	A12, A12b (covers, site structure)
`register_claim`	A2, A2b (provenance, witnessed assertion)
`verify_witness`	A2c (witness classes)
`declare_equivalence`	A10, A23, A30 (witnessed sameness, scoped equivalence)
`transport`	A16 (transport discipline)
`glue`	A13 (sheaf condition)
`propose_predicate`	A17, A19 (predicate invention, proposal operator)
`accept_predicate`	A29, A24 (predicate acceptance, predicate package)
`query`	A25 (query semantics)
`refuse_or_retract`	A27 (refusal); A2, A25, A26 (grounds, dependent uses and bounded correction)

I.6 Consequence

The interface requires a receiving operation to preserve the grounds and scope of what it inherits. Exact amalgamation is one possible result under its hypotheses. A justified statistical comparison is another kind of achievement; unfinished checking supplies neither.

After correction, the same discipline follows the premise actually consumed. A use must cease claiming withdrawn support, retain an independently sustained conclusion on its identified grounds, or expose the reassessment still required. Coverage ends where the established dependency record and completed work end. The interface cannot call an action remedied merely because the assertion supporting it has changed.

Obligation Reference

The following map gathers requirements developed in the Part V dossier. These are manuscript obligations, not reports of a complete implementation. Implementation correspondence follows separately.

Receiving operation	Required grounds and scope	Unearned inference prohibited	Outcomes and retained evidence	Governing contract
Submit a predicate proposal; register an assertion; certify a result	Operation 2 requires a checked witness for its assertion; certification requires completed applicable checks	Proposal submission, assertion registration or a high score establishes predicate admission	Proposal, scoped acceptance, demonstrated rejection or incomplete check; dossier and check record	A17, A19b, A24, A29; Operations 2, 7–8
Substitute a representation	Established mapping and property preservation in the receiving scope	Name match preserves every property	Transport receipt, scope violation or Inconclusive; mapping, footprint and witnesses	A16, A23, A30; Operations 4–5
Apply to a different purpose	Evidence adequate to the new question; applicable authority	Earlier usefulness supplies new permission or an untested property	Further evaluation, narrower use or unfinished qualification; changed requirements	A24–A25; Operations 8–9
Compare local results	Typed comparisons with the hypotheses of the claimed guarantee	Tolerance or voting establishes exact gluing	Exact amalgamation, bounded statistical result, disagreement or incomplete comparison; maps and evidence	A13, A17; Operation 6; Problem 8
Continue after a version change	Preservation on declared queries, scope, evidence and authority	A pin, superset or new number preserves every result	Supported compatibility, breaking change or unresolved assessment; version and test records	A26
Stop at a checking budget	Declared procedure, completed work and remaining obligations	Exhausted budget counts as successful checking	Scoped result or Inconclusive; costs and unchecked obligations	A21, A24–A25
Maintain a consequential pending use	I.1.6 account: cause, further work or method limit, responsible disposition, review point and interim authority	An unanswered check supplies permission to act or authority for indefinite delay	Incomplete evidence remains distinct from a recorded disposition; continued action needs its own grounds	I.1.6; A25–A26; applicable institutional process
Accept correction and reassess reuse	Authorized, evidenced source update; premises actually consumed	Every descendant is invalid, or a source receipt proves propagation complete	Four evidentiary dispositions plus separate action status; coverage, notices, independent grounds and gaps	A26; Operation 10
Reconsider an action	Grounds and authority under the relevant process	Updating evidence performs reversal or remedy	Referral, pending or evidenced completion; responsible process and outcome	A26; external institutional authority

Incident Correspondence

These incidents, examined in Volume III, test different transitions in the receiving account. Their established explanations remain indispensable. Evidence law, deployment control and authentication already identify failures here; the correspondence follows what subsequent operations did on the strength of the missing or mistaken grounds.

Incident and documented event	Receiving inference and established discipline	What following the dependence adds
Horizon. In the appeals resolved in Hamilton, the Court of Appeal found that prosecutions had proceeded without adequate investigation of whether apparent shortfalls represented actual loss, and without corroboration in the relevant cases.	A discrepancy in an accounting system could enter a criminal case as evidence against its operator. Disclosure and criminal proof required investigation that the recorded difference did not itself supply.	The question follows the assertion from account to investigation to prosecution: which additional grounds made each stronger use warranted? Correcting a balance and setting aside a conviction are different acts. The judgment supplies the legal findings; A12 supplies no substitute test of guilt.²
Knight Capital. The SEC found that new code reached seven of eight servers. A reused flag activated old Power Peg code on the eighth. During the incident, removing the new code from the seven enlarged the failure.	Configuration, testing and operational risk controls failed. A rollback instruction needed an account of what each server would execute afterward. This is not a demonstrated violation of logical conservativity.	A changed component must be assessed with its operating dependencies. Incoming-order checks could not stand in for controls on the orders subsequently generated or the firm's aggregate exposure. A repair instruction itself creates a new consequential use requiring grounds.³
Wormhole. A vulnerability in the Solana-side verification path enabled unbacked wrapped ether to be minted. Historical source shows instruction data being read through helpers that did not authenticate the supplied instructions account; checked replacements test its address.	Authentication must establish that purported evidence of signature verification comes from the required source. Acceptance by the receiving program did not make the forged attestation valid.	The receiving mint relied on a verification condition that had not been established. Closing the technical vulnerability could stop that route without restoring the asset backing already lost. Jump Crypto separately reported replenishing that backing.⁴

These identifications do not establish that adopting this specification would have prevented the incidents. They locate work an implementation or institution must actually perform. A record of a test cannot substitute for the test; a trace to an affected transaction cannot supply the means or authority to repair its consequences.

Bulla Correspondence

Bulla supplies related capabilities at different maturity levels. The inspected implementation is pinned to commit dd5806a8; the correspondence concerns those paths and their tests. It is not a claim of complete Third-Mode compliance. The complete source-and-test map accompanies the publication record.

Obligation	Records	Checks	Enforces	Not supplied	Deliberately not decided	Evidence
Identify an occurrence and its reported grounds	Distinct content, occurrence, attestation and log identities	Hashes, supported envelope and supplied signatures	Rejects invalid input at that verification boundary	Truth or complete observation of the reported execution	Actual event time from a signed claimed time; worldly truth	Action receipts⁵
Choose whether to rely	Receipt reference, policy and RELY, REFUSE or ESCALATE result	Policy and recorded verdict recompute	Record builder rejects a mismatched verdict; decision alone stops no action	Future correction monitoring or remedy	Legitimacy, fault and damages	Reliance⁶
Preserve accepted correction references	Named affected requirements and competing corrections	Target, lineage and external authority in the inspected profiles	Withholds affected eligibility; preserves a fork without choosing its winner	General dependent-use discovery or reassessment of independent support	Which correction is substantively right	Source-only profiles⁷
State coverage	Supplied observed and missing IDs	Qualifying receipts against the declared denominator	Invalid receipts do not reduce missing evidence	Proof that every real action was observed	Missing evidence as proof of wrongdoing	Coverage and profile checks⁸
Preserve the assurance actually obtained	Grounding and bound fields; profile evaluation references	Supported recorded predicates; exact hash comparison in the inspected profile case	Ineligible states do not pass that requirement gate	Exact sheaf gluing or general statistical calibration	Adequacy for an external legal or scientific purpose	Receipt and profile checks⁷
Stop a call	Gate outcome and refusal record	Supplied registry and evidence under configured rules	Blocks before dispatch only in enforce mode on the classified, gated path	Universal interception or reversal	PROCEED as universal authentication or legitimate permission	Recourse gate and proxy⁹
Retain history and expose further remedy	Declared retention, forum and consequence references	Specified bindings and profile eligibility	No general payment, deletion or remedy executor	Enforced retention expiry, forum access or collection	Adequate process and appropriate relief	Receipts and source-only profiles⁷

The Assurance Linker and Incident Packet examined here are experimental source-only profiles excluded from the distribution. Their named worklists do not implement A26's general correction contract. A receipt verifier may authenticate an assertion without verifying its external truth. A proxy can prevent a classified call on an enforced path without controlling every way an action could occur. Those boundaries determine what can be claimed about the implementation; a stronger manuscript obligation remains a requirement to be met.

See Grounds of the Articles, Articles 2–3 and the Constitutional Machine Design Brief, provisions on review, reversibility and remedy. Article 2 concerns independent, timely and effective contestation; Article 3 concerns competent independent human judgment for material adverse action, including cumulative omissions and delays. These are the manuscript's proposed constitutional duties, not claims that the ten operations implement a tribunal or state current law. I.1.6 imports no universal time limit or automatic outcome for every domain. ↩
Hamilton and others v Post Office Ltd [2021] EWCA Crim 577, judgment, 23 April 2021, especially §§11–22 and 207–209. The latter findings distinguish filtered or insufficiently investigated data, actual loss and corroboration. The correspondence concerns the judgment's identified cases, not every Horizon transaction or a claim that every accounting discrepancy was false. See Volume III, “The Membrane”. ↩
SEC, In the Matter of Knight Capital Americas LLC, Release 34-70694, 16 October 2013, findings 12–16, 20–28. A consent administrative order: Knight neither admitted nor denied the findings, except jurisdiction. Orders and executions remain distinct. See Volume III, “Charters in Code”. ↩
Wormhole's Governor background, inspected at the file revision of 24 June 2025, retrospectively describes the February 2022 exploit. The technical comparison is between verify_signatures at ca509f2 and the change to checked helpers at 7edbbd3, together with Solana 1.9.4's helper definitions. The old routine did check the reported instruction's program identifier; what the checked helpers add is authentication of the instructions account itself. Repository history is not proof of a deployment date or an exploit replay. Jump Crypto's account, 11 February 2022, reports purchasing and supplying the missing ether; this does not establish every holder's eventual outcome. See Volume III, “Fractal Polis”. ↩
Pinned bulla/src/bulla/action_receipt.py, particularly verify_receipt, lines 1033–1291. The inspected v0.4 identity, signature and time-tamper tests distinguish digest validity from authentication and physical occurrence. The publication correspondence preserves exact source hashes, declarations and the selected test record. ↩
Pinned bulla/src/bulla/reliance.py, lines 191–340 and 436–557. The policy can expressly accept an unresolved dimension; that choice does not resolve it. REFUSE may report a verification-policy shortfall rather than falsity of the underlying claim. Selected tests check strict/pragmatic policies and recomputation of a recorded verdict. ↩
Pinned bulla/src/bulla/experimental/assurance_linker.py and incident_packet.py; the publication source map identifies their exact locations and hashes. The Linker examines explicitly supplied affected requirement IDs and can report CHALLENGE_REQUIRED. Incident Packet preserves correction forks without selecting their winner. Neither implements generic independent-support reassessment. Their source-only status, external authority context and NOT_COMPUTED fields remain operative boundaries. ↩ ↩² ↩³
Pinned bulla/src/bulla/coverage.py, event_coverage, lines 525–718, and the Incident Packet denominator tests. The denominator is an input whose binding can be checked. That does not establish its complete correspondence to real events or an observer's organizational independence. ↩
Pinned bulla/src/bulla/recourse_gate.py, lines 159–357, and live_proxy.py, lines 554–582 and 1089–1143. The inspected gateway tests cover the configured interception path. A retained fixture probe produces PROCEED with authenticity=None when inclusion is valid but the served deed lacks its signature and full certificate. PROCEED therefore cannot be offered as proof that every authenticity check completed. ↩

← Back to Appendices Back to The Proofs →

Explore Res Agentica

Reading

Minimum Third-Mode Interface

I.1 Core Types

I.1.1 Primitive Types

I.1.2 Witness Types

I.1.3 Equivalence Types

I.1.4 Cover Types

I.1.5 Artifact Types

I.1.6 Incomplete Checks and Pending Uses

I.2 The Ten Operations

Operation 1: `create_context`

Operation 2: `register_claim`

Operation 3: `verify_witness`

Operation 4: `declare_equivalence`

Operation 5: `transport`

Operation 6: `glue`

Operation 7: `propose_predicate`

Operation 8: `accept_predicate`

Operation 9: `query`

Operation 10: `refuse_or_retract`

I.3 Compliance Criteria

I.3.1 Minimum Test Suite

I.4 What This Specification Does Not Cover

I.5 Relationship to Anchors

I.6 Consequence

Obligation Reference

Incident Correspondence

Bulla Correspondence

Search the book

In this chapter

I.1 Core Types

I.1.1 Primitive Types

I.1.2 Witness Types

I.1.3 Equivalence Types

I.1.4 Cover Types

I.1.5 Artifact Types

I.1.6 Incomplete Checks and Pending Uses

I.2 The Ten Operations

Operation 1: create_context

Operation 2: register_claim

Operation 3: verify_witness

Operation 4: declare_equivalence

Operation 5: transport

Operation 6: glue

Operation 7: propose_predicate

Operation 8: accept_predicate

Operation 9: query

Operation 10: refuse_or_retract

I.3 Compliance Criteria

I.3.1 Minimum Test Suite

I.4 What This Specification Does Not Cover

I.5 Relationship to Anchors

I.6 Consequence

Obligation Reference

Incident Correspondence

Bulla Correspondence

Footnotes

Operation 1: `create_context`

Operation 2: `register_claim`

Operation 3: `verify_witness`

Operation 4: `declare_equivalence`

Operation 5: `transport`

Operation 6: `glue`

Operation 7: `propose_predicate`

Operation 8: `accept_predicate`

Operation 9: `query`

Operation 10: `refuse_or_retract`