# RG-SCP Validation V1-03
## Primorial Geometry / Self-Suppression Kernel
### Prime-Cutoff Wheel、Saturated Hard Sector、Exact Demand Formula 與 Rough-Composite Wall

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

---

## 摘要

V1-02 已建立 factor-obstruction kernel：

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

以及 divisor self-suppression：

$$
r\mid N,
\quad
r\mid(N-p),
\quad
p,r\in\mathbb P
\Longrightarrow
p=r.
$$

V1-03 現在只處理：

$$
\boxed{
\text{finite prime cutoffs}
+
\text{self-suppression geometry}.
}
$$

本輪刻意不進：

- M6 fixed-point；
- $\Delta_6$；
- capacity；
- AP analytic bounds；
- minimality transport。

本輪首先不直接把：

$$
M_k
=
\prod_{i=1}^{k}p_i
$$

設成 primitive。

真正 arithmetic 核心其實不是「第 $k$ 個 prime」本身，而是：

> $N$ 是否被 cutoff 以下所有質數整除？

因此先定義：

$$
\boxed{
P(y)
=
\prod_{\substack{
r\in\mathbb P\\
r\le y
}}
r
}
$$

以及：

$$
\boxed{
\operatorname{PrimeSaturatedAt}(N,y)
:
\Longleftrightarrow
\forall r\in\mathbb P,
\quad
r\le y
\Rightarrow
r\mid N.
}
$$

再定義 wheel-hard predicate：

$$
\boxed{
\operatorname{WheelHard}(N,y,p)
:
\Longleftrightarrow
\operatorname{ReducedPrimeInput}(N,p)
\land
\gcd(N-p,P(y))=1.
}
$$

V1-03 的最核心 theorem 是：

## Saturated Hard-Sector Theorem

若：

$$
\operatorname{PrimeSaturatedAt}(N,y),
$$

則：

$$
\boxed{
\operatorname{WheelHard}(N,y,p)
\Longleftrightarrow
\operatorname{ReducedPrimeInput}(N,p)
\land
y<p.
}
$$

這個 theorem **完全不需要**：

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

它只是 target-state divisor geometry。

若再令：

$$
y=p_k,
$$

且：

$$
M_k\mid N,
$$

就得到 primorial corollary：

$$
\boxed{
\mathbb H_{p_k}(N)
=
\left\{
p\in\mathbb P:
p_k<p,
\quad
2p\le N
\right\}.
}
$$

所以 exact demand：

$$
\boxed{
D_N(p_k)
=
\pi(N/2)-k
}
$$

在：

$$
p_k\le N/2
$$

時成立。

這仍然不需要 failure。

只有再加入：

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

才得到：

$$
\boxed{
p>p_k
\Longrightarrow
N-p
\text{ is composite and }
\operatorname{lpf}(N-p)>p_k.
}
$$

亦即：

# Primorial Rough-Composite Wall

本輪還正式建立：

1. cutoff hard-set nesting；
2. hard predicate與「沒有 small obstruction」的 exact 等價；
3. M6 = $y=3$ 的 exact hard-sector corollary；
4. exact hard-count formula；
5. rough-composite predicate；
6. failure下 hard survivor必落入 rough-composite sector。

同時明確禁止重新引入：

$$
M_k^{\mathrm{eff}}(N)
$$

或 `effective wheel`。

V0 已證明它：

- 對 $p>p_k$ 不增加 ordinary wheel以外的資訊；
- 在 self-cell可能反而錯誤分類。

所以 V1 formal core只保留：

$$
\boxed{
P(y),
\quad
\operatorname{WheelHard},
\quad
\operatorname{PrimeSaturatedAt}.
}
$$

---

# 1. V1-03 的唯一任務

本輪要 formalize 的不是：

> wheel 是否能證 Goldbach。

而是：

$$
\boxed{
\text{small-prime divisibility geometry 到底 exact 強迫什麼？}
}
$$

只把確定的 finite quotient / divisor structure鎖成 theorem。

---

# 2. Prime cutoff set

定義：

$$
\boxed{
\mathbb P_{\le y}
=
\left\{
r\in\mathbb P:
r\le y
\right\}.
}
$$

formal implementation可用：

```lean
def PrimeCutoffFinset (y : Nat) : Finset Nat :=
  (Finset.range (y + 1)).filter Nat.Prime
```

實際 syntax依 Lean API調整。

---

# 3. Prime cutoff product

定義：

$$
\boxed{
P(y)
=
\prod_{r\in\mathbb P_{\le y}}r.
}
$$

Lean-oriented：

```lean
def PrimeCutoffProduct (y : Nat) : Nat :=
  ∏ r in PrimeCutoffFinset y, r
```

---

# 4. 為什麼先用 $P(y)$，而不是 $M_k$

`nthPrime` / prime indexing在不同 proof-assistant API中容易帶入：

- zero-based；
- one-based；
- off-by-one；
- theorem-name依賴。

而：

$$
P(y)
$$

只依賴：

$$
r\le y.
$$

這正是 hard-sector theorem真正使用的資訊。

所以：

$$
\boxed{
P(y)
}
$$

是 V1-03 primitive。

---

# 5. Prime divisors of cutoff product

## Theorem V1-03-T01

若：

$$
r\in\mathbb P,
$$

則：

$$
\boxed{
r\mid P(y)
\Longleftrightarrow
r\le y.
}
$$

這是 cutoff product的第一個核心 bridge。

---

# 6. T01 proof方向

### 右推左

若：

$$
r\le y
$$

且 $r$ prime，

則：

$$
r
$$

出現在 product中。

### 左推右

若：

$$
r
$$

prime且：

$$
r\mid P(y),
$$

由 Euclid lemma / prime divisibility of finite product，

$r$ 必等於某個 product factor，

所以：

$$
r\le y.
$$

---

# 7. Prime saturation predicate

定義：

$$
\boxed{
\operatorname{PrimeSaturatedAt}(N,y)
:
\Longleftrightarrow
\forall r,
\quad
r\in\mathbb P
\land
r\le y
\Rightarrow
r\mid N.
}
$$

Lean-oriented：

```lean
def PrimeSaturatedAt (N y : Nat) : Prop :=
  ∀ r, Nat.Prime r → r ≤ y → r ∣ N
```

---

# 8. Product divisibility characterization

## Theorem V1-03-T02

$$
\boxed{
P(y)\mid N
\Longleftrightarrow
\operatorname{PrimeSaturatedAt}(N,y).
}
$$

因：

$$
P(y)
$$

是 distinct primes的 squarefree product。

---

# 9. Formalization strategy for T02

如果直接證 product divides iff all factors divide較麻煩，

可先拆：

## T02a

$$
P(y)\mid N
\Longrightarrow
\operatorname{PrimeSaturatedAt}(N,y).
$$

## T02b

$$
\operatorname{PrimeSaturatedAt}(N,y)
\Longrightarrow
P(y)\mid N.
$$

T02b需要 finite pairwise-coprime product divisibility。

如果 API麻煩，

可以先只把：

$$
\operatorname{PrimeSaturatedAt}
$$

當 primitive theorem assumption。

primorial corollary等 T02 bridge完成後再開。

---

# 10. Wheel-hard predicate

定義：

$$
\boxed{
\operatorname{WheelHard}(N,y,p)
:
\Longleftrightarrow
\operatorname{ReducedPrimeInput}(N,p)
\land
\operatorname{Coprime}(N-p,P(y)).
}
$$

Lean-oriented：

```lean
def WheelHard (N y p : Nat) : Prop :=
  ReducedPrimeInput N p ∧
  Nat.Coprime (N - p) (PrimeCutoffProduct y)
```

---

# 11. Hard set

可定義：

$$
\boxed{
\mathbb H_y(N)
=
\left\{
p:
\operatorname{WheelHard}(N,y,p)
\right\}.
}
$$

formal proof初期優先 predicate。

Finset版本後補：

```lean
def WheelHardFinset (N y : Nat) : Finset Nat := ...
```

---

# 12. Small-obstruction predicate

定義：

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

當：

$$
r\in\mathbb P,
$$

$$
r\le y,
$$

以及：

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

Lean-oriented：

```lean
def SmallObstruction (N y p r : Nat) : Prop :=
  Nat.Prime r ∧
  r ≤ y ∧
  r ∣ (N - p)
```

---

# 13. Has-small-obstruction predicate

$$
\boxed{
\operatorname{HasSmallObstruction}(N,y,p)
:
\Longleftrightarrow
\exists r,
\operatorname{SmallObstruction}(N,y,p,r).
}
$$

---

# 14. WheelHard iff no small obstruction

## Theorem V1-03-T03

若：

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

則：

$$
\boxed{
\operatorname{WheelHard}(N,y,p)
\Longleftrightarrow
\neg
\operatorname{HasSmallObstruction}(N,y,p).
}
$$

這是 graph-isolation interface的 predicate版本。

---

# 15. T03 proof核心

由：

$$
r\mid P(y)
\Longleftrightarrow
r\le y
$$

for prime $r$，

有：

$$
\gcd(N-p,P(y))=1
$$

當且僅當：

$$
N-p
$$

沒有任何：

$$
r\le y
$$

的 prime divisor。

---

# 16. 為什麼不直接建 graph

V1-03 不需要 graph library。

先用：

```text
SmallObstruction
HasSmallObstruction
WheelHard
```

建立 exact relation。

之後若需要 graph，

它只是一個 representation layer。

這避免 graph API污染 arithmetic core。

---

# 17. Cutoff nesting

## Theorem V1-03-T04

若：

$$
y_1\le y_2,
$$

且：

$$
\operatorname{WheelHard}(N,y_2,p),
$$

則：

$$
\boxed{
\operatorname{WheelHard}(N,y_1,p).
}
$$

---

# 18. T04 proof

如果 complement避開所有：

$$
r\le y_2,
$$

自然也避開：

$$
r\le y_1.
$$

可由 T03 no-small-obstruction語義證，

不必操作 product divisibility。

---

# 19. Hard-set nesting

set形式：

$$
\boxed{
\mathbb H_{y_2}(N)
\subseteq
\mathbb H_{y_1}(N)
}
$$

當：

$$
y_1\le y_2.
$$

這是 V0/R03 wheel-hard nesting的 general cutoff form。

---

# 20. General self-suppression lemma

V1-02 已有：

若：

$$
r,p\in\mathbb P,
$$

$$
r\mid N,
$$

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

則：

$$
p=r.
$$

本輪將它重用成 saturation geometry。

---

# 21. Saturated cutoff：small prime input一定不 hard

## Lemma V1-03-L01

若：

$$
\operatorname{PrimeSaturatedAt}(N,y),
$$

$$
p\in\mathbb P,
$$

$$
p\le y,
$$

且：

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

則：

$$
\boxed{
\neg\operatorname{WheelHard}(N,y,p).
}
$$

---

# 22. L01 proof

因 saturation：

$$
p\mid N.
$$

當然：

$$
p\mid p.
$$

所以：

$$
p\mid(N-p).
$$

且：

$$
p\le y.
$$

所以：

$$
\operatorname{HasSmallObstruction}(N,y,p).
$$

由 T03：

not hard。

---

# 23. Saturated cutoff：large prime input一定 hard

## Lemma V1-03-L02

若：

$$
\operatorname{PrimeSaturatedAt}(N,y),
$$

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

且：

$$
y<p,
$$

則：

$$
\boxed{
\operatorname{WheelHard}(N,y,p).
}
$$

---

# 24. L02 proof

反設有 small obstruction：

$$
r\le y,
$$

$$
r\in\mathbb P,
$$

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

由 saturation：

$$
r\mid N.
$$

V1-02 self-suppression推出：

$$
p=r.
$$

但：

$$
r\le y<p.
$$

矛盾。

所以沒有 small obstruction。

由 T03：

hard。

---

# 25. Saturated Hard-Sector Theorem

## Theorem V1-03-T05

若：

$$
\operatorname{PrimeSaturatedAt}(N,y),
$$

則：

$$
\boxed{
\operatorname{WheelHard}(N,y,p)
\Longleftrightarrow
\operatorname{ReducedPrimeInput}(N,p)
\land
y<p.
}
$$

這是本輪主 theorem。

---

# 26. T05 不需要 failure

這點必須寫進 theorem metadata：

```yaml
uses_goldbach_failure: false
```

它只使用：

- prime input；
- saturation；
- divisibility；
- self-suppression。

這是 V0-R03 最重要的 source correction之一。

---

# 27. Hard sector不是 conjectural object

所以：

$$
\mathbb H_y(N)
$$

在 saturation branch可 exact 算出：

$$
\boxed{
\mathbb H_y(N)
=
\left\{
p\in\mathbb P:
2p\le N,
\quad
p>y
\right\}.
}
$$

不需要知道：

$$
N-p
$$

prime還是 composite。

---

# 28. Exact finite prime count

定義：

$$
\boxed{
\pi_{\le}(x)
=
\#\left\{
p\in\mathbb P:
p\le x
\right\}.
}
$$

這是 finite exact count。

在 formal core中它不是 PNT analytic source。

---

# 29. Reduced prime count

也可定義：

$$
\boxed{
\Pi^{-}(N)
=
\#\left\{
p\in\mathbb P:
2p\le N
\right\}.
}
$$

若：

$$
N
$$

even，

則：

$$
\Pi^{-}(N)
=
\pi(N/2).
$$

formalization優先用：

$$
2p\le N
$$

版本。

---

# 30. Hard-count definition

$$
\boxed{
D_N(y)
=
|\mathbb H_y(N)|.
}
$$

這與 V0/R06 demand object一致。

V1-03可以先定義：

```lean
def WheelDemand (N y : Nat) : Nat :=
  (WheelHardFinset N y).card
```

若 Finset implementation尚未完成，

先證 set-bijection theorem。

---

# 31. Saturated hard-count theorem

## Theorem V1-03-T06

若：

$$
\operatorname{PrimeSaturatedAt}(N,y),
$$

則：

$$
\boxed{
D_N(y)
=
\#\left\{
p\in\mathbb P:
2p\le N,
\quad
p>y
\right\}.
}
$$

---

# 32. Count formula with $\pi$

若再有：

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

且：

$$
y\le N/2,
$$

則：

$$
\boxed{
D_N(y)
=
\pi(N/2)-\pi(y).
}
$$

這只是 finite count identity，

不是 analytic estimate。

---

# 33. Primorial interface

數學 notation：

$$
p_1=2,
\quad
p_2=3,
\quad
p_3=5,
\ldots
$$

以及：

$$
\boxed{
M_k
=
\prod_{i=1}^{k}p_i.
}
$$

本輪不要求 Lean core立刻選定 nth-prime API。

先定 interface：

```text
PrimePrefix k
Primorial k
KthPrime k
```

並要求證：

$$
M_k=P(p_k).
$$

---

# 34. Primorial divisibility implies saturation

## Theorem V1-03-T07

若：

$$
M_k\mid N,
$$

則：

$$
\boxed{
\operatorname{PrimeSaturatedAt}(N,p_k).
}
$$

因每個：

$$
r\le p_k
$$

的 prime都是前 $k$ 個 primes之一。

---

# 35. Saturation implies primorial divisibility

若：

$$
\operatorname{PrimeSaturatedAt}(N,p_k),
$$

則：

$$
\boxed{
M_k\mid N.
}
$$

所以：

$$
\boxed{
M_k\mid N
\Longleftrightarrow
\operatorname{PrimeSaturatedAt}(N,p_k).
}
$$

這是 primorial notation與 general cutoff kernel的 bridge。

---

# 36. Primorial hard-sector theorem

## Corollary V1-03-C01

若：

$$
M_k\mid N,
$$

則：

$$
\boxed{
\operatorname{WheelHard}(N,p_k,p)
\Longleftrightarrow
\operatorname{ReducedPrimeInput}(N,p)
\land
p_k<p.
}
$$

不需要 failure。

---

# 37. Primorial demand formula

## Theorem V1-03-T08

若：

$$
M_k\mid N,
$$

以及：

$$
p_k\le N/2,
$$

則：

$$
\boxed{
D_N(p_k)
=
\pi(N/2)-k.
}
$$

因：

$$
\pi(p_k)=k.
$$

這個 theorem在 canonical ledger歸 V1-03 / R03 geometry。

---

# 38. Indexing firewall

若 Lean API採 zero-based nthPrime，

repo內必須提供 one-based wrapper：

```lean
def kthPrime1 (k : Nat) (hk : 1 ≤ k) : Nat := ...
```

或完全避免 theorem statement使用 API indexing。

數學文件一律維持：

$$
p_1=2.
$$

不能因 implementation API改變 paper notation。

---

# 39. M6 as $y=3$

因：

$$
P(3)=2\cdot3=6,
$$

所以：

$$
\boxed{
\operatorname{WheelHard}(N,3,p)
}
$$

就是：

$$
\operatorname{ReducedPrimeInput}(N,p)
\land
\gcd(N-p,6)=1.
$$

這與舊：

$$
\mathbb H_6(N)
$$

一致。

---

# 40. $6\mid N$ exact hard sector

## Corollary V1-03-C02

若：

$$
6\mid N,
$$

則：

$$
\boxed{
\operatorname{WheelHard}(N,3,p)
\Longleftrightarrow
\operatorname{ReducedPrimeInput}(N,p)
\land
3<p.
}
$$

---

# 41. M6 hard count

若：

$$
6\mid N,
$$

且：

$$
3\le N/2,
$$

則：

$$
\boxed{
D_N(3)
=
\pi(N/2)-2.
}
$$

因：

$$
\pi(3)=2.
$$

對：

$$
N\ge6
$$

成立。

---

# 42. Failure enters only now

到目前：

- hard sector；
- hard count；
- nesting；
- primorial formula；

全部不需要 Goldbach failure。

現在才加入：

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

---

# 43. Rough-above-cutoff predicate

定義：

$$
\boxed{
\operatorname{RoughCompositeAbove}(m,y)
}
$$

當：

1. $m$ composite；
2. 每個 prime divisor $r$ 都滿足：
   $$
   y<r.
   $$

Lean-oriented：

```lean
def RoughCompositeAbove (m y : Nat) : Prop :=
  Composite m ∧
  ∀ r, Nat.Prime r → r ∣ m → y < r
```

---

# 44. Equivalent coprime form

對 composite：

$$
m,
$$

有：

$$
\boxed{
\operatorname{RoughCompositeAbove}(m,y)
\Longleftrightarrow
\operatorname{Composite}(m)
\land
\gcd(m,P(y))=1.
}
$$

這可作 theorem。

---

# 45. Failure hard survivor becomes rough composite

## Theorem V1-03-T09

若：

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

以及：

$$
\operatorname{WheelHard}(N,y,p),
$$

則：

$$
\boxed{
\operatorname{RoughCompositeAbove}(N-p,y).
}
$$

---

# 46. T09 proof

由 failure + reduced input：

$$
N-p
$$

not prime。

V1-02 lower bound：

$$
N-p\ge2.
$$

所以 composite。

WheelHard給：

$$
\gcd(N-p,P(y))=1.
$$

因此任何 prime divisor：

$$
r\le y
$$

都不可能整除：

$$
N-p.
$$

所以所有 prime divisors：

$$
>y.
$$

---

# 47. Least-factor consequence

## Corollary V1-03-C03

若：

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

且：

$$
\operatorname{WheelHard}(N,y,p),
$$

則：

$$
\boxed{
\operatorname{lpf}(N-p)>y.
}
$$

這把 hard geometry接回 V1-02 factor source。

---

# 48. Primorial rough-composite wall

## Theorem V1-03-T10

若：

$$
M_k\mid N,
$$

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

且：

$$
p_k<p,
$$

$$
2p\le N,
$$

$$
p\in\mathbb P,
$$

則：

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

以及：

$$
\boxed{
\operatorname{lpf}(N-p)>p_k.
}
$$

---

# 49. Wall set

定義：

$$
\boxed{
\mathcal W_k(N)
=
\left\{
N-p:
p\in\mathbb P,
\quad
p_k<p,
\quad
2p\le N
\right\}.
}
$$

若：

$$
M_k\mid N
$$

且 failure，

則：

$$
\boxed{
\mathcal W_k(N)
\subseteq
\left\{
m:
\operatorname{RoughCompositeAbove}(m,p_k)
\right\}.
}
$$

這是 exact set form。

---

# 50. Rough wall的 source meaning

單個：

$$
N-p
$$

rough composite並不稀奇。

真正 relational target是：

> 同一個 $N$ 生成的大量 complements同時 rough且 composite。

但 V1-03 只 formalize elementwise + set inclusion。

跨-$p$ capacity theorem留 V1-07。

---

# 51. Cutoff hard graph interface

定義 relation：

$$
r\sim_{N,y}p
$$

當：

$$
\operatorname{SmallObstruction}(N,y,p,r).
$$

則：

$$
\operatorname{WheelHard}(N,y,p)
$$

等價於：

> $p$ 在這個 truncated obstruction relation中沒有 right neighbor。

這只是 interface。

不需要建 graph object。

---

# 52. Graph deficiency future bridge

若定義：

$$
\delta_{N,y}
=
\#\left\{
p:
\operatorname{ReducedPrimeInput}(N,p)
\land
\operatorname{WheelHard}(N,y,p)
\right\},
$$

則：

$$
\delta_{N,y}
=
D_N(y).
$$

真正：

$$
R_G^{-}
$$

只在 cutoff到 proper-factor full range或使用 V1-07 canonical capacity後出現。

所以 V1-03 不把：

$$
D_N(y)
$$

誤叫 Goldbach representation count。

---

# 53. Hard-set nesting and demand monotonicity

由 T04：

若：

$$
y_1\le y_2,
$$

則：

$$
\mathbb H_{y_2}(N)
\subseteq
\mathbb H_{y_1}(N).
$$

所以：

$$
\boxed{
D_N(y_2)
\le
D_N(y_1).
}
$$

這是 exact cutoff monotonicity。

---

# 54. Saturation monotonicity

若：

$$
\operatorname{PrimeSaturatedAt}(N,y_2)
$$

且：

$$
y_1\le y_2,
$$

則：

$$
\boxed{
\operatorname{PrimeSaturatedAt}(N,y_1).
}
$$

trivial但可供 theorem automation。

---

# 55. Hard-sector formula與 failure分層

formal theorem命名必須分開。

## Unconditional

```text
saturated_wheelHard_iff_prime_above_cutoff
primorial_hard_sector
primorial_demand_formula
```

## Conditional on failure

```text
failure_hard_implies_rough_composite
primorial_failure_rough_wall
```

不要把 failure塞進第一組 theorem。

---

# 56. Effective wheel forbidden

V1-03 明確不定義：

```text
EffectiveWheel
EffectiveHard
SuppressedWheel
```

原因已在 V0-R03 audit完成。

如果未來某 experiment想保留 legacy metric，

必須放：

```text
RGSCP.Discovery.Legacy
```

不能進：

```text
RGSCP.Core
```

---

# 57. Obstruction availability alphabet不作 primitive

同理：

$$
\Sigma_{\mathrm{avail}}(N;y)
$$

不進 core。

真正 exact primitive已經是：

$$
\operatorname{SmallObstruction}(N,y,p,r).
$$

availability是：

$$
(p,r)
$$

dependent，

不應壓成只依：

$$
N,y
$$

的簡化 alphabet。

---

# 58. Formal count implementation

可以定義：

```lean
def WheelHardFinset (N y : Nat) : Finset Nat :=
  (ReducedPrimeFinset N).filter
    (fun p => Nat.Coprime (N - p) (PrimeCutoffProduct y))

def WheelDemand (N y : Nat) : Nat :=
  (WheelHardFinset N y).card
```

V1-01 若尚未正式建立 `ReducedPrimeFinset`，

本輪可只寫 interface requirement。

---

# 59. Exact prime-count helper

```lean
def PrimeCountLe (x : Nat) : Nat :=
  ((Finset.range (x + 1)).filter Nat.Prime).card
```

這是 finite exact combinatorial count。

它不使用：

- PNT；
- asymptotic；
- analytic approximation。

所以 source：

$$
\mathcal S_0
$$

加 primality predicate，

不是：

$$
\mathcal S_5.
$$

---

# 60. Count bridge

對 even：

$$
N,
$$

可證：

$$
\boxed{
\#\{p\in\mathbb P:2p\le N\}
=
\pi(N/2).
}
$$

Lean若 Nat division API麻煩，

formal core可直接保留左側 cardinality。

paper / report再寫：

$$
\pi(N/2).
$$

---

# 61. Primorial count interface

需要：

$$
\boxed{
\pi(p_k)=k.
}
$$

但這依賴 kth-prime indexing convention。

所以 V1-03 formal implementation可先用：

$$
\pi(p_k)
$$

形式，

等 prime-index wrapper固定後再 rewrite為：

$$
k.
$$

---

# 62. Canonical theorem queue

```yaml
V1_03:
  - id: T01
    name: prime_dvd_cutoff_product_iff_le
    status: to_formalize

  - id: T02
    name: cutoff_product_dvd_iff_prime_saturated
    status: to_formalize

  - id: T03
    name: wheelHard_iff_no_small_obstruction
    status: to_formalize

  - id: T04
    name: wheelHard_mono_cutoff
    status: to_formalize

  - id: T05
    name: saturated_wheelHard_iff_prime_above_cutoff
    status: to_formalize

  - id: T06
    name: saturated_wheelDemand_exact
    status: to_formalize

  - id: T07
    name: primorial_divides_implies_saturation
    status: to_formalize

  - id: T08
    name: primorial_demand_formula
    status: to_formalize

  - id: T09
    name: failure_hard_implies_rough_composite
    status: to_formalize

  - id: T10
    name: primorial_failure_rough_wall
    status: to_formalize
```

---

# 63. Lean-oriented skeleton

```lean
namespace RGSCP

def PrimeCutoffFinset (y : Nat) : Finset Nat :=
  (Finset.range (y + 1)).filter Nat.Prime

def PrimeCutoffProduct (y : Nat) : Nat :=
  ∏ r in PrimeCutoffFinset y, r

def PrimeSaturatedAt (N y : Nat) : Prop :=
  ∀ r, Nat.Prime r → r ≤ y → r ∣ N

def SmallObstruction
    (N y p r : Nat) : Prop :=
  Nat.Prime r ∧
  r ≤ y ∧
  r ∣ (N - p)

def HasSmallObstruction
    (N y p : Nat) : Prop :=
  ∃ r, SmallObstruction N y p r

def WheelHard
    (N y p : Nat) : Prop :=
  ReducedPrimeInput N p ∧
  Nat.Coprime (N - p) (PrimeCutoffProduct y)

def RoughCompositeAbove
    (m y : Nat) : Prop :=
  Composite m ∧
  ∀ r, Nat.Prime r → r ∣ m → y < r

end RGSCP
```

這是 specification，不宣稱當前 Lean syntax/API 已 compile。

---

# 64. Unit test：cutoff product

應驗：

$$
P(1)=1,
$$

$$
P(2)=2,
$$

$$
P(3)=6,
$$

$$
P(5)=30,
$$

$$
P(7)=210.
$$

---

# 65. Unit test：$N=30,\ y=5$

因：

$$
2,3,5\mid30,
$$

所以：

$$
\operatorname{PrimeSaturatedAt}(30,5).
$$

reduced primes：

$$
2,3,5,7,11,13.
$$

hard iff：

$$
p>5.
$$

所以：

$$
\mathbb H_5(30)
=
\{7,11,13\}.
$$

---

# 66. Unit test：$N=30,\ y=3$

$$
P(3)=6.
$$

hard reduced primes應：

$$
\{5,7,11,13\}.
$$

即所有：

$$
p>3.
$$

---

# 67. Unit test：target not saturated

取：

$$
N=34,
\quad
y=3.
$$

$$
2\mid34
$$

但：

$$
3\nmid34.
$$

所以：

$$
\neg\operatorname{PrimeSaturatedAt}(34,3).
$$

此時：

$$
p>3
$$

不代表一定 hard。

例如：

$$
p=7,
$$

$$
34-7=27,
$$

被：

$$
3
$$

整除，

所以不 hard。

這證明 saturated theorem的 assumption不可刪。

---

# 68. Unit test：self-cell

取：

$$
N=30,
\quad
y=5,
\quad
p=5.
$$

因：

$$
5\mid30
$$

且：

$$
5\mid25,
$$

所以：

$$
p=5
$$

不是 hard。

這也再次說明 effective wheel不可用。

---

# 69. Unit test：large prime hard

$$
N=30,
\quad
y=5,
\quad
p=7.
$$

$$
30-7=23.
$$

$$
\gcd(23,30)=1.
$$

所以 hard。

即使 complement恰好 prime，

hard predicate仍 true。

這證明：

$$
\boxed{
\text{hard}
\neq
\text{composite}.
}
$$

failure未加入前不能稱 obstruction success。

---

# 70. Unit test：failure-conditional roughness

因實際：

$$
N=30
$$

不是 failure，

不能用它測 rough-composite theorem的 premise。

實驗層若想 unit test implication，

可直接測：

```text
if GoldbachFailure N then ...
```

或使用 synthetic proposition branch，

不能虛構：

$$
F_G(30)=1.
$$

這是 truth discipline。

---

# 71. Unit test：M6

取：

$$
N=60.
$$

$$
6\mid60.
$$

對 reduced prime：

$$
p=5,
$$

$$
60-5=55,
$$

與 $6$ coprime。

對：

$$
p=3,
$$

$$
60-3=57,
$$

被 $3$ 整除。

所以 hard iff：

$$
p>3.
$$

---

# 72. Unit test：nesting

同一：

$$
N,p,
$$

若：

$$
p
$$

hard at：

$$
y=7,
$$

必 hard at：

$$
y=5,
3,
2.
$$

反向不保證。

---

# 73. Failure wall theorem不應反推 failure

如果對某個 subset：

$$
p>y
$$

觀察到：

$$
N-p
$$

rough composite，

不能直接推出：

$$
F_G(N).
$$

因可能仍有：

- small $p$ representation；
- hard subset外 representation。

所以 T09/T10只有：

$$
\boxed{
\text{failure}
\Rightarrow
\text{rough wall}
}
$$

不是 equivalence。

---

# 74. Primorial demand不應被叫 capacity

$$
D_N(p_k)
=
\pi(N/2)-k
$$

是 survivor demand。

它不表示：

- composite count；
- obstruction capacity；
- Goldbach representation count。

這個 terminology firewall延續 V0-R06。

---

# 75. Source provenance

本輪 source：

## $\mathcal S_0$

- finite products；
- order；
- gcd；
- divisibility；
- finite counting。

## $\mathcal S_1$

- failure下 complement composite；
- lpf consequence。

## $\mathcal S_2$

- cutoff / wheel geometry。

沒有：

- $\mathcal S_3$ fixed point；
- $\mathcal S_4$ minimality；
- $\mathcal S_5$ analytic；
- $\mathcal S_6$ heuristic。

---

# 76. Proof-compression status

V1-03 真正的 compression是：

若：

$$
P(y)\mid N,
$$

就不用逐個檢查：

$$
r=2,3,5,\ldots\le y
$$

對每個大 prime input的 complement。

一個 saturation assumption同時推出：

$$
\boxed{
\forall p>y,
\quad
\gcd(N-p,P(y))=1.
}
$$

這是：

$$
\boxed{
\text{synchronized constraint compression within } \mathcal S_2.
}
$$

不是 source escape。

---

# 77. Constraint metadata：Saturated hard sector

```yaml
constraint:
  id: K_SAT_HARD

  statement:
    PrimeSaturatedAt(N,y)
    -> WheelHard(N,y,p) iff ReducedPrimeInput(N,p) and y<p

  exact: true
  source:
    - S0
    - S2

  uses_failure: false
  target_equivalent: false
  proof_compression_gain: true
  source_escape: false
```

---

# 78. Constraint metadata：Rough wall

```yaml
constraint:
  id: K_ROUGH_WALL

  statement:
    GoldbachFailure(N)
    and WheelHard(N,y,p)
    -> RoughCompositeAbove(N-p,y)

  exact: true
  source:
    - S1
    - S2

  uses_failure: true
  target_equivalent: false
  proof_compression_gain: relational
```

---

# 79. V1-03 Formal Acceptance Gate

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

### G1

PrimeCutoffProduct definition固定。

### G2

prime divisor iff cutoff membership theorem完成。

### G3

PrimeSaturatedAt bridge完成或明確作 primitive interface。

### G4

WheelHard iff no small obstruction完成。

### G5

cutoff nesting完成。

### G6

saturated hard-sector equivalence完成。

### G7

hard-count exact theorem完成。

### G8

primorial bridge indexing無 off-by-one。

### G9

M6 corollary與 $P(3)=6$ 一致。

### G10

failure hard survivor implies rough composite完成。

### G11

effective wheel完全不出現在 core。

### G12

no `sorry`.

---

# 80. Bug / Falsification Checklist

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

1. `PrimeCutoffProduct 3 ≠ 6`；
2. prime $r>y$ 被判成 cutoff product factor；
3. target saturation下 $p\le y$ 卻被標 hard；
4. target saturation下 $p>y$ 卻被標 non-hard；
5. WheelHard definition偷偷加入 complement composite；
6. failure hypothesis被錯放進 hard-sector equality；
7. primorial theorem依賴 effective wheel；
8. $p_k$ indexing把 $p_1$ 變成 $3$；
9. hard count被叫 Goldbach count；
10. prime complement在 nonfailure state被錯當 rough composite；
11. `smooth` terminology重新出現在 theorem name；
12. analytic prime-count estimate進入 exact finite count proof。

---

# 81. Formal dependency graph

```text
V1-02 SelfSuppression
  ↑
PrimeCutoffProduct
  ↓
PrimeSaturatedAt
  ↓
SmallObstruction
  ↓
WheelHard
  ↓
SaturatedHardSector
  ↓
HardCount
  ↓
PrimorialDemand
```

failure branch：

```text
V1-01 GoldbachFailure
  ↓
V1-02 complement composite
  +
WheelHard
  ↓
RoughCompositeAbove
  ↓
Primorial Rough Wall
```

---

# 82. V1-03 Verdict

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

但仍：

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

本輪完成的是：

> 把 primorial / wheel line壓成一個更一般、更 formal-friendly 的 saturation theorem，並嚴格把 unconditional hard geometry 與 failure-conditional rough compositeness分離。

---

# 83. 下一輪

下一篇建議：

# RG-SCP Validation V1-04
## M6 Fixed-Point / Exact Fiber Kernel

只做：

- $M6^*$；
- $T_{\mathrm{top}}$；
- $T_{\mathrm{top}}=\operatorname{lpf}$；
- fixed points $=P^*$；
- exact fiber multiplier $U_p$；
- additive candidate domain nonempty；
- reduced additive candidate domain。

先把 fixed-point source本身鎖死。

下一輪仍不進：

- $\Delta_6$；
- shadow；
- two-channel theorem。

那些留 V1-05。

---

# 84. 最短版本

V1-03 的 machine core可以壓成三層。

## Layer A — Cutoff Geometry

$$
P(y)
=
\prod_{r\le y,\ r\in\mathbb P}r.
$$

$$
\operatorname{WheelHard}(N,y,p)
\Longleftrightarrow
\operatorname{ReducedPrimeInput}(N,p)
\land
\gcd(N-p,P(y))=1.
$$

## Layer B — Saturation

若：

$$
P(y)\mid N,
$$

則：

$$
\boxed{
\operatorname{WheelHard}(N,y,p)
\Longleftrightarrow
\operatorname{ReducedPrimeInput}(N,p)
\land
p>y.
}
$$

所以：

$$
\boxed{
D_N(y)
=
\pi(N/2)-\pi(y).
}
$$

## Layer C — Failure

若再有：

$$
F_G(N)=1,
$$

則每個 hard complement：

$$
\boxed{
N-p
}
$$

都是：

$$
\boxed{
y\text{-rough composite}.
}
$$

primorial只需令：

$$
y=p_k.
$$

這就是 V1-03 的完整 kernel。

---

# 附錄 A：Lean-Oriented Skeleton

```lean
namespace RGSCP

def PrimeCutoffFinset (y : Nat) : Finset Nat :=
  (Finset.range (y + 1)).filter Nat.Prime

def PrimeCutoffProduct (y : Nat) : Nat :=
  ∏ r in PrimeCutoffFinset y, r

def PrimeSaturatedAt (N y : Nat) : Prop :=
  ∀ r, Nat.Prime r → r ≤ y → r ∣ N

def SmallObstruction
    (N y p r : Nat) : Prop :=
  Nat.Prime r ∧
  r ≤ y ∧
  r ∣ (N - p)

def HasSmallObstruction
    (N y p : Nat) : Prop :=
  ∃ r, SmallObstruction N y p r

def WheelHard
    (N y p : Nat) : Prop :=
  ReducedPrimeInput N p ∧
  Nat.Coprime (N - p) (PrimeCutoffProduct y)

def RoughCompositeAbove
    (m y : Nat) : Prop :=
  Composite m ∧
  ∀ r, Nat.Prime r → r ∣ m → y < r

end RGSCP
```

---

# 附錄 B：Canonical Test Vector

```yaml
cutoff_products:
  P1: 1
  P2: 2
  P3: 6
  P5: 30
  P7: 210

cases:
  - N: 30
    y: 5
    saturated: true
    reduced_primes: [2,3,5,7,11,13]
    hard: [7,11,13]

  - N: 30
    y: 3
    saturated: true
    hard: [5,7,11,13]

  - N: 34
    y: 3
    saturated: false
    witness:
      p: 7
      complement: 27
      hard: false

  - N: 60
    y: 3
    saturated: true
    p3:
      p: 3
      hard: false
    p5:
      p: 5
      hard: true
```

---

# 附錄 C：Source Signature

```yaml
RG-SCP-V1-03:
  S0_elementary:
    role:
      - finite_product
      - gcd
      - divisibility
      - finite_count

  S1_factor_lpf:
    role:
      - failure_composite
      - rough_composite_consequence

  S2_finite_quotient_wheel:
    role:
      - cutoff_product
      - hard_sector
      - primorial_geometry

  S3_fixed_point:
    forbidden_dependency: true

  S4_minimality:
    forbidden_dependency: true

  S5_analytic:
    forbidden_dependency: true

  S6_heuristic:
    forbidden_dependency: true

proof_compression:
  synchronized_constraint_compression: true
  source_escape: false
```

---

# 附錄 D：Superseded / Forbidden

```yaml
forbidden_in_core:
  - effective_wheel
  - effective_hard_branch
  - primorial_smooth_shift
  - heuristic_pressure
  - analytic_prime_density

terminology:
  target_primorial_condition:
    use: primorial_divisibility

  future_shift_condition:
    use: primorial_divisible_shift
```

---

# 附錄 E：Commit Decision

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

formal_status:
  machine_checked: false
  lean_compiled: false
  sorry_free: not_yet_tested

canonical_decisions:
  - generalize_primorial_to_prime_saturation_cutoff
  - use_PrimeCutoffProduct_as_primitive
  - hard_sector_geometry_is_unconditional
  - failure_only_enters_at_rough_composite_wall
  - exact_hard_count_uses_finite_prime_count
  - primorial_is_corollary_of_saturation
  - M6_is_y3_corollary
  - effective_wheel_forbidden

next_round:
  V1-04_M6_FixedPoint_Exact_Fiber_Kernel

commit_to_sync_core: true
```