Kernel + generated-views data model: the Lean gate is cleared

[rsthornton]

Context

The 6/09 architecture decision (K ≅ 2 is BERT's kernel; Klir/Bunge/Mobus are derived lenses) was gated on proving the view-derivations in Lean before touching the Rust data model. That gate cleared 2026-06-11: systems-science-foundations Systems/Klir/ViewGeneration.lean (commit abee84d, zero sorry).

What is now proven, and what it licenses here:

• One kernel model + lens overlays is a theorem, not a bet. The kernel (things + dependency relation + the on-ness constraint) generates the Klir/Bunge/Mobus presentations as faithful views with identity round trips. Views never need separate storage; they are derived artifacts.
• The preconditions are the validation rules. Generating a Bunge view requires the model to contain at least one bond between distinct components (HasBond); generating a Mobus view requires no self-dependencies (Irreflexive). These are machine-checked hypotheses — BERT's "view as X" affordances should gate on exactly these checks, and the error messages can say why (Bunge Def 1.1 / Mobus k ≠ o).
• View-switching provably never mutates the model. Round trips are identities; switching lenses is read-only by theorem.
• Slot count is a view property. The 8-tuple's slots are elaborations the Mobus view fills; the kernel stores none of them as primary data. "Why 8 not 7" is dissolved.

Scope

• Sketch the Rust data-model mapping: kernel struct ↔ proven Kernel; view layer ↔ toKlir/toBunge/toMobus with their hypotheses as validators
• Decide migration path for existing JSON models (kernel extraction = the proven projection direction)
• UX unchanged by design: users draw entities/flows; the morphism stays hidden

Related: #75 (these lemmas are the composable blocks), #77 (the reference JSONs should be generated views, with the costs as their validation rules), #81 / gov-graphs#37 (cross-model inference sits on the shared kernel).

---

Spec: docs/system-language-spec-v2-addendum.md (committed 24ef433d on feature/bert-core — lands on main when that branch merges). Audit findings in the comment below.

Sequencing prerequisite: feature/bert-core is ~40 commits ahead of main (bert-core extraction + the compose thread + this spec), no PR open. Merge it before starting this refactor — building the kernel work on top of an unmerged 40-commit branch compounds the eventual integration.

[rsthornton]

SL v2.0 spec addendum drafted (2026-06-11): docs/system-language-spec-v2-addendum.md. This issue's implementation now has its spec. Key decisions that bind the refactor:

• Mode ladder: Core (= Klir, by theorem) / Structural (= Bunge, requires a bond) / Operational (= Mobus structural face, requires irreflexivity + the existing §2.6 constraints) / Full (+ dynamical face, the backward-compat default) / Cybernetic (future). Operational vs Full is the two-faces split (BERT = structure C/N/E/G/B, compose = dynamics T/H/Δt), not an ontology change.
• Preconditions are the mode-entry validators, with error text citing the tradition that charges them (Bunge Def 1.1 / Mobus §4.3).
• Read-only mode switching is a spec guarantee (round trips are identities) — the same invariant compose's lens-invariance test enforces empirically at the domain level.

bert-core audit findings (addendum §A6), for this issue's scope:

1. bert-core is the Full view with no kernel object — fine; the refactor decides first-class struct vs derived projection (either satisfies the spec; the projection function must exist).
2. Presentation data mixed with semantic data (System.radius, System.transform, Interaction.endpoint_offset) — the kernel/view separation suggests the same split inside bert-core.
3. Dynamical face is stringly-typed (transformation/history/time_constant as String) while compose carries the typed parameters — Full-mode validation limited to non-emptiness until the faces share types.
4. No self-loop check exists — new mode-gated validator rule (legal in Core/Structural, illegal Operational+).

[rsthornton]

Parts 1–3 landed → PR #92 (open for review, not merged — flagship data-model merge stays a human call, as Part 0/#90 was).

• Part 1 — WorldModel::kernel() projection (Rust twin of Lean Kernel.toKlir) + Mode enum (Core/Structural/Operational/Full) + mode field. Absent ≡ Full → old files byte-stable, save path emits no mode key.
• Part 2 — validate_mode(model, target) mode-entry gate. validate() untouched (zero breakage). Preconditions cite traditions: Bunge Def 1.1 (bond), Mobus §4.3 (self-loop, the one new rule). Modes are parallel lenses, not a cumulative tower — Structural and Operational impose independent preconditions, matching the proof's parallel toBunge/toMobus.
• Part 3 — kernel round-trip + mode-boundary regression tests. cargo test -p bert-core → 27 pass.

Scope held: +413/−0, additive, no struct rewrite/migration.

Filed: #93 (three-substrate agreement test: BERT ⇔ GSR ⇔ Lean).
Still OUT (per spec): presentation/semantic split (A6.2), typing the dynamical face (A6.3), mode-transition UI (§A5, → Wednesday's lenses prototype), Cybernetic mode.