docs: fix staleness across all research docs + Zargham feedback + gitignore

.gitignore

@@ -42,3 +42,7 @@ Thumbs.db
 
 # Pyright
 .pyright/
+
+# Claude Code
+.claude/
+__marimo__/

CLAUDE.md

@@ -87,7 +87,7 @@ gds-framework  ←  core engine (pydantic only, no upstream deps)
 
 gds-sim            ←  discrete-time simulation (standalone, pydantic only)
     ↑
-    ├── gds-analysis   ←  spec→sim bridge, reachability (gds-framework + gds-sim)
+    ├── gds-analysis   ←  spec→sim bridge, reachability (gds-framework + gds-sim + gds-continuous[opt])
     └── gds-psuu       ←  parameter sweep + Optuna (gds-sim)
 
 gds-continuous     ←  continuous-time ODE engine (standalone, pydantic only) [scipy]

docs/research/formal-representability.md

@@ -175,7 +175,7 @@ Token overlap is the auto-wiring predicate:
 compatible(p1, p2) := tokenize(p1.name) ∩ tokenize(p2.name) != empty
 ```
 
-**Definition 1.3 (GDSSpec).** A specification is an 8-tuple:
+**Definition 1.3 (GDSSpec).** A specification is an 9-tuple:
 
 ```
 S = (T, Sp, E, B, W, Theta, A, Sig)
@@ -190,7 +190,7 @@ A     : Name -> AdmissibleInputConstraint   (state-dependent input constraints)
 Sig   : MechName -> TransitionSignature     (mechanism read dependencies)
 ```
 
-While presented as an 8-tuple, these components are cross-referencing:
+While presented as an 9-tuple, these components are cross-referencing:
 blocks reference types, wirings reference blocks, entities reference types,
 admissibility constraints reference boundary blocks and entity variables,
 transition signatures reference mechanisms and entity variables.
@@ -443,7 +443,7 @@ Specifically:
 
 ## 4. Layer 1 Representability: Specification Framework
 
-**Property 4.1 (GDSSpec Structure is R1).** The 8-tuple
+**Property 4.1 (GDSSpec Structure is R1).** The 9-tuple
 S = (T, Sp, E, B, W, Theta, A, Sig) round-trips through OWL losslessly
 for all structural fields.
 

docs/research/paper-implementation-gap.md

@@ -266,26 +266,21 @@ states are from each other.
 
 **Paper reference:** Assumption 3.2 -- d_X : X x X -> R, a metric.
 
-**Concrete design:**
+**Implemented** in `gds-framework` (`constraints.py`):
 
 ```python
-@dataclass(frozen=True)
-class StateMetric:
-    """A metric on the state space, enabling distance-based analysis."""
+class StateMetric(BaseModel, frozen=True):
     name: str
-    metric: Callable[[dict, dict], float]   # (state_1, state_2) -> distance
-    covers: list[str]                        # entity.variable names in scope
+    variables: list[tuple[str, str]]          # (entity, variable) pairs
+    metric_type: str = ""                     # annotation: "euclidean", etc.
+    distance: Callable[[Any, Any], float] | None = None  # R3 lossy
     description: str = ""
 ```
 
-For common cases, provide built-in metrics:
+Runtime analysis in `gds-analysis` (`metrics.py`):
 
 ```python
-# Euclidean metric over all numeric state variables
-euclidean_state_metric(spec: GDSSpec) -> StateMetric
-
-# Weighted metric with per-variable scaling
-weighted_state_metric(spec: GDSSpec, weights: dict[str, float]) -> StateMetric
+trajectory_distances(spec, trajectory, metric_name=None) -> dict[str, list[float]]
 ```
 
 **Impact:**
@@ -307,28 +302,24 @@ set of immediately reachable next states.
 
 **Paper reference:** Definition 4.1 -- R(x) = union_{u in U_x} {f(x, u)}.
 
-**Concrete design:**
+**Implemented** in `gds-analysis` (`reachability.py`):
 
 ```python
 def reachable_set(
-    spec: GDSSpec,
-    state: dict,
-    f: Callable[[dict, dict], dict],   # state update function
-    input_sampler: Callable[[], Iterable[dict]],  # enumerates/samples U_x
-) -> set[dict]:
-    """Compute R(x) by evaluating f(x, u) for all admissible u."""
+    model: Model,
+    state: dict[str, Any],
+    *,
+    input_samples: list[dict[str, Any]],
+    state_key: str | None = None,
+    exhaustive: bool = False,
+    float_tolerance: float | None = None,
+) -> ReachabilityResult:
 ```
 
-For finite/discrete input spaces, this is exact enumeration. For
-continuous input spaces, this requires sampling or symbolic analysis.
-
-**Impact:**
-- First dynamical analysis capability
-- Enables "what-if" analysis: "from this state, what states can I reach?"
-- Foundation for configuration space (Step 5)
-
-**Prerequisite:** Steps 1 (U_x), 3 (metric for measuring distance).
-Requires gds-sim or equivalent runtime.
+For discrete input spaces, pass exhaustive samples with `exhaustive=True`.
+For continuous spaces, results are approximate (no coverage guarantee).
+Returns `ReachabilityResult` with `states`, `n_samples`, `n_distinct`,
+`is_exhaustive` metadata.
 
 ### Step 5: Configuration Space X_C
 
@@ -338,22 +329,17 @@ the set of states from which any other state in X_C is reachable.
 **Paper reference:** Definition 4.2 -- X_C subset X such that for each
 x in X_C, there exists x_0 and a reachable sequence reaching x.
 
-**Concrete design:**
+**Implemented** in `gds-analysis` (`reachability.py`):
 
 ```python
-def configuration_space(
-    spec: GDSSpec,
-    f: Callable,
-    input_sampler: Callable,
-    initial_states: Iterable[dict],
-    max_depth: int = 100,
-) -> set[frozenset]:
-    """Compute X_C via BFS/DFS over R(x) from initial states."""
+def reachable_graph(model, initial_states, *, input_samples, max_depth, ...) -> dict
+def configuration_space(graph: dict) -> list[set]:
+    """Iterative Tarjan SCC. Returns SCCs sorted by size (largest = X_C)."""
 ```
 
-For finite state spaces, this is graph search over the reachability
-graph. For continuous state spaces, this requires approximation
-(grid-based, interval arithmetic, or abstraction).
+`reachable_graph` builds the adjacency dict via BFS; `configuration_space`
+finds strongly connected components. For discrete systems with exhaustive
+input samples, the result is exact.
 
 **Impact:**
 - Answers "is the target state reachable from the initial condition?"
@@ -455,6 +441,7 @@ require external tooling (SymPy, JuliaReach).
 | 3 (metric) | gds-framework (constraints.py, spec.py) | **Done** — StateMetric, OWL, SHACL |
 | 4 (R(x)) | gds-analysis (reachability.py) | **Done** — `reachable_set()`, `ReachabilityResult` |
 | 5 (X_C) | gds-analysis (reachability.py) | **Done** — `configuration_space()` (iterative Tarjan SCC) |
+| 5b (B(T)) | gds-analysis (backward_reachability.py) | **Done** — `backward_reachable_set()` + `extract_isochrones()` |
 | 6 (D'F) | gds-analysis (future) | Research frontier |
 | 7 (controllability) | gds-analysis (future) | Research frontier |
 
@@ -475,11 +462,12 @@ gds-framework  <--  gds-sim  <--  gds-analysis
 
 Some paper concepts are intentionally absent for good architectural reasons:
 
-1. **Continuous-time dynamics (xdot = f(x(t)))** -- The paper presents this
-   as an alternative representation. The software is discrete-time by design.
-   Continuous-time would require a fundamentally different execution model.
-   Per RQ2 in research-boundaries.md, temporal semantics should remain
-   domain-local.
+1. ~~**Continuous-time dynamics (xdot = f(x(t)))**~~ -- **Now implemented.**
+   The `gds-continuous` package provides an ODE engine (RK45, Radau, BDF,
+   etc.) with event detection and parameter sweeps. `gds-analysis` uses it
+   for backward reachability. `gds-symbolic` compiles symbolic ODEs to
+   `gds-continuous` callables via lambdify. The discrete/continuous split
+   is bridged, not absent.
 
 2. **The full attainability correspondence F as an axiomatic foundation** --
    The paper notes (Section 3.2) that Roxin's original work defined GDS via

docs/research/representation-gap.md

@@ -170,11 +170,13 @@ boundary, seen from the outside.
 
 The canonical spectrum across five domains revealed a structural divide:
 
-| Domain | |X| | |f| | Form | Character |
+| Domain | dim(X) | dim(f) | Form | Character |
 |---|---|---|---|---|
 | OGS (games) | 0 | 0 | h = g | Stateless — pure maps |
 | Control | n | n | h = f . g | Stateful — observation + state update |
 | StockFlow | n | n | h = f . g | Stateful — accumulation dynamics |
+| Software (DFD/SM/C4/ERD) | 0 or n | 0 or n | varies | Diagram-dependent |
+| Business (CLD/SCN/VSM) | 0 or n | 0 or n | varies | Domain-dependent |
 
 Games compute equilibria. They don't write to persistent state. Even corecursive
 loops (repeated games) carry information forward as *observations*, not as

docs/research/research-boundaries.md

@@ -6,7 +6,7 @@
 
 ## Status: What Has Been Validated
 
-Three independent DSLs now compile to the same algebraic core:
+Six independent DSLs now compile to the same algebraic core:
 
 | DSL | Domain | Decision layer (g) | Update layer (f) | Canonical |
 |---|---|---|---|---|
@@ -26,7 +26,7 @@ Key structural facts:
 - Canonical `h = f ∘ g` has survived three domains with no extensions required.
 - No DSL uses `ControlAction` — all non-state-updating blocks map to `Policy`.
 - Role partition (boundary, policy, mechanism) is complete and disjoint in every case.
-- Cross-built equivalence (DSL-compiled vs hand-built) has been verified at Spec, Canonical, and SystemIR levels for all three DSLs.
+- Cross-built equivalence (DSL-compiled vs hand-built) has been verified at Spec, Canonical, and SystemIR levels for all validated DSLs.
 - OGS canonical validation confirms `f = ∅`, `X = ∅` — compositional game theory is a **degenerate dynamical system** where `h = g` (pure policy, no state transition). See [RQ3](#research-question-3-ogs-as-degenerate-dynamical-system) below.
 
 A canonical composition pattern has emerged across DSLs:
@@ -358,7 +358,7 @@ These are view-layer concerns (Layer 4). Whether to consolidate `PatternIR` into
 
 ### Background
 
-With three DSLs compiling to GDSSpec, the framework now supports two independent analytical lenses on the same system:
+With six DSLs compiling to GDSSpec, the framework now supports two independent analytical lenses on the same system:
 
 1. **Game-theoretic lens** (via PatternIR) — equilibria, incentive compatibility, strategic structure, utility propagation
 2. **Dynamical lens** (via GDSSpec/CanonicalGDS) — reachability, controllability, stability, state-space structure
@@ -437,7 +437,7 @@ Do not attempt to resolve the tension architecturally. Keep the lenses parallel.
 
 These questions mark the boundary between:
 
-- **Structural compositional modeling** — validated by three DSLs, canonical proven stable
+- **Structural compositional modeling** — validated by six DSLs, canonical proven stable
 - **Dynamical execution and control-theoretic analysis** — the next frontier
 
 They are the first genuine architectural fork points after validating canonical centrality.
@@ -450,9 +450,9 @@ Neither question requires immediate resolution. Both are triggered by concrete f
 |---|---|
 | Building a structural controllability analyzer | RQ1 (MIMO semantics) |
 | Building a shared simulation harness | RQ2 (timestep semantics) |
-| Adding a continuous-time DSL | RQ1 + RQ2 |
+| Adding a continuous-time DSL | RQ1 + RQ2 | **Done** — `gds-continuous` |
 | Adding a hybrid systems DSL | RQ1 + RQ2 |
-| Extracting state-space matrices (A, B, C, D) | RQ1 |
+| Extracting state-space matrices (A, B, C, D) | RQ1 | **Done** — `gds-symbolic` linearize |
 | Consolidating OGS PatternIR into GDSSpec | RQ3 (refactoring decision) |
 | Adding a stateless DSL (signal processing, Bayesian networks) | RQ3 (validates X=∅ pattern) |
 
@@ -467,7 +467,7 @@ After three independent domains with three distinct canonical profiles (`h = g`,
 - The role system (Boundary, Policy, Mechanism) covers all three domains without `ControlAction`.
 - The type/space system handles semantic separation across all three domains.
 - The temporal loop pattern is structurally uniform and semantically adequate for structural modeling.
-- Cross-built equivalence holds at Spec, Canonical, and SystemIR levels for all three DSLs.
+- Cross-built equivalence holds at Spec, Canonical, and SystemIR levels for all validated DSLs.
 
 The canonical form `(x, u) ↦ x'` with varying dimensionality of X now functions as a **unified transition calculus** — not merely a decomposition of dynamical systems, but a typed algebra of transition structure that absorbs stateless (games), stateful (control), and state-dominant (stockflow) formalisms under one composition substrate.
 

docs/research/semantic-web-summary.md

@@ -111,10 +111,10 @@ fields survive. Known lossy fields:
 
 | Metric | Count |
 |---|---|
-| R1 concepts (fully representable) | 12 |
+| R1 concepts (fully representable) | 13 |
 | R2 concepts (SPARQL-needed) | 3 |
-| R3 concepts (not representable) | 6 |
-| SHACL shapes | 13 |
+| R3 concepts (not representable) | 7 |
+| SHACL shapes | 18 |
 | SPARQL templates | 7 |
 | Verification checks expressible in SHACL | 6 of 15 |
 | Verification checks expressible in SPARQL | 6 more |
@@ -131,6 +131,23 @@ graph, R1) and `U_behav` (constraint predicate, R3) for ontological
 engineering. Same for `StateMetric` and `TransitionSignature`. The
 canonical decomposition `h = f . g` IS faithful to the paper.
 
+## Open Question: Promoting Common Constraints to R2
+
+Zargham's feedback: *"We can probably classify them as two different
+kinds of predicates -- those associated with the model structure
+(owl/shacl/sparql) and those associated with the runtime."*
+
+Currently all `TypeDef.constraint` callables are treated as R3 (lossy).
+But many common constraints ARE expressible in SHACL:
+
+- `lambda x: x >= 0` --> `sh:minInclusive 0`
+- `lambda x: 0 <= x <= 1` --> `sh:minInclusive 0` + `sh:maxInclusive 1`
+- `lambda x: x in {-1, 0, 1}` --> `sh:in (-1 0 1)`
+
+A constraint classifier could promote these from R3 to R2, making them
+round-trippable through Turtle. The general case (arbitrary callable)
+remains R3. See #152 for the design proposal.
+
 ## Files
 
 - `packages/gds-owl/` -- the full export/import/SHACL/SPARQL implementation

docs/research/verification-plan.md

@@ -153,7 +153,7 @@ are inherently coupled.
 
 | Artifact | Location | Format |
 |---|---|---|
-| R3 undecidability proof | `docs/research/verification/r3-undecidability.tex` | LaTeX |
+| R3 undecidability proof | `docs/research/verification/r3-undecidability.md` | Markdown + LaTeX |
 | R1/R2 completeness argument | `docs/research/verification/representability-proof.md` | Markdown |
 
 ### Dependencies
@@ -243,7 +243,9 @@ Prove: if the constraint set `C(x, t; g)` is compact, convex, and continuous,
 then an attainability correspondence exists.
 
 This is a runtime/R3 concern -- it requires evaluating `f` on concrete state.
-Implementation target: future `gds-analysis` package.
+The `gds-analysis` package now exists with reachability (`reachable_set`,
+`configuration_space`, `backward_reachable_set`) but existence proofs
+require additional analytical machinery beyond trajectory sampling.
 
 ### 4b. Local Controllability (Paper Theorem 4.4)
 
@@ -253,8 +255,9 @@ is 0-controllable from a neighborhood around equilibrium.
 ### 4c. Connection to Bridge Proposal
 
 Steps 3-7 of the bridge proposal in [paper-implementation-gap.md](paper-implementation-gap.md)
-map to this phase. Steps 1-2 (AdmissibleInputConstraint, TransitionSignature)
-are already implemented and provide the structural skeleton.
+map to this phase. Steps 1-5 are complete (AdmissibleInputConstraint,
+TransitionSignature, StateMetric, reachable_set, configuration_space).
+Steps 6-7 remain open (#142).
 
 ### Dependencies
 

packages/gds-analysis/CLAUDE.md

@@ -6,17 +6,19 @@
 
 - **Import**: `import gds_analysis`
 - **Dependencies**: `gds-framework>=0.2.3`, `gds-sim>=0.1.0`
+- **Optional**: `[continuous]` for `gds-continuous[scipy]` + numpy (backward reachability)
 
 ## Architecture
 
-Four modules, each bridging one aspect of structural specification to runtime:
+Five modules, each bridging one aspect of structural specification to runtime:
 
 | Module | Function | Paper reference |
 |--------|----------|-----------------|
 | `adapter.py` | `spec_to_model(spec, policies, sufs, ...)` → `gds_sim.Model` | — |
 | `constraints.py` | `guarded_policy(policy_fn, constraint)` → wrapped policy | Def 2.5 |
-| `metrics.py` | `trajectory_distances(results, spec)` → distance matrix | — |
-| `reachability.py` | `reachable_set(spec, model, state, inputs)` → R(x) | Def 4.1, 4.2 |
+| `metrics.py` | `trajectory_distances(results, spec)` → distance matrix | Assumption 3.2 |
+| `reachability.py` | `reachable_set(model, state, inputs)` → R(x) | Def 4.1, 4.2 |
+| `backward_reachability.py` | `backward_reachable_set(dynamics, ...)` → B(T) | Def 4.1 (backward) |
 
 ### spec_to_model adapter