diff --git a/0-Core-Formalism/lean/Semantics/AGENTS.md b/0-Core-Formalism/lean/Semantics/AGENTS.md
index 107bafd7..6b51347e 100644
--- a/0-Core-Formalism/lean/Semantics/AGENTS.md
+++ b/0-Core-Formalism/lean/Semantics/AGENTS.md
@@ -122,6 +122,18 @@ New codec module (`Semantics.BraidDiatCodec`) layers the mountains-on-mountain s
 
 Key invariants: DIAT mass (`a + b = 2k + 1`), MMR strictly decreasing heights, Q0_2 4-state packing.
 
+### BraidSpherionBridge — SpherionState ↔ BraidState equivalence
+
+New bridge module (`Semantics.BraidSpherionBridge`) wires the mountains-on-mountain formalism to the braid strand formalism:
+
+- **`SpherionSpike`** — `spike(m : Mountain, crossPair : Fin 4)` ties a Mountain to which braid pair fires
+- **`spikeToStrandUpdate`** — applies a spike's crossing to a `BraidState` via `braidCross`
+- **`strandFlow`** — iterates `spikeToStrandUpdate` over a spike train
+- **`braidCross_merge_correspondence`** — (admit) braidCross on (i,j) ↔ Mountain.merge for corresponding pair
+- **`receipt_correspondence`** — (admit) BraidReceipt = SpherionState receipt dimensions
+
+Key remaining admits: `IntNodeToPhaseVec` linearity (`IntNode.add ↔ PhaseVec.add`), step count accumulation, full receipt dimension mapping.
+
 ### goldenContractionEnergyDecrease — proof status
 
 **Statement:** For Burgers fields with non-negative `u` and pointwise contraction `u'[i] ≤ u[i]`, the golden-contraction dissipation step reduces kinetic energy.
diff --git a/4-Infrastructure/AGENTS.md b/4-Infrastructure/AGENTS.md
index 8c22a0e3..b7ed9ac2 100644
--- a/4-Infrastructure/AGENTS.md
+++ b/4-Infrastructure/AGENTS.md
@@ -303,6 +303,7 @@ python3 4-Infrastructure/storage/storage_agent.py --loop --interval 900
 - `4-Infrastructure/shim/tang9k_uart_beacon_probe.py`
 - `4-Infrastructure/shim/hutter_jxl_starfield_eigenprobe.py`
 - `4-Infrastructure/shim/hutter_jxl_starfield_replay_verify.py`
+- `4-Infrastructure/shim/braid_diat_codec.py` — Python extraction of BraidDiatCodec (ChiralityDIAT + MountainPacked + BraidResidual + BraidDiatFrame); benchmark artifact at `shared-data/artifacts/braid_diat_codec_benchmark.json`
 - `4-Infrastructure/hardware/emergency_boot/emergency_boot_shim.py` — Python I/O shim
   for Geometry Emergency Boot Witness (6502 calculator-efficiency FPGA controller)
   Specification: `6-Documentation/docs/specs/GEOMETRY_EMERGENCY_BOOT_WITNESS_2026-04-08.md`