# The logical framework and data plane (path B)

For the category-theory reader, most likely arriving from Coln. Eight
stops. maitria is independent work by the maitria coalition; the kinship
described below is intellectual, and nothing here carries an ARIA
endorsement.

## 1. Lineage, stated plainly

geolog-zeta is the public ancestor, a prototype of roughly 36,000 lines
([github.com/davidad/geolog-zeta](https://github.com/davidad/geolog-zeta)),
now dormant. Its postmortem was inverted into the engineering covenants
of what came after. The engine of record today is **geolog-alpha**, which
keeps zeta's lessons and replaces its semantic core; the historical
toolkit snapshot knows it by its campaign-era working name, geolog-beta. (The letters are working
names, not version order; arrival ran zeta, then beta, now alpha.)
That repository is [public](https://github.com/maitria-coalition/geolog-alpha).

Now the kinship. Coln is the Categorical Core implementation of ARIA's
Safeguarded AI programme, led by Martin Kleppmann and Owen Lynch, and it
is a sibling of this line rather than a competitor to it. geolog-alpha is
built to complement Coln and to converge with it at the wire format. On
several axes the two arrived independently at the same answer, including
content-addressed canonical identity and commit-DAG truth with tables as
replayed views, which is worth more as evidence than either project's
say-so. The detail is written down and served:
[a design-delta survey](/TR_coln_delta.pdf) of geolog-alpha and Coln, 13
pages, deltas in both directions at pinned revisions on both sides, with
each divergence steelmanned before it is judged. Six of Coln's choices
come out as replicate-candidates; seven of geolog-alpha's are held as
advantages. Read it before deciding which of us is wrong about anything.

## 2. Theories, instances, and the chase

Doctrine first. **geolog is a logical framework, not an expressive
logic.** It is a relational substrate adequate to host a theory of the
proof trees of an expressive logic, with the model theory of geometric
theories underneath. (geolog names the framework; geolog-alpha is the
engine that implements it.)

The cycle has three steps. Declare a theory, giving sorts, functions,
relations, and geometric axioms. Populate an instance with facts. Run the
chase, which completes the instance to its free model, witnessing
existentials, congruence-closing equalities, and materializing derived
facts to fixpoint. Tables are not authored; they are entailed.

A small example fixes the picture. Take sorts $V$ and $E$ with functions
$s, t \colon E \to V$, and one axiom saying that whenever
$t(e_1) = s(e_2)$ there exists an edge $e_3$ with $s(e_3) = s(e_1)$ and
$t(e_3) = t(e_2)$. Assert three vertices and two composable edges. The
chase produces the composite as a derived row, with the equalities its
existence forces already closed, and merging that instance with another
replica is set union on commits followed by re-derivation. Nothing
structural can conflict.

Elaboration errors carry counterexamples rather than line numbers, and
reference semantics in the Datalog and egglog family give the engine
something independent to be differentially tested against. The Geolog
part of the [book](/book.pdf) is the working account: Quick Start,
Tutorial, and Reference Manual are full drafts in the served PDF.

## 3. GeologMeta, the homoiconic meta-schema

One schema is fixed by the system. GeologMeta is the theory of theories,
and it is itself a geolog theory. Everything else, the certificate
vocabulary included, is delta rows against GeologMeta carried on signed,
content-addressed revisions, so a schema migration is data like anything
else.

Two consequences matter. Every declared object gets a canonical
content-addressed identity, the declaring revision's hash together with a
counter. And type checking becomes a validity judgment over meta-rows,
uniform across user theories, with no privileged path for the system's
own schema.

Before the first production byte, the design went through repeated
external adversarial review and an encodability audit over an entire
pre-existing schema corpus. Gaps became typed extensions rather than
exceptions (campaign ledger, day 3).

## 4. Ground formats

Two tiers, for a reason worth stating. Some carriers should never change,
and some must.

The primordial tier is fixed forever: $\mathbb{Q}$, $\mathbb{Z}$,
$\mathbb{N}$, $\mathbb{B}$, together with strings over Unicode. It also
includes the Lawvere rationals $\mathbb{Q}_{\ge 0} \cup \{\infty\}$, the
carrier for $[0,\infty]$-enrichment, whose quantale operations appear as
ordinary ground functions rather than as a special case in the engine.

The extensible tier exists because new numeric formats keep arriving; the
first extension covers IEEE floats beside FP8 and NVFP4-class block
formats. A new ground type enters as declared rows, and any dispatching
code must hold a certificate relationship to the declaration that added
it. Implementations pin to a definitional wasm reference, and an
accelerated path is admissible only when cotested against that reference,
same inputs through both, outputs compared, with a signed witness. Floats
are finite only: NaN and $\pm\infty$ are rejected at ingress and $-0$ is
normalized there.

## 5. Tensors, two primitives and no more

A tensor over a finite family of finite index sets is a finite function
from their product into a semiring. Tensor product is a lazy
index-arithmetic view that allocates nothing. Contraction is taken along
a map of finite index sets, summing over the indices the map does not
hit. Einsum and broadcasting are corollaries rather than primitives.

The load-bearing side condition is that every un-hit index must be an
output. That makes the one value-relevant free choice, a silent
cardinality scaling, unrepresentable rather than merely discouraged.

The condition is younger than the definition it repairs, and the
emendation history is preserved (ledger, day 3). Adversarial review caught an ill-typed index
family in the definition's 2025Q4 ancestor. An interim repair
over-restricted the form. A probe asking which choices can affect values
selected the version now in use.

Compilation follows the same discipline. Einsum lowers to contraction
rows, with the index map and the output set carried as data, and never to
eager $\Sigma\Pi$ expansion. The tensor former is primordial, which is
where the block-sparse codec binds, and per-block precision is typed
rather than smuggled.

## 6. The certificate vocabulary as hosted theories

The calculus of [path A](/md/certificates.md) lives inside the framework
rather than beside it. The vocabulary is two geolog theories: the
Bernstein-Logic core, and the full QTSL vocabulary above it. Proof trees,
sequents, and cell complexes are declared objects in those theories, and
certificates are carried on the same signed revisions, the same store,
and the same sync as everything else. Fixtures, goldens, and a mutant
battery sit beside the theories, in the public
[qtsl](https://github.com/maitria-coalition/qtsl) repository.
Certificate fixtures for the published experiments are already public and
byte-committed in
[qtsl-experiments](https://github.com/maitria-coalition/qtsl-experiments).

One property of that arrangement is pleasant enough to point at. The
Bernstein-Logic theory's file boundary is the certified checker's
fragment boundary, so the scope of the machine-checked soundness theorem
is something you can see by looking at where a file ends rather than by
reading a paragraph about it. The certified checker's landed theorem covers that fragment today;
certified arms for the System-and-Spec rule family are the assembly that
remains.

The geometric-form normalizer, with a linter that has teeth, went green
at three hash-stability strengths and was differentially tested against
an independent reference (ledger, day 4).

## 7. The Semantic Universe

For this audience, the chapter to read first is The Semantic Universe.
The compositional semantics is assembled by a double Grothendieck
construction over a wiring base. Open hypernets include into it as a
single machine-checked lax double functor, with strictness on the
identity-carrying locus proved as a theorem rather than assumed at the
outset. Say lax, and mean it; the strictness that holds is local and
earned.

Above that sit machine-checked adequacy statements connecting the
model-type catalogue's formers to the Semantic Universe's own semantics.
The catalogue covers ordinary, partial, delay, stochastic, and random
differential equations, jump-diffusions, Markov chains in both time
styles, Markov decision processes, Markov automata, and bags of
interchangeable units. Several of the stochastic formers are connected to
a martingale-problem floor, with the remaining gap named in the module
instead of papered over. The companion chapters are Hypernets: Primitive
Functions, Hypernets: Markov Kernels, Systems: Mathematical Models, and
Systems: Composition Patterns, all in the served [book](/book.pdf).

The systems vocabulary here is built on public work by others, gratefully
and by name: the double operadic theory of systems of David Jaz Myers,
and of Sophie Libkind and David Jaz Myers; and compositional Lyapunov
certificates via assume-guarantee reasoning, from Matteo Capucci and
David Jaz Myers.

## 8. S-complexes, and the frontier

S-complexes have moved from stated direction to shipped substance.
Diagrams as Data: S-Complexes is a chapter of the book's Geolog part, and
the genus lives in the geolog standard library as an ordinary theory.
There is no subtraction in a geometric theory, so
$\partial \circ \partial = 0$ is carried subtraction-free, as contraction
rows.

Above the relational core, three directions have design notes and no
shipped code, and they are named as invitations rather than promises.
e-complexes, meaning higher-dimensional quantitative Datalog with a
GPU-friendly evaluation story. Directed higher inductive types with
computation by rewriting. Higher Petri nets and event structures for
processes and provenance.

One road not yet taken deserves naming for this audience: proofs as cell
complexes, with certificates as 2-complexes whose boundaries are the
circuits being equated, replacing proof trees at the base layer.
Genuinely attractive, genuinely unbuilt, and awaiting a champion.