Glossary

These summaries point to the anchors where the definitions and their hypotheses appear.

A

Adjunction: A pair of functors $F \dashv G$ with a natural bijection $\text{Hom}(F(A), B) \cong \text{Hom}(A, G(B))$. In a specified preorder, can characterize a least or greatest approximation relative to the given map; it does not supply a cost model. See A9.

Anchor: A formal definition that later chapters depend on. The 32 anchors (A1–A32) constitute the book's mathematical spine. See Appendix F.

Attested witness: A witness whose support includes an attestation. Computation can check signatures or provenance; accepting the testimony requires its own grounds. Returns ok_if_trusted(authority) rather than a definitive verdict. See A2c.

C

Category: A collection of objects and morphisms between them, with composition and identity laws. The structural foundation for the book's formal machinery. See Appendix A.

Certification: The proposed process that distinguishes successful certification, demonstrated violation and incomplete checking under a declared scope. Certification follows proposal in the Third Mode pipeline. See A19b.

Coherence: In the exact model, matching local sections have a unique amalgamation when the specified presheaf is a sheaf. An arbitrary collection of records or approximate agreements has no such automatic guarantee. See A13.

Coherence budget: The declared resource or expenditure limit for a specified checking regime, including relevant computational and organizational work. Systems must declare their coherence budgets explicitly. See A21.

Commitment set: A set of propositions that the system has asserted. Consistency requires $C \nvdash \bot$. See A1.

Conservative extension: A theory extension with exactly the same consequences in the old language. The stronger model-expansion criterion is sufficient in classical first-order logic. Instance readability and unchanged query behavior are separate compatibility claims. See A17b.

Context: A view or scope within which truth is assessed. Chosen contexts form a site when their maps and covering families satisfy the required axioms. See A12, A12b.

Cover: A family $\{U_i \to U\}$ that jointly covers $U$ in the sense specified by the Grothendieck topology. See A12.

D

Decidable witness: A witness whose verification is total and deterministic, always returning ok or fail. See A2c.

Dossier: See Predicate package.

E

Equivalence: A relation whose meaning depends on the declared mathematical objects or use. Equivalence of categories has inverse functors up to natural isomorphism. A10 instead records scoped sameness, property transport and its supporting evidence; the shared word does not identify the two constructions.

Epistemic status: A4 distinguishes derivability of a proposition, derivability of its negation and derivability of neither, under its stated consistency assumption. If both are derivable, that assumption fails; a different treatment of conflict requires its own logic. Absence policy is a separate choice. See A4, A15.

F

Fibration: A functor $p: E \to B$ satisfying the lifting property. Captures dependent types: the fiber $E_b$ over $b \in B$ represents types valid in context $b$. See A14.

Functor: A structure-preserving map between categories, sending objects to objects and morphisms to morphisms while respecting composition and identity. See Appendix A, A9.

G

Gluing: The sheaf condition's second requirement: compatible local sections amalgamate to a unique global section. If $s_i \in F(U_i)$ agree on overlaps, there exists unique $s \in F(U)$ restricting to each $s_i$. See A13.

Grothendieck topology: A specification of which families of morphisms count as covers for each object. Defines the site structure on a category. See A12b.

H

Hard invariant: A constraint that must hold; violation triggers rejection. Contrast with soft constraint. See A18.

I

Invariant: A property that survives allowed transformations. Under group action $G \curvearrowright X$, function $f$ is invariant iff $f(g \cdot x) = f(x)$ for all $g$. See A7.

Isomorphism: Invertibility of a morphism in a specified category. Written $A \cong B$. Requires maps $f: A \to B$ and $g: B \to A$ with $g \circ f = \text{id}_A$ and $f \circ g = \text{id}_B$. See A8.

L

Locality: The sheaf condition's first requirement: global sections are determined by their local restrictions. If $s|_{U_i} = t|_{U_i}$ for all $i$ in a cover, then $s = t$. See A13.

Logic selection: The choice of inference rules for a view. Classical logic derives excluded middle generally; intuitionistic logic need not. Different views may operate under different logics. See A15.

M

Matching family: A collection of local sections $\{s_i \in F(U_i)\}$ that agree on overlaps: $s_i|_{U_i \cap U_j} = s_j|_{U_i \cap U_j}$. Every matching family glues uniquely for a sheaf; one successful family does not establish the sheaf condition. See A13.

Morphism: An arrow between objects in a category. Morphisms compose associatively and have identity elements. See Appendix A.

N

N-ary event: An event with multiple participants in distinct roles, whose representation retains event grouping and role bindings. Keyed binary encodings can preserve these too. See A31.

P

Predicate invention: Signature extension $\Sigma \to \Sigma'$ introducing a new predicate with grounding, compatibility and invariant obligations. A13 applies to the exact-gluing case. A requirement of the fuller Third Mode design; fixed-vocabulary reuse need not perform this operation. See A17 and A32.

Predicate package (dossier): A predicate with its full specification: signature, intension, tests, invariants, provenance, scope, execution requirements and version obligations. See A24.

Presheaf: A contravariant functor $F: \mathcal{C}^{\text{op}} \to \mathbf{Set}$ assigning data to each context with restriction maps. A sheaf is a presheaf satisfying locality and gluing. See A13.

Probabilistic witness: A witness for a specified statistical claim under its sampling, model and evaluation assumptions. Completed evaluation retains the appropriate uncertainty; unmet assumptions or unfinished checks can leave it inconclusive. See A2c.

Proposal operator: A function $P$ that takes a query and returns scored candidates. Typically implemented via embedding similarity or retrieval. Produces hypotheses, not certified truths. See A19.

Provenance: The origin and derivation history of a claim. Typed as $\Gamma \vdash \pi : \Pi(p)$, asserting that $\pi$ is evidence for $p$ in context $\Gamma$. See A2.

R

Refusal obligation: An established unsatisfiability result carries its grounds under the declared checking regime. Missing evidence or an exhausted budget receives an incomplete status, not a fabricated counterexample. See A27.

Restriction map: The map $F(f):F(U) \to F(V)$ supplied by a presheaf for an arrow $f:V\to U$. Subset inclusion is one example; the context model must specify its actual maps. See A12.

S

Scope: The declared domain of a predicate or equivalence claim. Downward closure requires that the chosen refinement maps preserve its property footprint and evidence conditions. See A30.

Sense boundary: A context-indexed equivalence relation that partitions terms into senses. Different contexts may draw boundaries differently. See A6.

Sheaf: A presheaf satisfying locality and gluing. The formal model for coherent data: local information glues to global information iff it agrees on overlaps. See A13.

Site: A category equipped with a Grothendieck topology. The structure on which presheaves and sheaves are defined. See A12b.

Soft constraint: A constraint whose violation incurs cost but does not trigger rejection. Contrast with hard invariant. See A18.

Signature: A specification $\Sigma = (T, P, I)$ of types, predicates, and constraints. Adding a predicate is a signature morphism $\Sigma \to \Sigma'$. See A3.

T

Third Mode: The proposed design with four requirements in A32. Appendix I specifies the ten-operation contract, including correction across dependent reuse, whose behavior an implementation must separately demonstrate.

Touchstone: One of 10 recurring test cases (T1–T10) that examine particular failure modes and scoped responses. See Appendix E.

Transport: Moving a property along an equivalence. Given $e: A \simeq B$ and $P: A \to \text{Type}$, transport defines $P': B \to \text{Type}$. Substitution requires transport certificates. See A10, A16.

U

Univalence (full): The HoTT axiom $(A \simeq B) \simeq (A = B)$: equivalent types are equal. In a univalent universe, type equivalences supply identifications along which type families transport. See Appendix D.

Univalence (engineering): The engineering comparison discussed under A16: a witnessed equivalence and the required property evidence can license scoped substitution. Its deployed evaluator must perform the declared checks; the univalence axiom does not certify that execution.

V

Versioning rules: The specified compatibility and migration obligations for a change. Deductive conservativity, preservation of instances and preservation of query results must be distinguished. See A26.

View: A context with its associated local theory $T(U) = (\Sigma, I, L_U)$, including signature, constraints, and logic. See A4, A12.

W

Witness: Evidence for a claim, typed by verification regime (decidable, probabilistic, or attested). Downstream consumers must receive $(p, \pi)$, not bare $p$. See A2b, A2c.

Witnessed sameness: A relation supplied with the grounds required for its use. A10 distinguishes equality, isomorphism, equivalence and adjunction-derived approximation. These are different constructions, not a universal ranking of identical objects. The relevant setting, maps and preserved properties determine what substitution is justified.

---

Term Mapping: This Book vs. Standard Literature

The Third Mode uses terms from multiple fields. This table maps our usage to standard terminology and explains departures.

Our Term	Standard Term(s)	Field	Why Different
Anchor	Definition, Axiom	Mathematics	Marks a definition that later arguments depend on
Coherence	Sheaf condition, Descent	Algebraic geometry	"Coherence" foregrounds the systems concern (data agreement)
Commitment set	Belief set, Knowledge base	Belief revision, KR	"Commitment" emphasizes assertional force, not mere belief
Context	View, Scope, Module, Theory	Databases, Logic, SE	Here includes a consequence relation and a separate predicate-scoped absence profile
Conservative extension	Conservative extension	Logic	Standard term, unchanged
Cover	Cover, Covering family	Sheaf theory	Standard term, unchanged
Decidable witness	Computable certificate	CS theory	"Decidable" aligns with complexity theory usage
Epistemic status	Derivability status; interpreted evidence status	Logic	A4’s consistency assumption and A15’s absence policy remain distinct
Gluing	Descent, Patching	Algebraic geometry	"Gluing" is more intuitive for systems audience
Invariant	Invariant	Group theory, SE	Standard term, unchanged
Matching family	Matching family, Compatible family	Sheaf theory	Standard term, unchanged
N-ary event	Reified event, Event object	KR, Databases	Emphasizes arity; aligns with Davidson/Parsons
Obstruction	Disagreement witness; descent obstruction in a specified construction	Logic, Sheaf theory	A failed comparison is not automatically a cohomology class
Predicate invention	Predicate invention, Concept learning	ILP, ML	Standard term from ILP literature
Predicate package	Concept, Definition, Schema	KR, Databases	"Package" emphasizes bundled obligations
Presheaf	Presheaf, Functor	Category theory	Standard term, unchanged
Probabilistic witness	Soft evidence, Uncertain certificate	Probabilistic reasoning	"Witness" aligns with proof-theoretic usage
Provenance	Provenance, Lineage	Databases	Standard term, unchanged
Restriction map	Restriction, Pullback	Sheaf theory	Standard term, unchanged
Scope	Context, Domain of discourse	Logic	"Scope" emphasizes bounded validity
Scoped equivalence	Contextual identity, Indexed relation	Type theory, KR	Emphasizes scope annotation
Sense boundary	Word sense, Concept	WSD, Ontology	"Boundary" emphasizes partition structure
Sheaf	Sheaf	Algebraic geometry	Standard term, unchanged
Site	Site	Topos theory	Standard term, unchanged
Third Mode	Author’s terminology	—	Names the proposed combination without asserting priority for its component disciplines
Touchstone	Test case, Benchmark	SE, ML	"Touchstone" emphasizes diagnostic role
Transport	Transport, Path induction	HoTT	Standard term from HoTT literature
Univalence	Univalence	HoTT	Standard term, unchanged
Witness	Proof term, Certificate	Type theory, CS	"Witness" aligns with existential witness usage

Notes on Field Alignment

Category Theory / Sheaf Theory: We use standard terminology (presheaf, sheaf, cover, site, restriction, gluing) without modification. Readers familiar with algebraic geometry or topos theory will recognize the concepts.

Type Theory / HoTT: We use standard terminology (transport, univalence, fibration) where it applies. A16 concerns checked property-specific operations in an engineering representation. It is not a theorem about the impossibility of computational univalence; Appendix D distinguishes axiomatic and constructive settings.

Databases / Knowledge Representation: We use "context" rather than "view" or "scope" to emphasize the logic-annotated structure. "Predicate package" and "commitment set" are non-standard but map to familiar concepts.

Machine Learning / ILP: "Predicate invention" is standard in ILP. "Proposal operator" names the candidate-producing operation used here; the name carries no priority claim.

Software Engineering: "Invariant," "versioning," and "conservative extension" have established uses. A "coherence budget" applies familiar cost accounting to a declared checking regime.

Deliberate Departures

Some terms are deliberately non-standard:

• Anchor vs. "Definition": Anchors have a specific role in the book's dependency structure. Not all definitions are anchors.
• Touchstone vs. "Test case": Touchstones are recurring diagnostic scenarios, not one-time tests.
• Third Mode: The author's name for the combination of obligations specified here; its name does not establish mathematical priority or unique institutional adequacy.
• Commitment vs. "Belief": “Commitment” foregrounds the consequences of making an assertion; beliefs can also incur costs when revised.