# RG-SCP Validation V1-06
## Survivor / Canonical Coverage Kernel
### Legal Cutoff、Survivor Demand、Composite Coverage、Least-Factor Cells 與 Canonical Closure

**系列：** RG-SCP Validation  
**階段：** V1 — Formal Core  
**輪次：** 06  
**日期：** 2026-09-28  
**版本：** v0.1  
**作者：** Neo.K；Aletheia（GPT-5.6 Sol）  
**狀態：** Formal specification ready；尚未宣稱 Lean compile / sorry-free

---

## 摘要

V0-R06 已將原本的 incidence-centered demand/capacity 路線重構。

真正 canonical 的 coverage 不是：

$$
I_N(y),
$$

因為 $I_N(y)$ 會對同一 composite complement 的多個 deep prime factors 重複計數。

本輪 formalize 的主 object 是：

$$
\boxed{
C_N^{\mathrm{can}}(y)
=
\#\{p\in\mathbb H_y(N):N-p\text{ composite}\}.
}
$$

沿用 V1-03 的 survivor / wheel-hard domain：

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

本輪把 cutoff 改成 Nat-friendly 定義：

$$
\boxed{
\operatorname{LegalCutoff}(N,y)
:
\Longleftrightarrow
2\le y
\land
2y<N.
}
$$

這取代 paper notation中的：

$$
y<N/2,
$$

並避免 Nat division。

對 legal cutoff，所有 reduced Goldbach witnesses 都必 survivor：

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

因為令：

$$
q=N-p,
$$

reduced orientation給：

$$
p\le q.
$$

若：

$$
q\le y,
$$

則：

$$
N=p+q\le2q\le2y<N,
$$

矛盾。

因此：

$$
q>y,
$$

而 prime $q$ 不可能含任何：

$$
\le y
$$

的 prime divisor。

接著定義：

$$
\boxed{
\operatorname{CompositeSurvivor}(N,y,p)
:
\Longleftrightarrow
\operatorname{WheelHard}(N,y,p)
\land
\operatorname{Composite}(N-p).
}
$$

每個 survivor complement至少為 $2$，所以恰分成：

- prime complement；
- composite complement。

因此有 canonical disjoint partition：

$$
\boxed{
\mathbb H_y(N)
=
\mathbb G_N^{-}
\bigsqcup
\mathbb C_y(N).
}
$$

其中：

$$
\mathbb G_N^{-}
=
\{p:\operatorname{GoldbachReducedPair}(N,p)\},
$$

$$
\mathbb C_y(N)
=
\{p:\operatorname{CompositeSurvivor}(N,y,p)\}.
$$

所以 formal primitive應寫：

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

由：

$$
C_N^{\mathrm{can}}(y)\le D_N(y),
$$

才得到 corollary：

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

這是 Phase-I canonical demand/coverage identity。

對 legal even $N$：

$$
\boxed{
\operatorname{GoldbachFailure}(N)
\Longleftrightarrow
D_N(y)=C_N^{\mathrm{can}}(y).
}
$$

也就是：

> failure exact 等價於 survivor demand 被 composite coverage 完全吃滿。

最後用 least factor分割 composite survivors：

$$
\boxed{
B_r(N;y)
=
\{p:
\operatorname{CompositeSurvivor}(N,y,p),
\operatorname{lpf}(N-p)=r
\}.
}
$$

每個 composite survivor屬唯一一個 cell，而且 cell factor滿足：

$$
\boxed{
y<r,
\qquad
r^2\le N-p,
\qquad
r^2\le N-2.
}
$$

所以：

$$
\boxed{
\mathbb C_y(N)
=
\bigsqcup_{r>y}B_r(N;y).
}
$$

真正 closure template因此是：

$$
\boxed{
D_N(y)\ge L_N(y),
\qquad
C_N^{\mathrm{can}}(y)\le U_N^{\mathrm{can}}(y),
}
$$

若：

$$
\boxed{
U_N^{\mathrm{can}}(y)<L_N(y),
}
$$

則：

$$
\boxed{
R_G^{-}(N)>0.
}
$$

---

# 1. Dependency Boundary

允許：

- V1-01 reduced Goldbach kernel；
- V1-02 Composite / minFac；
- V1-03 WheelHard / PrimeCutoffProduct；
- finite set / cardinality arithmetic。

禁止：

- $I_N$；
- $\Omega_N$；
- AP columns；
- Brun–Titchmarsh；
- minimality transport；
- heuristic。

---

# 2. Legal Cutoff

定義：

$$
\boxed{
\operatorname{LegalCutoff}(N,y)
:
\Longleftrightarrow
2\le y
\land
2y<N.
}
$$

Lean-oriented：

```lean
def LegalCutoff (N y : Nat) : Prop :=
  2 ≤ y ∧ 2 * y < N
```

---

# 3. Goldbach Complement Above Cutoff

## Theorem V1-06-T01

若：

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

且：

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

則：

$$
\boxed{
y<N-p.
}
$$

這是 survivor inclusion的 arithmetic kernel。

---

# 4. Goldbach Input Survives

## Theorem V1-06-T02

若：

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

且：

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

則：

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

因此：

$$
\boxed{
\mathbb G_N^{-}
\subseteq
\mathbb H_y(N).
}
$$

---

# 5. Composite Survivor

定義：

```lean
def CompositeSurvivor
    (N y p : Nat) : Prop :=
  WheelHard N y p ∧
  Composite (N - p)
```

數學式：

$$
\boxed{
\operatorname{CompositeSurvivor}(N,y,p)
=
\operatorname{WheelHard}(N,y,p)
\land
\operatorname{Composite}(N-p).
}
$$

---

# 6. Survivor Dichotomy

## Theorem V1-06-T03

若：

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

則：

$$
\boxed{
\operatorname{Prime}(N-p)
\;\dot\lor\;
\operatorname{Composite}(N-p).
}
$$

因 WheelHard包含 reduced input，而 V1-02 已證：

$$
2\le N-p.
$$

---

# 7. Survivor Partition

## Theorem V1-06-T04

若：

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

則：

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

等價於：

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

且兩 branch互斥。

---

# 8. Canonical Finite Sets

定義：

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

$$
\mathbb C_y(N)
=
\{p:\operatorname{CompositeSurvivor}(N,y,p)\}.
$$

以及：

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

$$
C_N^{\mathrm{can}}(y)=|\mathbb C_y(N)|.
$$

Lean layer：

```text
SurvivorFinset
CompositeSurvivorFinset
SurvivorDemand
CanonicalCoverage
```

---

# 9. Disjoint Finset Partition

## Theorem V1-06-T05

對 legal cutoff：

$$
\boxed{
\operatorname{SurvivorFinset}(N,y)
=
\operatorname{GoldbachReducedFinset}(N)
\;\dot\cup\;
\operatorname{CompositeSurvivorFinset}(N,y).
}
$$

---

# 10. Primary Count Identity

## Theorem V1-06-T06

對 legal cutoff：

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

這是 formal primitive。

不是：

$$
R=D-C
$$

先行。

---

# 11. Subtraction Corollary

由：

$$
C_N^{\mathrm{can}}(y)\le D_N(y),
$$

得到：

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

這是 paper-facing canonical identity。

---

# 12. Failure Equals Full Coverage

## Theorem V1-06-T07

若：

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

與：

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

則：

$$
\boxed{
\operatorname{GoldbachFailure}(N)
\Longleftrightarrow
D_N(y)
=
C_N^{\mathrm{can}}(y).
}
$$

---

# 13. Pointwise Failure Characterization

## Theorem V1-06-T08

同樣 assumptions下：

$$
\boxed{
\operatorname{GoldbachFailure}(N)
\Longleftrightarrow
\forall p,
\operatorname{WheelHard}(N,y,p)
\to
\operatorname{Composite}(N-p).
}
$$

Goldbach pair若存在，T02保證它一定是 survivor，所以右式不可能成立。

---

# 14. Coverage Cell

定義：

```lean
def CoverageCell
    (N y r p : Nat) : Prop :=
  CompositeSurvivor N y p ∧
  Nat.minFac (N - p) = r
```

即：

$$
\boxed{
B_r(N;y)
=
\left\{
p:
\operatorname{CompositeSurvivor}(N,y,p),
\operatorname{lpf}(N-p)=r
\right\}.
}
$$

---

# 15. Coverage Factor

定義：

```lean
def CoverageFactor
    (N y r : Nat) : Prop :=
  Nat.Prime r ∧
  y < r ∧
  r * r ≤ N - 2
```

數學上：

$$
\boxed{
r\in\mathbb P,
\quad
y<r,
\quad
r^2\le N-2.
}
$$

---

# 16. Cell Factor Above Cutoff

## Theorem V1-06-T09

若：

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

則：

$$
\boxed{
y<r.
}
$$

理由：

- $r$ 是 complement 的 prime divisor；
- survivor complement與 $P(y)$ coprime；
- 所以 $r$ 不可能在 cutoff內。

---

# 17. Cell Factor Is Proper

## Theorem V1-06-T10

若：

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

則：

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

因此：

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

---

# 18. Unique Coverage Cell

## Theorem V1-06-T11

若：

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

則存在唯一：

$$
r
$$

使：

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

canonical witness：

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

---

# 19. Cell Partition

因此：

$$
\boxed{
\mathbb C_y(N)
=
\bigsqcup_{\substack{
r\in\mathbb P\\
y<r\\
r^2\le N-2
}}
B_r(N;y).
}
$$

formal Tier 1先證：

$$
\forall p\in\mathbb C_y(N),
\quad
\exists!r,
\operatorname{CoverageFactor}(N,y,r)
\land
\operatorname{CoverageCell}(N,y,r,p).
$$

indexed Finset sum可放 Tier 2。

---

# 20. Cell Cardinalities

定義：

$$
\boxed{
C_r^{\mathrm{can}}(N;y)
=
|B_r(N;y)|.
}
$$

最終可證：

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

over legal coverage factors。

這個 sum完全無 overlap。

---

# 21. V1-02 Cell Bridge

V1-02：

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

沒有 survivor cutoff。

本輪有：

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

反之若：

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

加：

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

則得到 CoverageCell。

所以沒有新增 factor source。

---

# 22. Data Roles

## Demand

$$
D_N(y)
$$

只需要：

- prime input；
- small-factor divisibility。

所以：

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

## Canonical Coverage

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

直接讀 complement compositeness。

又：

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

所以：

```yaml
status: exact
role:
  - truth_adjacent
  - posthoc_diagnostic
truth_leakage: high_for_same_target
```

---

# 23. Abstract Lower/Upper Interfaces

本輪不指定：

$$
L_N(y)
$$

與：

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

來源。

只建立 logical interface：

$$
\boxed{
L\le D_N(y)
}
$$

以及：

$$
\boxed{
C_N^{\mathrm{can}}(y)\le U.
}
$$

---

# 24. Canonical Closure Theorem

## Theorem V1-06-T12

若：

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

$$
L\le D_N(y),
$$

$$
C_N^{\mathrm{can}}(y)\le U,
$$

且：

$$
\boxed{
U<L,
}
$$

則：

$$
\boxed{
R_G^{-}(N)>0.
}
$$

如果再有：

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

則：

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

---

# 25. Formal-Friendly Proof of Closure

不要依賴 Nat subtraction。

反設：

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

由：

$$
D=R+C
$$

得到：

$$
D=C.
$$

所以：

$$
L\le D=C\le U,
$$

與：

$$
U<L
$$

矛盾。

這是最穩定的 Lean proof route。

---

# 26. Primorial Bridge

V1-03 已證 saturation / primorial branch中：

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

V1-06 不重證。

只允許把 exact demand代入 closure theorem。

---

# 27. Failure Primorial Consequence

若：

$$
M_k\mid N
$$

且：

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

則：

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

這只是 failure consequence，不是 proof input。

---

# 28. Incidence Deferred

本輪不定義：

$$
m_y(N,p),
\quad
I_N(y),
\quad
\Omega_N(y).
$$

因 canonical semantics先鎖：

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

V1-07 再把 incidence接回來作 audit / AP interface。

---

# 29. Unit Test：$N=10,\ y=2$

Reduced primes：

$$
2,3,5.
$$

survivors：

$$
3,5.
$$

所以：

$$
D_{10}(2)=2.
$$

兩個 complements：

$$
7,5
$$

都 prime。

因此：

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

$$
C_{10}^{can}(2)=0.
$$

驗：

$$
\boxed{
2=2+0.
}
$$

---

# 30. Unit Test：$N=26,\ y=2$

Reduced primes：

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

survivors：

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

所以：

$$
D_{26}(2)=5.
$$

prime complements：

$$
23,19,13.
$$

所以：

$$
R_G^{-}(26)=3.
$$

composite survivors：

$$
21,15.
$$

所以：

$$
C_{26}^{can}(2)=2.
$$

驗：

$$
\boxed{
5=3+2.
}
$$

---

# 31. Unit Test：Coverage Cells

對：

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

$$
p=5
\Rightarrow
N-p=21,
\quad
\operatorname{lpf}(21)=3.
$$

$$
p=11
\Rightarrow
N-p=15,
\quad
\operatorname{lpf}(15)=3.
$$

所以：

$$
C_3^{can}(26;2)=2.
$$

prime survivor：

$$
p=7,
\quad
N-p=19
$$

不得進任何 coverage cell。

---

# 32. Illegal Cutoff Test

$$
N=10,
\quad
y=5.
$$

$$
2y=10\not<10.
$$

所以：

$$
\operatorname{LegalCutoff}(10,5)
$$

false。

T02 / T04 / T06 不得套用。

---

# 33. Formal Acceptance Gate

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

1. `LegalCutoff` 使用 $2y<N$；
2. Goldbach witness survives cutoff；
3. survivor prime/composite dichotomy；
4. disjoint partition；
5. $D=R+C^{can}$；
6. $R=D-C^{can}$ corollary；
7. failure iff $D=C^{can}$；
8. failure iff all survivors composite；
9. CoverageCell 明確含 CompositeSurvivor；
10. cell factor $>y$；
11. cell factor proper square bound；
12. unique least-factor cell；
13. abstract lower-vs-upper closure theorem；
14. $I,\Omega,$ AP 尚未進 core；
15. no `sorry`.

---

# 34. Bug Checklist

若發生任一，停止：

- Goldbach pair在 legal cutoff下不是 survivor；
- prime survivor進 composite coverage；
- composite survivor無 cell；
- composite survivor進兩個 least-factor cells；
- $D\neq R+C^{can}$；
- failure但 $D\neq C^{can}$；
- success但 $D=C^{can}$；
- cell factor $\le y$；
- prime complement因 `minFac` 被誤收 cell；
- illegal cutoff仍套 partition；
- $I$ 被重新叫 canonical capacity；
- exact $C^{can}$ 被標成 leakage-free predictor。

---

# 35. Source Signature

```yaml
RG-SCP-V1-06:
  S0_elementary:
    role:
      - cutoff_arithmetic
      - finite_partition
      - cardinality

  S1_factor_lpf:
    role:
      - composite_survivor
      - coverage_cells

  S2_wheel:
    role:
      - survivor_domain

  S3_fixed_point:
    forbidden_dependency: true

  S4_minimality:
    forbidden_dependency: true

  S5_analytic:
    forbidden_dependency: true

  S6_heuristic:
    forbidden_dependency: true

canonical_identity:
  D_equals_R_plus_Ccan: true

data_roles:
  D:
    proof_input: true
  C_can:
    truth_adjacent: true
```

---

# 36. Lean-Oriented Skeleton

```lean
namespace RGSCP

def LegalCutoff (N y : Nat) : Prop :=
  2 ≤ y ∧ 2 * y < N

def CompositeSurvivor
    (N y p : Nat) : Prop :=
  WheelHard N y p ∧
  Composite (N - p)

def CoverageCell
    (N y r p : Nat) : Prop :=
  CompositeSurvivor N y p ∧
  Nat.minFac (N - p) = r

def CoverageFactor
    (N y r : Nat) : Prop :=
  Nat.Prime r ∧
  y < r ∧
  r * r ≤ N - 2

-- Finset layer:
-- SurvivorFinset
-- CompositeSurvivorFinset
-- SurvivorDemand
-- CanonicalCoverage
-- CoverageCellFinset

end RGSCP
```

---

# 37. Theorem Queue

```yaml
V1_06:
  T01: goldbach_reduced_complement_gt_cutoff
  T02: goldbach_input_survives_legal_cutoff
  T03: survivor_prime_or_composite
  T04: survivor_iff_goldbach_or_composite_survivor
  T05: survivor_finset_disjoint_union
  T06: demand_eq_rgminus_plus_canonical_coverage
  T07: failure_iff_demand_eq_canonical_coverage
  T08: failure_iff_all_survivors_composite
  T09: coverage_cell_factor_above_cutoff
  T10: coverage_cell_factor_square_le_complement
  T11: composite_survivor_has_unique_coverage_cell
  T12: lower_gt_upper_implies_goldbach_success
```

---

# 38. Verdict

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

仍然：

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

本輪完成的是：

> 把 demand / capacity 的主語義壓成一個完全無 overlap 的 finite partition，並把 incidence mass正式排除在 canonical capacity definition之外。

---

# 39. 下一輪

下一篇：

# RG-SCP Validation V1-07
## Incidence Audit / AP Suppression Kernel

只做：

- $m_y(N,p)$；
- $I_N(y)$；
- $\Omega_N(y)$；
- $I=C^{can}+\Omega$；
- $R=D+\Omega-I$；
- incidence columns；
- raw AP columns；
- divisor-column exact indicator；
- small-factor self-cell exact theorem。

不做 Brun–Titchmarsh proof，不做 minimality transport。

---

# 附錄 A：Commit Decision

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

formal_status:
  machine_checked: false
  lean_compiled: false
  sorry_free: not_yet_tested

canonical_decisions:
  - LegalCutoff_uses_2y_lt_N
  - Goldbach_reduced_inputs_survive_cutoff
  - survivor_partition_is_primary
  - D_equals_R_plus_Ccan_is_primary
  - R_equals_D_minus_Ccan_is_corollary
  - failure_equals_full_canonical_coverage
  - CoverageCell_requires_composite_survivor
  - least_factor_cells_are_unique
  - incidence_and_AP_deferred

next_round:
  V1-07_Incidence_Audit_AP_Suppression_Kernel

commit_to_sync_core: true
```