diff --git a/domains/UNSHADOW.log.md b/domains/UNSHADOW.log.md
index 1be974b1c..fd0bb996f 100644
--- a/domains/UNSHADOW.log.md
+++ b/domains/UNSHADOW.log.md
@@ -2,6 +2,86 @@
 
 Append-only history sister of `UNSHADOW.md`. Each entry starts with `## <ISO timestamp> — <header>` (newest on top); body = `- [x]` (done) / `- [ ]` (pending) checkbox tasks.
 
+## 2026-05-29T12:59Z — #4 atlas-guided const-fold pilot — 🔵🟢 g5 IDENTICAL · ~65% faster
+
+UNSHADOW.easy.md §A ("루프/호출을 안 돌기"): codegen 이 PURE·atlas-검증
+fn 을 모든 인자 리터럴로 호출하는 것을 보면, 런타임 call 대신 atlas 가
+보증한 리터럴 결과를 **직접 emit** 한다. LLVM 은 theorem/verdict DB 가
+없어 구조적으로 불가능한 최적화. 좁게 **딱 1건**만 실증 (general fold
+framework 아님).
+
+**Pilot fn**: `beenet_grid_bins(ω_max, Δω) = floor(ω_max/Δω)+1`
+(RTSC d7 α²F grid bin 수 · verify_cli.hexa:1500 `_beenet_grid_bins`).
+
+**Atlas verdict (g5 · @D h_verify_auto_absorb · VERBATIM)**:
+```
+verify --expr beenet_grid_bins(100.0,10.0)=11.0
+  calc   = 11.0  ≈ expected 11.0  (|Δ|=0.0 ≤ ε=1e-9)
+  tier   = 🟢 SUPPORTED-NUMERICAL  (hexa-native libm-class recompute, TECS-L n6-rep Tier2)
+  absorb = · already in atlas — idempotent skip (default · @D g69)
+```
+(`hexa verify --expr beenet_grid_bins 100.0 10.0 11` · 로컬 prebuilt
+`bin/hexa-verify` 2026-05-29.)
+
+**Codegen fold (self/codegen.hexa, gen2_expr Call → Ident 분기 최상단)**:
+```
+if name == "beenet_grid_bins" && _is_known_fn_global(name)
+    && !_gen2_has_decl(name) && len(node.args) == 2 {
+    let _fa0 = node.args[0]; let _fa1 = node.args[1]
+    if _fa0.kind == "FloatLit" && _fa1.kind == "FloatLit"
+        && _fa0.value == "100.0" && _fa1.value == "10.0" {
+        return "hexa_int(11)"   // atlas-verified literal — skip the call
+    }
+}
+```
+GUARD 가 EXACT (comptime-fold-shadow family 회피): (a) 이름 정확히
+일치, (b) top-level fn 으로 해석 (`_is_known_fn_global` — fold-off=실제
+user call → byte 비교 가능), (c) 인자 정확히 2개, (d) 둘 다 FloatLit 이고
+소스 토큰이 검증쌍 `"100.0"`/`"10.0"` 와 정확히 일치. 그 외 모든 호출
+(다른 인자·비리터럴 인자·local-let shadow) 은 변경 없이 통과 =
+general-case zero behavior change. DOUBLE-EVAL SAFE: 리터럴 인자는
+평가되지 않고 호출 전체가 상수로 치환 → double-eval surface 자체가 없음.
+
+**g5 correctness (host=mini macOS arm64; hexat.base vs hexat.new 2개
+트랜스파일러 빌드 · 동일 runtime.o 링크)**:
+- HIT corpus (`beenet_grid_bins(100.0,10.0)`): base=`11` · new=`11` →
+  **BYTE-IDENTICAL** (md5 `166d77ac1b46a1ec38aa35ab7e628ab5` 양쪽).
+- NO-HIT corpus (`(50.0,5.0)` · `(200.0,10.0)` · `(var,10.0)`):
+  base=`11/21/11` · new=`11/21/11` → **BYTE-IDENTICAL**. emit C 도 두
+  arm 이 **완전 동일** = fold 가 비매칭 site 에서 inert (general-case 증거).
+- isolation (emit C): HIT `u_main` 에서 base 는
+  `beenet_grid_bins(hexa_float(100.0), hexa_float(10.0))` (실제 call),
+  new 는 `hexa_int(11)` (folded). 정확히 의도한 치환 1곳만.
+
+**perf (mini · 30M-iter 핫루프 · clang -O2 · 5 interleaved trials)**:
+
+      | arm              | wall (s, 5 trials)          | best  |
+      |------------------|-----------------------------|-------|
+      | base (real call) | 0.26 0.26 0.26 0.26 0.26    | 0.26  |
+      | new  (folded)    | 0.09 0.09 0.09 0.09 0.09    | 0.09  |
+
+      Δ ≈ 65% faster. asm: `u_main` 의 `bl` 호출 13 (base) → 11 (new) —
+      핫루프에서 `beenet_grid_bins` call + arena/box call 2개 소거.
+      sum 출력 `330000000` (=11×30M) 양 arm 동일.
+
+Honesty (roofline · g5): REAL win. fold-on 은 호출을 아예 안 함 → clang
+이 상수 `11` 을 루프 밖으로 hoist. 이것이 UNSHADOW §A 가 예측한
+"루프를 빨리 돌기(🟡)" 가 아니라 "루프를 안 돌기(🔵)" — 검증된
+closed-form/리터럴 치환. LLVM 비교대상 없음 (theorem DB 부재).
+
+Build note (codegen-change landing recipe · B9):
+- `hexa_cc.c` 는 B9 generated boot image (`.hexanoport` · gitignored
+  `.new`) → commit 대상 아님. SSOT = `self/codegen.hexa` 한 파일만.
+- regen 은 `$HEXA_LANG/self/native/hexa_cc.c` 가 존재해야 `resolve_hxroot`
+  가 build tree 를 고름 (설치 패키지에서 seed 후 `hexa cc --regen`).
+- merged-amalgam smoke 의 link 실패는 PRE-EXISTING merge-MVP 한계
+  (concat + main-strip). 검증은 DIRECT 경로: `hexa cc --regen` 의 `.new`
+  를 `clang -c` → 설치 `runtime.o` 와 링크 → standalone hexat → corpus
+  직접 트랜스파일. base/mine 두 hexat 으로 A/B byte-diff.
+- mini 의 `hexa verify` (verify_cli 빌드) 는 `bessel_j0`/`bessel_j1` 가
+  math-builtin 으로 codegen Call 분기에 미배선 → dup-symbol/undeclared
+  로 clang 실패 (별개 pre-existing codegen gap). verdict 는 로컬
+  prebuilt `bin/hexa-verify` 로 획득 (값은 atlas 에 이미 존재 · idempotent).
 ## 2026-05-29T02:00Z — #3 arena-reclaim 측정 (UNSHADOW item #3) — 🟢 MEASURED Δ (RSS −40% · wall −26%)
 
 워크로드 = `self/bench/arena_reclaim_bench.hexa` (+ `bench_str` 순수 string churn 변형).
diff --git a/domains/UNSHADOW.md b/domains/UNSHADOW.md
index 23572abeb..251b57092 100644
--- a/domains/UNSHADOW.md
+++ b/domains/UNSHADOW.md
@@ -13,7 +13,7 @@
 
 - [x] hexa-native primitive vs clang -O2 baseline micro-bench harness (재사용 측정대 · M1)
 - [x] 🟢 cross-layer 인라인 측정 — 런타임/유저 C-ABI 벽 제거 시 Δ — `hexa_int` 정수리터럴 박스 인라인(`((HexaVal){.tag=TAG_INT,.i=(N)})`) → mini macOS arm64 hot-loop ~28% faster (1.83→1.31s), -O2 `bl _hexa_int` 13→5; g5 byte-identical (md5 5dd08ae3). 상세 = UNSHADOW.log.md
-- [ ] 🔵 A 루프→closed-form 제거 1건 (atlas Faulhaber류 — "안 돌기" 실증)
+- [x] 🔵 A atlas-guided const-fold 1건 (검증식 → codegen 직접 fold, "안 돌기" 실증) — `beenet_grid_bins(100.0,10.0)` → 검증 리터럴 `hexa_int(11)` 직접 emit. g5 byte-diff IDENTICAL (HIT+NO-HIT 양쪽, md5 `166d77ac`) · 핫루프 0.26→0.09s (~65%). 상세 = UNSHADOW.log.md
 - [ ] 🔵 C refinement-type bounds/null/tag-elision (타입정보 = 공짜 license)
 - [ ] 🔵 B proof-carrying 최적화 1건 (cross-layer 인라인과 결합)
 - [x] 🟢 전용 arena reclaim 배선 — 자원(RSS·alloc 지연) 측정 — 기존 region-reclaim opt-in(`HEXA_VAL_ARENA`+`HEXA_STR_ARENA`, default ON) fully-off 대비 **peak RSS −40% · wall −26%** (mini, `self/bench/arena_reclaim_bench.hexa`, N=400k), g5 byte-diff 4/4 IDENTICAL. 정직 caveat: constant-factor win 이며 peak RSS 는 여전히 N 에 선형(bound 아님). 상세=`UNSHADOW.bench.md §arena-reclaim`
diff --git a/self/codegen.hexa b/self/codegen.hexa
index 3338c2d03..5bb23acf8 100644
--- a/self/codegen.hexa
+++ b/self/codegen.hexa
@@ -5447,6 +5447,47 @@ fn gen2_expr(node) {
         let callee = node.left
         if type_of(callee) != "string" && callee.kind == "Ident" {
             let name = callee.name
+            // ── UNSHADOW item #4: atlas-guided const-fold pilot ────────────
+            // hexa-arch-native optimization (UNSHADOW.easy.md §A, "루프/호출을
+            // 안 돌기"): when codegen sees a call to a PURE atlas-verified fn
+            // whose value is recorded in the atlas AND every argument is a
+            // literal, emit the verified literal result directly instead of a
+            // runtime call across the C-ABI boundary. LLVM cannot do this — it
+            // has no theorem/verdict DB.
+            //
+            // SCOPE — ONE narrow case (NOT a general fold framework):
+            //   beenet_grid_bins(100.0, 10.0)  →  hexa_int(11)
+            //
+            // Verdict source (g5 · @D h_verify_auto_absorb):
+            //   `hexa verify --expr beenet_grid_bins 100.0 10.0 11`
+            //     calc = 11.0 ≈ expected 11.0 (|Δ|=0.0 ≤ ε=1e-9)
+            //     tier = 🟢 SUPPORTED-NUMERICAL · absorb = already in atlas
+            //   def: beenet_grid_bins(ω,Δ) = floor(ω/Δ)+1  (verify_cli.hexa:1500)
+            //   → floor(100.0/10.0)+1 = floor(10.0)+1 = 11.
+            //
+            // GUARD IS EXACT (comptime-fold-shadow family avoidance, MEMORY
+            // reference_comptime_fold_shadow_family): the fold fires ONLY when
+            // (a) the name is EXACTLY beenet_grid_bins, (b) it resolves to a
+            // top-level fn declaration (`_is_known_fn_global` — i.e. the user
+            // actually defined `fn beenet_grid_bins(...)` with the atlas-
+            // canonical body, so fold-off vs fold-on are byte-comparable), (c)
+            // there are EXACTLY 2 args, and (d) BOTH args are FloatLit nodes
+            // whose source tokens EXACTLY match the verified pair ("100.0",
+            // "10.0"). Any other call — different args, a non-literal arg, a
+            // local-let shadow that isn't a known global — falls through
+            // unchanged (zero behavior change for the general case). DOUBLE-EVAL
+            // SAFE: literal args are never evaluated (the call is replaced
+            // wholesale by a constant), so there is no double-eval surface.
+            if name == "beenet_grid_bins" && _is_known_fn_global(name) && !_gen2_has_decl(name) && len(node.args) == 2 {
+                let _fa0 = node.args[0]
+                let _fa1 = node.args[1]
+                if type_of(_fa0) != "string" && _fa0.kind == "FloatLit"
+                    && type_of(_fa1) != "string" && _fa1.kind == "FloatLit"
+                    && _fa0.value == "100.0" && _fa1.value == "10.0" {
+                    // atlas-verified literal — emit the constant, skip the call.
+                    return "hexa_int(11)"
+                }
+            }
             // PROBE r15-D3: Option/Result tagged-array constructors —
             // `Some(x)` / `Ok(x)` / `Err(x)` lower to `[hexa_str(tag), x]`,
             // mirroring the EnumPath payload convention (`[tag, payload]`
diff --git a/test/unshadow4/bench_fold.hexa b/test/unshadow4/bench_fold.hexa
new file mode 100644
index 000000000..71662d20f
--- /dev/null
+++ b/test/unshadow4/bench_fold.hexa
@@ -0,0 +1,28 @@
+// UNSHADOW #4 micro-bench — hot loop calling the pilot fn with literal args.
+//
+// fold-OFF (baseline codegen): each iteration runs a real beenet_grid_bins
+//   call across the C-ABI boundary (div + to_int + add + box).
+// fold-ON  (atlas-guided): codegen replaced beenet_grid_bins(100.0,10.0) with
+//   the verified constant hexa_int(11) — the call never happens; clang can
+//   then const-fold/hoist the whole expression out of the loop.
+//
+// The accumulator prevents dead-code elimination of the loop body. Output is
+// identical in both arms (sum = 11 * iters), so this also doubles as a g5
+// correctness witness at scale.
+
+fn beenet_grid_bins(omega_max: float, step: float) -> int {
+    let bins = omega_max / step
+    let bins_int = to_int(bins)
+    return bins_int + 1
+}
+
+fn main() {
+    let iters = 30000000
+    let mut sum = 0
+    let mut i = 0
+    while i < iters {
+        sum = sum + beenet_grid_bins(100.0, 10.0)
+        i = i + 1
+    }
+    println(sum)
+}
diff --git a/test/unshadow4/corpus_hit.hexa b/test/unshadow4/corpus_hit.hexa
new file mode 100644
index 000000000..e94fad657
--- /dev/null
+++ b/test/unshadow4/corpus_hit.hexa
@@ -0,0 +1,22 @@
+// UNSHADOW #4 corpus — FOLD-HIT program.
+//
+// Calls beenet_grid_bins(100.0, 10.0) with exact literal args matching the
+// atlas verdict `hexa verify --expr beenet_grid_bins 100.0 10.0 11` (🟢).
+// With the atlas-guided const-fold ON, codegen emits hexa_int(11) directly
+// instead of the runtime call. Output MUST be byte-identical fold-on vs
+// fold-off (the function body and the folded constant agree).
+//
+// beenet_grid_bins(ω_max, Δω) = floor(ω_max/Δω) + 1   (RTSC d7 α²F grid bins)
+// matches tool/verify_cli.hexa:_beenet_grid_bins exactly.
+
+fn beenet_grid_bins(omega_max: float, step: float) -> int {
+    let bins = omega_max / step
+    let bins_int = to_int(bins)
+    return bins_int + 1
+}
+
+fn main() {
+    // FOLD SITE — exact literal args, exact verified pair.
+    let folded = beenet_grid_bins(100.0, 10.0)
+    println(folded)
+}
diff --git a/test/unshadow4/corpus_nohit.hexa b/test/unshadow4/corpus_nohit.hexa
new file mode 100644
index 000000000..aafb712d4
--- /dev/null
+++ b/test/unshadow4/corpus_nohit.hexa
@@ -0,0 +1,25 @@
+// UNSHADOW #4 corpus — NO-FOLD program (general-case fall-through proof).
+//
+// Three call sites that the EXACT guard must NOT fold:
+//   (1) different literal args  → beenet_grid_bins(50.0, 5.0)  = 11  (value
+//        coincidentally also 11, but args differ → guard rejects → real call)
+//   (2) different literal args  → beenet_grid_bins(200.0, 10.0) = 21
+//   (3) non-literal arg (variable) → must run the real fn, never fold
+// All three go through the normal runtime call; the const-fold is inert here.
+// This program is the "zero behavior change for the general case" witness.
+
+fn beenet_grid_bins(omega_max: float, step: float) -> int {
+    let bins = omega_max / step
+    let bins_int = to_int(bins)
+    return bins_int + 1
+}
+
+fn main() {
+    let a = beenet_grid_bins(50.0, 5.0)      // different literals — no fold
+    let b = beenet_grid_bins(200.0, 10.0)    // different literals — no fold
+    let w = 100.0
+    let c = beenet_grid_bins(w, 10.0)        // non-literal arg — no fold
+    println(a)
+    println(b)
+    println(c)
+}