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 provides those structures, mapping each formal anchor to a concrete implementation format.

Predicate Dossier Schema

A predicate package (A24) requires more than a definition—it requires the full apparatus for testing, versioning, and accountability. The predicate dossier is the concrete implementation.

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:

• tests.positive must be non-empty; a predicate without positive examples cannot be tested
• invariants must include any hard constraints from the containing schema
• scope must be a downward-closed set of contexts
• 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 determines what guarantees the witness provides and how downstream consumers should treat verification results.

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';
}

Decidable witnesses include hash equality (document content matches expected hash), schema isomorphisms (two schemas are structurally equivalent via explicit field mapping), arithmetic proofs with derivation chains, and unsat cores for T1 resolution.

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 };
}

Probabilistic witnesses include embedding similarity (cosine similarity exceeds threshold, used for T2 candidate proposal), statistical tests (hypothesis test with p-value and sample size), and classifier outputs (model prediction with calibrated confidence).

Critical: Probabilistic witnesses must declare their confidence bounds. A witness claiming 95% confidence must have been calibrated on representative data.

Attested Witnesses

Attested witnesses depend on authority rather than computation. Verification checks provenance and trust, not truth.

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';
}

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

When the system refuses a query (A27), it must provide a machine-checkable explanation. The proof object formalizes this receipt.

interface ProofObject {
  // What was proven
  conclusion: 
    | { type: 'unsat'; constraints: Constraint[] }
    | { type: 'equivalence'; left: Term; right: Term; 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:

• Small unsat core: subset of constraints that are inconsistent
• Derivation chain: sequence of inference steps leading to $\bot$
• The system need not find the globally minimal core (NP-hard), but should attempt local minimization

Equivalence proofs for T2 (reference) require:

• The terms being equated
• The scope in which equivalence holds
• The witness (embedding match, human attestation, or computed isomorphism)

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: Combining witnesses for $p$ and $q$ yields a witness for $p \land q$. The result class is the weakest of the inputs: decidable + probabilistic = probabilistic.

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: Narrowing scope. If $\pi$ witnesses $p$ in scope $S$, then $\pi$ also witnesses $p$ in any $S' \subseteq S$.

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:

• Every claim must have at least one supporting witness (A2)
• 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: 'conservative' | 'breaking';
  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): All old queries remain valid. No migration required.

Breaking change: Some old truths invalidated. Migration plan required, specifying:

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

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; proof: ProofObject }
    | { 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: Audit entries for predicate invention and schema evolution should be retained indefinitely. Query audit entries may be aggregated after a retention period.

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. Without this visibility, systems drift toward incoherence under load without warning.

Format Index

Format	Implements	Purpose
Predicate Dossier	A24	Full predicate specification with tests and versioning
Witness Object	A2b, A2c	Evidence with typed verification
Proof Object	A27	Machine-checkable refusal receipts
Citation Graph	A2	Provenance tracking
Version Entry	A26	Schema evolution with migration
Audit Entry	A21	Accountability and cost tracking

These formats are the implementation surface of the Third Mode. They translate the categorical machinery—sheaves, fibrations, transport—into data structures that engineers can instantiate, serialize, and verify.