diff --git a/docs/thesis.md b/docs/thesis.md
index 9aa13bb..159be04 100644
--- a/docs/thesis.md
+++ b/docs/thesis.md
@@ -57,9 +57,14 @@ Capability 전달 (Alias/Move 모델의 제3의 규칙):
    capability는 second-class "use" 전달을 기본으로 한다.
 - 기본은 use(호출 동안의 임시 접근): 호출자는 호출 후에도 계속 보유하고,
   피호출자는 사용만 할 수 있다
-- use로 받은 capability는 탈출 불가: 반환 금지, struct 저장 금지,
-  channel 전송 금지, 호출보다 오래 사는 closure에 capture 금지
-  ※ 탈출 검사는 함수 로컬로 결정 가능
+- use로 받은 capability는 탈출 불가: 반환 금지, struct 저장 금지, channel 전송 금지
+- use는 전염된다: use 값을 capture한 closure는 그 자체가 use 값이 되고,
+  use 값은 use로 표시된 파라미터 위치로만 전달할 수 있다
+  ※ closure를 저장하는 sink는 일반 fn 파라미터를 요구하므로 use-closure를 넘길 수
+     없다 → compile error. 판정에 필요한 정보가 전부 시그니처에 있고 검사는 로컬
+  ※ capture 전면 금지는 with_retry(fn(){ pay.refund() }) 같은 정당한 패턴까지
+     죽이므로 기각. 별도의 nonescaping 개념을 만들지 않고 use의 전염으로 정의해
+     "한 개념 한 방식"을 지킨다 (Swift @noescape, second-class values의 검증된 경로)
 - 소유권 이전이 필요할 때만 명시적 move
 근거: non-duplication은 "복제 금지"이지 "재사용 금지"가 아니다. use는 복제를
 만들지 않으므로 보안 정리와 양립하고, 탈출 금지가 locality를 보존한다.
@@ -69,8 +74,16 @@ Affinity 전이 (보안 주장의 필수 전제):
   컴파일러가 타입 정의에서 유도하며 전이적으로 적용된다
 - copyable 선언과 affine 필드의 공존은 compile error
 - 타입의 affinity는 exported interface surface의 일부이며 interface hash에 포함된다
-근거: 이 규칙이 없으면 Box{pay}를 복사하는 것만으로 capability가 사실상 복제되어
-non-duplication 정리가 깨진다.
+- 이 전이는 closure 환경에도 동일하게 적용된다 (callable affinity):
+  v0의 callable은 두 종류다 —
+    fn(...)         copyable. copyable·immutable 환경만 capture 가능
+    affine fn(...)  affine 값을 소유할 수 있고, 자신도 affine이라 move 규칙을 따름
+  affine 값을 capture한 closure의 타입은 자동으로 affine fn이 되며 fn 위치에 대입 불가.
+  affinity는 callable 타입 표기의 일부로 공개 시그니처와 interface hash에 포함된다
+  ※ bound method와 partial application도 "환경을 보관하는 값"이므로 같은 규칙
+  ※ use-closure(위 Capability 전달)는 affinity와 직교하는 파라미터 위치 속성이다
+근거: 이 규칙이 없으면 Box{pay}를 복사하거나 affine 값을 capture한 closure를
+복사하는 것만으로 capability가 사실상 복제되어 non-duplication 정리가 깨진다.
 
 동시성 (철학 1,2,3에서 파생 — Alias/Move 모델의 특수 사례):
 - green thread (async/await의 function coloring은 철학 5 위반)
@@ -79,7 +92,16 @@ non-duplication 정리가 깨진다.
   공유는 deep immutable만 (borrow checker는 complexity budget 초과)
 - spawn closure는 by-move capture 또는 immutable capture만 허용.
   mutable 참조 capture는 문법적으로 금지
-- spawn은 effect로 선언 → 동시성이 시그니처에 드러남
+- spawn은 primitive가 아니라 TaskScope capability의 메서드다.
+  effect spawn은 아래 "정적/동적 층 분리"대로 그 타입에 묶인다
+  (PaymentGateway.refund와 동형)
+- TaskScope는 use-only(second-class)라 블록 밖으로 탈출할 수 없다
+  — Capability 전달의 use 메커니즘을 그대로 재사용한다
+- join/cancel은 handle 소비 관례가 아니라 scope 구문의 실행 의미로 강제한다:
+  scope { ... } 블록 종료 시 런타임이 자식 전원을 join/cancel한다
+  ※ v0는 affine 미소비(누수)를 허용하므로 handle 기반 보장은 애초에 불가능하다.
+     실행 의미로 옮겨야 그 허점이 사라진다
+- 루트 TaskScope는 main에 주입 → ambient authority 없이 권한 사슬이 main부터 닫힌다
 
 Effect 다형성 (철학 2,5에서 파생):
 - effect 변수는 타입 파라미터와 정확히 같은 규율을 따른다:
@@ -91,7 +113,16 @@ Effect 다형성 (철학 2,5에서 파생):
   ※ 전역 추론이 배제하는 것은 "선언 없이 프로그램 전체를 보고 알아내기"이지
      선언된 변수의 로컬 해소가 아니다. map 체크에 필요한 것은
      map과 인자의 시그니처뿐 (locality 유지)
-- effect는 순서 없는 집합, 변수는 집합 변수, 합성은 합집합 → 결정 가능·로컬
+- effect는 순서 없는 집합, 변수는 집합 변수, 합성은 합집합
+- 합집합이 있는 이상 일반 unification이 아니다 (해가 유일하지 않다).
+  v0는 해소를 pattern unification으로 제한해 유일성과 선형 비용을 산다:
+    · effect 변수는 어떤 파라미터의 effect 자리에 "단독으로" 등장해야 한다(결정 위치)
+    · 변수의 해는 그 결정 위치에서 읽어오기만 한다
+    · 합집합 식은 결과 위치에만 허용하며 절대 분해하지 않는다
+    · 합집합 식이 기대 타입과 대조되는 위치는 compile error + 명시적 인스턴스화 요구
+  ※ map·filter·fold류는 전부 이 형태에 들어간다. 역산이 필요한 시그니처(peel류)는
+     작성 자체가 거부된다 — 표현력을 팔아 결정성을 사는 거래이고,
+     이 언어에서는 항상 그 방향이 맞다
 - row polymorphism 불필요: 차집합("이 effect만 빼고")이 필요해지는 것은
   handler를 넣을 때이고, 그것은 v0 범위 밖
 - 완화 장치 하나만 예약: 클로저 인자의 effects 생략 시 {}로 기본 해석
@@ -115,15 +146,19 @@ interface hash의 입력 = 모듈 exported surface 전체의 의미적 정규형
 - 타입의 affinity (copyable / affine)
 - exported constant의 타입과 값
 - capability/effect 선언
-- re-export 목록
+- re-export된 선언을 완전히 해소한 정의 본문 (목록이 아니다)
+  ※ A의 enum에 variant가 추가되면 B의 소스가 그대로여도 B의 hash가 변하고,
+     C의 exhaustive match가 재검사된다. "의미적 정규형"을 구현 수준까지 내린 것
 원칙: downstream 검사 결과에 영향을 줄 수 있는 모든 것을 포함한다. 의심스러우면
 넣는다 — 과잉 포함의 비용은 재검사지만 누락의 비용은 잘못된 캐시라는 비대칭.
 
 invalidation 전파 = 고정점 규칙 ("direct dependents로만 전파"가 아니다):
-1. 변경된 모듈의 direct dependents를 재검사
-2. 그중 interface hash가 실제로 바뀐 모듈만 다음 단계로 전파
-3. hash가 안정되는 지점에서 중단
-※ implementation-only 변경은 1단계에서 멈춘다 (hash 불변 → 전파 0)
+1. 변경된 모듈 자체를 재검사
+2. 재검사 전후의 interface hash를 비교
+3. 달라졌을 때만 그 모듈의 dependents를 큐에 추가
+4. 큐가 빌 때까지(= hash가 안정되는 고정점까지) 1~3 반복
+※ 순서가 중요하다. dependents를 먼저 재검사하면 "본문만 수정 시 downstream 0건"이
+   성립하지 않는다 — hash 비교가 dependents 재검사보다 앞서야 한다
 
 Generics (철학 2에서 파생):
 - 기본 shared implementation, monomorphization은 명시적 요청 시만