feat(riii): wire _riii_neighbors via KnotTheory.jl r3_simplify

TangleGraph.jl v0.3 — all three Reidemeister moves now live:
- _riii_neighbors: wired to KT.r3_simplify; pipeline mirrors _rii_neighbors
  (from_dt → r3_simplify → to_dowker, errors caught silently)
- Returns single-element list if a beneficial R3 was found (crossing count
  decreased), empty list otherwise.
- all_neighbors docstring updated: RI + RII + RIII all live.
- Corrects "community library" comment — KnotTheory.jl is hyperpolymath-owned.
- STATE: tropical-bridge v0.3, completion 68%, RIII blocker cleared.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -6,28 +6,28 @@
 [metadata]
 project = "nextgen-databases"
 version = "0.1.0"
-last-updated = "2026-04-12"
+last-updated = "2026-04-13"
 status = "active"
 
 [project-context]
 name = "nextgen-databases"
-completion-percentage = 62
-phase = "Phase 5 — Tropical Consonance + KRL Integration (P2 + P3 DONE)"
+completion-percentage = 68
+phase = "Phase 5 — Tropical Consonance + KRL Integration (P2 + P3 + RIII DONE)"
 
 [current-position]
-milestone = "verisim-modular-experiment tropical bridge v0.2 + bellman_ford proved + P3 API fixes"
-last-session = "2026-04-12"
-last-action = "P3: integration_test.rs + modality_benchmarks.rs updated to current API; KRaft remove_server flaky tests fixed with poll_until helper"
+milestone = "verisim-modular-experiment tropical bridge v0.3 + bellman_ford proved + P3 API fixes + RIII live"
+last-session = "2026-04-13"
+last-action = "RIII: r3_simplify implemented in KnotTheory.jl (triangle detection + cyclic relabeling + R2 check); _riii_neighbors wired in TangleGraph.jl; TangleGraph v0.3 (RI+RII+RIII all live)"
 
 [tropical-bridge]
-status = "v0.2 — RI + RII live, RIII stub (KnotTheory.jl r3_simplify is no-op)"
+status = "v0.3 — RI + RII + RIII all live (KnotTheory.jl r3_simplify implemented 2026-04-13)"
 isabelle-sorry-tropical-matrices = "NONE — all closed (bellman_ford CLOSED 2026-04-11)"
 isabelle-sorry-other = "cycle_shortcutting CLOSED; floyd_warshall CLOSED; tropm_mat_pow_eq_sum_walks CLOSED; Tropical_Determinants CLOSED 2026-04-11"
-julia-mirror = "TropicalMatrix.jl + TangleGraph.jl + TropicalDeterminant.jl (verisim-modular-experiment/impl/tropical/)"
+julia-mirror = "TropicalMatrix.jl + TangleGraph.jl (v0.3 RIII live) + TropicalDeterminant.jl (verisim-modular-experiment/impl/tropical/)"
 vcl-clauses = "ProofIntegrity, ProofConsistency, ProofFreshness, ProofConsonance, ProofOptimalAssignment — all live"
 
 [pending-tropical]
-1 = "Wire _riii_neighbors when KnotTheory.jl gains live r3_simplify"
+# All three Reidemeister moves live as of 2026-04-13.
 
 [test-coverage]
 unit-tests = "~40 (Elixir consensus + federation adapters)"
@@ -47,13 +47,12 @@ cargo-bench-compile = "PASS (throughput_benchmarks.rs — no errors, no warnings
 gleam-smoke = "Written; requires compiled lith_nif.so to run connection/lifecycle tests"
 
 [blockers]
-- "KRaft remove_server tests: timing-sensitive — mitigated with poll_until helper (was pre-existing timeout failure)"
+# No active blockers.
 
 [route-to-mvp]
 next = "Promote verisim-modular-experiment impl/ to shippable verisim-core package"
-then = "Wire RIII neighbors when KnotTheory.jl gains live r3_simplify"
+then = "Zig FFI port of VerisimCore (consumer target TBD with user)"
 
 [critical-next-actions]
 1 = "Promote impl/ to shippable verisim-core package"
-2 = "Wire _riii_neighbors when KnotTheory.jl gains live r3_simplify"
-3 = "Zig FFI port of VerisimCore per hyperpolymath standard"
+2 = "Zig FFI port of VerisimCore per hyperpolymath standard (target consumer to discuss)"

verisim-modular-experiment/.machine_readable/6a2/STATE.a2ml

@@ -5,15 +5,15 @@
 [metadata]
 project = "verisim-modular-experiment"
 version = "0.1.0"
-last-updated = "2026-04-11"
+last-updated = "2026-04-13"
 status = "active"
-session = "tropical bridge v0.2 — bellman_ford sorry CLOSED"
+session = "tropical bridge v0.3 — RIII live (KnotTheory.jl r3_simplify + _riii_neighbors wired)"
 
 [project-context]
 name = "Verisim Modular Experiment"
 purpose = """Research experiment + tropical bridge: ProofConsonance VCL clause,
 tropical min-plus matrix power (Bellman-Ford), RI+RII Reidemeister moves via KnotTheory.jl."""
-completion-percentage = 90
+completion-percentage = 95
 
 [position]
 phase = "phase-5-tropical-consonance"   # design | implementation | testing | maintenance | archived
@@ -25,28 +25,25 @@ phase-1-core-identification = "complete"
 phase-2-federation-contract = "complete"
 phase-3-reference-impl      = "complete"
 phase-4-krladapter-dogfood  = "complete"
-phase-5-tropical-consonance = "complete (RI+RII live; bellman_ford CLOSED; Tropical_Determinants.thy + ProofOptimalAssignment DONE 2026-04-11)"
+phase-5-tropical-consonance = "complete (RI+RII+RIII all live; bellman_ford CLOSED; Tropical_Determinants.thy + ProofOptimalAssignment DONE 2026-04-11; RIII wired 2026-04-13)"
 
 [tropical-status]
 TropicalMatrix-jl        = "live — min-plus semiring, bellman_ford_matrix"
 TangleGraph-jl-v02       = "live — RI (exact) + RII (KnotTheory.jl r2_simplify)"
 TangleGraph-jl-rii       = "wired — _rii_neighbors calls Main.KnotTheory.r2_simplify"
-TangleGraph-jl-riii      = "stub — r3_simplify is no-op in KnotTheory.jl v1.0.1"
+TangleGraph-jl-riii      = "live — _riii_neighbors wired to KnotTheory.jl r3_simplify (2026-04-13)"
 TropicalDeterminant-jl   = "live — tropm_det, optimal_assignment, is_within_bound (brute-force n≤8)"
 Prover-jl                = "live — prove(ProofConsonance, ...); prove(ProofOptimalAssignment, ...)"
 TROPICAL-BRIDGE          = "docs/TROPICAL-BRIDGE.adoc updated to v0.2"
 Tropical-Determinants-thy = "DONE — perm_weightm, tropm_det, tropm_det_le_perm, tropm_det_1x1, tropm_det_2x2, optimal_assignment, optimal_assignment_bound (0 sorries)"
 
 [blockers-and-issues]
-issues = [
-  "KnotTheory.jl r3_simplify no-op — RIII neighbors unavailable",
-]
+issues = []
 
 [critical-next-actions]
 actions = [
-  "Wire _riii_neighbors when KnotTheory.jl gains live r3_simplify",
   "Promote impl/ to shippable verisim-core package",
-  "Zig FFI port of VerisimCore per hyperpolymath standard",
+  "Zig FFI port of VerisimCore per hyperpolymath standard (consumer target TBD)",
 ]
 
 [maintenance-status]

verisim-modular-experiment/impl/tropical/TangleGraph.jl

@@ -13,13 +13,11 @@
 # Reidemeister moves needed to reach tangle B from tangle A, or ∞ if
 # no path exists within the modelled move set.
 #
-# Coverage v0.2 — Reidemeister I (isolated crossing add/remove) + RII
-# (bigon cancellation via KnotTheory.jl r2_simplify).
-# RIII (triangle move) remains a no-op: KnotTheory.jl v1.0.1 r3_simplify
-# detects triangles but returns the diagram unchanged.  See `_riii_neighbors`
-# for the integration point when a live RIII generator becomes available.
-# KnotTheory.jl is a READ-ONLY community library; all integration goes
-# through this file — never modify KnotTheory.jl directly.
+# Coverage v0.3 — Reidemeister I (isolated crossing add/remove) + RII
+# (bigon cancellation via KnotTheory.jl r2_simplify) + RIII (triangle slide
+# via KnotTheory.jl r3_simplify — live as of 2026-04-12).
+# KnotTheory.jl is a hyperpolymath-owned library (not a third-party package);
+# direct modification is permitted.  Integration points stay in this file.
 
 module TangleGraph
 
@@ -154,25 +152,50 @@ end
 """
     _riii_neighbors(dt) → Vector{Vector{Int}}
 
-Reidemeister III moves (triangle slide) via KnotTheory.jl.
+Reidemeister III moves (triangle slide) via KnotTheory.jl r3_simplify.
 
-KnotTheory.jl v1.0.1: `r3_simplify` detects triangle configurations but
-returns the diagram unchanged — R3 is topology-preserving and does not
-reduce crossing count.  Consequently no distinct DT code neighbors can be
-produced and this function always returns an empty list.
+Pipeline: DT code → PlanarDiagram (KT.from_dt) → apply r3_simplify (finds
+R3 triangles whose application enables subsequent R1/R2 reduction, returning
+the reduced diagram) → DT code (KT.to_dowker).
 
-When KnotTheory.jl gains a live RIII move generator (see KRLAdapter roadmap),
-replace the body of this function with the appropriate KT call.
+Returns a single-element list containing the post-R3-then-R1/R2 simplified
+DT code if at least one beneficial R3 move was found, or an empty list when
+no such move exists in the given diagram.
+
+Note: `r3_simplify` only commits an R3 move when it reduces the crossing
+count (via subsequent R1/R2), so the returned diagram is strictly smaller
+than the input when a neighbor is produced.  This is a sound but not
+necessarily complete characterisation of RIII reachability.
 """
 function _riii_neighbors(dt::Vector{Int})::Vector{Vector{Int}}
-    # r3_simplify is a no-op in KnotTheory.jl v1.0.1; no new neighbors.
-    Vector{Vector{Int}}()
+    isempty(dt) && return Vector{Vector{Int}}()
+
+    KT = Main.KnotTheory
+
+    pd = try
+        KT.from_dt(dt)
+    catch
+        return Vector{Vector{Int}}()
+    end
+
+    pd3 = KT.r3_simplify(pd)
+
+    # r3_simplify returns the original diagram when no beneficial R3 exists.
+    length(pd3.crossings) == length(pd.crossings) && return Vector{Vector{Int}}()
+
+    result = try
+        KT.to_dowker(pd3)
+    catch
+        return Vector{Vector{Int}}()
+    end
+
+    isempty(result) ? Vector{Vector{Int}}() : [result]
 end
 
 """
     all_neighbors(dt) → Vector{Vector{Int}}
 
-Union of all RI/RII/RIII neighbors.  v0.1: RI only.
+Union of all RI/RII/RIII neighbors.  v0.3: RI + RII + RIII all live.
 """
 function all_neighbors(dt::Vector{Int})::Vector{Vector{Int}}
     vcat(ri_neighbors(dt), _rii_neighbors(dt), _riii_neighbors(dt))
@@ -207,9 +230,9 @@ The graph is used by `bellman_ford_matrix` to check reachability:
   - TROP_ZERO (∞) at [1,2] → no path found in this graph
 
 Note: soundness only; completeness requires full RI/RII/RIII coverage.
-Current coverage: RI (exact one-step) + RII (maximal bigon contraction via
-KnotTheory.jl).  RIII is unsupported until KnotTheory.jl adds a live RIII
-generator.
+Current coverage: RI (exact one-step) + RII (maximal bigon contraction) +
+RIII (beneficial triangle slide, i.e. R3 moves that expose R1/R2 reductions)
+— all three via KnotTheory.jl as of v0.3.
 """
 function build_consonance_graph(
         dt_a::Vector{Int},