diff --git a/VERIFICATION_LOG.md b/VERIFICATION_LOG.md
index 6f530f83..bddde953 100644
--- a/VERIFICATION_LOG.md
+++ b/VERIFICATION_LOG.md
@@ -100,6 +100,8 @@ agree before the formula is accepted.
 | 005 | P3: Contraction d_F(C(p),C(q))<d_F(p,q) | ✅ VERIFIED | 0.100441 < 0.440258 | 2026-06-23 |
 | 006 | P4: Information loss I_loss(p) | ✅ VERIFIED | 0.106727 nats | 2026-06-23 |
 | 007 | P5: Φ-corkscrew f(n) | ✅ VERIFIED | f(20121)=(-137.80079576,-33.64432624), dist=264.41810784 | 2026-06-23 |
+| 008 | F("a+b=c") byte-frequency map | ✅ VERIFIED | (0,0.2,0,0.2,0,0,0.6,0) | 2026-06-23 |
+| 009 | √p embedding ‖φ(F("a+b=c"))‖₂ | ✅ VERIFIED | 1.00000000 | 2026-06-23 |
 
 ---
 
@@ -123,5 +125,37 @@ agree before the formula is accepted.
 with m>n, then (m-n)ψ ∈ 2πℤ, requiring ψ/2π ∈ ℚ. But φ² = φ+1 is irrational,
 so 1/φ² is irrational. Contradiction. Therefore f is injective.
 
+---
+
+## VERIFICATION 008: Byte-Frequency Map F("a+b=c")
+
+**Formula:** F(E)ᵢ = countᵢ(E) / Σⱼ countⱼ(E)
+
+**Input:** E = "a+b=c" (5 characters)
+**Byte classes:** control(0), punct-low(1), digits(2), punct-mid(3), upper(4), punct-high(5), lower(6), extended(7)
+**Verified by:** Alpha, Beta, Gamma
+**Consensus:**
+- ASCII: a=97→6, +=43→1, b=98→6, ==61→3, c=99→6
+- Counts: (0, 1, 0, 1, 0, 0, 3, 0), total = 5
+- F("a+b=c") = (0.000000, 0.200000, 0.000000, 0.200000, 0.000000, 0.000000, 0.600000, 0.000000)
+- Sum = 1.000000 ✓, all ≥ 0 ✓
+**Date:** 2026-06-23
+**Status:** ✅ VERIFIED
+
+---
+
+## VERIFICATION 009: √p Embedding of F("a+b=c")
+
+**Formula:** φ(p) = (√p₁, ..., √p₈), verify ‖φ(p)‖₂ = 1
+
+**Input:** p = F("a+b=c") = (0, 0.2, 0, 0.2, 0, 0, 0.6, 0)
+**Verified by:** Alpha, Beta, Gamma
+**Consensus:**
+- φ(p) = (0, 0.44721360, 0, 0.44721360, 0, 0, 0.77459667, 0)
+- ‖φ(p)‖₂² = 1.00000000
+- ‖φ(p)‖₂ = 1.00000000 ✓
+**Date:** 2026-06-23
+**Status:** ✅ VERIFIED
+
 **Rule:** Status PENDING → 3-agent verification → VERIFIED or REJECTED.
 No formula moves from PENDING to VERIFIED without all 3 agents agreeing.