Repository navigation
docs(h-element): reconcile with bert-lenses #86, and correct a stale status - #112
Conversation
Add bert-core/src/transition.rs: one entry point validate_transition (from = model.mode(), never a parameter) over the meet-semilattice of Mode. Descent strips out-of-mode fields into a serializable LossWitness (strip-don't-restamp) with a rebuild() inverse; ascent checks the target edge's Lean hypothesis (Kernel.HasBond / Kernel.Irreflexive) via validate_mode and refuses by name. Cross-moves compose through the meet (Core). Catalogue per memo §2 as amended (A1 meet-semilattice terminology, A2 L1 scoped against H, A3 milieu/environment membership is spec-level → empty Structural→Core witness). Layering per §3: transitions never reject interface-routed flows; only validate_operational does (bert#108). Property tests L1–L7 verbatim, plus identity/cross-move coverage and a Lean-citation drift gate that greps ViewGeneration.lean (skips if the SSF repo is absent). Pinned Lean/Rust correspondence table in the module doc. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
…ting Interface-routed flows no longer refuse in the Operational projection. Per bert#108's ratified decision (Option 3, identity default), an interface is a component sited in the boundary B that recapitulates a work process, so the routing lowers to an InterfacePrimitive::Impeding filter. Unparameterized (the only form 4.2 ships) the characteristic is the identity — the degenerate zero-width conduit — so the flow attaches directly to its declared endpoints and runs as if the interface were absent. Implemented as an EDGE annotation (OperationalFlow::interface_routing), not a node insertion: the edge form makes the identity default exactly observationally equivalent to direct attachment, which a spliced node (one tick of added latency) would violate. Every model refused today for interface routing is now runnable with zero re-authoring. Interface-reference integrity is still enforced upstream by validate (a dangling interface id errors there, unchanged). Adds OperationalSpec::content_hash — a canonical (HashMap-order-independent) digest of the whole projection, the key a recorded run H hangs on so a later structural edit surfaces H as stale. Updates the interim-refusal tests to pin the new lowering: the seam test now asserts the Impeding provenance and identity equivalence; the L6 transition test (whose comment scoped the refusal to "until 4.2 lowering ships") now asserts the refusal citing #108 is gone. The L6 transition-layer law (Operational accepts interface routing = Upgrade) is untouched. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
…-supplied Adds RecordedRun: H, the trajectory a circuit traces under (T, Δt), kept OUTSIDE the WorldModel (memo A2) and keyed to OperationalSpec::content_hash of the projection it ran on. A structural edit moves the spec's hash, so H surfaces as stale (history_for returns None) rather than the old trajectory posing as current. Runs accept an explicit Δt (record) and a horizon form (record_over, ticks = T/Δt); Δt=1 reproduces raw stepping byte for byte. Acceptance test (the bert#108 4.2 contract): a model routing a flow through a boundary interface — refused before the identity-default lowering — now projects, builds a circuit, and runs 30 ticks with the ledger balanced, with zero model edits. Plus the H-invalidation contract test and the Δt-supply pin. Module gated #[cfg(test)] (as sweep): the engine mechanism and its contract tests land here; wiring H into the app's Run surface is the lenses Arc-4 half. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
… vs tuple-H distinction (grounding F1/F2) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
bert-compose was binary-only. Add src/lib.rs as the crate root owning the modules, so main.rs becomes a thin native entry point (`use bert_compose::App`) and another shell can link the engine. The minimal public surface is what a host needs to run an authored model and read its recorded trace: `from_spec` (the OperationalSpec → Circuit path), the `Circuit`/`Node`/`NodeKind` vocabulary, and the `run` module. Promote `RecordedRun` (run.rs) from `#[cfg(test)]` to live API — the app is now the caller it was waiting for. Its doc-comments move to "recorded trace" vocabulary (grounding F1): the observer's downstream record, never serialized, distinct from the 8-tuple's H slot (authored System.history). Gate the test-only `predator_prey_alpha_growth` fixture with `#[cfg(test)]` so the lib build stays dead-code clean. Baseline preserved: 60 bert-core + 52 bert-compose tests green, clippy clean. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
…ProcessPrimitive> One component, one fundamental process (bert-lenses#5, decided 2026-07-11): apparent plurality is a signal to decompose further — expressed as structure one level down, never as a list on one node. Vec<ProcessPrimitive> was an escape hatch from the decomposition the methodology wants to force. Wire compat: legacy `primitives` array still reads via a field alias (empty → None, one entry → Some); a multi-entry array is REFUSED at load with a decompose message — serde has no warning channel, and with zero multi-entry artifacts in existence (verified across all model libraries), refusing beats silently dropping an author's data. Files self-migrate to the scalar `primitive` key on next save. 7 new serde tests cover scalar / legacy-single / legacy-empty / missing / multi-refusal / write-form / self-migration. Consumers updated: operational projection drops its .first(); compose export/round-trip; TypeDB transpiler emits 0-or-1 primitive_assignment (schema unchanged); Mesa json_bridge reads both forms (list-internal). Also fixes latent transpiler test breakage: three tests loaded gitignored test-buffering.json (present only in long-lived checkouts); now load the tracked -v2 fixture. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
…ert-lenses#5) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
…p analysis LanguageTransformer BERT model hand-rendered in SysML v2. Inline comments mark BERT semantics with no SysML v2 home (boundary porosity, member_autonomy, flow usability, Force interactions) — requirements sketch for the BERT JSON ↔ SysML v2 translator. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
…he seam (#111) A source's emission was a single node param, written per-flow in from_spec (last wire wins) and split uniformly across the fanout — so a source with two differently-quantified outflows could not carry both rates, and the first real bert-lenses model executed at unit scale while its tethered trillions sat in declared_params. Rate is an edge attribute in Mobus's formalism (Eq. 4.5's (f, cap) pairs; ch.6 §6.4.3.2: "The same entity may be both a source and a sink of many different flows"). Wire now carries an optional declared rate and substance (the #111 sibling: out_substance was also last-wire-wins); the fanout split generalizes from uniform to rate-weighted with activity remaining total emission, so back-pressure and the conservation ledger are untouched. A lone pushed outflow keeps the node-param carrier (degenerate case, live inspector knob, lossless save/load round-trip); gradient amounts stay per-node as the source's fixed potential. New fixtures cross the seam INTO EXECUTION — the prior coverage stopped at "the imported amount reaches the spec", which is how the collapse hid. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
…ck by tick (bert-lenses#16) Wire.rate_series carries a forced emission series; the kernel resolves series[min(tick, len-1)] (last value held past the data horizon, #34), routed through both source_wire_rate and source_emission so the conservation ledger stays balanced. OperationalFlow.rate_series rides Interaction.parameters exactly as conductance does (skip_serializing_if, so unforced specs serialize and hash unchanged). export.rs sets the series on the wire, taking precedence over the scalar rate. Wire drops Copy (a Vec field; all wire access is field-by-ref, so no whole-value copy is needed). The unforced path is byte-for-byte unchanged. Tested at both kernel and spec->circuit levels (the #111 lesson) with a non-monotonic spike-crash fixture so a mean-collapse or frozen-series bug cannot pass. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
…e weights (rung 2) The equal-split fanout (wire_amount) now divides a process's activity across its pushed outwires in proportion to per-wire weights when any is declared, reusing rung-1's wire_declared_rate — so a weight is a constant OR a series (time-varying allocation from real data comes free). Shares sum to activity, so mass is conserved. With no weight declared it reduces to the uniform split, byte-for-byte unchanged. This is rung-2's one tool capability: a computed interior flow (a legible weighted allocation) rather than a forced one. A splitter reads the same per-wire quantity a source reads as a rate, but as a relative weight (Mobus Eq. 4.5 edge attribute). Tests: splitter_divides_by_static_weights (75/25, conserves), splitter_weights_can_vary_per_tick (split shifts as the series changes). Compose 59/59. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
…s (rung 2) The rate_series assignment moves out of the Source-only branch: a pushed flow's series rides its wire whatever the sender — a Source reads it as a forced emission rate (#16), a Splitting/process reads it as an allocation weight (rung 2). Without this a computed interior (a splitter's outflow) could never carry a weight series. Seam test from_spec_carries_a_splitter_weight_series: weights 3 and 1 on a splitter's two outflows → 75/25 split, conserves. Unforced source path and rung-1 forcing unchanged (compose 60/60; unforced target-4 still reproduces manifest a744db4baaa1dae6). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
…ts own Δt (rung 3)
Wire.dt_stride: a forced rate_series is sampled once every `dt_stride` fast ticks
and zero-order-held between — the channel's own Δt = dt_stride × base Δt, Mobus's
per-node Δt_{i,l} as an integer multiple (ch4 §4.3.3.6). A slow (e.g. annual)
channel carries its real data stream at index tick/dt_stride; between updates the
last real value is held (zero-order hold). None/1 = every tick, the single-clock
case — byte-for-byte the pre-rung-3 behavior.
This is rung-3's foundation: the tool's first honest treatment of Δt (the last
8-tuple element on a placeholder). A later true per-subsystem-clock engine
generalizes this; it does not replace it. Grounded in the ch4/5/6 recon
(rung3-mobus-recon.md), which found multi-timescale load-bearing, not peripheral.
Tests: forced_wire_holds_series_at_its_own_dt (stride 3 holds each value 3 ticks,
conserves), unset_stride_advances_every_tick (back-compat). compose 62/62.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-Authored-By: Claude <noreply@anthropic.com>
…survives to the wire (rung 3) OperationalFlow.dt_stride (skip_serializing_if → hash-stable), read from a `dt_stride` parameter on the interaction exactly as rate_series rides `series`; from_spec sets wire.dt_stride so a forced series zero-order-holds on its own clock. Values ≤1 are treated as absent (every-tick, unchanged). Seam test from_spec_carries_a_slow_channel_stride: stride 3 survives spec → circuit and holds each value 3 ticks. bert-core 67/67, compose 63/63. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
…status Two things were wrong, in opposite directions. The status line said "not yet implemented — H is a string field, never read during _act()". That was true when written; _condition_T() now exists (agents.py:333, called at :304) and reads self.history. And the key formula T(t+1) = f(T(t), H(t), Input(t)) contradicts an ADOPTED position in bert-lenses (its #86, 2026-07-18): H is a record, never an input to T — if T reads H the Mesarovic-Takahara semigroup axiom fails, and any history-dependence must be folded into the carrier instead. That document is later and normative for the kernel and SL; this one predates it and had never been reconciled with it. Fair to the implementation: Option C picked Buffering because the stock IS the history, and storage genuinely is a carrier variable — that satisfies the rule's own escape clause. What does not is narrower: _release_factor is computed from a smoothed 10-snapshot window including a second derivative, and neither the trend nor the acceleration is in the carrier. Documents the fix rather than making it: promote smoothed trend and acceleration to carrier variables so node state becomes (storage, trend, accel). Adaptation unchanged, transition Markovian again. Fold into the carrier, not abandon adaptation. No code touched. Recorded so the inconsistency is visible rather than latent in a public doc. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
Review: PR #112Scope mismatch: this diffs far more than "doc-only"The PR description says "Doc-only. No code touched.", but Only the last commit ( Suggestion: rebase this branch onto a 1. The actual doc change (
|
Doc-only. No code touched.
Two problems, in opposite directions.
The status line was stale. It said H is "not yet implemented — currently a string field, never read during
_act()". True when written;_condition_T()now exists (python/agents.py:333, called at:304) and readsself.history.And the key formula contradicts an ADOPTED position in the other repo.
T(t+1) = f(T(t), H(t), Input(t))versus bert-lenses #86 (2026-07-18): H is a record, never an input to T — if T reads H the Mesarovic–Takahara semigroup axiom fails, with history-dependence to be folded into the carrier instead. That document is later and normative for the kernel and SL; this one predates it and had never been reconciled with it. Since this repo is public, the contradiction was visible externally.Being fair to the implementation: Option C picked Buffering precisely because the stock is the history, and storage genuinely is a carrier variable — that already satisfies the rule's own escape clause. What does not is narrower:
_release_factorcomes from an exponentially-smoothed 10-snapshot window including a second derivative (agents.py:346), and neither the smoothed trend nor the acceleration is in the carrier. Same for the agent-level_prediction_factor/_effort_factor.The fix is documented, not made: promote smoothed trend and acceleration to carrier variables so node state becomes
(storage, trend, accel). Adaptive behaviour unchanged, transition Markovian again, axiom holds. Fold into the carrier, not abandon adaptation.Surfaced while consolidating the life-cycle thread (bert-lenses #144), where the same trap appears one order up: stage-transition predicates designed as "read H, detect decline" would be the identical violation.