docs: update research docs and add nav for verification framework

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)

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:
 

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