Implementation Formats

The categorical machinery of Parts II–V—sheaves, fibrations, transport—must eventually become data structures that engineers can instantiate, serialize, and verify. This appendix sketches records for those obligations. They are proposed explanatory formats, not a shipped schema or proof that an implementation enforces the contracts. The governing scope and verification conditions remain those of the anchors and Appendix I.

Predicate Dossier Schema

A predicate package (A24) requires more than a definition—it requires the full apparatus for testing, versioning, and accountability. The excerpt below shows identity, evidence, scope and version fields. The complete A24/A29 package also requires its evaluator, execution dependencies, confounder and abstention treatment, and operational budget; those obligations are not waived by their omission from this excerpt.

interface PredicateDossier {
  // Identity
  id: string;
  version: Version;
  
  // Signature (A3)
  signature: {
    name: string;
    arity: number;
    types: Type[];
  };
  
  // Definition
  intension: Definition;  // Rule, model, or exemplar-based
  
  // Test Suite (A29)
  tests: {
    positive: Exemplar[];   // Must classify as q
    negative: Exemplar[];   // Must not classify as q
    boundary: Exemplar[];   // Classification uncertain (explicit)
  };
  
  // Constraints (A18)
  invariants: Constraint[];  // Hard invariants that must hold
  
  // Provenance (A2)
  provenance: {
    source: string;         // Origin of definition
    author: string;         // Who created/approved
    timestamp: Date;        // When created
    derivedFrom?: string[]; // Parent predicates if any
  };
  
  // Scope (A30)
  scope: Scope;  // Contexts where predicate is valid
  
  // Versioning (A26)
  versionHistory: VersionEntry[];
  compatibility: CompatibilityDeclaration;
}

Field constraints:

• This exemplar-based admission policy requires positive examples. Other proof or testing regimes may justify an intentionally empty predicate; no general impossibility follows from the missing examples.
• invariants must include any hard constraints from the containing schema
• scope declares the domain of use; downward closure must be justified by the chosen refinement and property-preservation rules
• version follows semantic versioning: breaking changes increment major version

Witness Object Structure

Witnesses (A2b) must carry enough information for downstream verification. The witness object makes the verification contract explicit.

interface Witness<T> {
  // The claim being witnessed
  claim: T;
  
  // Evidence supporting the claim
  evidence: Evidence;
  
  // Verification regime (A2c)
  class: 'decidable' | 'probabilistic' | 'attested';
  
  // Validity scope
  scope: Scope;
  
  // Verification procedure
  verifier: Verifier<T>;
  
  // Provenance chain
  derivation?: DerivationStep[];
}

The class field declares a verification regime. The checked evidence, procedure, hypotheses and use determine what assurance follows; the field alone grants none.

Decidable Witnesses

Decidable witnesses support total, deterministic verification. The verifier always terminates and returns a definitive answer.

interface DecidableWitness<T> extends Witness<T> {
  class: 'decidable';
  evidence: 
    | { type: 'hash_match'; expected: Hash; actual: Hash }
    | { type: 'schema_isomorphism'; mapping: FieldMap }
    | { type: 'arithmetic_proof'; steps: ArithmeticStep[] }
    | { type: 'unsat_core'; core: Constraint[]; derivation: ProofStep[] };
  verifier: (claim: T, evidence: this['evidence']) => 'ok' | 'fail';
}

These total verifiers decide their stated predicates when supplied with valid inputs. An operation waiting for an input or unable to run the verifier must report its own incomplete check. A hash match establishes equality of the compared digests; identifying their contents additionally relies on the stated hashing assumptions. It establishes neither the truth of the document nor the occurrence of a reported execution. The unsat-core example concerns the checked constraints of T1.

Probabilistic Witnesses

Probabilistic witnesses support verification that terminates with statistical confidence rather than certainty.

interface ProbabilisticWitness<T> extends Witness<T> {
  class: 'probabilistic';
  evidence:
    | { type: 'embedding_similarity'; score: number; threshold: number; model: string }
    | { type: 'statistical_test'; test: string; pValue: number; n: number }
    | { type: 'classifier_output'; model: string; confidence: number; calibration?: Calibration };
  verifier: (claim: T, evidence: this['evidence']) => 
    { status: 'ok'; confidence: number; bounds: [number, number] } | 
    { status: 'fail'; confidence: number } |
    { status: 'inconclusive'; missing: Obligation[] };
}

These records can hold scores and test results. An embedding threshold can support candidate selection; it is not a calibrated probability of identity. A p-value is not a probability that the claim is true. To support a statistical assertion, the record must bind the estimand, sampling or calibration procedure, assumptions and resulting bounds. Missing support leaves the proposed claim unverified.

Critical: State what a reported confidence level means and which procedure warrants it. Numerical fields do not make a confidence assertion valid. Approximate outcomes do not inherit exact sheaf gluing.

Attested Witnesses

An attested witness includes someone’s testimony. Computation can check its provenance or authentication; accepting the testimony for a particular use requires grounds concerning the attester, the claim and the receiving purpose.

interface AttestedWitness<T> extends Witness<T> {
  class: 'attested';
  evidence:
    | { type: 'human_label'; labeler: Authority; timestamp: Date }
    | { type: 'institutional_assertion'; institution: Authority; document: Reference }
    | { type: 'expert_judgement'; experts: Authority[]; consensus: ConsensusType };
  verifier: (claim: T, evidence: this['evidence'], trustedAuthorities: Authority[]) =>
    'ok_if_trusted' | 'authority_not_trusted' | 'fail' |
    { status: 'inconclusive'; missing: Obligation[] };
}

Attested witnesses include human labels (domain expert marked this item as "puffy dress"), institutional assertions (FDA approval document for drug classification), and expert judgement (panel consensus on boundary case).

Critical: Attested witnesses make trust explicit. The verifier returns ok_if_trusted when the authority chain is valid, leaving the trust decision to the caller.

Proof Object Format

An established logical refusal identifies its derivation. This proof object represents a supported machine-checkable regime. A written proof may instead be referenced with its review status where that is the declared regime. A rejection for missing permission and an unfinished check require different records; neither manufactures a proof of unsatisfiability.

// RelationKind retains A10's distinction; see Appendix I, I.1.3.
interface ProofObject {
  // What was proven
  conclusion: 
    | { type: 'unsat'; constraints: Constraint[] }
    | { type: 'equivalence'; left: Term; right: Term; relation_kind: RelationKind; scope: Scope }
    | { type: 'conservative_extension'; base: Signature; extension: Signature };
  
  // The proof itself
  proof: ProofStep[];
  
  // Verification metadata
  verifier: {
    algorithm: string;      // e.g., 'resolution', 'smt', 'type_checking'
    version: string;
    timestamp: Date;
  };
  
  // Human-readable summary
  summary: string;
}

interface ProofStep {
  rule: string;             // e.g., 'resolution', 'modus_ponens', 'transport'
  premises: number[];       // Indices of prior steps used
  conclusion: Formula;
  justification?: string;   // Human-readable explanation
}

Unsat proofs for T1 (contradiction) require:

• Verified unsat core: a subset of constraints that are inconsistent
• Derivation chain: sequence of inference steps leading to $\bot$
• Claim subset or cardinality minimality only when that additional property has been established

Equivalence proofs for T2 (reference) require:

• The terms being related and the declared relation kind (A10), retained in the claim being witnessed
• The scope in which equivalence holds
• The evidence under its actual regime: a checked map, a scoped attestation, or statistical evidence with its assumptions. A bare embedding match is a proposal, not an equivalence proof.

Witness Composition Rules

Witnesses can be combined to support more complex claims. Composition must preserve typing.

type CompositionRule =
  | { type: 'conjunction'; witnesses: Witness<any>[]; resultClass: WitnessClass }
  | { type: 'transport'; witness: Witness<any>; equivalence: EquivalenceWitness; resultScope: Scope }
  | { type: 'restriction'; witness: Witness<any>; toScope: Scope };

Conjunction: Exact proofs of $p$ and $q$ combine into a proof of $p \land q$. Combining statistical or attested evidence requires its own joint assumptions and bounds. Choosing the weakest class label does not calculate the resulting uncertainty.

Transport: Given witness for $P(a)$ and equivalence $a \sim_S b$, derive witness for $P(b)$ in scope $S$. Requires that $P$ is transportable along the equivalence (A16).

Restriction: Reuse in a smaller scope requires the claim and its evidence conditions to survive the specified restriction. A universal pointwise claim can restrict to a subset. An aggregate estimate over one population does not thereby estimate every subpopulation.

Forbidden: Scope widening. A witness valid in scope $S$ cannot be promoted to scope $S' \supset S$ without additional evidence.

Citation Graph Structure

Claims reference witnesses, witnesses reference evidence, evidence chains to sources. The citation graph makes this structure explicit.

interface CitationGraph {
  nodes: (Claim | Witness | Evidence | Source)[];
  edges: CitationEdge[];
}

interface CitationEdge {
  from: NodeId;
  to: NodeId;
  relation: 'supports' | 'derives_from' | 'cites' | 'contradicts';
  strength?: number;  // For probabilistic support
}

Invariants:

• Claims advertised as witnessed or certified identify their supporting grounds (A2); submission of a predicate proposal under Operation 7 does not supply a witness for an asserted claim
• Every witness must trace to at least one source
• Contradicts edges trigger consistency checking (A1)

Versioning Protocol

Schema evolution (T9) requires distinguishing safe changes from breaking changes.

interface VersionEntry {
  version: Version;
  timestamp: Date;
  changeType: 'preserving' | 'breaking' | 'unresolved';
  assessedScope: Scope;
  assessedQueries: QueryPattern[];
  grounds: EvidenceReference[];
  outstandingChecks: Obligation[];
  changes: Change[];
  migrationPath?: MigrationPlan;  // Required if breaking
}

interface MigrationPlan {
  // Queries that need rewriting
  affectedQueries: QueryPattern[];
  
  // Predicate mappings
  predicateMappings: { old: PredicateId; new: PredicateId; transform: Transform }[];
  
  // Data migration
  dataMigration?: {
    script: MigrationScript;
    estimatedCost: Cost;
    reversible: boolean;
  };
}

Conservative extension (A17b): The theory acquires no new old-language consequences. Unchanged query behavior, data readability and permission to reuse a result require their separate compatibility checks.

Breaking change: A declared compatibility requirement has failed. The earlier result may remain true under its original definition; migration must identify the changed use. The plan specifies:

• Which queries are affected
• How predicates map from old to new
• Whether the change is reversible

Correction Across Reuse

A citation is not necessarily a dependency. A receiving use must identify which property or premise it consumes, from which evidence version, and under which scope and policy. The following records reference A26's complete disposition contract; they do not add an eleventh Appendix I operation.

interface CorrectionRecord {
  sourceAssertion: ClaimReceiptRef;
  sourceEvidence: VersionedEvidenceRef[];
  correctedPremise: PropertyOrPremiseRef;
  correction: CorrectedAssertionOrWithdrawal;
  grounds: EvidenceRef[];
  acceptedBy: AuthorityRef;
  authorityBasis: PolicyOrDelegationRef;
  acceptedAt: Date;
  examinedBoundary: DependencyCoverage;
  reassessments: DependentReassessment[];
  outstanding: RecipientOrDependencyOrAction[];
}

interface DependentReassessment {
  use: VersionedUseRef;
  consumedPremise: PropertyOrPremiseRef;
  consumedEvidence: VersionedEvidenceRef[];
  receivingScopeAndPolicy: ScopeAndPolicyRef;
  disposition: 'support_withdrawn' | 'independent_support_retained'
             | 'reassessment_incomplete' | 'dependency_unaffected';
  grounds: EvidenceRef[];
  currentClaimStatus: ScopedStatus;
  notification: 'not_sent' | 'sent' | 'acknowledged' | 'unreachable';
  actionReview: 'not_applicable' | 'outstanding' | 'referred' | 'completed';
  actionReviewEvidence?: AuthorizedProcessRef;
  unresolvedObligations: Obligation[];
}

When an incomplete check or reassessment governs a consequential pending use, its obligation and receiving-process references must also carry Appendix I, I.1.6's account: cause, further work or known method limit, responsible disposition, review point, governing response and interim grounds. The schematic status or missing array alone is not that account. These are manuscript requirements for the records' meaning, not a new executable type or Bulla behavior.

A consumedPremise reference may identify a compound premise and derivation. For (A and B) or (D and E), the evidence references and reassessment grounds must distinguish the route affected by withdrawal from an alternative still adequate for the receiving use. Unexamined independence leaves reassessment incomplete. A26 develops this case; no additional operation or record kind is required.

The accepted source update and the treatment of dependent uses have separate completion states. Affected uses stop advertising withdrawn support; independent grounds can preserve a conclusion. Unknown recipients limit coverage. An unauthorized withdrawal is not accepted merely because it arrives in this format. An incomplete authority check remains incomplete, and a substantive challenge may require consideration through the relevant process. Routine retirement does not mark a claim false. An action already taken requires a further authorized process; a correction record cannot report remedy complete without its evidence.

Audit Trail Format

Accountability requires recording what the system did and why.

interface AuditEntry {
  timestamp: Date;
  operation: 
    | { type: 'predicate_invented'; dossier: PredicateDossier }
    | { type: 'equivalence_declared'; left: Term; right: Term; witness: Witness<any> }
    | { type: 'query_answered'; query: Query; result: Result; witnesses: Witness<any>[] }
    | { type: 'query_refused'; query: Query; grounds: ProofObject | ReviewedProofRef }
    | { type: 'query_rejected'; query: Query; reason: RejectionWitness }
    | { type: 'query_inconclusive'; query: Query; outstanding: Obligation[] }
    | { type: 'correction_accepted'; record: CorrectionRecord }
    | { type: 'dependent_use_reassessed'; record: DependentReassessment }
    | { type: 'schema_evolved'; from: Version; to: Version; migration?: MigrationPlan };
  
  context: {
    user?: UserId;
    session?: SessionId;
    coherenceBudget: Cost;
    budgetConsumed: Cost;
  };
  
  // For debugging and accountability
  trace?: ExecutionTrace;
}

Retention policy: Preserve enough version and correction history to interpret the claims still in use. Retention and access require a stated purpose, duration and authority; retaining evidence of an institution's conduct does not authorize indefinite adverse use against a record's subject. Aggregation must preserve the distinctions the remaining inquiry requires.

Coherence budget tracking: Every operation consumes part of the coherence budget (A21). The audit trail records both the allocated budget and actual consumption, exposing which operations are coherence-expensive. The record should expose which required work stopped when the budget bound and which results remained supported.

Format Index

Format	Governing contract	Purpose
Predicate Dossier	A24, A29	Excerpt of the full package’s identity, evidence, scope and version fields
Witness Object	A2b, A2c	Evidence with typed verification
Proof Object	A27	Proof record for the supported verification regime
Citation Graph	A2	Provenance tracking
Version Entry	A26	Schema evolution with migration
Correction and reassessment	A26; Appendix I, Operation 10	Bounded treatment of actual dependence, coverage and outstanding actions
Audit Entry	A21, A26	Checking outcomes, correction status and cost tracking

These formats specify records an implementation could supply. Their presence in a document does not establish execution, complete correction coverage or compliance. The operative requirements remain those of the anchors and Appendix I.