Theoretical Foundations

0. The thesis

Every non-trivial system that lets you derive things from a source of truth faces the same question sooner or later: how far can you trust the derived thing? LATTICE’s answer, repeated at every layer in a different mathematical costume, is: only as far as something has been mechanically proven.

That single sentence is the thread running through this whole page. What changes from layer to layer is which branch of logic or theoretical computer science supplies the proof:

None of this is decoration. Read on, and by the end each row above should read as an obvious consequence of the theory next to it, not as jargon bolted on afterward.

1. Description logic and the open-world graph

Everything in LATTICE sits on top of a description logic — the family of decidable logics that OWL (the Web Ontology Language) is built from. A description logic is, deliberately, a restricted fragment of first-order predicate logic: it gives up some expressive power in exchange for a guarantee that a machine can always finish checking what follows from what you’ve asserted, in finite time. Full first-order logic doesn’t promise that. Description logics are engineered specifically so a reasoner never has to say “I don’t know if this terminates.”

Two consequences of choosing a description logic show up constantly once you start reading LATTICE’s specifications:

The open-world assumption

A description-logic reasoner never treats the absence of a statement as evidence that the statement is false. If nothing in the graph says who occupies a RoleOccupancy, the reasoner concludes nothing about who occupies it — not “nobody,” just “unstated.” This is the right default for a graph assembled incrementally from many sources, but it has a sharp consequence: a genuinely closed question (“is this GovernanceState one of exactly four values, and no others”) cannot be answered by OWL classes alone, because OWL can never conclude a class extent is exhaustive. LATTICE’s answer, used throughout, is to keep the OWL class open and push the closed question into a SHACL shape (sh:in over named individuals) — SHACL validates a graph as it stands, right now, closed-world, which is precisely the complementary tool OWL’s semantics deliberately withholds.

Picking the right fragment, on purpose

Not every part of LATTICE needs the same amount of logical horsepower, and asking for more than you need has a real cost: OWL 2 DL is decidable but can be expensive to reason over; OWL 2 EL is deliberately restricted so that classification stays polynomial-time even over very large ontologies. Surface’s nominal-class index form is a direct, stated example of choosing EL on purpose — a generated class is defined as Carrier ⊓ ∃R.{v}, using owl:hasValue, specifically because that construct is inside OWL 2 EL. A form requiring more expressive power than EL would need its own index kind; the design note is explicit that this was a deliberate tractability trade, not an oversight. SPC makes the identical trade at a larger scale: its structural layer (sorts, behaviours, session types) is written in full OWL 2 DL, because the structural questions genuinely need that expressiveness, while its domain-refinement predicates — the part that reaches into an imported ontology to constrain a message payload — are recommended to stay inside the tractable EL++ fragment specifically so a reasoner checking those constraints doesn’t inherit DL’s worst-case cost.

2. Order theory, and why it’s called LATTICE

A lattice, in the mathematical sense the project takes its name from, is a partially ordered set in which every pair of elements has both a unique greatest lower bound (a meet) and a unique least upper bound (a join). That’s a more specific claim than “things are ordered” — it’s a claim about structure: given any two elements, there’s always a well-defined “most specific thing both fit under” and “least specific thing that covers both.” Concept hierarchies have exactly this shape, which is why lattice theory turns up wherever ontologies, taxonomies, or type systems are involved.

LATTICE leans on order theory at three distinct scales, and it’s worth seeing them side by side, because they’re the same mathematics doing three different jobs.

The layer dependency order is a strict partial order

The rule “a lower layer never names a term belonging to a higher one” defines a strict partial order over the layers — some pairs are directly comparable (Foundation precedes Vocabulary), some are only comparable through a chain (Foundation precedes Behaviour, via several intermediate steps), and a few are simply incomparable (Eligibility and Instrument’s shared dependency on Party doesn’t make Eligibility and Instrument comparable to each other). Drawing that order as a diagram is exactly a Hasse diagram — the standard way order theory visualises a partial order, where an edge means direct precedence and nothing implied by transitivity is drawn twice.

This order is exactly what makes an automated import-closure check meaningful in CI: with an unambiguous partial order, “did anything import upward” becomes a single well-formed question instead of a matter of convention.

Closure operators, appearing three times under three names

A closure operator takes a relation and extends it to include everything reachable by following that relation any number of times (its reflexive-transitive closure), and a relation only supports a well-defined closure if it’s acyclic — otherwise “everything reachable” is either infinite or ill-defined. LATTICE needs exactly this operation in three unrelated-looking places, and it’s worth naming them together because the repository itself never quite says “these are the same mathematical operation” in one place — but they are:

Well-foundedness (no cycles) is stated in LATTICE as a runtime claim, not a static one — SPARQL cannot express a property path over a variable predicate, so no fixed SHACL shape can verify acyclicity for a relation that’s only known at declaration time. The generator has to actually walk the graph and check, and it records the result as evidence (a discharged law) rather than a proof anyone could have derived by inspection alone.

Ordered value spaces

Quantification generalises the same theme one level further down, into raw values: every ValueSpace states, explicitly, which order theory shape it has — a total order (every pair comparable, like a number line), a cyclic order (like clock positions, where “which is lower” has no consistent answer without picking an arbitrary cut point), or no order (equality-only, comparable but not rankable). Getting this declaration right is what makes a bounded region — a Range for a total order, a CyclicRange for a cyclic one — a well-defined concept in the first place, rather than a guess about what “between” ought to mean for a particular kind of value.

3. Conservative extension: the safety property underneath Surface

Model theory has a precise name for a very useful idea: a theory T′ is a conservative extension of a theory T if every consequence of T′ that’s expressible purely in T’s own vocabulary was already a consequence of T — in other words, extending the theory added new things you can say, but proved nothing new about the things you could already say. It’s the formal way of saying “this addition is purely additive, never revisionist.”

That’s exactly the property Surface is built to guarantee, and it’s exactly why the layer’s name for restating a value as a retrievable symbol — indexing — is safe to regenerate or throw away at will: an index always mints its own, brand-new terms, so by construction it can never prove anything new about a term that already existed. Adding one entails nothing new about source terms; removing one loses no fact anyone actually authored. That conservativity, not the speed gain, is the entire reason a generated index is allowed to be treated as disposable cache.

Promotion is the one mechanism in Surface that isn’t automatically conservative, and the design note treats that honestly rather than hiding it. A promotion restates a value onto a property that may belong to Surface’s own namespace, or may be a property some other, consuming layer already declares. In the second case, the emitted triples are literally indistinguishable from facts a person authored by hand — no annotation on the record changes that, because the assertion carries the authored property, not a generated one. Rather than weaken conservativity to pretend this case doesn’t exist, Surface names it: every generated surface records a signatureScope — LocalSignature or SourceSignature — and a specific law (X6) constrains the dangerous case precisely: a promotion reaching an authored property must preserve the source value’s exact meaning and must be written out directly rather than left as a bare, reasoner-dependent definition. A lossy promotion is barred from an authored property altogether (X5) — it’s confined to Surface’s own namespace, where its derived nature stays visible in the identifier itself.

This is conservative extension used as an engineering discipline, not just a proof technique: instead of asking every consumer to somehow know, by convention, which generated facts are “real” and which are restatements, the theory gives a mechanical test — does this cross the signature boundary, and if so, was the crossing exact — and the law is enforced by the compiler, not by trust.

4. Three-valued logic: living with “we don’t know yet”

Classical logic assumes every proposition is either true or false, and nothing else. That’s a convenient fiction for pure mathematics, but it’s a bad fit for a graph that’s frequently, legitimately incomplete — and LATTICE deliberately doesn’t force the fit. Eligibility’s decisions, and Quantification’s comparisons, both resolve to one of three values, not two:

This is the same move logicians make with Kleene’s strong three-valued logic: rather than defaulting an unknown input to either true or false, “unknown” is treated as its own value that propagates honestly through a computation instead of silently resolving to a guess. Concretely: if a candidate range’s lower bound is present but its upper bound is missing, the right answer to “is this contained in the required interval” isn’t a coin-flip between Permitted and Denied — it’s a distinct, first-class Undetermined, with its own recorded reason (missing value, insufficient granularity, an absent conversion context, and so on), because those different reasons call for different remediation.

There’s a quiet but important reason this pairs naturally with the open-world assumption from Section 1: an open-world reasoner already refuses to treat “the graph doesn’t say X” as “X is false,” so a two-valued decision procedure built on top of it would have to invent a default somewhere — and any invented default is a policy decision masquerading as a logical one. Three-valued evaluation removes the need to invent anything: “don’t know” stays “don’t know,” all the way out to whoever has to act on the answer.

5. Category theory in MORK: turning “which one is this” into a computable optimisation

MORK’s job — aligning messy source material onto a target ontology — sounds like it should require judgement all the way down. Its documentation is candid that you don’t need to follow the mathematics to use it, but the mathematics is what lets MORK’s judgement be checked rather than just trusted:

Concept lattices, and the name comes full circle

The cheapest, always-available layer of MORK’s inference is spotting that certain source fields habitually travel together — an attachment point, a limit, and a share appearing together signals a reinsurance “layer,” say. This is a textbook application of Formal Concept Analysis: given a table of objects and the attributes each one has, FCA finds every maximal group of objects sharing a maximal set of attributes — a “formal concept” — and orders those concepts by which ones’ object-sets contain which others’. That ordering always forms a complete lattice. It’s a fully deterministic, purely combinatorial technique — no training, no probability — which is exactly why MORK’s own comparison table lists it opposite “community detection” with a confidence of 100%, in contrast to every probabilistic alternative listed alongside it.

The profunctor: bridging a guess and a proof

Source data and target ontology are, in MORK’s own framing, two fundamentally different kinds of thing: the source side is probabilistic — hypotheses with varying confidence — while the target side is logical — an ontology’s restrictions and disjointness axioms are either satisfied or they aren’t. A profunctor, in category theory, is a structured way of relating two categories that don’t share a common type of morphism — here, essentially a matrix scoring every (source hypothesis, target element) pair, so that mapping reduces to finding the lowest-cost assignment across that matrix. MORK’s documentation decomposes this into three phases worth naming, because each is individually a smaller, more tractable question than “solve the whole mapping”:

The Galois connection: from guessing to knowing

A Galois connection is a pairing between two ordered structures that behave as mutual, order-reversing best-approximations of each other — the textbook example relates a set of objects to a set of properties exactly the way Formal Concept Analysis does above. Once enough confirmed mappings accumulate, MORK’s documentation describes a Galois connection emerging between source communities and target classes, characterised precisely: every concept in a community maps to a property the target class requires, and every required property has some concept in the community mapping to it — a perfect, checkable fit, not merely a plausible one. That’s the mechanism behind MORK’s central claim, its own convergence theorem, that the fraction of fields still needing AI or human intervention shrinks the more the system has already confirmed.

Composing mapping context: the Writer monad

When one mapping’s outcome has to feed into how a dependent mapping is interpreted — Aardvark’s identity depends on Aardvark’s name property having already been resolved — MORK needs a principled way to thread that accumulated context through a chain of otherwise-independent mapping steps. This is precisely the job of a Writer monad in functional programming: a computation that carries an accumulating side-channel of context alongside its main result, composed automatically at every step rather than threaded by hand. MORK’s own glossary names it directly: “the mathematical mechanism that ensures axiom context accumulates correctly as mappings compose,” realised concretely as a Kleisli-style composition property (broaderApplicative) that applies a dependent mapping within the context — the outcome — of the mapping it depends on, rather than in isolation from it.

6. Session types in SPC: a type system for conversations

An ordinary type describes a single value — “this is an integer.” A session type describes something structurally richer: the entire sequence of sends and receives a participant in a protocol will perform, including its branching and its recursion, before the exchange ends. SPC (“Subject-oriented Process Calculus”) is built on the multiparty flavour of this idea, and its purpose is exactly the one stated in the root README: where Behaviour models what state something is in and what can cause it to change, SPC gives the live exchange between the agents driving those changes a formal contract to align to, rather than an ad hoc protocol.

A single global type describes the whole choreography — who sends what to whom, in what order, across every participant at once. Each participant’s local type is obtained by projecting that global type down onto just their own point of view, discarding everything they can’t see. A participant that behaves exactly according to its own local type is, by the standard theory this style of session typing is drawn from, guaranteed free of certain classes of miscommunication by construction — not by testing every possible interleaving by hand.

SPC reifies the runtime state of a whole such system as a configuration (which subject is doing what, which messages are in flight, who’s externally visible), and evolves it one recorded reduction step at a time, in deliberate lockstep with the global type itself being consumed as the choreography plays out. The property tying the two together is the standard type-theoretic guarantee called subject reduction (or type preservation): a well-typed configuration, once it takes a step, lands on another well-typed configuration. SPC’s own specification is candid that OWL alone cannot fully enforce this, nor a handful of sibling correctness properties — the duality between a send-type and its matching receive-type, and contractiveness of a recursive type — flagging them explicitly for an external validator or a hand-written rule rather than pretending a description logic reasoner can check them unaided. That’s itself a small, honest instance of Section 1’s lesson: pick the logic that actually has the expressive power the question needs, and say plainly when a question has stepped outside it.

Where SPC meets a domain ontology

A session type constrains the shape of a conversation; it says nothing, on its own, about what a message’s payload actually means in domain terms. SPC bridges the two through a declared domain bridge (mapping SPC’s sorts and values onto an imported ontology’s concepts and individuals) and states the relationship between its own structural layer and that imported knowledge base in a single, dense line worth unpacking:

A functor maps one category’s objects and structure-preserving arrows onto another’s while preserving composition; contravariant means it reverses the direction of every arrow it maps. Read plainly: the more specific — the more narrowed — a behaviour becomes on the process-calculus side, the more the corresponding description-logic knowledge base has to state to characterise it, and the map between the two directions is itself built from conservative extension (Section 3’s exact technique, reused at a different scale): adding domain detail on the DL side is guaranteed not to invalidate anything already established about the process-calculus side. It’s the same “purely additive, never revisionist” property, doing its job at the seam between two genuinely different formal systems rather than within one ontology layer.

SPC also frames a whole subject network as an open system — a system with an explicit external interface that other systems can be plugged into, described formally as a structured cospan, a standard construction from applied category theory for composing open systems along shared boundaries: S = (Σ, α, B, ι, o), L(I) → S ← L(J). The point of stating it this way, rather than as an ad hoc “system with some ports,” is that composition of open systems then inherits whatever properties the underlying category-theoretic construction already guarantees, instead of needing to be proven fresh for every new way two subject networks might be wired together.

7. Determinism and content-addressing: proof by re-computation

Not every guarantee in LATTICE comes from a branch of logic — one of the load-bearing ones is closer to a discipline from functional programming and reproducible builds: if a computation is deterministic, you can verify a claim about its output by simply running it again and comparing, rather than reasoning about the computation’s correctness in the abstract. This is the idea underneath the whole staged compiler pipeline that turns a Surface contract, or an Eligibility condition, into an executable SPARQL query, SHACL shape, or SWRL rule.

Concretely: the compiler’s own determinism law is discharged by compiling twice and comparing artefact hashes byte-for-byte — not by an argument that the code should be deterministic, but by actually checking, every time, that it was. Underneath that check sits content-addressing: identity is computed from a canonical form of what something actually contains, not from an arbitrary label. LATTICE goes further than a single hash, though, because “has this changed” turns out to be at least four genuinely different questions, and collapsing them into one hash throws away distinctions a real deployment needs:

The same discipline shows up in how a batch of MORK mappings gets ordered before compilation — dependency edges are visited in a fixed, IRI-lexicographic order specifically so the same batch always orders the same way regardless of which order triples happened to arrive in — and in why a generated surface has to record exactly what it read to produce itself, one entry per source with a content hash, so staleness reduces to “does any recorded hash still match reality” instead of a question anyone has to reason about by hand.

8. One thread

Pull the thread all the way through and every section above turns out to be one recurring move, dressed in the mathematics that fits the specific question being asked:

• Description logic bounds what can be concluded from an incomplete graph, and SHACL is reached for exactly where that bound would otherwise be too weak.
• Order theory gives layering, hierarchies, and closures a precise shape — and a precise notion of when that shape is broken (a cycle) rather than a vague sense that something’s off.
• Conservative extension is the mechanical test that decides whether a generated fact is safe to discard, applied literally, not just invoked as a slogan.
• Three-valued logic refuses to let “we don’t know” collapse into a guess dressed up as an answer.
• Category theory turns “which mapping is correct” from a matter of taste into an optimisation with a checkable, provably-optimal solution once enough evidence exists.
• Session types turn “will this conversation go wrong” from a testing question into a typing question, decidable before anything runs.
• Determinism and content-addressing turn “do I trust this artefact” into “did recomputing it produce the same bytes,” which anyone — human or CI job — can just go and check.

And the practical, cross-cutting expression of all of it is the authority ceiling repeated at nearly every layer that generates anything: a derived artefact may declare itself Advisory or, at most, CachedReproducible — trustworthy because it’s provably reproducible from its source, and never higher, because a derived thing outranking the declaration it came from would invert the entire relationship this page has been describing. Every theory above exists to make that one sentence something a compiler can enforce, rather than something a README merely asks you to believe.

9. Further reading

This page stays deliberately at the level of “why,” with just enough of “what” to make the why concrete. For the fuller vocabulary and the mechanics each layer actually declares, see the LATTICE glossary. For the worked, running-code version of everything Surface, Eligibility, and MORK do, see the Field Guide. For the record of each individual decision named above, see the ADR index — in particular ADR-A16 through ADR-A20 for Surface’s conservativity laws, and the root ontology/mork/README.md and ontology/spc/README.md for the fuller mathematical treatments this page has only summarised.