Mathematical Foundations

Appendix K

17 min read

Appendix K: Mathematical Foundations

This appendix does not prove new theorems. It identifies exactly which theorems from model theory, sheaf theory, and type theory underpin the Third Mode's guarantees—and states what each guarantee does not promise.

The discipline is new. The mathematics is not.

The Borrowed Machinery

Every formal result invoked in The Proofs is a known theorem, often with proofs dating to the mid-twentieth century:

Guarantee	Underlying Theorem	Canonical Source
Safe vocabulary extension	Conservative extension	Shoenfield, Mathematical Logic (1967), §4.6
Local-to-global coherence	Sheaf gluing condition	Mac Lane & Moerdijk, Sheaves in Geometry and Logic (1992), Ch. II
Substitution under equivalence	Transport along paths	HoTT Book (2013), §2.3
Verification cost scaling	Cover refinement	Standard; see Bott & Tu (1982) for analogous arguments

The mathematical infrastructure exists. The engineering object does not.

What the Third Mode contributes is not a theorem but an architecture: a specification of exactly which verification steps must occur, exactly what artifacts must be emitted, and exactly how failures must be reported. Existing systems produce silence or exceptions where this architecture produces witnesses, receipts, and obstruction records.

What This Appendix Provides

For each load-bearing result, we state:

The theorem — What the mathematics guarantees
The operational consequence — What this means for system behavior
The failure mode — What would constitute a violation
The anchor — Where the main text invokes this machinery

For readers who want full proofs, the canonical sources are cited. For readers who want to understand how the proofs translate to system design, the operational consequences are the payload.

K.1 Conservative Extension Safety

Informal claim: Adding a new predicate to the vocabulary does not change the truth of existing statements.

Theorem(Conservative Extension)

Let $(\Sigma, I, L)$ be a theory (signature $\Sigma$ , constraints $I$ , logic $L$ ). Let $\Sigma' = \Sigma \cup \{q\}$ be an extension adding predicate $q$ with constraints $I' \supseteq I$ .

The extension is conservative over $(\Sigma, I, L)$ iff for every $\Sigma$ -sentence $\varphi$ :

(\Sigma', I', L) \vdash \varphi \quad \Longleftrightarrow \quad (\Sigma, I, L) \vdash \varphi

That is: the new predicate does not create new theorems in the old language.

Proof

Proof sketch (model-theoretic):

Let $M \models (\Sigma, I)$ be a model of the original theory.
Extension: We must show $M$ extends to $M' \models (\Sigma', I')$ . Since $q$ is new (not in $\Sigma$ ), we can interpret $q^{M'}$ as any subset of the appropriate product of domains that satisfies the new constraints $I' \setminus I$ . If such an interpretation exists, $M$ extends.
Conservativity: Suppose $(\Sigma', I', L) \vdash \varphi$ for a $\Sigma$ -sentence $\varphi$ . By completeness (for the relevant logic), $\varphi$ holds in all models of $(\Sigma', I')$ . In particular, it holds in all extensions of models of $(\Sigma, I)$ . Since $\varphi$ is a $\Sigma$ -sentence, its truth depends only on the $\Sigma$ -reduct. Therefore $\varphi$ holds in all models of $(\Sigma, I)$ . By completeness, $(\Sigma, I, L) \vdash \varphi$ .
The converse is immediate: if $(\Sigma, I, L) \vdash \varphi$ , then every model of $(\Sigma', I')$ is an extension of some model of $(\Sigma, I)$ , so $\varphi$ holds.

Failure mode: The extension fails to be conservative if the new constraints $I' \setminus I$ entail $\Sigma$ -sentences not provable from $I$ alone. Example: adding $q$ with constraint $q(x) \to p(x)$ where $p$ is an existing predicate creates a conservative extension. Adding $q$ with constraint $\forall x. q(x)$ and $q(x) \to p(x)$ forces $\forall x. p(x)$ , which is non-conservative if $\forall x. p(x)$ was not previously provable.

∎

Operational consequence: When the Third Mode accepts a new predicate (A17/A29), it must verify that the extension is conservative. If verification fails, the predicate is rejected with a counterexample: a model of $(\Sigma, I)$ that cannot extend to a model of $(\Sigma', I')$ while preserving existing truths.

Anchor: A17b (Conservative Extension). This theorem and its proof are developed in full in Chapter 16.

K.1.1 Verification Strategies

Conservative extension is a semantic property. In general, checking it is undecidable. In practice, we deploy a hierarchy of verification strategies, each with known tradeoffs.

Modes

Mode	Completeness	Soundness	Artifacts	When to Use
Syntactic check	Incomplete	Sound	Parse tree	Fast gate: reject obviously non-conservative extensions (e.g., constraint mentions $\Sigma$ -predicates with universal quantifiers)
SAT/SMT	Complete for decidable fragments	Sound	Unsat core or countermodel	Default for propositional or linear arithmetic constraints
Model-theoretic sampling	Incomplete	Unsound (heuristic)	Candidate countermodels	Exploratory: find likely failures before expensive proofs
Proof assistant	Complete	Sound	Formal proof object	High-assurance: when the predicate will be load-bearing

Artifacts

A verification attempt produces one of:

ConservativityProof: A formal proof object (possibly machine-checked) establishing the extension is conservative.
Countermodel: A model $M \models (\Sigma, I)$ and a $\Sigma$ -sentence $\varphi$ such that $(\Sigma', I') \vdash \varphi$ but $M \not\models \varphi$ . This is a concrete witness of non-conservativity.
UnsatCore: The minimal subset of $I'$ that, together with $I$ , entails the problematic $\Sigma$ -sentence. Used for diagnosis and predicate revision.
Timeout: The verification budget was exhausted. The system treats this as "unknown" and may escalate to a higher mode or reject the predicate pending manual review.

Complexity and Limits

For fragments commonly used in data integration:

Fragment	Conservativity Check	Complexity
Propositional	Decidable	NP-complete (reduces to SAT)
Equality constraints	Decidable	Polynomial with union-find
Linear arithmetic (QF_LRA)	Decidable	Polynomial (linear programming)
Full first-order	Undecidable	Semi-decidable (may not terminate)
Higher-order / dependent types	Undecidable	Requires proof assistant

The Coherence Budget Forces Approximation

Real systems operate under time and resource constraints. The coherence budget (A21) specifies how much verification effort is permitted per operation. When the budget is tight:

Approximate gates replace exact checks. A syntactic check may clear a predicate that a full SAT check would reject.
Deferred verification queues expensive checks for batch processing. The predicate is admitted provisionally (lifecycle state: provisional) pending full verification.
Risk-tiered modes apply stronger verification to predicates with wider scope or higher stakes (e.g., predicates used in financial reconciliation get proof-assistant level; catalog metadata gets SAT/SMT).

The system does not pretend these tradeoffs don't exist. Every verification attempt records the mode used, the budget consumed, and the confidence level of the result. An approximate clearance is not a guarantee—it is a bet, explicitly priced.

K.2 Gluing Correctness

Informal claim: If local claims agree on overlaps, the sheaf condition guarantees a unique global claim.

Theorem(Gluing Correctness)

Let $F : \mathbf{Ctx}^{\mathrm{op}} \to \mathbf{Set}$ be a sheaf on the context site $(\mathbf{Ctx}, J)$ . Let $\{U_i \to U\}$ be a cover of $U$ .

If sections $s_i \in F(U_i)$ satisfy the matching condition:

s_i|_{U_i \times_U U_j} = s_j|_{U_i \times_U U_j} \quad \forall i, j

then there exists a unique $s \in F(U)$ such that $s|_{U_i} = s_i$ for all $i$ .

Proof

Proof sketch (equalizer diagram):

The sheaf condition states that $F(U)$ is the equalizer of:
$\prod_i F(U_i) \xrightarrow[\rho_2]{\rho_1} \prod_{i,j} F(U_i \times_U U_j)$
where $\rho_1$ restricts the $i$ -th component to $U_i \times_U U_j$ , and $\rho_2$ restricts the $j$ -th component.
A family $(s_i) \in \prod_i F(U_i)$ is in the equalizer iff $\rho_1(s_i) = \rho_2(s_i)$ , i.e., $s_i|_{U_i \times_U U_j} = s_j|_{U_i \times_U U_j}$ for all $i, j$ .
Existence: The matching condition says $(s_i)$ is in the equalizer. Therefore there exists $s \in F(U)$ that maps to $(s_i)$ under restriction.
Uniqueness: The equalizer is a limit; the map $F(U) \to \prod_i F(U_i)$ is injective (this is the locality condition). Therefore $s$ is unique.

Failure mode: If the matching condition fails (some $s_i|_{U_i \times_U U_j} \neq s_j|_{U_i \times_U U_j}$ ), the family is not in the equalizer, and no global section exists. The failure is localized to the specific overlap(s) where disagreement occurs.

∎

Operational consequence: The glue operation (Appendix I) checks the matching condition. If satisfied, it returns the unique global claim. If not, it returns an ObstructionWitness identifying the disagreeing contexts and the specific claims that conflict.

Anchor: A13 (Sheaf Condition). This theorem and its proof are developed in full in Chapter 11.

K.3 Scoped Transport Safety

Informal claim: Transporting a property along a witnessed equivalence preserves truth within the declared scope.

Theorem(Scoped Transport Safety)

Let $e : A \simeq_S B$ be a witnessed equivalence with scope $S$ . Let $P : \mathbf{Entity} \to \mathbf{Prop}$ be a transportable property. Let $U \in S$ be a context in the equivalence's scope.

If $P(A)$ holds in context $U$ , and transport is well-defined for $P$ along $e$ , then $\mathrm{transport}_e(P)(B)$ holds in context $U$ .

Conversely, if $U \notin S$ (context outside scope), transport is undefined and the operation fails with a ScopeViolation.

Proof

Proof sketch:

Within scope: By definition of witnessed equivalence, $e$ provides a certificate that $A$ and $B$ are interchangeable for all transportable properties in contexts within $S$ . The transport map $\mathrm{transport}_e : P(A) \to P(B)$ is part of the equivalence structure. If $P(A)$ holds (has a proof/witness), then $\mathrm{transport}_e$ carries that witness to a witness of $P(B)$ .
Preservation of truth: The transport is functorial: it preserves the structure of the proof. If $P(A)$ was witnessed by $\pi$ , then $P(B)$ is witnessed by $\mathrm{transport}_e(\pi)$ .
Outside scope: The equivalence certificate is only valid in $S$ . If $U \notin S$ , the system has no warrant that $A$ and $B$ are interchangeable in $U$ . The transport operation checks $U \in S$ as a precondition. Failure produces a ScopeViolation artifact.

Failure mode: Attempting to use an equivalence outside its scope is a type error. The equivalence $\texttt{NYC} \simeq_{\text{postal}} \texttt{New York City}$ does not justify substitution in a real estate context, even if both terms denote entities.

∎

Operational consequence: The transport operation (Appendix I) enforces scope checking. Every successful transport produces a TransportReceipt that binds the original claim, the transported claim, and the certificate. The receipt is auditable: any consumer can verify that the transport was within scope.

Anchor: A10 (Witnessed Sameness), A16 (Transport Discipline), A30 (Scoped Equivalence). This theorem and its proof are developed in full in Chapter 14.

K.4 Coherence Budget Monotonicity

Informal claim: Checking coherence over a larger cover costs at least as much as checking over a smaller cover.

Theorem(Coherence Budget Monotonicity)

Let $\mathcal{C} = \{U_i \to U\}$ be a cover of $U$ , and let $\mathcal{C}' = \{U'_j \to U\}$ be a refinement of $\mathcal{C}$ (every $U'_j$ factors through some $U_i$ ).

Let $\mathrm{Cost}(\mathcal{C})$ be the cost of verifying the matching condition over cover $\mathcal{C}$ . Then:

\mathrm{Cost}(\mathcal{C}') \geq \mathrm{Cost}(\mathcal{C})

Equality holds only if $\mathcal{C}'$ introduces no new overlaps.

Proof

Proof sketch:

The cost of checking the matching condition is dominated by the number of pairwise overlap checks.
For cover $\mathcal{C}$ with $n$ components, the number of overlaps is $O(n^2)$ in the worst case.
A refinement $\mathcal{C}'$ with $m \geq n$ components has $O(m^2)$ overlaps.
Each overlap check has cost $\geq 1$ (at minimum, comparing values). Therefore $\mathrm{Cost}(\mathcal{C}') \geq \mathrm{Cost}(\mathcal{C})$ .
Equality case: If $\mathcal{C}'$ refines $\mathcal{C}$ by splitting components that have no overlaps with each other, no new overlap checks are introduced. But typically, refinement increases overlap complexity.

∎

Operational consequence: There is no free lunch in coherence. Finer-grained verification (more contexts, more overlaps) costs more. The coherence budget (A21) must account for this: systems that demand higher coherence guarantees must pay with higher verification costs.

Anchor: A21 (Coherence Cost Model). This theorem and its proof are developed in full in Chapter 19.

K.5 What These Results Guarantee

Together, these four results provide the formal backbone of the Third Mode's promises:

Result	Guarantee
Conservative Extension Safety	New predicates don't corrupt existing knowledge
Gluing Correctness	Local agreement implies unique global truth
Scoped Transport Safety	Equivalences are safely bounded
Coherence Budget Monotonicity	Verification cost is predictable

What they do NOT guarantee:

Completeness: The Third Mode does not guarantee that every true statement can be proved. It guarantees that accepted statements are coherent with existing commitments.
Decidability: Checking the matching condition may be undecidable for some presheaves. The Third Mode specifies what must be checked, not that checking is always tractable.
Convergence: Multiple agents proposing predicates may not converge to a shared vocabulary. The Third Mode provides discipline, not consensus.

K.6 Formal Dependencies

The results depend on the following formal machinery:

Result	Dependencies
Conservative Extension	Model theory, completeness for the ambient logic
Gluing Correctness	Sheaf theory, equalizer definition
Scoped Transport Safety	Equivalence structure, transport maps
Coherence Budget Monotonicity	Cover refinement, overlap counting

For full proofs, consult:

Shoenfield (1967) for conservativity in classical logic
Mac Lane & Moerdijk (1992) for sheaf theory
HoTT Book (2013) for transport along equivalences
Grothendieck (SGA4) for site theory

The Third Mode's contribution is not inventing these results but applying them operationally: specifying the artifacts, failure modes, and audit trails that make the guarantees enforceable in software.

K.7 Formal Mini-Spine: The Obstruction Localization Theorem

This section gives one result with full rigor: complete definitions, a precise theorem statement, and a proof. The goal is to demonstrate that the claim "gluing failures are localized and structured" is not metaphor but mathematics.

K.7.1 Definitions

Context Category

A context category $\mathbf{Ctx}$ is a category where:

Objects are contexts $U, V, W, \ldots$ —each representing a view with a signature (vocabulary), constraints, and absence policy.
Morphisms $f : U \to V$ are refinements: $U$ is a more specific context than $V$ (e.g., "FDA regulatory view" refines "US legal view").
Composition is associative; identities exist.

Grothendieck Topology

A Grothendieck topology $J$ on $\mathbf{Ctx}$ assigns to each object $U$ a collection $J(U)$ of covering sieves. A sieve $S$ on $U$ is a subfunctor of $\mathrm{Hom}(-, U)$ ; it is covering if it is in $J(U)$ .

For our purposes, we use the simpler notion of a covering family: a collection $\{f_i : U_i \to U\}_{i \in I}$ such that the sieve it generates is in $J(U)$ .

The pair $(\mathbf{Ctx}, J)$ is a site.

Presheaf

A presheaf on $(\mathbf{Ctx}, J)$ is a contravariant functor $F : \mathbf{Ctx}^{\mathrm{op}} \to \mathbf{Set}$ .

For each context $U$ , $F(U)$ is the set of local sections (claims that hold in $U$ ).
For each morphism $f : U \to V$ , $F(f) : F(V) \to F(U)$ is the restriction map (how a claim in $V$ appears when viewed from the more specific context $U$ ).

Matching Family

Let $\{f_i : U_i \to U\}_{i \in I}$ be a covering family of $U$ . A matching family for a presheaf $F$ is a collection of sections $\{s_i \in F(U_i)\}_{i \in I}$ such that for all $i, j \in I$ :

s_i|_{U_i \times_U U_j} = s_j|_{U_i \times_U U_j}

where $U_i \times_U U_j$ is the pullback (the "overlap" context where both $U_i$ and $U_j$ apply).

Sheaf

A presheaf $F$ is a sheaf if for every covering family $\{U_i \to U\}$ and every matching family $\{s_i\}$ , there exists a unique section $s \in F(U)$ such that $s|_{U_i} = s_i$ for all $i$ .

The unique $s$ is called the gluing of the family $\{s_i\}$ .

Obstruction

If $\{s_i\}$ is not a matching family (some $s_i|_{U_i \times_U U_j} \neq s_j|_{U_i \times_U U_j}$ ), we say there is an obstruction to gluing. Define:

\mathrm{Obs}(\{s_i\}) := \{(i, j) \mid s_i|_{U_i \times_U U_j} \neq s_j|_{U_i \times_U U_j}\}

This is the set of disagreeing pairs.

K.7.2 Theorem Statement

Theorem(Obstruction Localization)

Let $F$ be a presheaf on a site $(\mathbf{Ctx}, J)$ . Let $\{U_i \to U\}_{i \in I}$ be a covering family and $\{s_i \in F(U_i)\}_{i \in I}$ a collection of local sections.

Either:

$\{s_i\}$ is a matching family, in which case there exists at most one $s \in F(U)$ with $s|_{U_i} = s_i$ for all $i$ , or
$\{s_i\}$ is not a matching family, in which case $\mathrm{Obs}(\{s_i\}) \neq \emptyset$ , and this set exactly identifies the pairs $(i, j)$ where the obstruction occurs.

Moreover, if $F$ is a sheaf, case (1) guarantees existence and uniqueness of the gluing.

K.7.3 Proof

Proof

We prove each part.

Part 1: Matching implies at-most-one gluing.

Suppose $\{s_i\}$ is a matching family and $s, s' \in F(U)$ both satisfy $s|_{U_i} = s_i$ and $s'|_{U_i} = s_i$ for all $i$ .

Consider the equalizer diagram:

F(U) \xrightarrow{e} \prod_{i \in I} F(U_i) \xrightarrow[\rho_2]{\rho_1} \prod_{i,j \in I} F(U_i \times_U U_j)

where $e(s) = (s|_{U_i})_{i \in I}$ , and $\rho_1, \rho_2$ are the restriction maps to overlaps.

By assumption, $e(s) = e(s') = (s_i)_{i \in I}$ .

The map $e$ is injective for separated presheaves (and hence for sheaves). This separation property is precisely what distinguishes separated presheaves from arbitrary presheaves; for a sheaf, it holds by definition. Since we are proving uniqueness for sheaves, separation applies, and therefore $s = s'$ .

Part 2: Non-matching implies nonempty obstruction set.

Suppose $\{s_i\}$ is not a matching family. Then by definition, there exist $i, j$ such that $s_i|_{U_i \times_U U_j} \neq s_j|_{U_i \times_U U_j}$ . Hence $(i, j) \in \mathrm{Obs}(\{s_i\})$ , so $\mathrm{Obs}(\{s_i\}) \neq \emptyset$ .

Part 3: Obstruction set exactly identifies disagreements.

By construction, $(i, j) \in \mathrm{Obs}(\{s_i\})$ if and only if $s_i|_{U_i \times_U U_j} \neq s_j|_{U_i \times_U U_j}$ . The set contains no spurious pairs and omits no actual disagreements.

Part 4: Sheaf implies existence.

If $F$ is a sheaf and $\{s_i\}$ is a matching family, the sheaf condition guarantees existence of $s \in F(U)$ with $s|_{U_i} = s_i$ . Combined with Part 1, the gluing is unique.

∎

K.7.4 Operational Consequence

The Obstruction Localization Theorem justifies the ObstructionWitness artifact:

ObstructionWitness {
  cover: [U_i],
  local_sections: {U_i: s_i},
  disagreeing_pairs: Obs({s_i}),
  specific_conflicts: [(i, j, s_i|_{overlap}, s_j|_{overlap})]
}

When a gluing attempt fails, the system does not return a generic "conflict" error. It returns a structured object that names:

Which contexts were involved
What claims each context made
Which pairs disagreed
What the disagreeing values were

This is not a design choice but what the mathematics requires: the obstruction is localized to specific overlaps, and the disagreement is a computable predicate.

This theorem is why the Third Mode can promise auditable failure. The failure is not "something went wrong." It is "contexts $U_i$ and $U_j$ disagree on the overlap $U_i \times_U U_j$ , with these specific values."

The Obstruction Localization theorem and its full proof are also developed in Chapter 11.

← Back to Appendices Back to The Proofs →