# RG-SCP Validation V1-07
## Incidence Audit / AP Suppression Kernel
### Deep-Factor Multiplicity、Overlap Surplus、Incidence Columns、Raw AP Columns 與 Exact Self-Suppression

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

---

## 摘要

V1-06 已將 demand / capacity 主線鎖成：

$$
\boxed{
D_N(y)
=
R_G^{-}(N)
+
C_N^{\mathrm{can}}(y).
}
$$

因此：

$$
\boxed{
R_G^{-}(N)
=
D_N(y)
-
C_N^{\mathrm{can}}(y).
}
$$

其中：

$$
C_N^{\mathrm{can}}(y)
$$

是無重複的 composite-survivor coverage。

V1-07 現在把舊 RG-SCP 06 的 incidence language接回來，但明確限定為：

$$
\boxed{
\text{audit layer / upper-bound interface}
}
$$

而不是 canonical capacity。

對 survivor：

$$
p\in\mathbb H_y(N),
$$

定義 deep prime-factor set：

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

其 cardinality：

$$
\boxed{
m_y(N,p)
=
|\mathcal R_y(N,p)|
}
$$

稱為 deep-factor multiplicity。

對 prime survivor：

$$
m_y(N,p)=0.
$$

對 composite survivor：

$$
m_y(N,p)\ge1.
$$

因此定義：

$$
\boxed{
I_N(y)
=
\sum_{p\in\mathbb H_y(N)}
m_y(N,p)
}
$$

為：

# Deep Factor-Incidence Mass

而不是 canonical capacity。

再定義：

$$
\boxed{
\Omega_N(y)
=
\sum_{p\in\mathbb H_y(N)}
\left(m_y(N,p)-1\right)_+.
}
$$

在 Nat formalization中可以直接使用：

$$
m_y(N,p)-1,
$$

因：

$$
0-1=0
$$

於 Nat truncated subtraction。

本輪第一個核心 theorem 是：

$$
\boxed{
I_N(y)
=
C_N^{\mathrm{can}}(y)
+
\Omega_N(y).
}
$$

原因完全逐點：

- prime survivor：
  $$
  m=0,
  $$
  對三個量都不貢獻；
- composite survivor：
  $$
  m\ge1,
  $$
  對 canonical coverage貢獻 $1$，
  對 overlap貢獻 $m-1$，
  合計正好 $m$。

再與 V1-06：

$$
D=R+C^{\mathrm{can}}
$$

合併，得到 audit identity：

$$
\boxed{
R_G^{-}(N)
=
D_N(y)
+
\Omega_N(y)
-
I_N(y).
}
$$

formal primitive不建議直接用 Nat subtraction，而優先證：

$$
\boxed{
D_N(y)+\Omega_N(y)
=
R_G^{-}(N)+I_N(y).
}
$$

這樣完全避免 subtraction truncation。

本輪也正式解釋：

$$
D_N(y)>I_N(y)
$$

的真正語義。

由：

$$
D+\Omega=R+I,
$$

有：

$$
\boxed{
D_N(y)>I_N(y)
\Longleftrightarrow
R_G^{-}(N)>\Omega_N(y).
}
$$

所以：

$$
D>I
$$

確實是 Goldbach-success sufficient criterion，

但它不是一般 success characterization。

V0-R06 的 control：

$$
N=68,
\quad
y=2
$$

給：

$$
D=10,
\quad
C^{\mathrm{can}}=8,
\quad
R=2,
\quad
I=10,
\quad
\Omega=2.
$$

因此：

$$
D=I
$$

但：

$$
R=2>0.
$$

這就是為什麼：

$$
I
$$

不能再被視為 canonical coverage capacity。

接著本輪把 incidence按 deep obstruction prime：

$$
r
$$

分解。

定義：

$$
\boxed{
C_r^{\mathrm{inc}}(N;y)
=
\#\left\{
p\in\mathbb H_y(N):
y<r,
\quad
r\in\mathbb P,
\quad
r^2\le N-p,
\quad
r\mid(N-p)
\right\}.
}
$$

則：

$$
\boxed{
I_N(y)
=
\sum_r
C_r^{\mathrm{inc}}(N;y).
}
$$

再移除 survivor restriction，得到 raw AP column：

$$
\boxed{
A_r(N)
=
\#\left\{
p\in\mathbb P:
2p\le N,
\quad
p+r^2\le N,
\quad
r\mid(N-p)
\right\}.
}
$$

其中：

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

是 formal-friendly 版本的：

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

因此：

$$
\boxed{
C_r^{\mathrm{inc}}(N;y)
\le
A_r(N).
}
$$

而：

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

在：

$$
p\le N
$$

時等價於：

$$
\boxed{
p\equiv N\pmod r.
}
$$

所以：

$$
A_r(N)
$$

正是 prime arithmetic-progression column 加 proper-factor range。

本輪再把 divisor self-suppression強化成 exact cardinality theorem。

若：

$$
r\in\mathbb P,
\quad
r\mid N,
$$

則 raw AP column中任何 prime：

$$
p
$$

都必須：

$$
p=r.
$$

而：

$$
p=r
$$

實際落在 raw proper-factor range當且僅當：

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

所以：

$$
\boxed{
A_r(N)
=
\mathbf1_{\{r(r+1)\le N\}}
}
$$

under：

$$
r\in\mathbb P,
\quad
r\mid N.
$$

這比舊：

$$
A_r(N)\le1
$$

更精確。

small-factor demand側也有 exact self-cell theorem。

定義：

$$
\boxed{
S_\ell(N)
=
\left\{
p\in\mathbb P_N^{-}:
\ell\mid(N-p)
\right\}.
}
$$

若：

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

$$
\ell\in\mathbb P,
$$

$$
\ell\le y,
$$

且：

$$
\ell\mid N,
$$

則：

$$
\boxed{
S_\ell(N)=\{\ell\}.
}
$$

這不是「最多一個」，而是 exact singleton。

V1-07 最後只建立 AP upper-bound interface，不把任何 analytic theorem塞進 elementary core。

也就是：

$$
\boxed{
C_r^{\mathrm{inc}}(N;y)
\le
A_r(N)
}
$$

之後可以由：

- exact finite AP count；
- Brun–Titchmarsh；
- explicit PNT in AP；
- sieve bound；

提供：

$$
A_r(N)\le U_r(N).
$$

但具體：

$$
U_r
$$

全部屬：

$$
\mathcal S_5
$$

external analytic layer。

---

# 1. Dependency Boundary

允許：

- V1-01 reduced prime domain；
- V1-02 Composite / ProperPrimeFactor / self-suppression；
- V1-03 WheelHard / cutoff product；
- V1-06 CompositeSurvivor / CanonicalCoverage；
- finite cardinality / finite sums；
- modular equivalence / divisibility。

禁止：

- Brun–Titchmarsh proof；
- PNT in AP；
- sieve theorem；
- minimality transport；
- heuristic。

---

# 2. Deep Factor Predicate

定義：

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

當：

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

$$
y<r,
$$

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

以及：

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

Lean-oriented：

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

---

# 3. Deep Factor Finite Range

若：

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

則：

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

所以：

$$
r\le N.
$$

因此可用：

```text
Finset.range (N + 1)
```

作 finite enumeration universe。

---

# 4. Deep Factor Finset

概念：

```lean
def DeepFactorFinset
    (N y p : Nat) : Finset Nat :=
  (Finset.range (N + 1)).filter
    (fun r => DeepFactor N y p r)
```

實際 boolean / decidable syntax依 API調整。

---

# 5. Deep Multiplicity

定義：

$$
\boxed{
m_y(N,p)
=
|\mathcal R_y(N,p)|.
}
$$

Lean-oriented：

```lean
def DeepMultiplicity
    (N y p : Nat) : Nat :=
  (DeepFactorFinset N y p).card
```

---

# 6. Prime Survivor Has Zero Multiplicity

## Theorem V1-07-T01

若：

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

且：

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

則：

$$
\boxed{
m_y(N,p)=0.
}
$$

因任何：

$$
r
$$

若整除 prime complement，

只能：

$$
r=N-p,
$$

但這時：

$$
r^2>N-p
$$

因：

$$
N-p\ge2.
$$

所以不可能是 proper factor incidence。

---

# 7. Composite Survivor Has Positive Multiplicity

## Theorem V1-07-T02

若：

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

則：

$$
\boxed{
0<m_y(N,p).
}
$$

---

# 8. T02 Proof

令：

$$
r=\operatorname{minFac}(N-p).
$$

composite給：

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

survivor給：

$$
r>y.
$$

所以：

$$
r
$$

在 DeepFactorFinset中。

---

# 9. Multiplicity Zero iff Prime Survivor

## Theorem V1-07-T03

若：

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

則：

$$
\boxed{
m_y(N,p)=0
\Longleftrightarrow
\operatorname{Prime}(N-p).
}
$$

由 survivor prime/composite dichotomy + T01/T02。

---

# 10. Incidence Mass

定義：

$$
\boxed{
I_N(y)
=
\sum_{p\in\mathbb H_y(N)}
m_y(N,p).
}
$$

Lean-oriented：

```lean
def DeepIncidenceMass (N y : Nat) : Nat :=
  ∑ p in SurvivorFinset N y,
    DeepMultiplicity N y p
```

---

# 11. Overlap Surplus

定義：

$$
\boxed{
\Omega_N(y)
=
\sum_{p\in\mathbb H_y(N)}
\left(m_y(N,p)-1\right).
}
$$

因 Nat subtraction：

$$
0-1=0.
$$

所以 prime survivor自然貢獻 $0$。

Lean：

```lean
def OverlapSurplus (N y : Nat) : Nat :=
  ∑ p in SurvivorFinset N y,
    DeepMultiplicity N y p - 1
```

---

# 12. Pointwise Multiplicity Decomposition

## Theorem V1-07-T04

若：

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

則：

$$
\boxed{
m_y(N,p)
=
\mathbf1_{\{\operatorname{Composite}(N-p)\}}
+
\left(m_y(N,p)-1\right).
}
$$

Nat form按兩 case證：

### prime complement

$$
m=0,
$$

右側：

$$
0+0.
$$

### composite complement

$$
m\ge1,
$$

右側：

$$
1+(m-1)=m.
$$

---

# 13. Incidence-Coverage Identity

## Theorem V1-07-T05

$$
\boxed{
I_N(y)
=
C_N^{\mathrm{can}}(y)
+
\Omega_N(y).
}
$$

這是本輪主 audit identity。

不需要 Goldbach failure。

---

# 14. Formal-Friendly Combined Identity

V1-06：

$$
D=R+C^{can}.
$$

V1-07：

$$
I=C^{can}+\Omega.
$$

所以：

$$
\boxed{
D_N(y)+\Omega_N(y)
=
R_G^{-}(N)+I_N(y).
}
$$

對 legal cutoff成立。

這是 machine primitive建議形式。

---

# 15. Paper-Facing Audit Identity

由上式可寫：

$$
\boxed{
R_G^{-}(N)
=
D_N(y)
+
\Omega_N(y)
-
I_N(y).
}
$$

但 formal core不以 subtraction版本作 primitive。

---

# 16. Failure Incidence Identity

若：

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

則：

$$
R_G^{-}(N)=0.
$$

所以：

$$
\boxed{
I_N(y)
=
D_N(y)
+
\Omega_N(y).
}
$$

這比：

$$
D\le I
$$

更精確。

---

# 17. Old Demand-Incidence Inequality

## Corollary V1-07-C01

failure下：

$$
\boxed{
D_N(y)\le I_N(y).
}
$$

它只是：

$$
I=D+\Omega
$$

與：

$$
\Omega\ge0
$$

的弱 corollary。

---

# 18. Exact Meaning of $D>I$

## Theorem V1-07-T06

對 legal cutoff：

$$
\boxed{
D_N(y)>I_N(y)
\Longleftrightarrow
R_G^{-}(N)>\Omega_N(y).
}
$$

---

# 19. T06 Proof

由：

$$
D+\Omega=R+I.
$$

所以：

$$
D>I
$$

等價於：

$$
D+\Omega>I+\Omega.
$$

再 substitute：

$$
R+I>I+\Omega.
$$

由 Nat addition cancellation：

$$
R>\Omega.
$$

反向同理。

---

# 20. Consequence

因此：

$$
D>I
$$

只在：

$$
\boxed{
\text{representation count exceeds overlap surplus}
}
$$

時觸發。

它不是：

$$
R>0
$$

的等價形式。

---

# 21. Control Example：$N=68,\ y=2$

exact values：

$$
D_{68}(2)=10,
$$

$$
R_G^{-}(68)=2,
$$

$$
C_{68}^{can}(2)=8,
$$

$$
I_{68}(2)=10,
$$

$$
\Omega_{68}(2)=2.
$$

所以：

$$
10=2+8,
$$

$$
10=8+2,
$$

以及：

$$
10+2=2+10.
$$

但：

$$
D>I
$$

為 false。

所以 success不等於 demand-incidence deficit。

---

# 22. Incidence Column Predicate

固定：

$$
r,
$$

定義：

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

當：

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

且：

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

Lean：

```lean
def IncidenceAt
    (N y r p : Nat) : Prop :=
  WheelHard N y p ∧
  DeepFactor N y p r
```

---

# 23. Incidence Column

$$
\boxed{
C_r^{\mathrm{inc}}(N;y)
=
\#\left\{
p:
\operatorname{IncidenceAt}(N,y,r,p)
\right\}.
}
$$

這和：

$$
C_r^{\mathrm{can}}
$$

不同。

必須保留命名：

```text
IncidenceColumn
CanonicalCoverageCell
```

---

# 24. Incidence Double Counting Identity

## Theorem V1-07-T07

$$
\boxed{
I_N(y)
=
\sum_{\substack{
r\in\mathbb P\\
y<r\\
r^2\le N-2
}}
C_r^{\mathrm{inc}}(N;y).
}
$$

這是 finite double-counting / sum-swap theorem。

---

# 25. Raw Proper-Factor AP Predicate

定義：

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

當：

$$
p\in\mathbb P,
$$

$$
2p\le N,
$$

$$
p+r^2\le N,
$$

以及：

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

Lean-oriented：

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

對 AP theorem另外假設：

$$
r
$$

prime。

---

# 26. Why Use $p+r^2\le N$

這是：

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

的 Nat-safe additive形式。

好處：

- 不依賴 subtraction rewrite；
- 直接給 finite interval upper bound；
- divisor-column exact indicator更容易證。

---

# 27. Raw AP Column

定義：

$$
\boxed{
A_r(N)
=
\#\left\{
p:
\operatorname{RawAPInput}(N,r,p)
\right\}.
}
$$

它移除了 survivor restriction。

所以：

$$
\boxed{
C_r^{\mathrm{inc}}(N;y)
\le
A_r(N).
}
$$

---

# 28. Incidence-to-Raw Inclusion

## Theorem V1-07-T08

若：

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

則：

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

因：

- WheelHard給 reduced prime input；
- DeepFactor給：
  $$
  r^2\le N-p,
  $$
  等價：
  $$
  p+r^2\le N.
  $$

---

# 29. Column Cardinality Upper Bound

## Corollary V1-07-C02

$$
\boxed{
C_r^{\mathrm{inc}}(N;y)
\le
A_r(N).
}
$$

因此：

$$
\boxed{
I_N(y)
\le
\sum_r A_r(N).
}
$$

over legal deep factor range。

---

# 30. Arithmetic Progression Bridge

若：

$$
p\le N,
$$

則：

$$
\boxed{
r\mid(N-p)
\Longleftrightarrow
N\equiv p\pmod r.
}
$$

Lean可使用：

```text
Nat.ModEq r N p
```

而不一定手工操作 `%`。

---

# 31. Raw AP Exact Set Form

對 prime：

$$
r,
$$

$$
A_r(N)
$$

等價於：

$$
\#\left\{
p\in\mathbb P:
2p\le N,
\quad
p+r^2\le N,
\quad
p\equiv N\pmod r
\right\}.
$$

所以它確實是一個 prime-in-AP column。

---

# 32. Divisor Self-Suppression Reused

V1-02 已證：

若：

$$
r,p
$$

prime，

$$
r\mid N,
$$

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

則：

$$
p=r.
$$

因此 divisor raw AP column只能出現 self-input。

---

# 33. Divisor Column Exact Membership

## Theorem V1-07-T09

若：

$$
r\in\mathbb P,
$$

$$
r\mid N,
$$

則：

$$
\boxed{
\operatorname{RawAPInput}(N,r,p)
\Longleftrightarrow
p=r
\land
r+r^2\le N.
}
$$

---

# 34. T09 Forward

RawAPInput給：

- $p$ prime；
- $r\mid N-p$。

配：

$$
r\mid N
$$

由 self-suppression：

$$
p=r.
$$

剩 proper-factor range：

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

---

# 35. T09 Reverse

若：

$$
p=r,
$$

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

則：

- $p$ prime；
- $2r\le r+r^2\le N$，因 prime $r\ge2$；
- proper range成立；
- $r\mid N-r$，由 $r\mid N$。

所以 RawAPInput成立。

---

# 36. Divisor Column Exact Cardinality

## Theorem V1-07-T10

若：

$$
r\in\mathbb P,
$$

$$
r\mid N,
$$

則：

$$
\boxed{
A_r(N)
=
\begin{cases}
1,
&
r(r+1)\le N,
\\
0,
&
r(r+1)>N.
\end{cases}
}
$$

即：

$$
\boxed{
A_r(N)
=
\mathbf1_{\{r(r+1)\le N\}}.
}
$$

---

# 37. Why $r+r^2=r(r+1)$

formal proof可使用：

$$
r+r^2
=
r(1+r)
=
r(r+1).
$$

這只是 semiring normalization。

---

# 38. Raw AP Divisor Column Is Exact Suppression

舊 theorem只有：

$$
A_r(N)\le1.
$$

V1-07正式升格：

$$
\boxed{
A_r(N)
=
0\text{ or }1
}
$$

且由：

$$
r(r+1)\le N
$$

精確決定。

---

# 39. Small-Factor Screening Cell

定義：

$$
\boxed{
\operatorname{SmallScreenInput}(N,\ell,p)
:
\Longleftrightarrow
\operatorname{ReducedPrimeInput}(N,p)
\land
\ell\mid(N-p).
}
$$

其中 theorem premise會要求：

$$
\ell
$$

prime。

---

# 40. Small-Factor Self-Cell Theorem

## Theorem V1-07-T11

若：

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

$$
\ell\in\mathbb P,
$$

$$
\ell\le y,
$$

以及：

$$
\ell\mid N,
$$

則：

$$
\boxed{
\operatorname{SmallScreenInput}(N,\ell,p)
\Longleftrightarrow
p=\ell.
}
$$

---

# 41. T11 Forward

由：

$$
\ell\mid N
$$

與：

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

self-suppression：

$$
p=\ell.
$$

---

# 42. T11 Reverse

需證：

$$
p=\ell
$$

確實是 reduced prime input。

prime已有。

由：

$$
\ell\le y
$$

與：

$$
2y<N,
$$

有：

$$
2\ell<N,
$$

所以：

$$
2\ell\le N.
$$

又：

$$
\ell\mid N-\ell.
$$

因此成立。

---

# 43. Exact Singleton Form

set form：

$$
\boxed{
S_\ell(N)=\{\ell\}.
}
$$

在 T11 assumptions下。

這比：

$$
|S_\ell(N)|\le1
$$

更強。

---

# 44. Raw AP Nondivisor Column

若：

$$
r\nmid N,
$$

則 residue：

$$
N\bmod r
$$

是 nonzero。

對 prime $r$：

$$
\gcd(N,r)=1.
$$

所以 raw column可交給 standard reduced-residue AP theorem。

---

# 45. AP Upper-Bound Interface

本輪只定 abstract interface：

```text
APUpperBound(N,r,U):
  A_r(N) <= U
```

不把 Brun–Titchmarsh theorem proof塞入 core。

---

# 46. External Analytic Layer

未來可以有：

$$
\boxed{
A_r(N)
\le
U_r^{\mathrm{BT}}(N)
}
$$

或：

$$
U_r^{\mathrm{PNT/AP}},
$$

但 source標：

$$
\boxed{
\mathcal S_5.
}
$$

V1-07只需要：

> upper bound的 statement能接到 RawAPColumn。

---

# 47. Incidence Upper Envelope

由：

$$
C_r^{inc}\le A_r,
$$

可得：

$$
\boxed{
I_N(y)
\le
\sum_r A_r(N).
}
$$

但這是：

$$
\boxed{
\text{incidence mass upper bound},
}
$$

不是 canonical coverage upper bound的最終形式。

因：

$$
I\ge C^{can}.
$$

---

# 48. Raw AP Also Bounds Canonical Cells

對 canonical least-factor cell：

$$
B_r(N;y),
$$

若：

$$
p\in B_r(N;y),
$$

則：

- $p$ survivor；
- $r=\operatorname{lpf}(N-p)$；
- $r^2\le N-p$；
- $r\mid N-p$。

所以：

$$
\boxed{
B_r(N;y)
\subseteq
A_r(N).
}
$$

---

# 49. Canonical Capacity Raw AP Bound

因此：

$$
\boxed{
C_N^{can}(y)
=
\sum_r C_r^{can}(N;y)
\le
\sum_r A_r(N).
}
$$

這才是 raw AP sum接 canonical capacity的正式 bridge。

---

# 50. Why Raw AP Sum Is Loose

不是 theorem說「一定很鬆」。

但 exact slack來源至少有：

1. `A_r` 沒有限制 survivor；
2. `A_r` 沒有限制 $r$ 是 least factor；
3. 同一 $p$ 可出現在多個 $A_r$；
4. canonical cells互斥，但 raw columns重疊。

所以：

$$
\boxed{
\sum_r A_r
}
$$

是合法 upper bound，但不是 canonical object。

---

# 51. Incidence vs Canonical Cell

若：

$$
p
$$

的 complement有兩個 deep prime factors：

$$
r,s,
$$

則：

- incidence side計兩次；
- canonical side只計 least factor一次。

這就是：

$$
\Omega
$$

的來源。

---

# 52. $I$ Data Role

exact：

$$
I_N(y)
$$

需要讀 deep factorization。

所以：

```yaml
status: exact
role:
  - posthoc_diagnostic
  - audit_mass
truth_leakage: high
```

---

# 53. $\Omega$ Data Role

同樣：

```yaml
status: exact
role:
  - overlap_diagnostic
truth_leakage: high
```

---

# 54. $A_r$ Data Role

Raw AP column只用：

- prime $p$；
- range；
- residue/divisibility。

不問：

$$
N-p
$$

最終 prime或 composite。

所以：

```yaml
status: exact
role:
  - proof_input
truth_leakage: low
```

這是 V1-07 最重要的 source-role分界。

---

# 55. E0 Invariants

V1-07 完成後 E0必驗：

$$
\boxed{
I=C^{can}+\Omega.
}
$$

以及：

$$
\boxed{
D+\Omega=R+I.
}
$$

再驗 paper-facing：

$$
R=D+\Omega-I.
$$

---

# 56. E0 Divisor AP Invariant

若：

$$
r\mid N,
$$

且 $r$ prime：

$$
\boxed{
A_r(N)
=
\mathbf1_{\{r(r+1)\le N\}}.
}
$$

任何：

$$
A_r>1
$$

都是 implementation bug。

---

# 57. E0 Small-Factor Invariant

若：

$$
\ell\le y,
$$

$$
\ell\mid N,
$$

且 cutoff legal：

$$
\boxed{
S_\ell(N)=\{\ell\}.
}
$$

這是 demand-side regression test。

---

# 58. Formal Theorem Queue

```yaml
V1_07:
  T01: prime_survivor_has_zero_multiplicity
  T02: composite_survivor_has_positive_multiplicity
  T03: multiplicity_zero_iff_prime_survivor
  T04: pointwise_multiplicity_decomposition
  T05: incidence_eq_canonical_coverage_plus_overlap
  T06: D_gt_I_iff_R_gt_Omega
  T07: incidence_double_count_by_factor
  T08: incidence_column_subset_raw_AP_column
  T09: divisor_raw_AP_membership_exact
  T10: divisor_raw_AP_cardinality_indicator
  T11: small_factor_self_cell_exact
  T12: canonical_cell_subset_raw_AP
```

---

# 59. Lean-Oriented Skeleton

```lean
namespace RGSCP

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

def IncidenceAt
    (N y r p : Nat) : Prop :=
  WheelHard N y p ∧
  DeepFactor N y p r

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

def SmallScreenInput
    (N ell p : Nat) : Prop :=
  ReducedPrimeInput N p ∧
  ell ∣ (N - p)

-- finite-cardinality layer:
-- DeepFactorFinset
-- DeepMultiplicity
-- DeepIncidenceMass
-- OverlapSurplus
-- IncidenceColumn
-- RawAPColumn

end RGSCP
```

---

# 60. Unit Test：$N=68,\ y=2$

Survivors：

$$
3,5,7,11,13,17,19,23,29,31.
$$

multiplicity：

$$
m(3)=1,
$$

$$
m(5)=2,
$$

$$
m(7)=0,
$$

$$
m(11)=1,
$$

$$
m(13)=1,
$$

$$
m(17)=1,
$$

$$
m(19)=1,
$$

$$
m(23)=2,
$$

$$
m(29)=1,
$$

$$
m(31)=0.
$$

因此：

$$
D=10,
$$

$$
R=2,
$$

$$
C^{can}=8,
$$

$$
I=10,
$$

$$
\Omega=2.
$$

必驗：

$$
10=8+2,
$$

$$
10+2=2+10.
$$

---

# 61. Unit Test：Divisor Raw Column

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

$$
r(r+1)=12\le30.
$$

所以：

$$
A_3(30)=1,
$$

唯一 input：

$$
p=3.
$$

---

# 62. Unit Test：Another Divisor Column

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

$$
5\cdot6=30.
$$

所以：

$$
A_5(30)=1,
$$

唯一 input：

$$
p=5.
$$

boundary equality必須接受。

---

# 63. Unit Test：Divisor Column Empty

$$
N=42,
\quad
r=7.
$$

$$
7\cdot8=56>42.
$$

所以：

$$
A_7(42)=0.
$$

即使：

$$
7\mid42.
$$

這是舊「$\le1$」無法表達的 exact boundary。

---

# 64. Unit Test：Small Self Cell

$$
N=30,
\quad
y=5,
\quad
\ell=3.
$$

legal cutoff：

$$
2y=10<30.
$$

$$
3\mid30.
$$

所以：

$$
S_3(30)=\{3\}.
$$

同理：

$$
S_5(30)=\{5\}.
$$

---

# 65. Formal Acceptance Gate

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

1. DeepFactor finite range；
2. prime survivor multiplicity $0$；
3. composite survivor multiplicity $>0$；
4. $I=C^{can}+\Omega$；
5. $D+\Omega=R+I$；
6. $D>I\iff R>\Omega$；
7. incidence factor-column double count；
8. incidence column $\subseteq$ raw AP；
9. raw AP additive range使用 $p+r^2\le N$；
10. divisor AP membership exact；
11. divisor AP cardinality indicator exact；
12. small-factor self-cell exact singleton；
13. canonical cells $\subseteq$ raw AP；
14. analytic bounds只作 interface；
15. no `sorry`.

---

# 66. Bug Checklist

任一發生立即停止：

- prime survivor multiplicity非零；
- composite survivor multiplicity為零；
- $I\neq C^{can}+\Omega$；
- $D>I$ 被寫成 success iff；
- incidence column與 canonical cell混名；
- divisor raw AP column出現兩個 prime inputs；
- $N=42,r=7$ 被算成 $A_r=1$；
- small self-cell只證 $\le1$ 卻漏掉存在性；
- RawAPInput直接查 complement primality；
- Brun–Titchmarsh被當 elementary theorem；
- exact $I$ 被當 leakage-free predictor。

---

# 67. Source Signature

```yaml
RG-SCP-V1-07:
  S0_elementary:
    role:
      - finite_sums
      - double_count
      - divisibility
      - modular_bridge

  S1_factor_lpf:
    role:
      - deep_factor_multiplicity
      - overlap
      - canonical_cell_bridge

  S2_wheel:
    role:
      - survivor_restriction

  S5_analytic:
    role:
      - external_AP_upper_bound_interface_only

  S3_fixed_point:
    forbidden_dependency: true

  S4_minimality:
    forbidden_dependency: true

  S6_heuristic:
    forbidden_dependency: true

data_roles:
  I:
    audit_mass: true
    truth_adjacent: true

  Omega:
    overlap_diagnostic: true

  A_r:
    proof_input: true
```

---

# 68. Verdict

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

但：

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

本輪完成的是：

> 將 incidence 語言正式降級為 canonical coverage 的 audit expansion，並建立 raw AP columns作為未來 independent upper-bound theorem的合法接口。

---

# 69. 下一輪

下一篇：

# RG-SCP Validation V1-08
## AP Upper-Bound Interface / Canonical Cell Upper-Bound Contract

只做：

- `APUpperBound` 抽象接口；
- raw AP sum upper envelope；
- divisor-column suppression自動套用；
- canonical cell upper-bound interface；
- demand lower-bound interface；
- closure composition theorem；
- external analytic source isolation。

不直接證 Brun–Titchmarsh。

minimality transport留 V1-09。

---

# 附錄 A：Commit Decision

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

formal_status:
  machine_checked: false
  lean_compiled: false
  sorry_free: not_yet_tested

canonical_decisions:
  - I_is_incidence_mass_not_capacity
  - Omega_is_overlap_surplus
  - I_equals_Ccan_plus_Omega
  - D_plus_Omega_equals_R_plus_I_is_formal_primary
  - R_equals_D_plus_Omega_minus_I_is_audit_corollary
  - incidence_columns_are_distinct_from_canonical_cells
  - RawAPInput_uses_p_plus_r_square_le_N
  - divisor_raw_AP_column_has_exact_indicator
  - small_factor_self_cell_is_exact_singleton
  - analytic_AP_bounds_are_external_interfaces_only

next_round:
  V1-08_AP_UpperBound_Interface_Canonical_Cell_Contract

commit_to_sync_core: true
```