feat(tropical-bridge): wire Isabelle tropical proofs into VCL ProofConsonance

Adds the first live connection between the formally verified tropical matrix
theorems in tropical-resource-typing/ and the VeriSimDB/KRL stack.

New files:
- impl/tropical/TropicalMatrix.jl — min-plus semiring + bellman_ford_matrix;
  direct Julia mirror of tropm_mat_pow and bellman_ford (Tropical_Matrices_Full.thy)
- impl/tropical/TangleGraph.jl — TangleIR DT-code → tropical adjacency matrix;
  Reidemeister-I neighbourhood (RI⁻); RII/RIII stubs for KnotTheory.jl wire-up
- docs/TROPICAL-BRIDGE.adoc — formal correspondence table, gap register, next steps

Updated:
- impl/vcl/Query.jl — adds ProofConsonance clause (two octad ids + depth bound)
- impl/vcl/Prover.jl — prove(ProofConsonance) dispatches to Bellman-Ford path search
- examples/krladapter_integration.jl — demo_consonance() exercises all four cases

All four demo cases pass: trivial identity, DT-code match, RI-equivalent path
(1 move), and correct FAIL for trefoil vs figure-eight at RI-only depth.

Formal backing: bellman_ford (OFFICIAL SORRY 2) is still pending in Isabelle;
the Julia implementation is algorithmically justified by tropm_mat_pow_eq_sum_walks
(proved). Certificate upgrades to machine-checked once the sorry is closed.

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

Author: hyperpolymath

verisim-modular-experiment/docs/TROPICAL-BRIDGE.adoc

@@ -0,0 +1,147 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+= Tropical Bridge: Isabelle Proofs ↔ Julia Consonance Checker
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+2026-04-11
+:toc:
+:toc-placement: preamble
+:sectnums:
+:icons: font
+
+[.lead]
+This document is the formal correspondence table between the Isabelle/HOL
+theorems in `tropical-resource-typing/` and the Julia implementation in
+`impl/tropical/`.  It specifies what the Julia code is *justified by* and
+what gaps remain.
+
+== The Claim
+
+`ProofConsonance` in VCL checks tangle equivalence by asking:
+
+____
+Is the minimum number of Reidemeister moves from tangle A to tangle B
+finite (within the modelled move set)?
+____
+
+The answer is computed by `bellman_ford_matrix` in `TropicalMatrix.jl`,
+which is a direct Julia mirror of the Isabelle `bellman_ford` theorem.
+
+== Formal Correspondence Table
+
+[cols="1,2,2"]
+|===
+|Isabelle (tropical-resource-typing/) |Julia (impl/tropical/) |Notes
+
+|`tropical_min` type +
+`PosInf`, `Fin' n`
+|`Tropical` struct +
+`TROP_ZERO` (Inf), `Tropical(n)`
+|Min-plus carrier.  `Tropical_v2.thy`.
+
+|`a + b = min a b` on `tropical_min`
+|`trop_add(a, b) = min(a.val, b.val)`
+|`tropm_add_idem: a ⊕ a = a` guarantees idempotency.
+
+|`a * b = a + b` on `tropical_min` +
+(∞ absorbing)
+|`trop_mul(a, b)` — returns TROP_ZERO if either is ∞
+|`Tropical_v2.thy` instances.
+
+|`tropm_mat_id n`
+|`trop_mat_id(n)`
+|Diagonal TROP_ONE, off-diagonal TROP_ZERO.
+
+|`tropm_mat_mul n A B i j ≡ ∑ k. A i k * B k j`
+|`trop_mat_mul(A, B)[i,j] = min_k(A[i,k] + B[k,j])`
+|Direct transliteration.
+
+|`tropm_mat_pow n A k`
+|`trop_mat_pow(A, k)`
+|Right-iterated product; `A^0 = I`.
+
+|`tropm_mat_close n A i j ≡ A i j + tropm_mat_id n i j`
+|`trop_mat_close(A)`
+|Entry-wise min with identity.
+
+|`tropm_mat_pow_eq_sum_walks` +
+(proved — was OFFICIAL SORRY 1)
+|Used implicitly: `bellman_ford_matrix` correctness rests on this.
+|`A^k[i,j]` = sum over walks of length k.
+
+|`bellman_ford` +
+(OFFICIAL SORRY 2 — pending)
+|`bellman_ford_matrix(A)` — returns `(I ⊕ A)^{n-1}`
+|**See gap table below.**
+|===
+
+== Gap Table
+
+[cols="1,3,1"]
+|===
+|Gap |Impact |Mitigation
+
+|`bellman_ford` sorry not yet closed
+|Julia `bellman_ford_matrix` is algorithmically correct but lacks
+ machine-checked correctness certificate for the closed-form claim.
+ The algorithm is correct by the matrix-power walk interpretation
+ (`tropm_mat_pow_eq_sum_walks`, proved); only the no-negative-cycle
+ optimality claim is unverified.
+|Planned Session 2 of tropical proof work.
+
+|RI only (no RII/RIII)
+|`TangleGraph.v0.1` models RI moves only.  Two tangles related by RII
+ or RIII moves will receive INCONCLUSIVE (FAIL with reason string), not PASS.
+|`_rii_neighbors` and `_riii_neighbors` stubs in `TangleGraph.jl`; wire
+ to `KnotTheory.jl` once KRLAdapter is linked.
+
+|Infinite Reidemeister graph
+|The full Reidemeister move graph is infinite.  `build_consonance_graph`
+ bounds the BFS at `depth` hops.  Deep equivalences are undecidable in
+ general; the prover is sound but not complete.
+|Use knot invariants (Jones polynomial via `KnotTheory.jl`) as a
+ fast-fail before the tropical path search.
+|===
+
+== The Architecture
+
+----
+Isabelle/HOL                Julia (this package)       VCL layer
+------------------          ----------------------     ---------
+Tropical_v2.thy             TropicalMatrix.jl          Query.jl
+  tropical_min type   ───►    Tropical struct           ProofConsonance
+  add / mul ops               trop_add / trop_mul
+
+Tropical_Matrices_Full.thy  TropicalMatrix.jl
+  tropm_mat_pow       ───►    trop_mat_pow
+  tropm_mat_close             trop_mat_close
+  bellman_ford        ─ ─ ►   bellman_ford_matrix       Prover.jl
+  (sorry pending)               (implemented;            prove(ProofConsonance)
+                                 formal cert pending)
+                              TangleGraph.jl
+                                build_consonance_graph
+                                dt_codes_from_blob
+----
+
+== Usage
+
+[source,julia]
+----
+# Construct ProofConsonance and evaluate
+clause = ProofConsonance(octad_id_trefoil, octad_id_fig8, 3)
+result = prove(clause, store, manager)
+# → VerdictPass("Reidemeister path: 1 move(s) [tropical Bellman-Ford, ...]")
+# or VerdictFail("no path found within depth=3 [RI only; ...]")
+----
+
+== Next Steps
+
+1. *Close `bellman_ford` sorry* (Session 2, `tropical-resource-typing/`).
+   This upgrades the formal status from "algorithmically justified" to
+   "machine-checked."
+2. *Wire RII/RIII* — implement `_rii_neighbors` and `_riii_neighbors` in
+   `TangleGraph.jl` using `KnotTheory.jl` PD-code manipulations.
+3. *Tropical determinant* — add `Tropical_Determinants.thy` (tropical
+   permanent = max-weight perfect matching); expose as `ProofOptimalAssignment`
+   in VCL for optimal tangle adapter chain selection.
+4. *Jones fast-fail* — before Bellman-Ford, check `Jones(dt_a) ≠ Jones(dt_b)`
+   via `KnotTheory.jl` for an immediate disequivalence certificate.

verisim-modular-experiment/examples/krladapter_integration.jl

@@ -20,13 +20,18 @@ include(joinpath(@__DIR__, "..", "impl", "Crypto.jl"))
 include(joinpath(@__DIR__, "..", "impl", "drift", "Metrics.jl"))
 include(joinpath(@__DIR__, "..", "impl", "VerisimCore.jl"))
 include(joinpath(@__DIR__, "..", "impl", "FederationManager.jl"))
+# Tropical modules must be loaded before VCLProver (Prover dispatches to them)
+include(joinpath(@__DIR__, "..", "impl", "tropical", "TropicalMatrix.jl"))
+include(joinpath(@__DIR__, "..", "impl", "tropical", "TangleGraph.jl"))
 include(joinpath(@__DIR__, "..", "impl", "vcl", "Query.jl"))
 include(joinpath(@__DIR__, "..", "impl", "vcl", "Prover.jl"))
 
 using .Crypto
 using .VerisimCore
 using .Metrics
 using .FederationManager
+using .TropicalMatrix
+using .TangleGraph
 using .VCLQuery
 using .VCLProver
 
@@ -132,7 +137,76 @@ function demo()
     println("\n=== Client satisfied by Core alone. No Federable shapes needed. ===")
 end
 
+# -----------------------------------------------------------------------
+# Phase 5: Tropical consonance demo
+# -----------------------------------------------------------------------
+
+"""
+demo_consonance()
+
+Demonstrates PROOF CONSONANCE using tropical Bellman-Ford:
+
+1. Trivial case: same octad id → immediate PASS.
+2. Same DT code (same tangle, different provenance) → fast-path PASS.
+3. RI-equivalent tangles (differ by one isolated crossing) → tropical PASS.
+4. Unrelated tangles (trefoil vs figure-eight) → tropical FAIL (RI only).
+
+Formal backing: `bellman_ford` in Tropical_Matrices_Full.thy.
+See impl/tropical/TropicalMatrix.jl for the Julia mirror of the Isabelle proof.
+"""
+function demo_consonance()
+    println("\n=== PROOF CONSONANCE — tropical Bellman-Ford demo ===\n")
+
+    store   = Store()
+    manager = Manager()
+
+    # Helper: store a tangle and return its octad id
+    function store_tangle(t::TangleIRSurrogate)
+        id   = tangle_octad_id(t)
+        blob = tangle_to_semantic(t)
+        enrich!(store, id, :semantic, blob, "krl-demo")
+        id
+    end
+
+    # Case 1: same octad — trivially consonant
+    println("--- Case 1: same octad id ---")
+    trefoil = TangleIRSurrogate("trefoil", [4, 6, 2], :user, "B_1^3")
+    id_t    = store_tangle(trefoil)
+    r1 = prove(ProofConsonance(id_t, id_t), store, manager)
+    println("  Result: ", r1)
+
+    # Case 2: same DT code, different provenance — fast-path match
+    println("\n--- Case 2: same DT code, different provenance ---")
+    trefoil2 = TangleIRSurrogate("trefoil-rewritten", [4, 6, 2], :rewritten,
+                                  "Reidemeister III applied")
+    id_t2    = store_tangle(trefoil2)
+    r2 = prove(ProofConsonance(id_t, id_t2), store, manager)
+    println("  Result: ", r2)
+
+    # Case 3: RI-equivalent — trefoil with one RI⁺ crossing added then removed
+    # Simulated: DT code [4, 6, 2] vs [4, 6, 2] with an extra RI pair ±8
+    # In practice RI⁺ on trefoil gives a 4-crossing diagram with an ear
+    println("\n--- Case 3: RI-equivalent tangles ---")
+    # Synthetic RI⁺ of trefoil: prepend an isolated ±2 pair
+    trefoil_ri = TangleIRSurrogate("trefoil-ri", [2, -2, 4, 6, 2], :derived,
+                                    "trefoil + RI ear")
+    id_ri = store_tangle(trefoil_ri)
+    r3 = prove(ProofConsonance(id_t, id_ri, 3), store, manager)
+    println("  Result: ", r3)
+
+    # Case 4: different knots — trefoil [4,6,2] vs figure-eight [4,8,12,2,10,6]
+    println("\n--- Case 4: trefoil vs figure-eight (expected FAIL at RI depth) ---")
+    fig8 = TangleIRSurrogate("figure-eight", [4, 8, 12, 2, 10, 6], :user,
+                               "figure-eight knot")
+    id_f8 = store_tangle(fig8)
+    r4 = prove(ProofConsonance(id_t, id_f8), store, manager)
+    println("  Result: ", r4)
+
+    println("\n=== Consonance demo complete ===")
+end
+
 # Run the demo when executed as a script.
 if abspath(PROGRAM_FILE) == @__FILE__
     demo()
+    demo_consonance()
 end