From eeec672dc74608cc57615e8a8ac6ff01c2144f85 Mon Sep 17 00:00:00 2001
From: Brandon Schneider <ceo@sovereign-stack.local>
Date: Thu, 28 May 2026 19:16:00 -0500
Subject: [PATCH] feat: network latency as coursing agent in RouteCost
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

9th dimension: networkLatencyCost (12% weight)
- latencyClass: 0=local, 1=near, 2=far, 3=derp
- DERP relay (129ms) → qHalf cost → σ=1.0 (coarse BRAM)
- Local (<1ms) → qZero cost → σ=0.0 (exact BRAM)

Latency maps to FPGA voltage mode:
  local(0) → 1.2V σ₀ (exact)    BRAM Bank 0
  near(1)  → 1.0V σ₁ (normal)   BRAM Bank 1
  far(2)   → 0.8V σ₂ (approx)   BRAM Bank 2
  derp(3)  → 0.6V σ₃ (coarse)   BRAM Bank 3

Consistent latency is computable — not noise, but a fixed phase offset.
The latency IS the computation: it determines which precision to use.

Weights rebalanced: kernel 20→18, street 14→12, topology 16→14,
substrate 12→10, proof 14→12, risk 14→12, latency +12.
lake build: 2 jobs, 0 errors
---
 .../lean/Semantics/Semantics/RouteCost.lean   | 42 ++++++++++++++++---
 1 file changed, 36 insertions(+), 6 deletions(-)

diff --git a/0-Core-Formalism/lean/Semantics/Semantics/RouteCost.lean b/0-Core-Formalism/lean/Semantics/Semantics/RouteCost.lean
index 8619d6a1..a8c191ce 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/RouteCost.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/RouteCost.lean
@@ -79,6 +79,7 @@ structure RouteNode where
   risk : FailureRisk
   throat : Bool
   fammMemory : Bool
+  latencyClass : Nat := 0  -- 0=local (<1ms), 1=near (1-10ms), 2=far (10-100ms), 3=derp (>100ms)
   deriving Repr
 
 def FoundationKernel.index : FoundationKernel → Nat
@@ -200,18 +201,47 @@ def fammMemoryBonus (a b : RouteNode) : Nat :=
   else if a.fammMemory || b.fammMemory then qQuarter
   else qZero
 
+/-- Network latency cost as a coursing agent.
+
+    Consistent latency is computable — not noise, but a fixed phase offset.
+    DERP relay adds ~129ms per hop. This maps to the cost function:
+
+    - local (0): same node, <1ms → zero cost
+    - near (1): same cluster, 1-10ms → qEighth
+    - far (2): cross-network, 10-100ms → qQuarter
+    - derp (3): DERP relay, >100ms → qHalf
+
+    The latency class determines the FPGA voltage mode:
+    - local → σ₀ (1.2V, exact)
+    - near → σ₁ (1.0V, normal)
+    - far → σ₂ (0.8V, approximate)
+    - derp → σ₃ (0.6V, coarse)
+
+    This is the "coursing agent" — latency shapes the computation. -/
+def networkLatencyCost (a b : RouteNode) : Nat :=
+  if a.id == b.id then qZero
+  else
+    let maxClass := Nat.max a.latencyClass b.latencyClass
+    match maxClass with
+    | 0 => qZero      -- local: no latency cost
+    | 1 => qEighth    -- near: 1-10ms
+    | 2 => qQuarter   -- far: 10-100ms
+    | 3 => qHalf      -- derp: >100ms (DERP relay)
+    | _ => qOne       -- unknown: maximum cost
+
 def weighted (weight component : Nat) : Nat :=
   (weight * component) / 100
 
 def routeCostNat (a b : RouteNode) : Nat :=
   if a.id == b.id then qZero else
     let positive :=
-      weighted 20 (kernelDistance a b) +
-      weighted 14 (streetTransitionCost a b) +
-      weighted 16 (gwlTopologyDistance a b) +
-      weighted 12 (substrateExecutionCost a b) +
-      weighted 14 (proofObligationCost a b) +
-      weighted 14 (failureRisk a b)
+      weighted 18 (kernelDistance a b) +
+      weighted 12 (streetTransitionCost a b) +
+      weighted 14 (gwlTopologyDistance a b) +
+      weighted 10 (substrateExecutionCost a b) +
+      weighted 12 (proofObligationCost a b) +
+      weighted 12 (failureRisk a b) +
+      weighted 12 (networkLatencyCost a b)
     let bonus :=
       weighted 5 (throatBonus a b) +
       weighted 5 (fammMemoryBonus a b)