# RG-SCP Validation V1-02
## Obstruction / Reduced GFOC Kernel
### Proper Prime-Factor Witness、Reduced Exact Cover、Total Obstruction Map 與 Canonical Least-Factor Partition

**驗證系列：** RG-SCP Validation  
**階段：** V1 — Formal Core  
**輪次：** 02  
**日期：** 2026-09-28  
**版本：** v0.1  
**作者：** Neo.K；Aletheia（GPT-5.6 Sol）  
**性質：** Formalization Specification / Obstruction Kernel Contract / Lean-Oriented Core  
**前置：** V1-01 Basic / Reduced Goldbach / Counterexample Kernel  
**狀態：** Canonical formal-core specification；本文件不宣稱已完成 Lean kernel compilation

---

## 摘要

V1-01 已固定 RG-SCP 的 machine target semantics：

- `LegalEven`；
- `ReducedPrimeInput`；
- `GoldbachReducedPair`；
- `GoldbachSuccessReduced`；
- `GoldbachFailure`；
- `CounterexampleSet`；
- `MinimalCounterexample`；
- `ProofAdmissibleSet`。

V1-02 現在只加入第一個真正 arithmetic source：

$$
\boxed{
\mathcal S_1
=
\text{factor / least-prime-factor source}.
}
$$

本輪目標不是進 M6 或 wheel，而是把下列五件事變成單一 formal kernel：

1. reduced complement 的 composite / proper-prime-factor 等價；
2. reduced GFOC 的 exact characterization；
3. total proper obstruction map；
4. canonical least-prime-factor obstruction map；
5. canonical least-factor cells 與 divisor self-suppression。

核心 arithmetic object採平方界，而不用 real square root。

對：

$$
m\in\mathbb N,
$$

定義 proper prime-factor witness：

$$
\boxed{
\operatorname{ProperPrimeFactor}(m,r)
:
\Longleftrightarrow
r\in\mathbb P
\land
r\mid m
\land
r^2\le m.
}
$$

在本輪所有合法 reduced complement：

$$
m=N-p,
$$

都有：

$$
m\ge2.
$$

因此：

$$
\boxed{
m\text{ composite}
\Longleftrightarrow
\exists r,
\operatorname{ProperPrimeFactor}(m,r).
}
$$

另一方面，V0-R02 已發現 reduced domain 有一個更強的 global-cutoff theorem。

若：

$$
p\in\mathbb P,
\quad
2p\le N,
$$

則：

$$
N-p\text{ composite}
$$

當且僅當存在 prime：

$$
r
$$

滿足：

$$
\boxed{
r\mid(N-p),
\qquad
r^2\le N-2.
}
$$

所以定義 raw reduced obstruction class：

$$
\boxed{
\mathcal O_r^{-}(N)
=
\left\{
p:
\operatorname{ReducedPrimeInput}(N,p),
\quad
r\in\mathbb P,
\quad
r^2\le N-2,
\quad
r\mid(N-p)
\right\}.
}
$$

則對 legal even：

$$
N,
$$

Goldbach failure exact 等價於：

$$
\boxed{
\forall p,
\operatorname{ReducedPrimeInput}(N,p)
\Longrightarrow
\exists r,
\operatorname{RawObstruction}(N,p,r).
}
$$

也就是 reduced GFOC：

$$
\boxed{
F_G(N)=1
\Longleftrightarrow
\mathbb P_N^{-}
\subseteq
\bigcup_{r^2\le N-2}
\mathcal O_r^{-}(N).
}
$$

這一版沒有 wheel、M6、heuristic，也不需要逐點把 target predicate塞回 obstruction 定義。

接著定義 total proper obstruction map。

對 fixed：

$$
N,
$$

令 domain：

$$
\operatorname{ReducedPrimeSubtype}(N)
=
\left\{
p:\operatorname{ReducedPrimeInput}(N,p)
\right\}.
$$

一個 proper obstruction map 是一個 function：

$$
\Phi:
\operatorname{ReducedPrimeSubtype}(N)
\to
\mathbb N
$$

使：

$$
\Phi(p)\in\mathbb P,
$$

$$
\Phi(p)\mid(N-p),
$$

以及：

$$
\Phi(p)^2\le N-p.
$$

則：

$$
\boxed{
F_G(N)=1
\Longleftrightarrow
\operatorname{LegalEven}(N)
\land
\exists \Phi,
\operatorname{ProperObstructionMap}(N,\Phi).
}
$$

canonical choice採 least prime factor：

$$
\boxed{
\Phi_N^{\min}(p)
=
\operatorname{lpf}(N-p).
}
$$

但只在 failure branch才把它解讀為 proper obstruction map。

如果：

$$
N-p
$$

為 prime，

則：

$$
\operatorname{lpf}(N-p)=N-p
$$

只是 prime本身，不能被當作 proper obstruction。

因此 canonical least-factor cell明確加 composite typing：

$$
\boxed{
B_r(N)
=
\left\{
p:
\operatorname{ReducedPrimeInput}(N,p),
\quad
N-p\text{ composite},
\quad
\operatorname{lpf}(N-p)=r
\right\}.
}
$$

在 failure state：

$$
\boxed{
\mathbb P_N^{-}
=
\bigsqcup_r B_r(N).
}
$$

最後 formalize divisor self-suppression：

若：

$$
r\mid N,
$$

$$
r\mid(N-p),
$$

且：

$$
p,r
$$

都是 prime，

則：

$$
\boxed{
p=r.
}
$$

這將成為 V1-03 Primorial Geometry、V1-07 Canonical Capacity、V1-09 Transport 的共同基礎。

本輪最重要的工程原則是：

$$
\boxed{
\text{Raw cover}
\neq
\text{canonical partition}
\neq
\text{proper obstruction map}.
}
$$

三者在 theorem / code 中必須使用不同名稱。

---

# 1. V1-02 的 dependency boundary

允許 import：

```text
V1-01 Foundation
Nat.Prime
Nat divisibility
Nat.minFac or equivalent least-factor API
finite sets / subtypes
```

禁止 import：

- M6；
- wheel；
- fixed point；
- AP prime bounds；
- demand / capacity；
- heuristic models。

本輪只建立：

$$
\boxed{
\text{factor-obstruction semantics}.
}
$$

---

# 2. Composite predicate

建議不要把：

$$
\neg\operatorname{Prime}(m)
$$

單獨叫 composite。

因：

$$
0,1
$$

也不是 prime。

定義：

$$
\boxed{
\operatorname{Composite}(m)
:
\Longleftrightarrow
2\le m
\land
\neg\operatorname{Prime}(m).
}
$$

Lean-oriented：

```lean
def Composite (m : Nat) : Prop :=
  2 ≤ m ∧ ¬ Nat.Prime m
```

若 Mathlib已有合適 predicate，可 bridge後使用既有 API。

---

# 3. Reduced complement lower bound

## Lemma V1-02-L01

若：

$$
\operatorname{ReducedPrimeInput}(N,p),
$$

則：

$$
\boxed{
2\le N-p.
}
$$

---

# 4. L01 proof

由：

$$
p
$$

prime：

$$
2\le p.
$$

又：

$$
2p\le N.
$$

所以：

$$
p\le N-p.
$$

因此：

$$
2\le p\le N-p.
$$

這個 lemma讓 reduced complement永遠避開：

$$
0,1.
$$

---

# 5. Reduced endpoint order

## Lemma V1-02-L02

若：

$$
\operatorname{ReducedPrimeInput}(N,p),
$$

則：

$$
\boxed{
p\le N-p.
}
$$

這是：

$$
2p\le N
$$

的 Nat additive形式。

後續所有 global-cutoff proof都依賴它。

---

# 6. Complement upper bound

## Lemma V1-02-L03

若：

$$
\operatorname{ReducedPrimeInput}(N,p),
$$

則：

$$
\boxed{
N-p\le N-2.
}
$$

因：

$$
p\ge2.
$$

所以 composite complement 的 small factor：

$$
r^2\le N-p
$$

自動推出：

$$
r^2\le N-2.
$$

---

# 7. Proper prime-factor witness

定義：

$$
\boxed{
\operatorname{ProperPrimeFactor}(m,r)
:
\Longleftrightarrow
\operatorname{Prime}(r)
\land
r\mid m
\land
r^2\le m.
}
$$

Lean-oriented：

```lean
def ProperPrimeFactor (m r : Nat) : Prop :=
  Nat.Prime r ∧
  r ∣ m ∧
  r * r ≤ m
```

---

# 8. 為什麼用平方界

數學文件常寫：

$$
r\le\sqrt m.
$$

formal core改用：

$$
r^2\le m.
$$

好處：

- 不引入 real numbers；
- 不引入 `Nat.sqrt` rounding semantics；
- composite factor theorem最自然；
- 後續 AP proper-factor range直接轉成：
  $$
  p\le N-r^2.
  $$

---

# 9. Proper witness真的 proper

## Lemma V1-02-L04

若：

$$
\operatorname{ProperPrimeFactor}(m,r)
$$

且：

$$
2\le m,
$$

則：

$$
\boxed{
1<r<m.
}
$$

---

# 10. L04 proof idea

prime：

$$
r
$$

給：

$$
1<r.
$$

若反設：

$$
r=m,
$$

則：

$$
m^2\le m.
$$

但：

$$
m\ge2
$$

推出：

$$
m<m^2.
$$

矛盾。

所以：

$$
r<m.
$$

因此 witness不是用 $m$ 本身冒充 factor。

---

# 11. Composite implies proper prime factor

## Theorem V1-02-T01

若：

$$
\operatorname{Composite}(m),
$$

則：

$$
\boxed{
\exists r,
\operatorname{ProperPrimeFactor}(m,r).
}
$$

這是標準 least-prime-factor / small-factor theorem。

---

# 12. T01 formal proof strategy

兩種策略。

## Strategy A — Mathlib minFac

取：

$$
r=\operatorname{minFac}(m).
$$

使用既有 theorem：

- minFac prime；
- minFac divides；
- composite時：
  $$
  r^2\le m.
  $$

具體 theorem names需在實際 Lean版本解析。

## Strategy B — finite least divisor construction

若 API不穩，

可自行在 divisor set上取最小 prime divisor。

第一版優先 Strategy A。

---

# 13. Proper prime factor implies composite

## Theorem V1-02-T02

若：

$$
2\le m
$$

且：

$$
\exists r,
\operatorname{ProperPrimeFactor}(m,r),
$$

則：

$$
\boxed{
\operatorname{Composite}(m).
}
$$

---

# 14. T02 proof

proper witness：

$$
1<r<m
$$

且：

$$
r\mid m.
$$

所以：

$$
m
$$

不能 prime。

配：

$$
2\le m.
$$

即 Composite。

---

# 15. Composite witness equivalence

## Theorem V1-02-T03

對：

$$
2\le m,
$$

有：

$$
\boxed{
\operatorname{Composite}(m)
\Longleftrightarrow
\exists r,
\operatorname{ProperPrimeFactor}(m,r).
}
$$

這是 V1-02 第一個核心 theorem。

---

# 16. Reduced complement prime/composite dichotomy

由 L01：

$$
2\le N-p.
$$

所以對 reduced input：

$$
\boxed{
N-p\in\mathbb P
}
$$

或：

$$
\boxed{
\operatorname{Composite}(N-p).
}
$$

不存在第三種：

$$
0/1
$$

邊界。

---

# 17. Global raw obstruction witness

定義：

$$
\boxed{
\operatorname{RawObstruction}(N,p,r)
}
$$

當：

$$
\operatorname{Prime}(r),
$$

$$
r\mid(N-p),
$$

以及：

$$
r^2\le N-2.
$$

Lean-oriented：

```lean
def RawObstruction (N p r : Nat) : Prop :=
  Nat.Prime r ∧
  r ∣ (N - p) ∧
  r * r ≤ N - 2
```

注意：

它本身不含：

```lean
ReducedPrimeInput N p
```

因 domain premise由 theorem外部給。

---

# 18. Composite reduced complement implies raw obstruction

## Theorem V1-02-T04

若：

$$
\operatorname{ReducedPrimeInput}(N,p)
$$

且：

$$
\operatorname{Composite}(N-p),
$$

則：

$$
\boxed{
\exists r,
\operatorname{RawObstruction}(N,p,r).
}
$$

---

# 19. T04 proof

由 T01取：

$$
r
$$

使：

$$
r^2\le N-p.
$$

再由 L03：

$$
N-p\le N-2.
$$

所以：

$$
r^2\le N-2.
$$

---

# 20. Raw obstruction implies composite reduced complement

這是 reduced-domain exactness最關鍵的方向。

## Theorem V1-02-T05

若：

$$
\operatorname{ReducedPrimeInput}(N,p)
$$

以及：

$$
\operatorname{RawObstruction}(N,p,r),
$$

則：

$$
\boxed{
\operatorname{Composite}(N-p).
}
$$

---

# 21. T05 proof核心

令：

$$
q=N-p.
$$

需要排除：

$$
q
$$

為 prime。

由 L02：

$$
p\le q.
$$

所以：

$$
N=p+q\le2q.
$$

又：

$$
q\ge p\ge2.
$$

因此：

$$
2q\le q^2.
$$

所以：

$$
N\le q^2.
$$

進而：

$$
N-2<q^2.
$$

Raw obstruction給：

$$
r^2\le N-2<q^2.
$$

所以：

$$
r<q.
$$

而：

$$
r\mid q,
$$

$$
r>1.
$$

所以：

$$
q
$$

有 nontrivial proper divisor，

故 composite。

這個 proof不需要 real square root。

---

# 22. Reduced pointwise global-cutoff characterization

## Theorem V1-02-T06

若：

$$
\operatorname{ReducedPrimeInput}(N,p),
$$

則：

$$
\boxed{
\operatorname{Composite}(N-p)
\Longleftrightarrow
\exists r,
\operatorname{RawObstruction}(N,p,r).
}
$$

這就是 V0-R02 的 audit strengthening正式進 kernel。

---

# 23. Prime complement iff no raw obstruction

由 L01 與 T06：

## Corollary V1-02-C01

若：

$$
\operatorname{ReducedPrimeInput}(N,p),
$$

則：

$$
\boxed{
\operatorname{Prime}(N-p)
\Longleftrightarrow
\neg
\exists r,
\operatorname{RawObstruction}(N,p,r).
}
$$

這是 obstruction graph isolated-vertex theorem的基礎。

---

# 24. Reduced GFOC predicate

定義：

$$
\boxed{
\operatorname{ReducedGFOC}(N)
:
\Longleftrightarrow
\forall p,
\operatorname{ReducedPrimeInput}(N,p)
\to
\exists r,
\operatorname{RawObstruction}(N,p,r).
}
$$

Lean-oriented：

```lean
def ReducedGFOC (N : Nat) : Prop :=
  ∀ p,
    ReducedPrimeInput N p →
    ∃ r, RawObstruction N p r
```

---

# 25. GFOC 不內建 LegalEven

本輪刻意不把：

$$
\operatorname{LegalEven}(N)
$$

塞進：

$$
\operatorname{ReducedGFOC}(N).
$$

原因：

- GFOC是 arithmetic cover predicate；
- failure才是 conjecture-domain predicate；
- theorem明確寫 legal assumption即可。

這比把 domain埋進每個 structural predicate更模組化。

---

# 26. Reduced GFOC exact theorem

## Theorem V1-02-T07

若：

$$
\operatorname{LegalEven}(N),
$$

則：

$$
\boxed{
\operatorname{GoldbachFailure}(N)
\Longleftrightarrow
\operatorname{ReducedGFOC}(N).
}
$$

---

# 27. T07 failure推 GFOC

failure：

$$
\neg\operatorname{GoldbachSuccessReduced}(N).
$$

所以對任何 reduced input：

$$
p,
$$

$$
N-p
$$

不 prime。

由 L01：

$$
N-p\ge2.
$$

所以 composite。

由 T06：

存在 raw obstruction。

---

# 28. T07 GFOC推 failure

GFOC保證每個 reduced input：

$$
p
$$

都有 raw obstruction。

由 T05：

$$
N-p
$$

composite。

所以不存在 reduced Goldbach witness。

配：

$$
\operatorname{LegalEven}(N),
$$

得到：

$$
\operatorname{GoldbachFailure}(N).
$$

---

# 29. Set-level GFOC form

可定義：

$$
\mathcal O_r^{-}(N)
=
\left\{
p:
\operatorname{ReducedPrimeInput}(N,p)
\land
\operatorname{RawObstruction}(N,p,r)
\right\}.
$$

則 T07等價於：

$$
\boxed{
F_G(N)=1
\Longleftrightarrow
\mathbb P_N^{-}
\subseteq
\bigcup_r
\mathcal O_r^{-}(N)
}
$$

其中：

$$
r^2\le N-2
$$

已在 RawObstruction內。

formal core優先使用 predicate form，

set union theorem作 corollary。

---

# 30. Reduced prime subtype

定義：

```lean
def ReducedPrimeSubtype (N : Nat) :=
  {p : Nat // ReducedPrimeInput N p}
```

對：

$$
p:
\operatorname{ReducedPrimeSubtype}(N),
$$

寫：

$$
p.1
$$

為 underlying natural。

---

# 31. Proper obstruction map structure

Lean-oriented：

```lean
structure ProperObstructionMap (N : Nat) where
  factor :
    ReducedPrimeSubtype N → Nat

  factor_prime :
    ∀ p, Nat.Prime (factor p)

  factor_dvd :
    ∀ p, factor p ∣ (N - p.1)

  factor_sq_le :
    ∀ p, factor p * factor p ≤ (N - p.1)
```

這是一個真正 total map。

---

# 32. Map本身不要求 LegalEven

和 GFOC一樣：

`ProperObstructionMap N`

只描述：

> 對所有 reduced inputs都有 proper factor assignment。

Goldbach theorem再額外加：

$$
LegalEven(N).
$$

---

# 33. Obstruction map implies GFOC

## Theorem V1-02-T08

若：

$$
\operatorname{ProperObstructionMap}(N)
$$

存在，

則：

$$
\boxed{
\operatorname{ReducedGFOC}(N).
}
$$

因每個 map factor滿足：

$$
r^2\le N-p.
$$

又：

$$
N-p\le N-2,
$$

所以：

$$
r^2\le N-2.
$$

---

# 34. GFOC implies proper obstruction map

## Theorem V1-02-T09

若：

$$
\operatorname{ReducedGFOC}(N),
$$

則：

$$
\boxed{
\operatorname{Nonempty}
\left(
\operatorname{ProperObstructionMap}(N)
\right).
}
$$

---

# 35. T09 proof strategy

GFOC只給 global-cutoff witness：

$$
r^2\le N-2,
$$

不一定直接給：

$$
r^2\le N-p.
$$

所以不能任意從 RawObstruction witness選 map factor。

正確做法：

對每個 reduced：

$$
p,
$$

由 GFOC + T05知：

$$
N-p
$$

composite。

再使用：

$$
\operatorname{lpf}(N-p)
$$

作 canonical factor。

由 composite small-factor theorem：

$$
\operatorname{lpf}(N-p)^2
\le
N-p.
$$

所以得到真正 proper map。

這是 important proof-detail。

---

# 36. Obstruction map characterization

## Theorem V1-02-T10

若：

$$
\operatorname{LegalEven}(N),
$$

則：

$$
\boxed{
\operatorname{GoldbachFailure}(N)
\Longleftrightarrow
\operatorname{Nonempty}
\left(
\operatorname{ProperObstructionMap}(N)
\right).
}
$$

這是 V0-R02 proper-map theorem的 formal target。

---

# 37. Canonical least-factor function

對：

$$
p:
\operatorname{ReducedPrimeSubtype}(N),
$$

定義概念：

$$
\boxed{
\operatorname{CanonicalFactor}_N(p)
=
\operatorname{lpf}(N-p).
}
$$

Lean-oriented：

```lean
def CanonicalFactor
    (N : Nat)
    (p : ReducedPrimeSubtype N) : Nat :=
  Nat.minFac (N - p.1)
```

實際 API需在 compile階段確認。

---

# 38. CanonicalFactor 的 typing

即使：

$$
N-p
$$

prime，

`CanonicalFactor`仍有值。

但這時：

$$
CanonicalFactor=N-p
$$

不是 proper obstruction。

所以：

$$
\boxed{
\text{CanonicalFactor}
}
$$

只是 total least-factor readout。

而：

$$
\boxed{
\text{CanonicalProperObstructionMap}
}
$$

只在 failure / composite branch成立。

---

# 39. Canonical map under failure

## Theorem V1-02-T11

若：

$$
\operatorname{GoldbachFailure}(N),
$$

則：

$$
\operatorname{CanonicalFactor}_N
$$

滿足：

$$
\boxed{
\operatorname{ProperObstructionMap}(N).
}
$$

這給 total proper map theorem一個 deterministic canonical witness。

---

# 40. Proper obstruction map一般不唯一

形式化不需要專門證大量非唯一例子，

但 theorem naming必須避免：

```text
the_obstruction_map
```

應使用：

```text
a_proper_obstruction_map
canonical_least_factor_map
```

canonical uniqueness只指：

$$
\operatorname{lpf}
$$

choice deterministic。

---

# 41. Composite least-factor cell

定義：

$$
\boxed{
\operatorname{LeastFactorCell}(N,r,p)
}
$$

當：

1. $p$ reduced prime input；
2. $N-p$ composite；
3. $\operatorname{lpf}(N-p)=r$。

Lean-oriented：

```lean
def LeastFactorCell
    (N r p : Nat) : Prop :=
  ReducedPrimeInput N p ∧
  Composite (N - p) ∧
  Nat.minFac (N - p) = r
```

---

# 42. 為什麼 cell必須含 Composite

若：

$$
N-p=q
$$

prime，

則：

$$
\operatorname{minFac}(q)=q.
$$

若不加 Composite，

prime complement會被塞進某個 least-factor cell。

那會污染：

- obstruction partition；
- canonical capacity；
- lpf load。

所以：

$$
\boxed{
\text{Composite typing is mandatory}.
}
$$

---

# 43. Cell factor prime

## Lemma V1-02-L05

若：

$$
\operatorname{LeastFactorCell}(N,r,p),
$$

則：

$$
\boxed{
r\in\mathbb P.
}
$$

由 composite + minFac prime theorem。

---

# 44. Cell factor proper

## Lemma V1-02-L06

若：

$$
\operatorname{LeastFactorCell}(N,r,p),
$$

則：

$$
\boxed{
r^2\le N-p.
}
$$

因此：

$$
r
$$

是真 proper obstruction factor。

---

# 45. Cell exclusivity

## Theorem V1-02-T12

若：

$$
\operatorname{LeastFactorCell}(N,r,p)
$$

以及：

$$
\operatorname{LeastFactorCell}(N,s,p),
$$

則：

$$
\boxed{
r=s.
}
$$

因：

$$
\operatorname{minFac}(N-p)
$$

單值。

---

# 46. Failure partition theorem

## Theorem V1-02-T13

若：

$$
\operatorname{GoldbachFailure}(N),
$$

則對所有：

$$
\operatorname{ReducedPrimeInput}(N,p),
$$

存在唯一：

$$
r
$$

使：

$$
\boxed{
\operatorname{LeastFactorCell}(N,r,p).
}
$$

形式：

$$
\boxed{
\forall p\in\mathbb P_N^{-},
\quad
\exists! r,
\operatorname{LeastFactorCell}(N,r,p).
}
$$

這就是 canonical obstruction partition的 machine theorem。

---

# 47. Set partition corollary

若將：

$$
B_r(N)
=
\{p:\operatorname{LeastFactorCell}(N,r,p)\},
$$

則 failure下：

$$
\boxed{
\mathbb P_N^{-}
=
\bigsqcup_r
B_r(N).
}
$$

formal core可先證 `exists_unique`，

Finset partition後補。

---

# 48. Divisor self-suppression

## Theorem V1-02-T14

若：

$$
r,p
$$

prime，

$$
r\mid N,
$$

$$
r\mid(N-p),
$$

以及：

$$
p\le N,
$$

則：

$$
\boxed{
p=r.
}
$$

---

# 49. T14 proof

由：

$$
p\le N,
$$

有：

$$
N=p+(N-p).
$$

若：

$$
r\mid N
$$

與：

$$
r\mid(N-p),
$$

則：

$$
r\mid p.
$$

因：

$$
p
$$

prime，

而：

$$
r
$$

prime且：

$$
r>1,
$$

所以：

$$
r=p.
$$

Lean中優先使用 add/sub divisibility lemma，避免不必要 modular arithmetic。

---

# 50. Reduced self-suppression corollary

若：

$$
\operatorname{ReducedPrimeInput}(N,p),
$$

$$
r\in\mathbb P,
$$

$$
r\mid N,
$$

且：

$$
r\mid(N-p),
$$

則：

$$
\boxed{
p=r.
}
$$

因 reduced input已給：

$$
p\le N.
$$

---

# 51. Raw obstruction self-cell

## Corollary V1-02-C02

若：

$$
r\in\mathbb P,
$$

$$
r\mid N,
$$

則：

$$
\boxed{
\mathcal O_r^{-}(N)
\subseteq
\{r\}.
}
$$

這是 V1-03 primorial suppression的直接依賴。

---

# 52. Canonical cell self-suppression

若：

$$
r\mid N,
$$

且：

$$
\operatorname{LeastFactorCell}(N,r,p),
$$

則：

$$
\boxed{
p=r.
}
$$

所以：

$$
B_r(N)
$$

最多只有 self-cell：

$$
p=r.
$$

---

# 53. $r=2$ special cell

若：

$$
\operatorname{GoldbachFailure}(N),
$$

則：

$$
N
$$

legal even。

對 reduced：

$$
p=2,
$$

有：

$$
N-2
$$

even，

且 failure使：

$$
N-2
$$

not prime。

因：

$$
N-2\ge2.
$$

對：

$$
N=4
$$

其實 failure false。

所以 failure branch自動：

$$
N\ge6.
$$

且：

$$
N-2\ge4.
$$

因此：

$$
\boxed{
\operatorname{lpf}(N-2)=2.
}
$$

---

# 54. Failure implies $N\ge6$

## Lemma V1-02-L07

若：

$$
\operatorname{GoldbachFailure}(N),
$$

則：

$$
\boxed{
6\le N.
}
$$

因：

$$
N=4
$$

已有：

$$
2+2.
$$

這不是後續 core的必要 theorem，

但可讓：

$$
B_2=\{2\}
$$

proof更乾淨。

---

# 55. Canonical $2$-cell theorem

## Theorem V1-02-T15

若：

$$
\operatorname{GoldbachFailure}(N),
$$

則：

$$
\boxed{
B_2(N)=\{2\}
}
$$

在 reduced input語義下。

這可留 Tier 2，不是 V1-02 acceptance必要條件。

---

# 56. GFOC source status

Reduced GFOC：

$$
F_G
\Longleftrightarrow
\text{all reduced complements have small proper factor witnesses}
$$

是：

$$
[\mathrm T/E].
$$

其 arithmetic source仍是：

$$
\boxed{
\mathcal S_1.
}
$$

不能因為：

- cover；
- map；
- partition；

三種表示不同就計成三個 source。

---

# 57. Proof-compression status

V1-02 本身主要完成：

$$
\boxed{
\text{proof-burden normalization}.
}
$$

它把：

$$
\forall p,
N-p\text{ composite}
$$

變成：

- raw cover；
- proper map；
- canonical partition。

真正 compression要到後續：

> 一個 theorem同時限制很多 cells / factors。

---

# 58. Raw cover / map / partition 的正式分工

## Raw Cover

用於：

- global cutoff；
- quotient geometry；
- graph isolation。

## Proper Map

用於：

- finite counterexample certificate；
- per-input witness assignment。

## Canonical Partition

用於：

- load；
- capacity；
- non-overlap counting；
- V1-07 canonical coverage。

不能混名。

---

# 59. Lean-oriented module split

建議：

```text
RGSCP/Core/
  Composite.lean
  ObstructionWitness.lean
  ReducedGFOC.lean
  ProperObstructionMap.lean
  LeastFactorCell.lean
  SelfSuppression.lean
```

如果 repo希望小檔案，

也可先合成：

```text
Obstruction.lean
```

再拆。

---

# 60. Lean-oriented skeleton

```lean
namespace RGSCP

def Composite (m : Nat) : Prop :=
  2 ≤ m ∧ ¬ Nat.Prime m

def ProperPrimeFactor (m r : Nat) : Prop :=
  Nat.Prime r ∧
  r ∣ m ∧
  r * r ≤ m

def RawObstruction (N p r : Nat) : Prop :=
  Nat.Prime r ∧
  r ∣ (N - p) ∧
  r * r ≤ N - 2

def ReducedGFOC (N : Nat) : Prop :=
  ∀ p,
    ReducedPrimeInput N p →
    ∃ r, RawObstruction N p r

def ReducedPrimeSubtype (N : Nat) :=
  {p : Nat // ReducedPrimeInput N p}

structure ProperObstructionMap (N : Nat) where
  factor : ReducedPrimeSubtype N → Nat
  factor_prime :
    ∀ p, Nat.Prime (factor p)
  factor_dvd :
    ∀ p, factor p ∣ (N - p.1)
  factor_sq_le :
    ∀ p, factor p * factor p ≤ (N - p.1)

def CanonicalFactor
    (N : Nat)
    (p : ReducedPrimeSubtype N) : Nat :=
  Nat.minFac (N - p.1)

def LeastFactorCell
    (N r p : Nat) : Prop :=
  ReducedPrimeInput N p ∧
  Composite (N - p) ∧
  Nat.minFac (N - p) = r

end RGSCP
```

這是 specification，不保證 theorem/API names已符合目前 Mathlib。

---

# 61. Canonical theorem queue

```yaml
V1_02:
  - id: T01
    name: composite_has_proper_prime_factor
    status: to_formalize

  - id: T02
    name: proper_prime_factor_implies_composite
    status: to_formalize

  - id: T03
    name: composite_iff_proper_prime_factor
    status: to_formalize

  - id: T04
    name: reduced_composite_implies_raw_obstruction
    status: to_formalize

  - id: T05
    name: raw_obstruction_implies_reduced_composite
    status: to_formalize

  - id: T06
    name: reduced_composite_iff_raw_obstruction
    status: to_formalize

  - id: T07
    name: failure_iff_reduced_gfoc
    status: to_formalize

  - id: T08
    name: proper_map_implies_gfoc
    status: to_formalize

  - id: T09
    name: gfoc_implies_proper_map
    status: to_formalize

  - id: T10
    name: failure_iff_proper_obstruction_map
    status: to_formalize

  - id: T11
    name: canonical_factor_is_proper_map_under_failure
    status: to_formalize

  - id: T12
    name: least_factor_cell_exclusive
    status: to_formalize

  - id: T13
    name: failure_has_unique_least_factor_cell
    status: to_formalize

  - id: T14
    name: divisor_self_suppression
    status: to_formalize
```

---

# 62. Mathlib API uncertainty ledger

實際 compile前要確認：

```text
Nat.minFac
Nat.minFac_prime
Nat.minFac_dvd
composite / minFac square-bound theorem
prime divisibility lemmas
Nat subtraction/addition bridge lemmas
```

如果 theorem name不同，

只改 implementation，

不能改 canonical theorem statement來迎合 API。

---

# 63. Formalization invariant：不為了 compile 改 theorem meaning

禁止：

> 某 theorem不好證，所以把 $r^2\le N-p$ 偷改成更弱條件。

允許：

> 使用等價 Nat formulation避免 sqrt。

所有 implementation repair都必須保持 V0/V1 statement semantics。

---

# 64. Boundary unit test：prime complement

取：

$$
N=22,
\quad
p=5.
$$

有：

$$
2p=10\le22,
$$

$$
N-p=17
$$

prime。

global cutoff：

$$
N-2=20.
$$

不應存在 prime：

$$
r
$$

使：

$$
r^2\le20
$$

且：

$$
r\mid17.
$$

所以：

```text
RawObstruction 22 5 r
```

對所有 $r$ false。

---

# 65. Boundary unit test：composite complement

取：

$$
N=26,
\quad
p=5.
$$

$$
N-p=21.
$$

proper factor：

$$
r=3.
$$

有：

$$
3^2=9\le21
$$

且：

$$
3\mid21.
$$

同時：

$$
9\le N-2=24.
$$

所以：

```text
ProperPrimeFactor 21 3 = true
RawObstruction 26 5 3 = true
```

---

# 66. Boundary unit test：square

$$
m=25,
\quad
r=5.
$$

$$
r^2=m.
$$

proper witness允許 equality：

$$
\boxed{
r^2\le m.
}
$$

所以不能誤用 strict：

$$
r^2<m.
$$

---

# 67. Boundary unit test：$N=4$

唯一 reduced input：

$$
p=2.
$$

complement：

$$
2
$$

prime。

沒有 raw obstruction。

所以：

$$
\operatorname{ReducedGFOC}(4)
$$

false，

與：

$$
F_G(4)=0
$$

一致。

---

# 68. Boundary unit test：$N=10$

reduced primes：

$$
2,3,5.
$$

complements：

$$
8,7,5.
$$

其中：

$$
p=2
$$

有 obstruction：

$$
r=2.
$$

但：

$$
p=3,5
$$

沒有 proper obstruction。

所以：

$$
\operatorname{ReducedGFOC}(10)
$$

false。

---

# 69. Self-suppression test

取：

$$
N=30,
\quad
r=3.
$$

若：

$$
3\mid(30-p)
$$

且：

$$
p
$$

prime，

則：

$$
p=3.
$$

測：

```text
p=3  -> true obstruction divisibility
p=2  -> false
p=5  -> false
p=7  -> false
```

這是 V1-03 前的重要 regression test。

---

# 70. Prime complement不能進 canonical cell

取：

$$
N=22,
\quad
p=5,
$$

$$
N-p=17.
$$

即使：

$$
\operatorname{minFac}(17)=17,
$$

也必須：

```text
LeastFactorCell 22 17 5 = false
```

因：

$$
Composite(17)
$$

false。

這是 V0 truth-leakage / typing audit後的重要 invariant。

---

# 71. Composite complement進唯一 cell

取：

$$
N=26,
\quad
p=5,
$$

$$
21=3\cdot7.
$$

則：

$$
\operatorname{minFac}(21)=3.
$$

所以：

```text
LeastFactorCell 26 3 5 = true
LeastFactorCell 26 7 5 = false
```

canonical cell選 least factor，不是任意 factor。

---

# 72. Proper map finite certificate semantics

若對 legal even：

$$
N,
$$

提供 structure：

```text
ProperObstructionMap N
```

就已 finite-certify：

$$
F_G(N)=1.
$$

因 map domain涵蓋所有 reduced prime inputs，

每個 input都有 proper prime factor witness。

這是固定 candidate counterexample的 certificate semantics。

---

# 73. 但 finite map不是 global proof

即使對：

$$
N\le B
$$

每個 legal even都建立：

- success witness；
- 或 obstruction map；

也只得到 finite theorem。

不能從 finite map existence推：

$$
\forall N.
$$

延續 V1-01 finite/global firewall。

---

# 74. GFOC 與 ProofAdmissible 接口

一旦 T07 formalized，

可以把：

$$
K_{\mathrm{GFOC}}(N)
:=
\operatorname{ReducedGFOC}(N)
$$

加入：

$$
ProofAdmissible.
$$

因：

$$
GoldbachFailure(N)
\to
ReducedGFOC(N).
$$

所以：

$$
\boxed{
K_{\mathrm{GFOC}}
}
$$

是第一個真正 arithmetic counterexample-necessary constraint。

---

# 75. 但 GFOC 本身仍 target-equivalent

因：

$$
LegalEven(N)
$$

下：

$$
F_G(N)
\Longleftrightarrow
ReducedGFOC(N).
$$

所以把：

$$
K_{\mathrm{GFOC}}
$$

加入：

$$
ProofAdmissible
$$

雖 sound，

但：

$$
\boxed{
\text{proof_compression_gain}=0
}
$$

除非後續把 GFOC壓成更弱、可獨立排空的 structural consequences。

---

# 76. Constraint ledger標記

```yaml
constraint:
  id: K_GFOC
  sound: true
  exact: true
  target_equivalent_on_legal_domain: true
  source_class:
    - S1
  proof_compression_gain: false
```

這是「kernel correctness」與「research usefulness」分離的例子。

---

# 77. V1-02 Formal Acceptance Gate

只有以下全部 PASS 才進 V1-03：

### G1

Composite definition不把 $0,1$ 算 composite。

### G2

ProperPrimeFactor使用平方界。

### G3

composite iff proper witness完成。

### G4

reduced complement lower/upper bounds完成。

### G5

raw obstruction iff reduced complement composite完成。

### G6

ReducedGFOC iff failure完成。

### G7

proper obstruction map iff failure完成。

### G8

canonical least-factor map只在 failure branch被證 proper。

### G9

LeastFactorCell含 Composite typing。

### G10

failure下 unique cell theorem完成。

### G11

divisor self-suppression完成。

### G12

no `sorry`.

---

# 78. Bug / Falsification Checklist

如果 implementation出現以下任一，立即停止：

1. prime complement被 RawObstruction捕捉；
2. prime complement進 LeastFactorCell；
3. square complement如 $25$ 的 factor $5$ 因 strict inequality被漏掉；
4. GFOC不加 LegalEven premise就被宣稱等價 failure；
5. proper map從 global-cutoff witness直接選 $r$，卻沒證 $r^2\le N-p$；
6. divisor self-suppression theorem忘記 $p\le N$ / reduced-domain bridge；
7. canonical map一般 state被當 proper obstruction map；
8. `minFac` API behaviour for $0,1$ 被依賴；
9. raw cover cardinality被當 partition cardinality；
10. factor source被拆成多個 independent sources。

---

# 79. Formal dependency graph

```text
V1-01 ReducedPrimeInput
  ↓
L01/L02/L03 reduced complement bounds
  ↓
Composite / ProperPrimeFactor
  ↓
T03 composite witness equivalence
  ↓
RawObstruction
  ↓
T06 reduced composite iff raw obstruction
  ↓
ReducedGFOC
  ↓
T07 failure iff GFOC
```

另一支：

```text
Composite
  ↓
minFac
  ↓
CanonicalFactor
  ↓
ProperObstructionMap
  ↓
LeastFactorCell
  ↓
Unique Partition
```

與：

```text
divisibility
  ↓
SelfSuppression
  ↓
V1-03 Primorial Geometry
```

---

# 80. V1-02 Verdict

$$
\boxed{
\mathrm{V1\mbox{-}02\ SPECIFICATION\ READY}
}
$$

但仍須區分：

$$
\boxed{
\text{formal specification ready}
\neq
\text{Lean kernel verified}.
}
$$

本輪完成的是：

> 把 RG-SCP 的 obstruction language壓成 machine-checkable contract，並把 raw cover、proper map、canonical partition三種語義完全拆開。

---

# 81. 下一輪

下一篇建議：

# RG-SCP Validation V1-03
## Primorial Geometry / Self-Suppression Kernel

只做：

- $M_k$；
- wheel-hard set；
- hard-set nesting；
- $M_k\mid N$ 的 exact hard-sector equality；
- exact cardinality；
- failure下 rough-composite wall；
- graph-isolation interface；
- 明確不重建 effective wheel。

仍不進 M6 fixed-point。

---

# 82. 最短版本

V1-02 把：

$$
\boxed{
N-p\text{ composite}
}
$$

形式化成：

$$
\boxed{
\exists r\in\mathbb P,
\quad
r\mid(N-p),
\quad
r^2\le N-p.
}
$$

在 reduced domain再提升成：

$$
\boxed{
N-p\text{ composite}
\Longleftrightarrow
\exists r\in\mathbb P,
\quad
r\mid(N-p),
\quad
r^2\le N-2.
}
$$

因此 legal even：

$$
N
$$

failure iff：

$$
\boxed{
\forall p\in\mathbb P_N^{-},
\quad
\exists r,
\operatorname{RawObstruction}(N,p,r).
}
$$

也 iff存在：

$$
\boxed{
\text{total proper obstruction map}.
}
$$

在 failure branch中 canonical map：

$$
\boxed{
\Phi_N^{\min}(p)
=
\operatorname{lpf}(N-p).
}
$$

並形成唯一 least-factor cells。

這就是後續 wheel、capacity與 transport共用的 factor kernel。

---

# 附錄 A：Lean-Oriented Skeleton

```lean
namespace RGSCP

def Composite (m : Nat) : Prop :=
  2 ≤ m ∧ ¬ Nat.Prime m

def ProperPrimeFactor (m r : Nat) : Prop :=
  Nat.Prime r ∧
  r ∣ m ∧
  r * r ≤ m

def RawObstruction (N p r : Nat) : Prop :=
  Nat.Prime r ∧
  r ∣ (N - p) ∧
  r * r ≤ N - 2

def ReducedGFOC (N : Nat) : Prop :=
  ∀ p,
    ReducedPrimeInput N p →
    ∃ r, RawObstruction N p r

def ReducedPrimeSubtype (N : Nat) :=
  {p : Nat // ReducedPrimeInput N p}

structure ProperObstructionMap (N : Nat) where
  factor : ReducedPrimeSubtype N → Nat
  factor_prime :
    ∀ p, Nat.Prime (factor p)
  factor_dvd :
    ∀ p, factor p ∣ (N - p.1)
  factor_sq_le :
    ∀ p, factor p * factor p ≤ (N - p.1)

def CanonicalFactor
    (N : Nat)
    (p : ReducedPrimeSubtype N) : Nat :=
  Nat.minFac (N - p.1)

def LeastFactorCell
    (N r p : Nat) : Prop :=
  ReducedPrimeInput N p ∧
  Composite (N - p) ∧
  Nat.minFac (N - p) = r

end RGSCP
```

---

# 附錄 B：Unit Tests

```yaml
tests:
  - case: prime_complement
    N: 22
    p: 5
    complement: 17
    raw_obstruction_exists: false
    least_factor_cell_exists: false

  - case: composite_complement
    N: 26
    p: 5
    complement: 21
    proper_factor:
      r: 3
    raw_obstruction_exists: true
    canonical_cell:
      r: 3

  - case: square_composite
    m: 25
    r: 5
    proper_factor: true

  - case: N4
    N: 4
    reduced_gfoc: false
    failure: false

  - case: N10
    N: 10
    reduced_gfoc: false
    failure: false

  - case: self_suppression
    N: 30
    r: 3
    only_prime_p_with_r_dividing_N_minus_p: 3
```

---

# 附錄 C：Source Signature

```yaml
RG-SCP-V1-02:
  S0_elementary:
    role:
      - arithmetic_bounds
      - divisibility
      - reduced_domain

  S1_factor_lpf:
    role:
      - composite_witness
      - proper_obstruction_map
      - canonical_factor
      - least_factor_cells

  S2_wheel:
    forbidden_dependency: true

  S3_fixed_point:
    forbidden_dependency: true

  S4_minimality:
    not_required: true

  S5_analytic:
    forbidden_dependency: true

  S6_heuristic:
    forbidden_dependency: true

proof_compression:
  current: normalization_only
  source_escape: false
```

---

# 附錄 D：Constraint Metadata

```yaml
K_GFOC:
  theorem:
    failure_implies: ReducedGFOC

  status:
    exact: true
    sound: true
    target_equivalent_on_legal_domain: true

  source:
    - S1

  proof_compression_gain:
    value: false

  future_use:
    - derive weaker structural necessary conditions
    - wheel projection
    - capacity decomposition
```

---

# 附錄 E：Commit Decision

```yaml
validation_round: V1-02
decision: SPECIFICATION_READY

formal_status:
  machine_checked: false
  lean_compiled: false
  sorry_free: not_yet_tested

canonical_decisions:
  - composite_typed_as_ge_2_and_not_prime
  - proper_factor_uses_square_bound
  - raw_reduced_GFOC_is_exact_on_legal_domain
  - total_proper_map_separate_from_raw_cover
  - canonical_factor_is_total_readout_but_proper_only_under_composite_failure
  - least_factor_cells_require_composite_typing
  - divisor_self_suppression_is_core
  - raw_cover_map_partition_names_must_remain_distinct

next_round:
  V1-03_Primorial_Geometry_Self_Suppression_Kernel

commit_to_sync_core: true
```