feat(vcl/tropical): ProofOptimalAssignment clause + TropicalDeterminant.jl

P2 of the tropical bridge: connects Tropical_Determinants.thy to the VCL
query layer and the Julia experiment implementation.

New files:
  impl/tropical/TropicalDeterminant.jl — Julia mirror of Tropical_Determinants.thy;
    tropm_det (brute-force n≤8), optimal_assignment, is_within_bound

Updated:
  impl/vcl/Query.jl — ProofOptimalAssignment clause (octad_id, n, bound)
  impl/vcl/Prover.jl — prove(ProofOptimalAssignment, ...) dispatching to
    TropicalDeterminant.optimal_assignment; cost matrix decoded from Semantic blob
  test/test_vcl.jl — 6 new ProofOptimalAssignment tests (1×1, 2×2, asymmetric,
    not-found, no-semantic, n>8); tropical module includes added
  examples/krladapter_integration.jl — TropicalDeterminant include added
  STATE.a2ml (both) — P2 marked complete; completion 85→90% / 50→55%

Formal backing: Tropical_Determinants.thy::optimal_assignment_bound
  tropm_det n A ≤ B  ↔  ∃ π. π permutes {..<n} ∧ perm_weightm n A π ≤ B

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -1,7 +1,7 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # STATE.a2ml — Project state checkpoint
 # Converted from STATE.scm on 2026-03-15
-# Updated: 2026-04-11 — bellman_ford sorry CLOSED; all Isabelle sorries gone
+# Updated: 2026-04-11 — bellman_ford CLOSED; Tropical_Determinants.thy + ProofOptimalAssignment DONE
 
 [metadata]
 project = "nextgen-databases"
@@ -11,24 +11,23 @@ status = "active"
 
 [project-context]
 name = "nextgen-databases"
-completion-percentage = 50
-phase = "Phase 5 — Tropical Consonance + KRL Integration"
+completion-percentage = 55
+phase = "Phase 5 — Tropical Consonance + KRL Integration (P2 DONE)"
 
 [current-position]
 milestone = "verisim-modular-experiment tropical bridge v0.2 + bellman_ford proved"
 last-session = "2026-04-11"
-last-action = "VQL→VCL rename (303 files); P1 hardening: VCLTypeChecker ArgumentError fixed, null-byte sanitisation added to VCLBridge tokenizer"
+last-action = "P2: Tropical_Determinants.thy (sorry-free), TropicalDeterminant.jl, ProofOptimalAssignment VCL clause + 6 tests"
 
 [tropical-bridge]
 status = "v0.2 — RI + RII live, RIII stub (KnotTheory.jl r3_simplify is no-op)"
 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"
-julia-mirror = "TropicalMatrix.jl + TangleGraph.jl (verisim-modular-experiment/impl/tropical/)"
-vcl-clauses = "ProofIntegrity, ProofConsistency, ProofFreshness, ProofConsonance — all live"
+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/)"
+vcl-clauses = "ProofIntegrity, ProofConsistency, ProofFreshness, ProofConsonance, ProofOptimalAssignment — all live"
 
 [pending-tropical]
-1 = "Add Tropical_Determinants.thy + ProofOptimalAssignment VCL clause"
-2 = "Wire _riii_neighbors when KnotTheory.jl gains live r3_simplify"
+1 = "Wire _riii_neighbors when KnotTheory.jl gains live r3_simplify"
 
 [test-coverage]
 unit-tests = "~40 (Elixir consensus + federation adapters)"
@@ -52,10 +51,9 @@ gleam-smoke = "Written; requires compiled lith_nif.so to run connection/lifecycl
 - "modality_benchmarks.rs uses old API — does not compile (pre-existing)"
 
 [route-to-mvp]
-next = "Add Tropical_Determinants.thy + ProofOptimalAssignment VCL clause"
-then = "Update integration_test.rs to current API"
+next = "Update integration_test.rs to current API"
 then = "Update modality_benchmarks.rs to current API"
 
 [critical-next-actions]
-1 = "Tropical_Determinants.thy new file — permanent = optimal assignment"
-2 = "Update integration_test.rs to current API"
+1 = "Update integration_test.rs to current API"
+2 = "Update modality_benchmarks.rs to current API"

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

@@ -13,7 +13,7 @@ session = "tropical bridge v0.2 — bellman_ford sorry CLOSED"
 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 = 85
+completion-percentage = 90
 
 [position]
 phase = "phase-5-tropical-consonance"   # design | implementation | testing | maintenance | archived
@@ -25,15 +25,17 @@ phase-1-core-identification = "complete"
 phase-2-federation-contract = "complete"
 phase-3-reference-impl      = "complete"
 phase-4-krladapter-dogfood  = "complete"
-phase-5-tropical-consonance = "in-progress (RI+RII live; bellman_ford CLOSED; Tropical_Determinants pending)"
+phase-5-tropical-consonance = "complete (RI+RII live; bellman_ford CLOSED; Tropical_Determinants.thy + ProofOptimalAssignment DONE 2026-04-11)"
 
 [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"
-Prover-jl          = "live — prove(ProofConsonance, ...)"
-TROPICAL-BRIDGE    = "docs/TROPICAL-BRIDGE.adoc updated to v0.2"
+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"
+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 = [
@@ -42,7 +44,6 @@ issues = [
 
 [critical-next-actions]
 actions = [
-  "Add Tropical_Determinants.thy + ProofOptimalAssignment VCL clause",
   "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",

verisim-modular-experiment/examples/krladapter_integration.jl

@@ -23,6 +23,7 @@ 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", "tropical", "TropicalDeterminant.jl"))
 include(joinpath(@__DIR__, "..", "impl", "vcl", "Query.jl"))
 include(joinpath(@__DIR__, "..", "impl", "vcl", "Prover.jl"))
 
@@ -32,6 +33,7 @@ using .Metrics
 using .FederationManager
 using .TropicalMatrix
 using .TangleGraph
+using .TropicalDeterminant
 using .VCLQuery
 using .VCLProver
 # KnotTheory must be loaded as a package so TangleGraph._rii_neighbors

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

@@ -0,0 +1,162 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+#
+# TropicalDeterminant.jl — Julia mirror of Tropical_Determinants.thy
+#
+# Computes the tropical (min-plus) determinant of an n×n cost matrix:
+#
+#   tropm_det(A) = min over all permutations π of (∑ᵢ A[i, π(i)])
+#
+# where the inner ∑ is ordinary nat-addition (tropical multiplication)
+# and the outer min is tropical addition. This equals the minimum-cost
+# perfect matching in the n×n assignment problem.
+#
+# Formal backing: Tropical_Determinants.thy (Isabelle 2025-1)
+#   theorem optimal_assignment
+#   theorem optimal_assignment_bound
+#
+# Performance: brute-force over all n! permutations — suitable for n ≤ 8.
+# For larger n, use the Hungarian algorithm (not yet implemented).
+#
+# Mirror fidelity:
+#   perm_weightm(n, A, π)  ↔  definition perm_weightm in .thy
+#   tropm_det(n, A)         ↔  definition tropm_det in .thy
+#   optimal_assignment(n,A) ↔  theorem optimal_assignment in .thy
+
+module TropicalDeterminant
+
+using ..TropicalMatrix: Tropical, TROP_ZERO, TROP_ONE, trop_add, trop_mul
+
+export perm_weightm, tropm_det, optimal_assignment, OptimalAssignmentResult
+
+# ---------------------------------------------------------------------------
+# perm_weightm: weight of a single permutation π on cost matrix A
+# ---------------------------------------------------------------------------
+
+"""
+    perm_weightm(n, A, π) -> Tropical
+
+The tropical product (= nat sum) of A[i, π(i)] for i ∈ {0, …, n-1}.
+
+Mirrors: `definition perm_weightm` in Tropical_Determinants.thy
+"""
+function perm_weightm(n::Int, A::Matrix{Tropical}, π::Vector{Int})::Tropical
+    weight = TROP_ONE   # identity for *, i.e., Fin'(0)
+    for i in 1:n
+        weight = trop_mul(weight, A[i, π[i]])
+    end
+    return weight
+end
+
+# ---------------------------------------------------------------------------
+# tropm_det: tropical determinant = minimum-cost perfect matching
+# ---------------------------------------------------------------------------
+
+"""
+    tropm_det(n, A) -> Tropical
+
+Tropical determinant: min over all permutations π of {1,…,n} of perm_weightm(n, A, π).
+
+Brute-force enumeration of all n! permutations. Suitable for n ≤ 8.
+
+Mirrors: `definition tropm_det` in Tropical_Determinants.thy
+"""
+function tropm_det(n::Int, A::Matrix{Tropical})::Tropical
+    n == 0 && return TROP_ONE   # empty product = 1 (zero rows)
+    det = TROP_ZERO             # identity for +, i.e., PosInf
+    # Generate all permutations of {1,…,n} (1-indexed to match Julia arrays)
+    for π in _permutations(n)
+        w = perm_weightm(n, A, π)
+        det = trop_add(det, w)  # min
+    end
+    return det
+end
+
+# ---------------------------------------------------------------------------
+# optimal_assignment: find a minimising permutation
+# ---------------------------------------------------------------------------
+
+"""
+    OptimalAssignmentResult
+
+Result of `optimal_assignment/2`:
+- `permutation`: 1-indexed permutation vector achieving the minimum cost
+- `cost`: minimum assignment cost (= tropm_det)
+- `is_finite`: false if the matrix has no finite-cost perfect matching
+
+Mirrors: `theorem optimal_assignment` in Tropical_Determinants.thy
+"""
+struct OptimalAssignmentResult
+    permutation::Vector{Int}
+    cost::Tropical
+    is_finite::Bool
+end
+
+"""
+    optimal_assignment(n, A) -> OptimalAssignmentResult
+
+Find a minimum-cost perfect matching.
+
+Formal guarantee (Tropical_Determinants.thy, theorem `optimal_assignment`):
+  ∃ π. π permutes {..<n} ∧ tropm_det n A = perm_weightm n A π
+       ∧ ∀ π'. π' permutes {..<n} → tropm_det n A ≤ perm_weightm n A π'
+"""
+function optimal_assignment(n::Int, A::Matrix{Tropical})::OptimalAssignmentResult
+    if n == 0
+        return OptimalAssignmentResult(Int[], TROP_ONE, true)
+    end
+    best_π    = collect(1:n)
+    best_cost = TROP_ZERO   # PosInf — will be replaced on first iteration
+    for π in _permutations(n)
+        w = perm_weightm(n, A, π)
+        # trop_add is min; if w < best_cost, update
+        new_min = trop_add(best_cost, w)
+        if new_min != best_cost || best_cost == TROP_ZERO
+            best_cost = w
+            best_π    = copy(π)
+        end
+    end
+    is_finite = isfinite(best_cost.val)
+    return OptimalAssignmentResult(best_π, best_cost, is_finite)
+end
+
+"""
+    is_within_bound(n, A, bound) -> Bool
+
+Check whether the optimal assignment cost ≤ bound.
+
+Mirrors: corollary `optimal_assignment_bound` in Tropical_Determinants.thy:
+  (∃ π. π permutes {..<n} ∧ perm_weightm n A π ≤ B) ↔ tropm_det n A ≤ B
+"""
+function is_within_bound(n::Int, A::Matrix{Tropical}, bound::Tropical)::Bool
+    cost = tropm_det(n, A)
+    # In min-plus: a ≤ b iff trop_add(a, b) = a (min(a,b) = a)
+    return trop_add(cost, bound) == cost || cost == bound
+end
+
+# ---------------------------------------------------------------------------
+# Private: permutation generator (Heap's algorithm, 1-indexed)
+# ---------------------------------------------------------------------------
+
+function _permutations(n::Int)
+    perms = Vector{Vector{Int}}()
+    _heap_perms!(collect(1:n), n, perms)
+    return perms
+end
+
+function _heap_perms!(a::Vector{Int}, k::Int, out::Vector{Vector{Int}})
+    if k == 1
+        push!(out, copy(a))
+        return
+    end
+    _heap_perms!(a, k - 1, out)
+    for i in 1:(k - 1)
+        if k % 2 == 0
+            a[i], a[k] = a[k], a[i]
+        else
+            a[1], a[k] = a[k], a[1]
+        end
+        _heap_perms!(a, k - 1, out)
+    end
+end
+
+end # module TropicalDeterminant

verisim-modular-experiment/impl/vcl/Prover.jl

@@ -194,4 +194,81 @@ function prove(clause::Main.VCLQuery.ProofConsonance, store, manager)
     end
 end
 
+
+# -----------------------------------------------------------------------
+# PROOF OPTIMAL_ASSIGNMENT — tropical determinant assignment check
+# -----------------------------------------------------------------------
+
+function prove(clause::Main.VCLQuery.ProofOptimalAssignment, store, manager)
+    # Fetch the octad holding the cost matrix
+    octad = Main.VerisimCore.get_core(store, clause.octad_id)
+    octad === nothing && return Main.VCLQuery.VerdictFail(
+        "octad not found in Core store")
+
+    # Require Semantic shape (cost matrix is stored as proof_bytes)
+    octad.semantic === nothing && return Main.VCLQuery.VerdictFail(
+        "octad has no Semantic shape — cannot extract cost matrix")
+
+    n = clause.n
+    n < 1 && return Main.VCLQuery.VerdictFail(
+        "matrix dimension must be ≥ 1 (got $(n))")
+    n > 8 && return Main.VCLQuery.VerdictFail(
+        "matrix dimension $(n) > 8: brute-force determinant not supported " *
+        "(Hungarian algorithm not yet wired)")
+
+    # Decode n×n Tropical cost matrix from the semantic blob
+    cost_matrix = _decode_cost_matrix(octad.semantic.proof_bytes, n)
+    cost_matrix === nothing && return Main.VCLQuery.VerdictFail(
+        "could not decode $(n)×$(n) Tropical cost matrix from Semantic blob")
+
+    # Compute optimal assignment via tropical determinant
+    #
+    # Formal guarantee: optimal_assignment_bound theorem (Tropical_Determinants.thy)
+    #   tropm_det n A ≤ B  ↔  ∃ π. π permutes {..<n} ∧ perm_weightm n A π ≤ B
+    TDet = Main.TropicalDeterminant
+    result = TDet.optimal_assignment(n, cost_matrix)
+
+    if !result.is_finite
+        return Main.VCLQuery.VerdictFail(
+            "no finite-cost perfect matching exists (det = PosInf)")
+    end
+
+    # Check the bound: trop_add(cost, bound) = cost means cost ≤ bound in min-plus
+    TM    = Main.TropicalMatrix
+    bound = clause.bound
+    within = TM.trop_add(result.cost, bound) == result.cost ||
+             result.cost == bound
+
+    if within
+        perm_str = join(result.permutation, "→")
+        return Main.VCLQuery.VerdictPass(
+            "optimal assignment cost $(result.cost.val) ≤ bound " *
+            "[permutation: $(perm_str); " *
+            "backed by Tropical_Determinants.thy::optimal_assignment_bound]")
+    else
+        return Main.VCLQuery.VerdictFail(
+            "optimal assignment cost $(result.cost.val) exceeds bound " *
+            "($(bound)) [tropical determinant]")
+    end
+end
+
+# Decode a flat sequence of nat values from proof_bytes into an n×n
+# Tropical matrix.  Expected encoding: n² little-endian uint32 values;
+# 0xFFFFFFFF encodes PosInf (∞).
+function _decode_cost_matrix(proof_bytes::AbstractVector{UInt8}, n::Int)
+    TM = Main.TropicalMatrix
+    expected = n * n * 4   # n² × 4 bytes
+    length(proof_bytes) < expected && return nothing
+    A = Matrix{TM.Tropical}(undef, n, n)
+    for row in 1:n, col in 1:n
+        offset = ((row - 1) * n + (col - 1)) * 4 + 1
+        raw = UInt32(proof_bytes[offset]) |
+              (UInt32(proof_bytes[offset+1]) << 8) |
+              (UInt32(proof_bytes[offset+2]) << 16) |
+              (UInt32(proof_bytes[offset+3]) << 24)
+        A[row, col] = raw == 0xFFFFFFFF ? TM.TROP_ZERO : TM.Tropical(Float64(raw))
+    end
+    return A
+end
+
 end # module

verisim-modular-experiment/impl/vcl/Query.jl

@@ -15,7 +15,7 @@
 module VCLQuery
 
 export ProofClause, ProofIntegrity, ProofConsistency, ProofFreshness,
-       ProofConsonance,
+       ProofConsonance, ProofOptimalAssignment,
        ProofVerdict, VerdictPass, VerdictFail
 
 # -----------------------------------------------------------------------
@@ -86,6 +86,32 @@ struct ProofConsonance <: ProofClause
 end
 ProofConsonance(a, b) = ProofConsonance(a, b, 2)
 
+"""
+PROOF OPTIMAL_ASSIGNMENT FOR <id> WITHIN <bound>
+
+Asks: does there exist a perfect matching in the cost matrix stored in the
+octad's Semantic blob with total cost ≤ bound (in the min-plus tropical
+semiring)?
+
+Uses the tropical determinant (min over all permutations of assignment
+cost products) to decide the optimal assignment problem.  The bound is a
+`Tropical` value from TropicalMatrix.jl.
+
+Formal backing:
+  `optimal_assignment_bound` theorem — Tropical_Determinants.thy
+  See docs/TROPICAL-BRIDGE.adoc for the Isabelle ↔ Julia correspondence.
+
+Fields:
+  octad_id  — OctadId of the octad holding the n×n cost matrix (Semantic blob)
+  n         — matrix dimension (number of agents = number of tasks)
+  bound     — claimed optimal cost ≤ bound (Tropical value)
+"""
+struct ProofOptimalAssignment <: ProofClause
+    octad_id::Any          # OctadId (duck-typed)
+    n::Int                 # matrix dimension
+    bound::Any             # Tropical value from TropicalMatrix.jl
+end
+
 # -----------------------------------------------------------------------
 # Results
 # -----------------------------------------------------------------------