Mathematical Foundations

Appendix K

20 min read

Text size

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 proposed discipline joins familiar mathematics to explicit design obligations. Those obligations require their own implementation evidence.

The Borrowed Machinery

The main sources of the established guarantees are existing mathematics. The cost framework is a separate proposal; Appendix L distinguishes further finite calculations from unfinished constructions:

Guarantee	Underlying Theorem	Canonical Source
Preservation of old-language consequences	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 expenditures	A21 cost categories and declared checking schedules	Chapter 19; no general monotonicity theorem

The proposed specification draws on that infrastructure. Existing systems already supply proofs, provenance, contracts and structured failures in various settings; this companion brings their obligations into one account of admission and subsequent use. Its interfaces require implementation evidence, and its unfinished constructions cannot borrow guarantees from the established results beside them.

What This Appendix Provides

For each result used by a later construction, 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: Under the stated model-expansion hypothesis, adding the predicate creates no new old-language theorems.

Theorem(Conservative Extension)

Let $(\Sigma,I)$ and $(\Sigma',I')$ be classical first-order theories, with $\Sigma'=\Sigma\cup\{q\}$ and $I\subseteq I'$ , using a sound and complete proof system. Suppose every model of $I$ has a $\Sigma'$ -expansion satisfying $I'$ . Then the extension is deductively conservative:

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')$ . The expansion hypothesis supplies an interpretation of $q$ satisfying the new constraints while leaving the old structure unchanged. Freshness of the symbol alone does not supply that interpretation.
Conservativity: Suppose $(\Sigma', I', L) \vdash \varphi$ for a $\Sigma$ -sentence $\varphi$ . By soundness, $\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 admission claims to preserve the old theory, A17/A29 require the corresponding conservativity argument. A separately authorized revision must identify what it changes. A verified old-language consequence of the new theory that fails in a model of the old theory refutes deductive conservativity. A model that cannot be expanded refutes the stronger expansion condition used above; by itself it is not that sentence-level counterexample. An inconclusive check establishes neither failure nor safety.

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

Method	What it can establish	Boundary
Syntactic sufficient condition	Conservativity for a proved class, such as explicit definitions with the required freshness conditions	A formula outside that class need not be non-conservative
SAT/SMT encoding	The obligation actually encoded, in a supported fragment	Solver success on a different satisfiability question is not a conservativity proof
Model sampling	A checked counterexample, when the relevant old-language consequence is supplied	Failure to find one is not a general guarantee
Proof assistant	The formalized proposition under its declared hypotheses and axioms	Proof checking is not a complete procedure for discovering a proof; goals may remain unfinished

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: An inconsistent subset returned for a declared encoding, such as new assumptions together with the negation of a proposed consequence. Minimality requires a separate check; an unsatisfiable core alone does not establish non-conservativity.
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

The complexity belongs to the encoded obligation. In a finite propositional language, the model-expansion test asks whether every old valuation satisfying $I(p)$ admits new values $q$ satisfying $I'(p,q)$ :

\forall p\,\bigl(I(p)\Rightarrow\exists q\,I'(p,q)\bigr).

This is not the single satisfiability test whose complexity the earlier table reported. Equality and linear-arithmetic encodings likewise require the actual projection or consequence conditions; union-find or linear programming does not solve every conservativity problem bearing those labels. The former generic complexity table and claim of a semi-decision procedure for arbitrary first-order conservativity are withdrawn. A tractable fragment must name its permitted formulas and the test being implemented.

The Coherence Budget and an Inconclusive Check

A21 limits how much checking the implementation undertakes. It does not convert an approximate result or timeout into a proof. A syntactic sufficient condition can establish safety when its hypotheses hold; a heuristic screen can guide investigation without certifying the extension.

Expensive verification may be deferred, but a pending proposal must not acquire certified standing merely because it has entered a queue. Risk-tiered policies can select stronger checks or decline a use. Each outcome must retain the attempted obligation, method, budget and result, including an explicit unknown. The budget governs the work purchased; it cannot enlarge what that work established.

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 amalgamates this family. The failure is localized to the specific overlap(s) where disagreement occurs.

∎

Operational consequence: An implementation of glue needs effective maps, comparison procedures and a construction for the specified sheaf. It can then return the amalgamation or established unequal restrictions. If checking remains incomplete, it must say so. The abstract existence theorem does not supply a terminating algorithm for every sheaf.

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.

Suppose the supplied transport includes a validated proof map $\tau_{e,U}:P(A)\to P(B)$ in the declared logical interpretation. If $P(A)$ holds with proof $\pi$ in context $U$ , then $P(B)$ holds with proof $\tau_{e,U}(\pi)$ there.

The proposed interface rejects use of this certificate outside S. That rule does not prove that another certificate or independently defined transport is impossible there.

Proof

Proof sketch:

Applying the validated map $\tau_{e,U}$ to $\pi$ gives a proof of $P(B)$ . Statistical or attested support requires its own interpretation and cannot acquire this proof guarantee merely by being called a witness.

∎

Operational consequence: The proposed transport operation checks the certificate, scope, property footprint and required maps. Established use outside the certificate’s scope produces ScopeViolation; an unfinished scope check produces Inconclusive. Neither certifies the requested substitution. Its receipt binds those inputs and the resulting claim. Whether a recipient can validate it depends on the evidence and checking procedure supplied; the receipt’s existence is not its own verification.

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 Costs and the Withdrawn Ordering

Corrected claim: Cover refinement alone does not order verification costs.

The former monotonicity theorem used the number of nonempty overlaps between distinct cover members as its cost. On the discrete space $U=\{a,b,c\}$ , the cover $\{\{a,b\},\{b,c\}\}$ has one such overlap. Its singleton refinement $\{\{a\},\{b\},\{c\}\}$ has none. The asserted inequality is false even under that unit-cost convention.

The proof's proposed injection from coarse overlap checks to fine overlap checks does not exist in this example. A refinement requires each fine member to factor through a coarse member; it does not require every old comparison to survive as a distinct new comparison. The theorem, its equality claim and the inference that refinement necessarily increases verification cost are withdrawn.

Operational consequence: A21 remains a framework for declaring compile-time, run-time and organizational expenditures, the checks to be performed, and the actions available when a budget binds. Comparisons must specify the information and obligations retained, checking frequencies and per-check costs. Keeping an old checking schedule and adding nonnegative charges cannot reduce its sum; replacing that schedule is a different question, which refinement alone does not settle.

Anchor: A21 (Coherence Cost Model). Chapter 19 develops the counterexample and the surviving budget framework. The correction history is recorded outside the narrative in the edition's correction record.

K.5 What These Results Guarantee

The preceding sections distinguish conditional mathematical guarantees from the cost accounting needed to choose a checking regime:

Result	Guarantee
Conservative Extension Safety	The stated extension creates no new old-language theorems
Gluing Correctness	Exact matching in the specified sheaf gives a unique amalgamation
Scoped Transport Safety	Validated transport carries the declared evidence within its scope
Coherence Cost Model (A21)	Declares expenditures and budgets; no universal cost ordering

What they do NOT guarantee:

Completeness: The Third Mode does not guarantee that every true statement can be proved. A particular implementation must establish the admission conditions it claims to enforce.
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 Cost Model	Declared work, checking schedule and cost estimates; refinement alone is insufficient

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 proposed contribution is to connect these results to operational obligations: which artifact establishes which claim, and what a recipient can do when the required check fails or remains incomplete. Specifying that connection is not evidence that it has been implemented.

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

The following definitions locate pairwise disagreement in a specified presheaf. The result separates that failure from uniqueness under separation and existence under the sheaf condition.

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 (the local data supplied by the model).
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)$ with the pullbacks used below. 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. If $F$ is separated for this cover, there exists at most one $s\in F(U)$ restricting to all $s_i$ . For an arbitrary presheaf, matching alone gives neither existence nor uniqueness, 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: Separation 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 restriction 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. Under the stated separation hypothesis, injectivity gives $s=s'$ . Without that hypothesis this step is unavailable.

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 the supplied sections disagree on an overlap, this specification calls for more than 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

For a finite cover with effective restriction maps and decidable equality, these disagreeing pairs can be computed. Returning them in this format is a design obligation motivated by the calculation. Abstract sheaf theory alone supplies no termination bound, and a non-sheaf can fail to glue a matching family even when this disagreement set is empty.

The witness substantiates this particular failure: “contexts $U_i$ and $U_j$ disagree on the overlap $U_i\times_U U_j$ , with these specific values.” Other failures—missing information, undecidable comparison or a budget exhausted before checking—need their own status. An empty disagreement list cannot stand in for a successful gluing.

Chapter 11 develops what these distinct outcomes permit a recipient to report. The complete obstruction-localization statement and proof are given here; its gluing-correctness proof remains in Chapter 11 and §K.2.

K.8 What the Machine Checks

A checked declaration establishes its conclusion under its actual hypotheses. It does not verify a chapter, an interpretation of a data source, or the operation of an institution. The definitions, written arguments and proposed interfaces in this companion retain those distinct statuses. Appendix L's H¹ classification and invention monad are not established by the projects below.

The September 11, 2026 audit compiled the unchanged selected source targets with Lean 4.28.0. Mathlib-dependent targets used the recorded revision 8f9d9cff6bd728b17a24e163c9402775d9e6a365. The declaration inventory records imports and hypotheses separately from kernel axioms: #print axioms does not reveal that a theorem assumes its substantive conclusion.

Project and source module	Exact declaration(s)	Checked conclusion and boundary
SCPI, `Torsor`	`filled_simplex_trivial_H1`; `nontrivialCircularCocycle_not_coboundary`	The specified three Z/2 transitions are a coboundary under the filled-triangle equation; the specified circular example is not. These are not arbitrary-site or institutional classifications.
SCPI, `Counterexample`; `AssumptionD`	`no_compatible_global_predicate`; `assumption_D_finite`	The fixed local predicates disagree; pointwise-agreeing predicates on a finite indexed subset cover glue uniquely. The underlying domain need not be finite.
SCPI, `Conservativity`; `Beth`	`conservativity_descent`; `beth_for_sites`	The first obtains its conclusion from `h_local`; the second manipulates proposition-level scaffolding. Compilation supplies no general semantic conservativity or Beth theorem.
SHEAF, `Algorithm`	`algorithm1_correct`	Zero back-edge residuals characterize the given cochain's coboundary status with an already supplied `TreePropagation` satisfying the tree equations. No BFS construction or all-group vanishing is proved.
SHEAF, `Monotonicity`	`h1_dim_nondecreasing_edge_addition`	A numerical inequality under explicit edge/rank-count assumptions. It concerns a different operation from A21's arbitrary cover refinement.
CompositionDoctrine, `RankMonotonicity`; `Characterization`	`rank_column_restriction_le`; `disclosure_characterization`	Rank does not increase on the specified injective column restriction. Numerical uniqueness holds on a `ReducibleDoctrine` with its stipulated reduction and characterization axioms. Application to a concrete semantic system requires that model identification.
CompositionDoctrine, `LocalCertificationSQ`	`csq_query_lower_bound_concrete`	The finite counting inequality follows under the declared nonnegative weights, union-bound and identification assumptions. Correspondence to an empirical query process is separate.
InterpolantEnvelope, `Finite`, `GoldenV02`, `ClaimFlow`, `Generalization`, `AssuranceLinker`	`full_package_safe`; `truncation_preserves_safety`; `no_free_precedent`; `adoption_and_applicability_are_separate_premises`; `capital_conservation`	Finite modeled safety and claim/authority rules. Some conclusions project assumed fields: `capital_conservation` uses the portfolio's `conserved` premise. These do not prove custody, collectibility, capture or enforceability.
AccountabilityDescent, `AuthorityCycle`; `QueryFiber`	`triangle_holonomy_eq_one_of_globalGauge`; `not_queryAnswerable_of_erasureCertificate`	A gauge implies the group identity; identical observations with different answers prevent answerability through those observations alone. Event occurrence and actual institutional authority are not established.

The fresh compilation covered the SCPI and SHEAF roots, the three specified CompositionDoctrine targets, and the InterpolantEnvelope and AccountabilityDescent roots. All seven targets passed. The inspected declarations used no sorryAx or authored kernel axiom; recorded dependencies were the standard propext, Classical.choice and Quot.sound where needed. The whole CompositionDoctrine root was not rebuilt: its unrelated Locality and RealizationSheafPhase2 modules retain two unfinished declarations. They do not enter the selected Characterization, RankMonotonicity or LocalCertificationSQ targets.

Three other evidence boundaries matter to the public research summaries:

Signed incidence: the archived completed source proves CorrespondenceTheorem.signed_incidence_det_in_unit. The accompanying fee_field_independent concludes True; it is a placeholder, not a rank-equality theorem. Field independence follows by the written nonzero-minor argument from total unimodularity. This standalone archived source is not imported by the SHEAF root and was inspected, not freshly compiled in this audit.
Repair-basis count: the corrected product of component sizes is supported by its written argument. No matching machine declaration was located. The checked rank and leverage identities do not count those bases.
Tarski Coherence: the unchanged locked evidence covers TarskiCoherence.QuiverGadget.hodgeTarski_characterization under its self-loop-free quiver and complete-lattice/Galois-connection hypotheses. Its 43-result record is a specified historical scope, not a count of every later helper. That project was not rebuilt in this audit; its existing source and build records are retained.

The accompanying publication correction record preserves the full source/import/declaration map and build results in publication/corrections/2026-09-11-proof-evidence/. Neither successful compilation nor the absence of machine checking decides the validity or importance of a written proof. The boundary is what the result says, what it assumes, and which later claim actually uses it.

← Back to Appendices Back to The Proofs →

Explore Res Agentica

Reading

Mathematical Foundations

The Borrowed Machinery

What This Appendix Provides

K.1 Conservative Extension Safety

K.1.1 Verification Strategies

Modes

Artifacts

Complexity and Limits

The Coherence Budget and an Inconclusive Check

K.2 Gluing Correctness

K.3 Scoped Transport Safety

K.4 Coherence Costs and the Withdrawn Ordering

K.5 What These Results Guarantee

K.6 Formal Dependencies

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

K.7.1 Definitions

K.7.2 Theorem Statement

K.7.3 Proof

K.7.4 Operational Consequence

K.8 What the Machine Checks

Search the book

In this chapter