The bert-lenses Kernel as a System

Status: LIVE.

What the kernel actually is, what it actually computes, and — honestly rated — how much of the LLM-integration story (docs/design/llm-integration-research.md) it can really bear. Written 2026-07-16 as a source-reading pass over crates/. Read this when you want to trust (or distrust) the substrate before building on it.

The two marks, and what each one is worth

This document carries two grades, and they are not the same grade. Until 2026-07-26 the stronger sections were headed — VERIFIED while the same document used "machine-checked" separately, with no legend and one line of body text disambiguating four headers. In a repo whose value proposition is the distinction between proof and inspection, one word doing both jobs is the worst word available (issue #232). So:

• CODE-READ — a human read the Rust and reports what it does. That is all. It is defeasible by the next refactor and by a careless reading, and it is the mark on every section heading below. It is the same strength of claim as the concordance's source-verified VERIFIED, but about a different object (this repo's code, not a tradition's text), so it gets a different word rather than a second definition of the same one.
• MACHINE-CHECKED — a named Lean declaration at the pinned SSF commit carries the weight, and lean-provenance.md maps the claim to that declaration by claim_id. Nothing in this document is machine-checked on its own authority; where the word appears, it points there.

The negative mark, borrowed from the concordance's UNGROUNDED: rows in the layered-guarantee table marked Thin or Declared are claims the kernel does not make good on, listed rather than omitted.

What the kernel is (and isn't)

The kernel is the Rust core in crates/, compiled to WASM, that owns systemhood — it is a decision procedure, not a database and not a renderer. Given a model, it decides what is well-formed, what counts as a system vs an aggregate, what each faithful lens says, and (via the compose engine) what a deterministic dynamics run under a model-declared invariant does (current engine: one supported dynamics-kind — Id-functor over ℝⁿ stocks with an additive conservation invariant; further kinds are declarable). Its verdicts are grounded in a machine-checked Lean formalization (systems-science-foundations/), not in house style — claim by claim, by claim_id, in lean-provenance.md. The React face computes nothing about systems — it renders kernel verdicts (web/src = face, crates/ = truth).

Five crates:

What it actually computes — the three things the LLM story rests on

All four sections below are CODE-READ: a direct read of the named source, nothing more. On the three the LLM story rests on, the code is richer than the research doc claimed, not thinner.

1. describe(model, lens) → the named per-lens formal object — CODE-READ (rich)

lenses.rs:305-347. Returns a #[serde(tag="lens")] discriminated union — the model typeset in each lens's own formal notation, with the actual named structure, not just counts:

• Klir S = (T, R): things, relations, directed, neutral, note.
• Bunge σ = ⟨C, E, S⟩ (CES; M carried as untyped mechanism_note prose, not a Lean-projected coordinate — see concordance §14): composition[] (named), environment[] (named), endostructure, exostructure, bondage, mere_relations, boundary_components[] (named), verdict, mechanism_note.
• Mobus S = ⟨C, N, E, G, B, T, H, Δt⟩ (8-tuple; Mobus's book prints a 7-tuple ⟨C, N, G, B, T, H, Δt⟩ — this formalization extends it to an 8-tuple with E first-class, a Lean improvement, not a claim that Mobus published 8; see concordance row 1): c[] (named), n, e_objects[] (named), milieu_note, g, b_interfaces[] (named), porosity, perceptive_fuzziness, t_note, h_note, dt_note, self_loop_conflicts[].

Counts are "read off the same kernel facts the canvas renders — never re-derived" (lenses.rs:344). This is the load-bearing fact for lens-faithful LLM reasoning: the kernel literally hands you the model in Bunge's or Mobus's vocabulary, named. The LLM never has to know a lens — it's fed the lens's own object.

2. lens_facts(model) → faithful per-element facts — CODE-READ

lenses.rs:83-106 (struct), :124 (fn). Everything the renderings + a critic need, keyed to canvas ids: boundary_thing_ids (components with an external flow), environment_thing_ids, orphan_env_thing_ids, authored_interface_thing_ids, boundary_props (porosity/fuzziness), aggregate (the Bunge Def 1.1 verdict, surfaced verbatim from validate_mode(Structural)), edges: EdgeFact[], ports: PortFact[]. Each EdgeFact (:33-48) carries bond, kind, locus (endo ∈ N / exo ∈ G — kernel-computed), self_loop, and mobus_ok (false iff a self-loop with no Mobus preimage — a real cross-lens incompatibility the tool states rather than hides).

3. validate_mode(model, mode) → per-lens legality, gated on Lean-named preconditions — CODE-READ

validate.rs:122-139. This is the hard guarantee. It never asks "is the model valid" — it asks "may this model be authored as this mode," each lens adding its own precondition — the named hypothesis its faithful-view theorem in ViewGeneration.lean is proved under:

• Core: on-ness (every interaction endpoint resolves) — via validate's reference checks.
• Structural (Bunge): check_bond (:143) — requires ≥1 bond between distinct components, else an "aggregate" error. Mirrors the Lean definition Kernel.HasBond — a Prop-valued def, not a theorem (claim kernel.bunge-gate).
• Operational (Mobus): check_self_loops (:158) — no self-dependency (k ≠ o, Mobus §4.3), else error, canvas-navigable via .with_subject. Mirrors the Lean definition Kernel.Irreflexive — again a def (claim kernel.mobus-gate).
• Full: self-loops + check_dynamical_face (warns if T/H/Δt nowhere populated).

Crucial subtlety (CODE-READ, :107-116; the Lean side is claim kernel.gates-independent, which is checked by exhibition and not by a theorem): the modes are parallel lenses, not a tower. Structural needs a bond, Operational needs irreflexivity, but neither inherits the other — they share only Core's on-ness. So "valid in Bunge" and "valid in Mobus" are separate claims about the same model, each gated on its own Lean-named precondition. Their independence is exhibited by the truth-table fixture's witness rows, not proved by any theorem — no entailment theorem exists in either direction, by design. That is what makes cross-lens disagreement meaningful.

4. analyze(model, lens) → all three from ONE projection — CODE-READ (this is the substrate)

lenses.rs:356-407. Bundles {validation, issue_targets, facts, description} from a single projection. Its own doc comment: "the atomic canvas verdict … one round trip, not a three-call waterfall that re-projects the same model each time." issue_targets are resolved here to canvas {thing, relation} ids via the projection's id maps — so a critic's claim can point at the exact element. This is the ModelContext substrate the research doc calls for, already built — it just isn't exposed to an LLM yet.

The layered guarantee — honestly rated

What this means for feeding the LLM (answering the skepticism directly)

What the kernel CAN reliably feed an LLM, today, from one analyze call: the model as each lens's named formal object (describe), the faithful per-element facts (lens_facts), and a Lean-grounded legality verdict (validate_mode), all keyed to canvas elements. That is real, deterministic, rich grounding — the LLM reasons over kernel-translated structure, not a raw graph it has to interpret. The lens-vocabulary guarantee (research doc §11) is as solid as claimed: the kernel does speak each lens, by name.

What it still cannot do, and where the LLM story is therefore thinner than the confident prose suggested:

• It cannot derive bondhood from behavior — bonds are declared + checked, so LLM reasoning about "is this really a bond" is reasoning about a declaration's plausibility, not reading a kernel-derived fact.
• It cannot ground reasoning about the dynamical face — T/H/Δt are notes. LLM analysis of dynamics has thin kernel support until those slots are typed.
• Dead-ends, unreachable states, and duplicate edges are now caught (#66 landed 2026-07-17 — see the layered-guarantee table above); the read-only analysis rung (Analyst panel, web/src/AnalystPanel.tsx) ships on top of this, live.

Honest bottom line: the substrate is real and richer than the research doc claimed for the two things that matter most — lens vocabulary and per-element structural facts. The remaining caveats are narrow and specific: the dynamical face is thin and bondhood is declared-not-derived. None of these undermine the analysis-first / lens-faithful plan; they scope it. Trust the structural + lens-vocabulary grounding; treat the dynamical face as aspirational.

Where the guarantees are documented (cross-refs)

• crates/bert-lenses-kernel/API.md — the frozen wasm boundary (every exported fn's shape + error contract).
• docs/archive/canvas-architecture.md — the canvas/face side (HISTORICAL, egui-era).
• lean-provenance.md — the pinned SSF commit, the generated per-claim map (every claim_id cited above), and the two gates that keep those citations resolving. Every MACHINE-CHECKED mark in this document points there.
• docs/design/llm-integration-research.md — the LLM story that rests on this kernel (its §4 substrate and §11 lens-fidelity claims are the ones this doc verifies).