The Coherence Topos and Vocabulary Evolution

This appendix examines mathematical resources for the proposed passage from a definition to its certification and reuse. Some constructions are available under stated hypotheses; others still lack the objects or laws required to support their intended conclusions.

Retrieval, schema evolution, knowledge representation and formal verification already provide ways to perform parts of this work. The question here is which guarantees survive their composition. A familiar technique is not inadequate merely because its name omits the rest of the proposed architecture.

Parts I–VI of The Proofs assembled the components: commitment sets (A1), witnessed equivalence (A10), context sites (A12b), the sheaf condition (A13), fibrations (A14), transport discipline (A16), predicate invention (A17), conservative extension (A17b), and the coherence cost model (A21). This appendix distinguishes standard mathematical consequences, finite calculations, proposed institutional interpretations and unfinished constructions. Their combination is a research direction; it is not itself a theorem.

The topos theorem (L.2) is a consequence, not a contribution — it follows from Giraud's theorem applied to the context site. It supplies a setting in which local truth and restriction can be studied. Identifying its internal logic with A4 or A15 requires further choices; constructing the proposed algebra of predicate invention in L.6 requires work not supplied here.

L.1 What This Appendix Claims

The contribution must be assessed result by result.

Standard mathematics (L.2–L.3) supplies sheafification, internal logic and exponentials, conditional on specified sites and sheaves. Their existence does not supply a particular certification procedure.

Finite calculations and an elementary counterexample (L.4.1–L.5) show what disjointness removes from a chosen Čech complex, what the tetrahedron boundary contributes in degree two, and why agreement on one population need not extend to another. These are explanatory applications, not priority claims for new mathematics.

Unfinished constructions (L.4 and L.6) concern an identity-matching classification and a proposed algebra of admissible vocabulary changes. The missing objects and proof obligations are identified where they arise. Neither can support a guarantee elsewhere in the book.

Antecedents, proposed extensions and research questions (L.7–L.8) locate the specification among existing work. A missing construction is an obligation of this proposal, not automatically a significant open problem for the field. The correction record identifies the superseded priority and theorem claims.

Notation

Symbols from Parts I–VI (commitment sets, anchors, etc.) follow the conventions in Appendix H. The following notation is specific to this appendix or used here with specialized meaning. Standard category-theoretic and sheaf-theoretic notation follows Mac Lane & Moerdijk¹.

Symbol	Meaning	Introduced
$(\mathbf{Ctx}, J)$	Context site: category $\mathbf{Ctx}$ with Grothendieck topology $J$	A12b
$\mathbf{PSh}(\mathbf{Ctx})$	Presheaf category $[\mathbf{Ctx}^{\mathrm{op}}, \mathbf{Set}]$	L.2
$\mathbf{Sh}(\mathbf{Ctx}, J)$	Sheaf category (the coherence topos)	L.2
$\Omega$	Subobject classifier; $\Omega(U)$ = $J$-closed sieves on $U$	L.2
$a$	Sheafification: left exact left adjoint to inclusion $i : \mathbf{Sh} \hookrightarrow \mathbf{PSh}$	L.2
$\mathcal{W}^{\mathcal{P}}$	Exponential sheaf: space of natural assignments from proposals to witnesses	L.3
$\check{C}^n(\mathcal{U}, F)$	Čech $n$-cochains of presheaf $F$ with respect to cover $\mathcal{U}$	L.4
$\check{H}^n(\mathcal{U}, F)$	Čech $n$-th cohomology group	L.4
$\delta^n$	Čech coboundary map $\check{C}^n \to \check{C}^{n+1}$	L.4
$C_i \times_U C_j$	Overlap (fiber product) of $C_i$ and $C_j$ over $U$	L.4.1
$\mathbf{Sig}$	Category of signatures with inclusion morphisms	L.5
$\Sigma, \Sigma'$	Signatures (finite sets of typed predicate/function symbols)	A17
$P$	Proposed collection of extensions, not an established endofunctor: $P(\Sigma)$ = single-predicate extension proposals	L.6.1
$P^*$	Proposed sequence construction; free-monad status unestablished	L.6.1
$\mathcal{I}$	Proposed admissibility quotient; monad status unestablished	L.6.2
$\pi : P^* \twoheadrightarrow \mathcal{I}$	Intended quotient map; monad-morphism claim withdrawn	L.6.2
$\eta, \mu$	Unit and multiplication a completed monad would require	L.6.2
$\mathbf{Sig}_{\mathcal{I}}$	Intended Kleisli category; not yet constructed	L.6.2
$\ker \pi$	Intended quotient relation, not an established cost invariant	L.6.3

L.2 The Coherence Topos

Throughout this appendix, $(\mathbf{Ctx}, J)$ is the context site from A12b and $\mathbf{Ctx}$ is assumed essentially small.

The Subobject Classifier and Epistemic Status

This gives a precise structure of local truth. It does not identify A4’s three derivability statuses under its consistency assumption. A proper nonempty truth value can record where a claim holds without recording a conflict, missing evidence or an official's uncertainty. Those interpretations require a model of the claims and their evidence.

A Boolean topos has complemented truth values; it need not have only two of them. On a discrete two-point space, the sheaf topos is $\mathbf{Set}\times\mathbf{Set}$ and the whole space has four open-set truth values. The two proper singletons are complements. A claim holding in one region and its negation in the other is not an internal contradiction: their conjunction is bottom.

A15's choice of reasoning rules and A4's evidentiary statuses require their own interpretation. Booleanness, two-valuedness and a closed-world policy are different properties. The former equivalence among them is withdrawn; its decisive counterexample and correction are recorded below. The standard internal logic remains available under its actual hypotheses.

L.3 Exponentials and Certification

The topos has exponentials. Suppose the proposals of A19 and witnesses of A2c have been represented by sheaves $\mathcal{P}$ and $\mathcal{W}$. In the following slice notation, $U$ denotes the sheafification of the representable context:

A global section $c \in \Gamma(\mathcal{W}^{\mathcal{P}})$ is a total natural assignment $\mathcal{P} \Rightarrow \mathcal{W}$. This is not yet A19b: its successful, violated and incomplete outcomes, applicable contexts and relation between a witness and its claim have not been represented. The exponential exists under the stated sheaf hypotheses, but it need not have a global section. A section, if supplied, would still need a validity interpretation and an effective procedure before it could serve as a certifier. Naturality states how the assignment commutes with restriction; it establishes neither the truth of a supplied observation nor authorization of its use.

L.4 Matching and Its Mathematical Representation

Three merchants can supply identifiers without supplying a unique account of which products they share. The following lists leave that matching problem underdetermined. To classify its possible answers, we would have to specify both the matchings and the transformations under which two answers count as the same.

The Setup: Three-Merchant Catalog

Let three merchant contexts $A,B,C$ cover a catalog context $U$. Their local product identifiers are:

• $F(A)=\{a_1,a_2,a_3\}$
• $F(B)=\{b_1,b_2,b_3\}$
• $F(C)=\{c_1,c_2\}$.

Suppose $a_3$ is identified with $c_1$, while $a_2$ might match either $b_1$ or $b_2$. Suppose also that $B$ and $C$ have no shared context. The overlap diagram has the path $B-A-C$ as its nerve. That shape does not settle which product $a_2$ names.

These data describe possible matchings, not a complete presheaf: the overlap values and all restriction maps have not been specified. A set-valued presheaf, once supplied, has a set of matching families defined by equality of restrictions. A unique glued section follows for a matching family when the presheaf is a sheaf. It does not follow merely because the identifiers can be listed.

The Čech Complex

For abelian coefficients, Čech cochains and differentials form a complex of groups. The sets of product identifiers above do not carry that structure. Non-abelian $H^1$ also requires more than sets: for example, a sheaf of groups and its torsors, or a fully specified descent groupoid. The overlap diagram and the phrase “witnessed identification” do not supply the objects, arrows and allowed equivalences of such a groupoid.

Free abelianization would introduce an abelian presheaf only after the missing restrictions were supplied. Relating its cohomology to catalog matchings would then require a comparison theorem. The choice of coefficients cannot be justified merely by the availability of a familiar calculation.

Global sections and the descent obstruction

The allowed equivalences determine what the classification would count. If they permit swapping $b_1$ and $b_2$ while preserving everything else specified, the choices $a_2\leftrightarrow b_1$ and $a_2\leftrightarrow b_2$ represent the same class. Product attributes might distinguish them, but the model would have to carry those attributes and require its equivalences to preserve them. Different printed identifiers alone cannot do that work.

The merchant classification remains unconstructed: it supplies no computed $H^1$, catalog count or general identity-resolution guarantee. Its missing descent objects, restrictions and equivalences are not supplied by Appendix K's separate finite overlap examples. The correction record retains the former classification claim and the failed relabeling argument.

L.4.1 Acyclicity of Hierarchical Sites

Disjoint sibling contexts permit a simple calculation. It is useful precisely because it shows which comparisons the representation has removed.

The zero value on the empty context is essential. An arbitrary presheaf need not have it. For two disjoint children, assigning zero to the nonempty contexts and $\mathbb Z/2$ to the empty one gives the distinct-index complex $0\to\mathbb Z/2\to0$, whose first cohomology is nonzero. The result concerns this generating cover and coefficient condition; extension to arbitrary covers or derived sheaf cohomology needs further hypotheses. The correction record preserves the overbroad claim and failed extension.

Within the stated disjoint cover there are no cross-sibling comparisons. That fact does not establish unique identity resolution throughout an organization, especially when the identity-classification construction above remains unfinished. Shared services, aliases or duplicated entities can make a nominal tree an inadequate representation of the work. Naming those shared contexts changes the diagram and the questions it can ask. The calculation identifies the consequence of omitting them; it proves no general cost advantage for hierarchy.

L.4.2 Higher Obstructions in Federated Sites

A different finite calculation retains all pairwise and triple intersections of four contexts but removes their common fourfold intersection. Its interest is what a hole in that particular complex permits, not a classification of federations by their number of members.

This is the standard cochain calculation for $S^2$ with $\mathbb Z/2$ coefficients. It establishes a fact about the displayed complex. It does not, without a comparison theorem and its hypotheses, identify derived sheaf cohomology for every site with a similar picture.

The coefficient convention is consequential. A strictly constant presheaf would also give $F(\emptyset)=\mathbb Z/2$. The resulting degree-three term and differential would fill the tetrahedron, eliminating this degree-two class. An absent common context must not be silently assigned whichever coefficient makes the desired obstruction appear.

Pairwise data satisfying all triple cocycle equations are 1-cocycles; here $\check H^1=0$, so they come from vertex data. Nonzero $\check H^2$ says that prescribed triple data need not come from one assignment of pairwise data. The degree determines which attempted reconstruction can fail.

A model of regulators or computational agents would have to say what those triple and pairwise data represent, why addition modulo two expresses their relation, and which actual agreements supply the coefficients. No such institutional data are calculated here. The arithmetic establishes the relation in the displayed complex; its institutional identification remains to be made. The correction record identifies the superseded interpretation.

L.4.3 What the Calculations Distinguish

The examples establish different amounts. The shape of a nerve and the choice of coefficients both affect a cohomology calculation; that familiar mathematical distinction is not a new classification of institutional power.

Material	Specified object	Established result	Interpretation still required
Merchant matching, L.4	Identifier lists and possible identifications	An underdetermined matching problem; no constructed $H^1$ classification	Complete descent objects, restrictions and allowed equivalences
Disjoint cover, L.4.1	Alternating Čech complex with $F(\emptyset)=0$	No positive-degree cochains	Whether a real hierarchy has the stipulated disjoint contexts
Tetrahedron boundary, L.4.2	Displayed $\mathbb Z/2$ complex	$\check H^1=0$, $\check H^2=\mathbb Z/2$	Meaning and evidence for its vertex, edge and face assignments
Filled triangle	Constant coefficients on the filled simplex	Positive cohomology vanishes	No general institutional guarantee follows

A complete graph records pairwise adjacency; it does not by itself supply all higher intersections or make every coefficient system acyclic. An architect must represent the relations that actually require checking before using such a calculation to choose a repair. The correction record preserves the withdrawn institutional classification.

L.5 Vocabulary Evolution: Composability and Its Limits

The chain preserves exactly the old-language consequences under these fixed hypotheses. Query behavior, evidence versions and authority to admit the extensions remain separate obligations; they do not compose merely because deductive conservativity does.

A finite agreement check concerns a population as well as a definition. At that fixed population, applying the same Boolean combination to pointwise-agreeing predicate values preserves their agreement. Adding an item asks the definitions to agree somewhere the earlier check did not examine. The following example keeps both definitions unchanged so that the additional demand is visible.

L.6 The Predicate Invention Monad

A monadic account of predicate invention is an unfinished construction. No endofunctor, free monad or admissibility quotient satisfying the proposed laws has been supplied. The present requirements below identify the missing work; the correction record preserves the former assertions and their failures.

L.6.1 The Proposal Endofunctor

At a signature $\Sigma$, the proposed collection

lists single-predicate extensions with a sort, arity and context-local definition. It is not itself an object of $\mathbf{Sig}$ as defined in L.5. A functor would require a chosen category and a total, composition-preserving action on its arrows. Renaming or extending a signature must specify what happens to every proposal, including collisions with a symbol already present.

The objects would also need to carry the information relevant to admission: definitions, invariants, logic, authority and the population against which extensional agreement is checked. Two proposals with the same symbol names can have different admissibility outcomes. Forgetting those differences before defining composition would remove the very work the proposed algebra is meant to explain.

L.6.2 The Admissibility Quotient

A completed construction must distinguish composing proposal descriptions from checking their admissibility. L.5 establishes composition of conservative extensions under fixed hypotheses. It does not establish that a finite agreement check remains adequate after the checked population changes.

To define the proposed quotient monad requires a total functor, natural unit and multiplication, a precise equivalence compatible with multiplication, and the unit and associativity laws. Failed proposals and changing populations must be represented in those definitions. Only then can a Kleisli category or a characterization of its algebras do further work. Neither is available here as a theorem.

L.6.3 The Algebraic Content of the Quotient

Independent proposals can be made in different orders and leave the same union of symbols. That elementary observation identifies something a representation might forget. Definitions, authorities, evidence and checked populations can still distinguish paths leaving the same names. A design that identifies those paths must establish why its subsequent operations no longer need the differences.

The cost framework requires no such quotient. A21 accounts for a declared procedure, including work saved by reuse and work required by changed grounds. Completing an algebra would not by itself price an implementation; leaving this algebra unfinished does not prevent a recipient from identifying the premise its conclusion consumed.

L.7 Relation to Existing Frameworks

The relevant antecedents already make substantial parts of the inquiry precise. Their constructions help identify what this proposal can use and what it still needs to supply. The superseded comparison is recorded below.

L.7.1 Spivak's Functorial Data Migration

Spivak models a database instance as a functor $I:\mathbf C\to\mathbf{Set}$ and a schema mapping as a functor $F:\mathbf C\to\mathbf D$. Precomposition gives the pullback, or inverse-image, functor $\Delta_F$; left and right Kan extensions give its adjoints⁴:

Precomposition does not fail to exist in this setting. The instance categories are themselves toposes, as the paper explicitly establishes; being Set-valued does not deprive them of internal logic or a subobject classifier. A schema mapping can also involve a newly extended schema. It is therefore incorrect to distinguish this proposal by claiming that Spivak's framework cannot represent schema growth or local truth.

The additional design question here concerns the grounds for accepting a proposed mapping or definition, the evidence that accompanies it and the work required when its domain changes. A17 and A21 specify obligations and accounting categories for that purpose. L.4 supplies no general cohomological classification of migration failures, and L.6 supplies no completed Kleisli construction extending Spivak's functors. Those proposed connections cannot yet do comparative work as established results.

L.7.2 Goguen's Sheaf Semantics

Goguen's sheaf semantics for concurrent interacting objects is a substantive antecedent for composing local states through shared context⁵. The sheaf condition was already doing that explanatory work; it is not a discovery of this appendix.

The present proposal asks how admission, evidence, versioning and budgets might be specified together when definitions change. Its extensional-population example makes one maintenance obligation explicit. That example does not establish the absence of analogous reasoning in Goguen's framework, and the unconstructed identity classification and monad cannot support a claim of mathematical extension.

L.7.3 Abramsky's Sheaf-Theoretic Contextuality

Abramsky and Brandenburger formulate non-locality and contextuality through compatibility and global sections⁶. Their empirical models have specified measurement contexts and outcome data. The obstruction concerns those structures, not an arbitrary disagreement between institutions.

The separate cohomology treatment by Abramsky, Mansfield and Barbosa uses a particular obstruction class associated with a supported section. Non-vanishing supplies a sufficient obstruction to extending that section; vanishing need not supply an extension. The stronger contextuality conclusion requires the appropriate obstruction for every supported section. The earlier claim that $H^1\neq0$ by itself implies strong contextuality was false. See The Cohomology of Non-Locality and Contextuality, 2012 version, Proposition 4.3 and its discussion⁷.

L.4's merchant data have not been given a corresponding coefficient construction. L.4.2 retains a standard finite complex, not a demonstrated translation of contextuality theory into regulatory coordination. The useful antecedent is a discipline of specifying the data and the obstruction together.

L.7.4 Caramello's Toposes as Bridges

Caramello develops transfers between theories through their classifying toposes⁸. Equivalent classifying toposes can connect theories presented differently; the interpretation of the transferred result depends on those presentations.

A specified context site has a sheaf topos that can be studied in this way. Identifying a geometric theory with the intended operations of vocabulary evolution is a further task. The standard existence of a classifying presentation does not complete the missing invention construction or establish an institutional equivalence.

L.7.5 Institution Theory

Goguen and Burstall's institutions provide signatures, sentences, models and a satisfaction condition governing change of signature⁹. This already makes vocabulary translation an object of formal study. It is a serious foundation for the preservation questions in A17b, rather than a framework disqualified because its abstract definition does not price an operation.

The proposed admission procedure must still choose which extensions to accept, what witnesses establish their obligations and how changed populations affect reuse. These are additional specification questions. They are not proof that institution theory lacks the resources to express the relations, or that an invention monad has now answered them.

L.7.6 Capabilities Comparison

Work needed	Established resource	Status of this appendix's further claim
Data migration and local truth	Functor categories, Kan extensions and sheaf semantics	A17's admission and evidence requirements remain a proposed discipline
Contextual obstruction	Specified global-section problems and scoped cohomology constructions	Merchant identity classification not constructed
Vocabulary translation	Signature morphisms and satisfaction conditions	Invention monad and quotient laws not established
Continued extensional agreement	Checks on a declared population	L.5 gives a finite counterexample to unrestricted reuse
Verification expenditure	A declared procedure and its cost estimates	A21 supplies accounting categories, not a universal ordering
Graded agreement	Requires a specified enriched model	Problem 8 remains open

The contribution currently available is a connected specification of proposals, checks, witnesses, scopes, versions and budgets, with standard mathematics and finite examples clarifying parts of it. Whether that composition yields a new formal result must be decided by an actual construction and proof. The earlier priority and superiority claims did not provide them.

L.8 Construction Obligations and Research Questions

The following research questions include construction obligations as well as possible extensions. Their connection to an application does not establish tractability or supply a missing mathematical object.

Problem 1: Classify the geometric theory of the coherence topos. Every Grothendieck topos classifies a geometric theory $\mathbb{T}$ such that models of $\mathbb{T}$ in any topos $\mathcal{E}$ correspond to geometric morphisms $\mathcal{E} \to \mathbf{Sh}(\mathbf{Ctx}, J)$. What is $\mathbb{T}$ for the coherence topos? Interpreting such a presentation as a theory of vocabulary evolution requires additional work relating its models to the intended operations. Connection: Caramello's "bridge" program¹⁰.

Problem 2: Cohomology of specified context sites. L.4.1 establishes vanishing for the stated disjoint generating cover and coefficients zero on the empty context. L.4.2 computes the tetrahedron-boundary complex. Neither proves a general institutional classification. Further work must specify the site, covering families and coefficients, then establish the hypotheses for any comparison of cover-level Čech and derived cohomology. A graph of pairwise overlaps does not determine the higher intersections. Relating any resulting invariant to the cost of maintaining an actual institution requires evidence beyond the cohomology calculation.

Problem 3: Extend to $(\infty,1)$-toposes. Witnesses (A10) carry structure: kinds, composition, coherence conditions. The correct categorical home may be an $(\infty,1)$-topos where witnesses are 1-morphisms and witness-equivalences are 2-morphisms. Does the coherence topos extend to an $\infty$-topos? Does the resulting type theory validate a scoped univalence axiom? Connection: Lurie¹¹, Shulman.

Problem 4: Morita equivalence of context sites. When do two context sites $(\mathbf{Ctx}_1, J_1)$ and $(\mathbf{Ctx}_2, J_2)$ produce equivalent sheaf categories? Such an equivalence compares sheaf categories; relating it to two institutions also requires compatible interpretations of their claims, evidence and operations. An organizational comparison would depend on those additional interpretations.

Problem 5: Decidable admission fragments. Which specified fragments permit effective checks of A17's grounding, overlap and conservativity obligations? Appendix K.1.1 distinguishes those obligations from satisfiability tests and proof checking. A result must state its language, permitted extensions, finite or effective data and success conditions. An unanswered search is not a negative decision. This question can be investigated independently of the monad proposal.

Problem 6: Construct an algebra of admissible evolution. Before an Eilenberg–Moore category of $\mathcal I$ can be characterized, L.6 needs objects carrying the relevant definitions and state, a total functor and a proved admissibility-compatible multiplication. If a monad is obtained, its algebras and any free or reflective constructions become further questions. L.6 supplies no monad premise for them; the correction record identifies the withdrawn theorem. Standard monad and algebra requirements apply¹².

Problem 7: Persistent cohomology of evolving context sites. As vocabulary evolves (new predicates are added, overlaps change), the context site $(\mathbf{Ctx}, J)$ changes and its cohomology groups evolve. Does the sequence $\{H^n_t\}_{t \geq 0}$ of cohomology groups over time form a persistence module in the sense of topological data analysis? If so, the persistence diagram would classify the lifetime of obstructions: some ambiguities are transient (resolved by adding a predicate that disambiguates), others are persistent (structural, arising from the federation topology). The transition maps and their direction must first be supplied: a sequence of groups alone is not a persistence module. A barcode would then describe that specified construction; no novelty or operational classification is established here.

Problem 8: Enriched coherence and graded agreement. The exact sheaf condition uses equality of restrictions. Probabilistic estimates and attestations can be represented as ordinary data, but equality of their records does not prove agreement of the claims to a tolerance. Approximate pairwise agreement need not have the transitivity or gluing properties of exact equality. Appendix I's tolerance-based options therefore do not inherit K.2's exact gluing guarantee.

An enriched account would have to specify the value category, restrictions, notion of matching and the guarantee for a resulting section. A possible graded obstruction must be defined in that model; the required exact baseline and its relation to the graded construction must also be supplied. K.7 distinguishes pairwise disagreement for a presheaf, uniqueness under separation and existence under the sheaf condition. Which of those statements has an appropriate graded counterpart remains open. Until supplied, the exact-fragment proofs do not validate the probabilistic or attested-witness layer merely because the same names are used. Relevant resources include Lawvere¹³ and Kelly¹⁴.

L.9 Connection to Agentic Systems

This section connects the mathematical framework to a concrete open problem in multi-agent AI: coherent vocabulary evolution in distributed computational agents.

Suppose one agent proposes sustainable(product) and another proposes eco_friendly(product). A third operation receives both. It needs to know whether the predicates express the same requirement, whether their evidence supports the intended use, or whether it should preserve them separately. This constructed example makes no claim that existing multi-agent systems uniformly lack those resources.

The specification separates several tasks that an answer would have to perform:

• Predicate admission (A17, L.5): proposals carry obligations. Conservative extensions compose under the fixed hypotheses stated in L.5; extensional agreement is evidence about a declared population. L.6 supplies no additional monad guarantee. A system extending a population must establish its enlarged assertion by an adequate update procedure, not treat the old certificate as evidence of checks never performed.

• Obstruction models (L.4): the finite complexes show how specified intersections and coefficients affect a calculation. They do not count the ambiguities of arbitrary agent identity claims or prove that hierarchical organizations escape them. The mathematical object and its interpretation must be supplied together.

• Scoped transport (A16, K.3): transport preserves the property for which the equivalence actually supplies a map, within its declared scope. L.3 provides an exponential when proposals and witnesses have been represented as sheaves; it does not construct the needed certificate.

• Cost accounting (A21, K.4): a budget declares what checking the system will purchase and what it will do when that budget binds. Refinement alone orders neither checks nor expenditure. A less costly procedure must still meet the obligations on which its result will be used.

• Coordination without shared objectives. Agents need not share every purpose to agree on specified overlaps. They do need compatible representations, valid restriction maps and adequate evidence for the comparisons on which composition depends. Exact gluing is a conditional mathematical result; choosing and enforcing its institutional conditions is further work.

  The enforcement layer lies outside The Proofs. The conservative extension condition (A17b) is a mathematical specification. Volume II examines productive work, complementary resources and control; Volume III, Chapter 7, examines evidence, independent verification and effective contest. A bond can support responsibility in some arrangements, but neither energy expenditure nor a receipt alone establishes legitimate authority or effective standing.

• Relation to antecedents (L.7): data migration, sheaf semantics and institution theory already explain substantial parts of this work. The proposed lifecycle specification joins these resources to evidence and budget requirements. Its unfinished constructions cannot yet support a claim to subsume those frameworks.

The target remains a substrate in which agents can propose, certify, transport and revise predicates without allowing one operation to manufacture the warrant of another. The defined obligations and exact-fragment results make part of that target inspectable. The remaining construction and implementation work must establish the rest; the terminology does not perform it.

Correction Record

The following status changes were established in the 11 September 2026 publication candidate. The 13 September 2026 reading revision consolidates repeated accounts here; it does not erase or replace the earlier findings. Prior source and review records remain unchanged. In particular, the merchant construction's “linear shadow” was not established by free abelianization, and the attempted extension of the hierarchy result invoked a spectral sequence without supplying the necessary comparison hypotheses. The withdrawn general table of hierarchies, peer networks and federations inherited those unsupported guarantees.

The current account retains the valid mathematics and states the missing constructions. The preserved source and review record is publication/corrections/2026-09-11-proof-evidence/; the full prior text remains in the edition history. This table records the decisive reasons, not new theorem claims.

Superseded claim	Decisive reason and surviving work
Logic selection identified with topos relativization	Booleanness does not imply two-valuedness or a closed-world policy. The discrete two-point example has four global truth values. L.2 retains standard internal logic and requires a separate interpretation of evidentiary status.
Merchant ambiguity classified by the displayed $H^1$	The presheaf, coefficients or descent groupoid were not constructed. The proposed relabeling quotient did not distinguish the two advertised matches: swapping $b_1$ and $b_2$ identifies them. L.4 retains the unresolved identity problem.
Acyclicity for every presheaf and hierarchical cover	The omitted hypothesis $F(\emptyset)=0$ is essential. For two disjoint children with zero nonempty values and $F(\emptyset)=\mathbb Z/2$, the positive cochain need not vanish. L.4.1 retains only the stated generating-cover calculation.
Tetrahedron computation established failure of compatible pairwise regulatory agreements	Here $\check H^1=0$; the nonzero class is in degree two. No institutional assignments or comparison theorem were supplied. L.4.2 retains the standard finite calculation and its coefficient convention.
Invention endofunctor, free monad and admissibility quotient	The proposed object assignment was not an endofunctor on the specified signature category. The attempted coproduct repair discarded source summands on a collision without defining a total arrow action. Two incompatible quotient relations were used and no compatible multiplication or laws were proved. L.6 states the requirements of a construction still to be supplied.
Novelty or superiority established by a table of missing capabilities	The cited antecedents already supply substantive migration, logical and contextual resources. Their absence was not established. L.7 grants those contributions and locates the additional specification questions.

None of these status changes supplies a new guarantee for probabilistic or approximate gluing. Problem 8's operative limitation remains beside the results it governs. A21's distinct correction and its consequences are recorded in Chapter 19 and the Codex correction notice.