diff --git a/0-Core-Formalism/lean/Semantics/AGENTS.md b/0-Core-Formalism/lean/Semantics/AGENTS.md
index 4850315f..b9874b68 100644
--- a/0-Core-Formalism/lean/Semantics/AGENTS.md
+++ b/0-Core-Formalism/lean/Semantics/AGENTS.md
@@ -526,15 +526,14 @@ Erdős 30 Improvement: ε ≥ 1/2 → ε ≥ 1/4 UNLOCKED
 | `decode_encode_roundtrip` | `subagent_codec` | Medium | Completed | Re-encoding a decoded frame yields matching header fields when chirality/n are consistent. |
 | `qr_encode_decode_roundtrip` | `subagent_codec` | Medium | Completed | QR field passes through encode/decode unchanged (proven and resolved). |
 | `solveEnergyExponential` | `subagent_arithmetic` | Low | Completed | Proved using Q16_16.mul_mono_left and one_mul (E_solve ≥ 2^depth). |
-
 ### Active Agent Assignments (current cycle)
 
 | Task | File | Assigned Agent | Priority | Status | Notes |
 |------|------|----------------|----------|--------|-------|
 | `convergencePreservesScore` and related | `HybridTSMPISTTorus.lean:219` | `subagent_revive` | Low | Assigned | 1 sorry at line 219. Quarantined module with 2 errors. Revive for build surface inclusion after proof resolution. |
-| `TopologicalBraidAdapter` proofs | `Semantics/TopologicalBraidAdapter.lean` | `subagent_revive` | Medium | Active | 3 sorries in new compiler bridge adapter module. |
+| `TopologicalBraidAdapter` proofs | `Semantics/TopologicalBraidAdapter.lean` | `subagent_revive` | Medium | Completed | All 3 sorries resolved (stableSignal_implies_coherent, noCfd_avoids_continuum, tensegrity_implies_braid_coherence). |
 
-**Progress tracking**: The active build surface compiled successfully. The 2 quarantined/TODO sites above are assigned to specialized agents for the next cycle.
+**Progress tracking**: The active build surface compiled successfully with TopologicalBraidAdapter fully verified. The quarantined/TODO site above is assigned to specialized agents for the next cycle.
 
 
 ### Q16InverseProof — Exact inverse proof (All Closed)
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/TopologicalBraidAdapter.lean b/0-Core-Formalism/lean/Semantics/Semantics/TopologicalBraidAdapter.lean
index b62db705..91c5ede8 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/TopologicalBraidAdapter.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/TopologicalBraidAdapter.lean
@@ -154,17 +154,21 @@ theorem stableSignal_implies_coherent (p : HardProblemState) (s : BraidSample) :
     decideGate p s = GateDecision.stableSignal →
     (colorRope p s).coherent = true := by
   intro h
-  simp only [decideGate] at h
-  -- TACTIC_GAP: unfold nested if-then-else branches; stableSignal requires .coherent ∧ ...
-  sorry
+  unfold decideGate at h
+  dsimp only at h
+  split_ifs at h with h1 h2 h3
+  simp only [Bool.and_eq_true, decide_eq_true_iff] at h3
+  rcases h3 with ⟨⟨⟨⟨h_coh, _⟩, _⟩, _⟩, _⟩
+  exact h_coh
 
 theorem noCfd_avoids_continuum (p : HardProblemState) (s : BraidSample) :
     decideGate p s = GateDecision.noCfdRoute →
     shouldRouteNoCfd p = true := by
   intro h
-  simp only [decideGate] at h
-  -- TACTIC_GAP: noCfdRoute is the first branch: if shouldRouteNoCfd p then noCfdRoute
-  sorry
+  unfold decideGate at h
+  dsimp only at h
+  split_ifs at h with h1
+  exact h1
 
 -- ============================================================
 -- §8 Yang-Baxter coherence
@@ -181,8 +185,8 @@ theorem tensegrity_implies_braid_coherence (p : HardProblemState) (s : BraidSamp
     totalTensegrityStrain p s defaultTensegrity ≤
       avgQ0 (satQ0 p.residualRisk) q0Max := by
   intro h
-  -- TACTIC_GAP: tensegrityCoherent IS this bound; unfold it
-  sorry
+  unfold tensegrityCoherent at h
+  exact decide_eq_true_iff.mp h
 
 -- ============================================================
 -- §9 Full pipeline + eval witnesses