# The campaign ledger — 16–22 July 2026

On 16 July 2026 the goal was stated plainly: *finish Bernstein Logic, with
an implementation checked against ARM semantics, by July 21 — ideally
consuming geolog's wire format, with the proofs of the cartpole and
double-pendulum controllers stored in geolog.*

Statuses: **shipped** (artefact exists; stated check run) · **in flight**
(named work open on the day of writing) · **frontier** (known-open, stated
as invitation). Entries never retro-edit; corrections append. Refusals and
nulls are entries too. Built by a coalition of ephemeral Claude Fable 5 and
GPT-5.6 Sol instances in a shared high-context workspace, directed by David
"davidad" Dalrymple, whose word is what an entry marked "decided" records — see
[how this was built](/md/colophon.md).

## Day 1 · Thursday 16 July — complete

- **Goal → requirements within hours**: 23 requirements in three tiers,
  nine work packages with acceptance criteria, the wire contract as first
  frozen interface — proof-calculus and data-plane workstreams parallel
  from day one.
- **Frame correction, same day**: geolog is a *logical framework* hosting a
  theory *of Bernstein Logic proof trees*, not an expressive logic; the
  wire format's job is delta rows against one fixed homoiconic meta-schema.
  Requirements rewritten the same afternoon; a "what geolog is (and is
  not)" primer now travels with the spec.
- **Coordinate projection entered the term grammar** as the degenerate case
  of a two-primitive tensor calculus (lazy tensor product; contraction
  along a map of finite index sets) — einsum arrives later as extension,
  not rework.
- **Honest mathematical surprise**: "zero new mathematics" was wrong at one
  joint — above dimension one the region machinery hands the kernel real
  barycentric weights while the kernel theorem eats rational ones;
  classical LP folklore (rational system with nonnegative real solution ⇒
  nonnegative rational solution) proven in-tree, ~300 lines. With the
  bridge: full-catalogue soundness **sorry-free at standard axioms**; first
  Bernstein-cone verdict above dimension one.
- **Machine-code route demonstrated on an existing artefact**: to prove the
  *route* before building along it, cake_lpr (an existing verified
  SAT-certificate checker) built out of the box and checked fresh
  certificates; its in-logic compilation at pinned sources reproduced the
  shipped AArch64 assembly *byte-for-byte*; its machine-code soundness
  theorem replayed from source at the pins (4h15m, 32-core rented box,
  49.2 GiB peak). The toolchain and replay discipline proven; the
  campaign's own checker did not yet exist.
- **Trusted-core diet**: emitted-C closure 3.58M → 34,311 lines (104×),
  zero external packages; first Lean-emitted C through CompCert (9/9 TUs
  after mechanical C11 normalization), binary output byte-identical to the
  production build.
- **First real certificate**: cartpole decrease end to end — exact-rational
  weight LPs per cell, 197-node proof term, 19 KB of certificate bytes (in
  the campaign-era wire format of the day, since retired for geolog rows),
  reference-checker ACCEPT, independent Rust-reader parse. And a refusal
  worth as much: on the widened domain the splitter refuses two sectors,
  and a direct scan confirms the decrease property genuinely fails there —
  the refusal tracks the law's true boundary.
- **Composition rules drafted** (interface-promise, syzygy, small-gain)
  with their Lean soundness satellite; small-gain reduces to a verified
  two-line identity — the checker never sees a fixpoint argument.
- **Tech report, day one**: 25-page self-contained draft written and put
  through an adversarial review round the same day.

## Day 2 · Friday 17 July — complete

- **Critical path complete in ~30 hours**: four real certificates
  (cartpole decrease + rate, double-pendulum small-gain + syzygy) through
  reader → compiler → signed commit → content-addressed cold store →
  replay → projection, projections **byte-identical** to producer bytes,
  twice; cross-language mutant battery all-reject.
- **Stretch bar met early**: both target controllers' certificates existed
  in the data plane by breakfast on day 2 — four days ahead of the bar's
  deadline.
- **Tech report complete at 35 pages** (appendices: effective sparse
  Handelman; the defect bound).
- **Meta-schema review day** — a live line-by-line review produced a dozen
  decisions: low-precision float ground sorts (FP8/NVFP4-class); asm-like
  opcodes; extensible ground types with certificate-bound dispatch ("new
  numeric formats will keep on coming") while $\mathbb{Q}/\mathbb{Z}/\mathbb{N}/\mathbb{B}$ stay fixed as Platonic; GPU implementations only
  when cotested against a wasm golden (same inputs through both
  implementations, outputs compared) with signed witness; a tensor former;
  Lawvere rationals ($[0,\infty]$, quantale ops at extension tier); a
  uniform multi-precision story.
- **Storage and sync became real code**: durable blocklace store; sans-io
  sync engine + wire codec, two adversarial rounds absorbed. First
  *production* bytes deliberately held for a write ceremony — the
  campaign's one true commitment point.
- **A first verified checker became a program**: HOL4/CakeML port of an
  early, *partial* checker — a fragment of the calculus, not the full
  catalogue — as a real binary: certificate bytes on stdin, verdict on
  stdout, kernel-checked, that prototype's machine-code chain green. The
  full-catalogue certified checker this prefigures is the one still
  assembling.
- **An honest no**: can that binary check a real ACAS-Xu-scale certificate
  today? No — not yet; the blocker is performance, not vocabulary. Design
  steer adopted the same hour: checker inner loops as relational joins over
  flat column stores, never materialized pointer structures; the
  performance seating began that evening.
- **Security-by-design moved**: capability algebra proposal drafted
  (deterministic replay of signed attenuable delegations, converging with
  Keyhive); blake3-subtree authenticated range proofs dispatched as a
  successor capability.
- **Programme corpus indexed**: thirteen decks + the thesis,
  concordance-style, deck claims mapped to built artefacts with divergences
  marked — the spine of the programme path.

## Day 3 · Saturday 18 July — complete

- **Ported prototype's debts paid**: all four named proof cheats in the HOL4
  port discharged, 17/17 receipts green — the *prototype's* machine-code
  chain rests on no IOUs (scope: the partial checker of day 2; the
  full-catalogue machine-code story remains the arc in flight).
- **Floats finite-only, decided and enacted**: NaN/inf rejected at the
  boundary, $-0$ normalized to $+0$.
- **Theories and instances first-class** in the meta-schema; authorization
  decided: per-instance assertion capabilities (non-totally-ordered), admin
  at theory and instance grain, conservative delegation defaults.
- **A slide-era bug found and upgraded**: adversarial review caught an
  ill-typed index family in the 2025Q4 tensor-contraction definition; an
  interim repair over-restricted it; the reopening probe — which choices
  can affect values? — selected the final side condition (every un-hit
  index is an output), making the one value-relevant free choice
  unrepresentable. Emendation history preserved in the definition's own
  record.
- **Catalogue grew admissible rules with proofs**: PConstExact (subsuming
  rational factorization), PBound, PSD certificate entries in three
  variants — kernel-clean soundness lemmas, twice-verified.
- **Pre-first-byte gate ran**: an encodability audit checked an entire
  existing schema corpus for expressibility in the meta-schema; a dataflow
  audit classified nineteen existing computations against the framework;
  gaps became typed extensions, not exceptions.
- **Zero-copy serialization decided** for envelope and store surfaces
  (rkyv-class), signature domain separated, byte-costs checked before
  ratification.
- **Overnight fuzz campaign launched**: three targets, twelve hours, four
  forks each, rented high-memory box, against the store's
  open/crash/state-machine surfaces.
- **Sound-for-first-byte**: by midnight the staged genesis reached the bar
  its name states — blocking finding set empty, final review round folded
  with zero staged bytes moving afterward, genesis re-pinned and golden
  byte-verified.
- **Nomenclature knot dissolved**: the "where does QTSL sit relative to
  Bernstein Logic" confusion traced to a turnstile collision — $\vdash$ vs
  $\vDash$, now separate kinds of judgment within one enormous logic
  (renamed to QTSL).

## Day 4 · Sunday 19 July — complete

- **Geometric normalization landed**: the normalizer putting BL's theory
  into geolog's geometric form — with a linter with teeth — green at three
  hash-stability strengths, differentially tested against an independent
  reference.
- **Overnight fuzz campaign returns** this morning; findings fold in as
  fixtures.
- **This site went up on staging** — programme path, toolkit map, this
  ledger, certificate path (stops 1–5) — buildable from the record with
  zero repository flips.
- **Appended at close — the fuzz campaign came back clean**: all three
  targets ran to full term against the store's open, crash, and
  state-machine surfaces (424.7M / 58.1M / 20.7M executions) — zero
  crashes, zero hangs, zero OOMs; 405 new coverage-expanding corpus entries
  banked as fixtures. An honest null, recorded as one.
- *Closed 21 July, with the fuzz return appended above. Corrections to
  earlier days, if any, append rather than editing history.*

## Day 5 · Monday 20 July — complete

- Producer scale-up; full-certificate ingestion on the verified-checker
  lane (the named gap between reference-checker acceptance and
  verified-binary acceptance at scale).
- Assembly rehearsal: certificate bytes out of the data plane, verdict out
  of the verified checker.
- *The two items above were the plan, written in advance; the entries below
  record the day itself, appended at its close. The ingestion arc they name
  continued into day 6.*
- **The storage decision — certificates are born as rows.** Decided: a
  certificate's only durable form is ordinary rows in a signed,
  content-addressed geolog commit — no separate proof-file format, nothing
  to version — and the campaign-era binary bridge format was retired across
  the whole project the same day. The front page's trichotomy — one set of
  sealed commit bytes, three independent checking routes — was written down
  the same day as the architecture of record.
- **Re-verification at scale**: the campaign's accumulated certificate
  corpus — 28,569 certificates from the producer-side science sweeps —
  re-verified end to end under both the sweep-era and current checkers:
  zero refusals, no certified bound moved.

## Day 6 · Tuesday 21 July — complete

- The programme catch-up — the campaign's real external coupling — with the
  end-to-end demonstration on the table and this site as the guided record.
- **The certified lane now parses the data plane's own bytes** — at the
  logic level, inside its proof boundary: the sealed geolog commit-body
  format entered the verified reader by morning — decode totality re-proven
  over the widened grammar, canonical encoding upgraded to a kernel theorem
  (the accept path executes a re-encode fixed-point gate), 21-case
  differential green against the independent Rust oracles (expected-accept
  rows byte-exact; eighteen hostile mutants refused in class). The
  machine-code tier of that arm is the assembling step.
- **The checkers' read path completed its cutover to rows**: certificate
  content is consumed from geolog row bodies; no code path reads or writes
  the retired bridge format.

- *Closed complete; this closure appended 2 August 2026, with nothing above
  it edited. The ingestion arc these entries carried ran on into day 7, and
  the machine-code tier named above as the assembling step is assembling
  still.*

## Day 7 · Wednesday 22 July — complete

- Finish-by target. The ledger closes as an artefact of record.

- *The finish-by target was met in the sense in which it was stated. The
  ledger closed on 22 July 2026 as an artefact of record, with the
  toolkit's core existing end to end, from producer through sealed geolog
  rows to checker verdict.*
- *The frontier list below stayed the forward edge rather than becoming a
  list of regrets; the afterword records which of its items have since
  moved. Appended 2 August 2026.*

## The frontier

- ACAS-Xu-scale checking on the verified binary (relational-join core:
  design steer → measured throughput).
- The assurance edifice as a freestanding distribution.
- Proofs as cell complexes (the 2-complex base-layer alternative).
- The completeness boundary: a meta-theorem characterizing the certificate
  fragment's expressive boundary.

## Afterword — 2 August 2026

The ledger above closed on 22 July 2026 and is preserved unedited;
corrections to it append, as they always did. Work has continued daily
since, in the same open-record style, and the record now accumulates in the
book and in the repositories rather than on this page. The book has grown
into a preview scaffold of roughly a thousand pages, served at
[/book.pdf](/book.pdf) and rebuilt from committed sources at every build,
and a mechanized descent now connects the chapters' patterns to the
Semantic Universe's own semantics: open hypernets include as a single
machine-checked lax double functor, the model-type catalogue's formers
carry machine-checked adequacy statements, the Specification Language is
presented as deduction rules over a formation judgment, and eighteen
rewrite rules are mechanized statement for statement in Lean and in HOL4,
with the four wrong-polarity siblings refuted by machine-checked
countermodels. The certificate vocabulary itself is now baked as two geolog
theories, the Bernstein-Logic core and the full QTSL vocabulary above it,
with fixtures, goldens, and a mutant battery beside them. Two technical
reports are served on this site, one on
[certifying stochastically and dynamically coloured Petri nets without a
non-Zeno axiom](/TR_zeno_variadic.pdf) and one
on [the design deltas between geolog-alpha and Coln](/TR_coln_delta.pdf).
The semiconductor ladder is underway with its first rung certified,
carrying linear-Lyapunov drain certificates for the Mini-Fab fluid model
under named static-priority dispatch, residual scheduling freedom resolved
adversarially, at release rates up to 95.9 of its 96 lots/week fluid
capacity, with the probe at 96 correctly failing. Three of the six
repositories are public
([kernels](https://github.com/maitria-coalition/kernels),
[mtk](https://github.com/maitria-coalition/mtk),
[qtsl-experiments](https://github.com/maitria-coalition/qtsl-experiments)),
and the rest are arriving. Two items on the frontier list moved:
machine-scale checking on the certified binary went from a design steer to
a measured replay of the stored corpus, 4,105 verification conditions
accepted with no divergence from the fast-path twin at a pooled median of
30 ms per file on one Arm core, and the completeness boundary gained a
first characterized fragment, written up in the book's Partial Completeness
chapter. This page stays as history; the current account is the book, and
the current receipts are in the repositories.

*Correction, appended 4 August 2026: the repository count above has moved —
five of the six repositories are now public, with
[geolog-alpha](https://github.com/maitria-coalition/geolog-alpha) and
[qtsl](https://github.com/maitria-coalition/qtsl) joining kernels, mtk, and
qtsl-experiments; the sixth is this site's own repository. The paragraph
above stays as written on 2 August.*