From 5e5ed9aa446903fc59efebf26de0e66137e9555d Mon Sep 17 00:00:00 2001 From: rohan Date: Sat, 28 Mar 2026 19:59:16 +0530 Subject: [PATCH] docs: update research docs for completed Steps 3-5 and add nav entries paper-implementation-gap.md: Steps 3-5 marked DONE with actual package locations (gds-framework for Step 3, gds-analysis for Steps 4-5). Prose updated to reflect gds-analysis as an existing package. formal-representability.md: Added StateMetric to G_struct (d_X_struct, R1) and G_behav (d_X_behav distance callable, R3) classifications. mkdocs.yml: Added verification plan, R3 proofs, R1/R2 decidability, research journal, and paper gap analysis to Design & Research nav. --- docs/research/formal-representability.md | 2 ++ docs/research/paper-implementation-gap.md | 30 +++++++++++------------ mkdocs.yml | 6 +++++ 3 files changed, 23 insertions(+), 15 deletions(-) diff --git a/docs/research/formal-representability.md b/docs/research/formal-representability.md index 4057d1b..2eae545 100644 --- a/docs/research/formal-representability.md +++ b/docs/research/formal-representability.md @@ -643,6 +643,7 @@ G_struct concepts and their tiers: - Space/entity structure: R1 (Property 4.1) - Admissibility dependency graph (U_x_struct): R1 (Property 4.5) - Transition read dependencies (f_read): R1 (Property 4.6) +- State metric variable declarations (d_X_struct): R1 (Assumption 3.2) - Acyclicity: R2 (Section 5.1, G-006) - Completeness/determinism: R2 (Section 5.2, SC-001, SC-002) - Reference validation (dangling wirings): R2 (Section 5.1, G-004) @@ -651,6 +652,7 @@ G_behav concepts and their tiers: - Transition functions: R3 (Property 4.4, f_behav) - Constraint predicates: R3 (Property 4.2, general case) - Admissibility predicates (U_x_behav): R3 (Property 4.5) +- State metric distance callable (d_X_behav): R3 (Assumption 3.2) - Auto-wiring process: R3 (Property 3.2) - Construction validation: R3 (Proposition 3.4) - Scheduling semantics: R3 (not stored in GDSSpec — external) diff --git a/docs/research/paper-implementation-gap.md b/docs/research/paper-implementation-gap.md index a32c710..d50781a 100644 --- a/docs/research/paper-implementation-gap.md +++ b/docs/research/paper-implementation-gap.md @@ -422,27 +422,27 @@ This connects directly to RQ1 (MIMO semantics) in research-boundaries.md. ## 5. Dependency Graph ``` -Step 1: AdmissibleInputConstraint (U_x declaration) -- DONE (gds-framework v0.2.3) -Step 2: TransitionSignature (f|_x declaration) -- DONE (gds-framework v0.2.3) +Step 1: AdmissibleInputConstraint (U_x declaration) -- DONE (gds-framework) +Step 2: TransitionSignature (f|_x declaration) -- DONE (gds-framework) | v -Step 3: StateMetric (d_X on X) -- requires runtime +Step 3: StateMetric (d_X on X) -- DONE (gds-framework) | v -Step 4: Reachable Set R(x) -- requires Steps 1, 3 +Step 4: Reachable Set R(x) -- DONE (gds-analysis) | v -Step 5: Configuration Space X_C -- requires Step 4 +Step 5: Configuration Space X_C -- DONE (gds-analysis) | v Step 6: Contingent Derivative D'F -- research frontier Step 7: Local Controllability -- research frontier ``` -Steps 1-2 are implemented in gds-framework with full OWL/SHACL support -in gds-owl. Steps 3-5 require runtime evaluation and belong in gds-sim -or a new gds-analysis package. Steps 6-7 are research-level and may -warrant a dedicated analytical package or external tooling integration. +Steps 1-3 are structural annotations in gds-framework with full OWL/SHACL +support in gds-owl. Steps 4-5 are runtime analysis in gds-analysis, which +bridges gds-framework to gds-sim. Steps 6-7 are research-level and may +require external tooling (SymPy, JuliaReach). --- @@ -452,13 +452,13 @@ warrant a dedicated analytical package or external tooling integration. |---|---|---| | 1 (U_x) | gds-framework (constraints.py, spec.py) | **Done** — SC-008, OWL, SHACL | | 2 (f\|_x signature) | gds-framework (constraints.py, spec.py, canonical.py) | **Done** — SC-009, OWL, SHACL | -| 3 (metric) | gds-sim or gds-analysis | Requires concrete state values | -| 4 (R(x)) | gds-analysis (new) | Dynamical computation | -| 5 (X_C) | gds-analysis | Dynamical computation | -| 6 (D'F) | gds-analysis | Research frontier | -| 7 (controllability) | gds-analysis | Research frontier | +| 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) | +| 6 (D'F) | gds-analysis (future) | Research frontier | +| 7 (controllability) | gds-analysis (future) | Research frontier | -A new `gds-analysis` package would depend on both `gds-framework` +The `gds-analysis` package depends on both `gds-framework` (for GDSSpec, CanonicalGDS) and `gds-sim` (for state evaluation), sitting at the top of the dependency graph: diff --git a/mkdocs.yml b/mkdocs.yml index 16dd1da..ce6d554 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -381,5 +381,11 @@ nav: - Layer 0 Milestone: guides/architecture-milestone-layer0.md - DSL Roadmap: guides/dsl-roadmap.md - Research Boundaries: research/research-boundaries.md + - Paper Implementation Gap: research/paper-implementation-gap.md - View Stratification: guides/view-stratification.md - Ecosystem: framework/ecosystem.md + - Formal Verification: + - Verification Plan: research/verification-plan.md + - R3 Non-Representability: research/verification/r3-undecidability.md + - R1/R2 Decidability: research/verification/representability-proof.md + - Research Journal: research/journal.md