# RG-SCP Validation V1-01
## Basic / Reduced Goldbach / Counterexample Kernel
### 基礎域、Reduced 表示、最小反例與 Proof-Admissible Outer Approximation

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

---

## 摘要

V0 已完成 RG-SCP 第一階段的 claim/source audit。

V1 不再新增概念，而開始把 V0 保留下來的 exact core 壓成可以送入 Lean / Coq / Isabelle 的 machine-oriented theorem spine。

第一輪只處理最底層六個 object：

1. legal even target domain；
2. reduced prime-input domain；
3. reduced Goldbach representation count；
4. failure predicate；
5. counterexample universe；
6. proof-admissible outer approximation。

本輪不引入：

- least prime factor；
- obstruction map；
- M6；
- wheel；
- fixed-point；
- demand / capacity；
- minimality transport。

原因是這些後續 object 都依賴本輪的 domain 與 target semantics。

本輪的 canonical target是建立：

$$
\boxed{
\text{GoldbachSuccessReduced}
}
$$

與：

$$
\boxed{
\text{GoldbachFailure}
}
$$

的單一 machine semantics。

最重要的 theorem spine：

$$
\boxed{
R_G^{-}(N)>0
\Longleftrightarrow
\exists p,q\in\mathbb P,
\quad
p+q=N
}
$$

對 legal even：

$$
N\ge4
$$

成立。

再建立：

$$
\boxed{
F_G(N)=1
\Longleftrightarrow
R_G^{-}(N)=0.
}
$$

以及：

$$
\boxed{
\mathcal C_G
=
\left\{
N:
\operatorname{LegalEven}(N)
\land
F_G(N)=1
\right\}.
}
$$

若：

$$
\mathcal C_G\neq\varnothing,
$$

則存在：

$$
\boxed{
N_*=\min\mathcal C_G.
}
$$

並有：

$$
\boxed{
4\le M<N_*,
\quad
M\text{ even}
\Longrightarrow
R_G^{-}(M)>0.
}
$$

最後建立 proof-admissible outer approximation schema：

給定 finite constraint family：

$$
K_1,\ldots,K_m,
$$

若每個都滿足：

$$
F_G(N)=1
\Longrightarrow
K_i(N),
$$

定義：

$$
\boxed{
\mathcal A_m^{\mathrm P}
=
\left\{
N:
\operatorname{LegalEven}(N)
\land
\bigwedge_{i=1}^{m}K_i(N)
\right\}.
}
$$

則：

$$
\boxed{
\mathcal C_G
\subseteq
\mathcal A_m^{\mathrm P}.
}
$$

如果：

$$
\mathcal A_m^{\mathrm P}
=
\varnothing,
$$

則：

$$
\boxed{
\mathcal C_G=\varnothing.
}
$$

這是 RG-SCP reverse-closure architecture 的 machine-level non-circular kernel。

---

# 1. V1-01 的唯一任務

本輪不是證 Goldbach。

本輪只做：

$$
\boxed{
\text{把 target 語義形式化到後續 theorem 無法再漂移。}
}
$$

只要這一層有 domain bug，

後面的：

- obstruction；
- wheel；
- fixed point；
- capacity；
- transport；

全部都可能建立在錯誤 target 上。

---

# 2. Canonical carrier

建議第一版全部使用：

$$
\mathbb N.
$$

不使用：

- integers；
- reals；
- arbitrary semirings。

因 Goldbach target本身只需要 naturals。

Lean orientation：

```lean
namespace RGSCP

open Nat
```

---

# 3. Prime predicate

第一版直接使用 Mathlib / proof assistant既有 prime predicate。

抽象寫：

$$
\operatorname{Prime}(n).
$$

Lean conceptual form：

```lean
Nat.Prime n
```

本系列不自行重新定義 primality。

---

# 4. Legal even target

定義：

$$
\boxed{
\operatorname{LegalEven}(N)
:
\Longleftrightarrow
4\le N
\land
2\mid N.
}
$$

Lean-oriented：

```lean
def LegalEven (N : Nat) : Prop :=
  4 ≤ N ∧ Even N
```

或：

```lean
4 ≤ N ∧ 2 ∣ N
```

二者擇一，整個 repo 統一。

---

# 5. Even predicate 選擇

建議 Lean core優先使用：

```lean
Even N
```

若 Mathlib lemma鏈更方便。

需要 residue arithmetic時再 bridge：

$$
\operatorname{Even}(N)
\Longleftrightarrow
2\mid N.
$$

不要在不同 module交替使用兩種 definition而無 bridge。

---

# 6. Reduced prime-input domain

定義：

$$
\boxed{
\mathbb P_N^{-}
=
\left\{
p\in\mathbb P:
2\le p
\land
2p\le N
\right\}.
}
$$

形式化建議用：

$$
2p\le N
$$

而不是：

$$
p\le N/2
$$

作 primitive condition。

原因：

- 避免 Nat integer division；
- proof assistant對 multiplication inequality更乾淨；
- 不需 floor semantics。

Lean-oriented：

```lean
def ReducedPrimeInput (N p : Nat) : Prop :=
  Nat.Prime p ∧ 2 * p ≤ N
```

注意：

prime：

$$
p\ge2
$$

本身已自帶 lower bound。

所以不必重複：

$$
2\le p.
$$

---

# 7. Canonical reduced domain set

可定義：

```lean
def ReducedPrimeSet (N : Nat) : Finset Nat :=
  (Finset.range (N + 1)).filter
    (fun p => Nat.Prime p && 2 * p ≤ N)
```

但 formal proof初期不一定要立刻用 `Finset`。

更穩妥是先分：

## Proposition layer

```lean
ReducedPrimeInput N p
```

## Finite counting layer

之後再建立：

```lean
ReducedPrimeFinset N
```

避免 theorem proof被 Finset implementation細節拖累。

---

# 8. Reduced representation predicate

定義：

$$
\boxed{
\operatorname{GoldbachReducedPair}(N,p)
:
\Longleftrightarrow
p\in\mathbb P
\land
2p\le N
\land
N-p\in\mathbb P.
}
$$

Lean-oriented：

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

---

# 9. Nat subtraction safety

`N - p` 使用 Nat subtraction。

由：

$$
2p\le N
$$

可推出：

$$
p\le N.
$$

所以在 reduced pair domain不會有 underflow語義問題。

應先形式化：

## Lemma V1-01-L01

若：

$$
2p\le N,
$$

則：

$$
p\le N.
$$

以及：

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

---

# 10. Reduced Goldbach success

定義：

$$
\boxed{
\operatorname{GoldbachSuccess}^{-}(N)
:
\Longleftrightarrow
\exists p,
\operatorname{GoldbachReducedPair}(N,p).
}
$$

Lean-oriented：

```lean
def GoldbachSuccessReduced (N : Nat) : Prop :=
  ∃ p, GoldbachReducedPair N p
```

---

# 11. Standard unordered Goldbach success

另定義：

$$
\boxed{
\operatorname{GoldbachSuccess}(N)
:
\Longleftrightarrow
\exists p,q\in\mathbb P,
\quad
p+q=N.
}
$$

Lean-oriented：

```lean
def GoldbachSuccess (N : Nat) : Prop :=
  ∃ p q,
    Nat.Prime p ∧
    Nat.Prime q ∧
    p + q = N
```

---

# 12. Reduced completeness theorem

## 定理 V1-01-T01

若：

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

則：

$$
\boxed{
\operatorname{GoldbachSuccessReduced}(N)
\Longleftrightarrow
\operatorname{GoldbachSuccess}(N).
}
$$

這是整個 RG-SCP reduced-domain semantics 的第一個核心 theorem。

---

# 13. T01：Reduced 推 standard

若存在：

$$
p
$$

使：

$$
p
$$

prime，

$$
2p\le N,
$$

且：

$$
N-p
$$

prime，

令：

$$
q=N-p.
$$

則：

$$
p+q=N.
$$

所以 standard success。

這一向非常直接。

---

# 14. T01：Standard 推 reduced

若：

$$
N=p+q
$$

其中：

$$
p,q
$$

prime，

則：

$$
p\le q
$$

或：

$$
q\le p.
$$

若：

$$
p\le q,
$$

則：

$$
2p\le p+q=N.
$$

所以：

$$
p
$$

是 reduced witness。

反之用：

$$
q.
$$

因此一定存在 reduced endpoint。

---

# 15. Reduced theorem不需要 even assumption嗎？

事實上：

$$
\operatorname{GoldbachSuccess}(N)
\Longrightarrow
\operatorname{GoldbachSuccessReduced}(N)
$$

對任意 natural：

$$
N
$$

都成立，

因只用 ordering。

所以可以將 T01拆成更一般 theorem：

## V1-01-T01a

$$
\boxed{
\operatorname{GoldbachSuccess}(N)
\Longleftrightarrow
\operatorname{GoldbachSuccessReduced}(N)
}
$$

對所有：

$$
N.
$$

前提只需 Nat subtraction bridge正確。

如果 Lean proof乾淨，就使用 general theorem。

LegalEven只在 conjecture domain使用。

---

# 16. Representation witness symmetry

可建立：

## V1-01-L02

若：

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

令：

$$
q=N-p.
$$

則：

$$
p+q=N.
$$

且：

$$
p\le q.
$$

proof：

$$
2p\le N
$$

等價於：

$$
p\le N-p
$$

在：

$$
p\le N
$$

下。

這個 lemma後續 transport會反覆使用。

---

# 17. Reduced representation count

定義 finite set：

$$
\boxed{
\mathcal G_N^{-}
=
\left\{
p:
\operatorname{GoldbachReducedPair}(N,p)
\right\}.
}
$$

以及：

$$
\boxed{
R_G^{-}(N)
=
|\mathcal G_N^{-}|.
}
$$

Lean-oriented：

```lean
def GoldbachReducedFinset (N : Nat) : Finset Nat :=
  (Finset.range (N + 1)).filter
    (fun p => Nat.Prime p && 2 * p ≤ N && Nat.Prime (N - p))

def RGminus (N : Nat) : Nat :=
  (GoldbachReducedFinset N).card
```

實作時 boolean / Prop filtering需要依 Lean API調整。

---

# 18. Count positivity theorem

## 定理 V1-01-T02

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

這是 finite-set cardinality basic theorem。

之後整個 RG-SCP都統一用：

$$
R_G^{-}
$$

而不是 full ordered count。

---

# 19. 不再需要 full $R_G$

原系列早期：

$$
R_G(N)
$$

可能數 ordered first endpoint。

V0 後 canonical target改成：

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

所以 formal core中：

$$
\boxed{
R_G^{-}
}
$$

為 primary count。

若需要對照 full count，再另建 bridge theorem。

不要兩套 count混用。

---

# 20. Failure predicate

定義：

$$
\boxed{
F_G(N)
:
\Longleftrightarrow
\operatorname{LegalEven}(N)
\land
R_G^{-}(N)=0.
}
$$

這是本輪建議的 strongest typed version。

Lean-oriented：

```lean
def GoldbachFailure (N : Nat) : Prop :=
  LegalEven N ∧ RGminus N = 0
```

---

# 21. 為什麼把 legal domain放進 failure predicate？

可以有兩種設計。

## Design A

```lean
GoldbachFailure N :=
  LegalEven N ∧ RGminus N = 0
```

## Design B

```lean
GoldbachFailure N :=
  RGminus N = 0
```

然後 theorem全部另加：

```lean
LegalEven N
```

V1-01 建議：

$$
\boxed{
\text{Design A}
}
$$

原因：

- counterexample set自然 typed；
- odd $N$ 不會被誤當 Goldbach failure；
- $N<4$ 不會進 counterexample universe；
- serialization更安全。

---

# 22. Success predicate與 legal domain

可定義 global conjecture success：

$$
\boxed{
\operatorname{GoldbachConjectureAt}(N)
:
\Longleftrightarrow
\operatorname{LegalEven}(N)
\to
R_G^{-}(N)>0.
}
$$

但不要把：

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

本身綁 legal domain。

因 success pair在其他 $N$ 上仍是合法數學 object。

這樣 layering較乾淨。

---

# 23. Failure equivalence

## 定理 V1-01-T03

若：

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

則：

$$
\boxed{
\operatorname{GoldbachFailure}(N)
\Longleftrightarrow
R_G^{-}(N)=0.
}
$$

由 definition立即。

---

# 24. Success / failure exclusivity

## V1-01-T04

若：

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

則：

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

由 T02 與 Nat cardinality：

$$
R=0
\Longleftrightarrow
\neg(R>0).
$$

---

# 25. Counterexample universe

定義：

$$
\boxed{
\mathcal C_G
=
\left\{
N\in\mathbb N:
\operatorname{GoldbachFailure}(N)
\right\}.
}
$$

Lean-oriented：

```lean
def CounterexampleSet : Set Nat :=
  {N | GoldbachFailure N}
```

---

# 26. Global Goldbach proposition

定義：

$$
\boxed{
\operatorname{StrongGoldbach}
:
\Longleftrightarrow
\forall N,
\operatorname{LegalEven}(N)
\to
R_G^{-}(N)>0.
}
$$

Lean-oriented：

```lean
def StrongGoldbach : Prop :=
  ∀ N, LegalEven N → 0 < RGminus N
```

---

# 27. Counterexample emptiness equivalence

## 定理 V1-01-T05

$$
\boxed{
\operatorname{StrongGoldbach}
\Longleftrightarrow
\mathcal C_G=\varnothing.
}
$$

Claim class：

$$
[\mathrm E].
$$

這是 exact但不是新數論 theorem。

---

# 28. Set emptiness Lean form

Lean可能較方便證：

```lean
CounterexampleSet = ∅
```

或：

```lean
¬ CounterexampleSet.Nonempty
```

建議同時提供 bridge：

## V1-01-L03

$$
\boxed{
\mathcal C_G=\varnothing
\Longleftrightarrow
\neg\mathcal C_G.\operatorname{Nonempty}.
}
$$

---

# 29. Minimal counterexample existence

## 定理 V1-01-T06

若：

$$
\mathcal C_G
$$

非空，

則存在：

$$
N_*
$$

使：

$$
N_*\in\mathcal C_G
$$

且：

$$
\forall M<N_*,
\quad
M\notin\mathcal C_G.
$$

形式：

$$
\boxed{
\mathcal C_G\neq\varnothing
\Longrightarrow
\exists N_*,
\quad
N_*\in\mathcal C_G
\land
\forall M<N_*,
M\notin\mathcal C_G.
}
$$

---

# 30. Lean implementation choice

可使用：

- `Nat.find`；
- `sInf` on Nat；
- well-order theorem。

建議最簡單：

```lean
have hne : ∃ N, GoldbachFailure N := ...
let Nstar := Nat.find hne
```

再用：

```lean
Nat.find_spec
Nat.find_min'
```

具體 API依 Mathlib版本調整。

---

# 31. Minimal counterexample package

建議定義 structure：

```lean
structure MinimalCounterexample where
  N : Nat
  fail : GoldbachFailure N
  minimal : ∀ M < N, ¬ GoldbachFailure M
```

這樣後續 R07 transport theorem可以直接傳：

```lean
mc : MinimalCounterexample
```

而不是每個 theorem重複：

- failure；
- minimality；
- legal domain。

---

# 32. Minimality predecessor-success

## 定理 V1-01-T07

若：

```text
mc : MinimalCounterexample
```

以及：

$$
4\le M<mc.N,
$$

$$
M
$$

even，

則：

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

---

# 33. T07 proof

由：

$$
M<mc.N,
$$

minimality給：

$$
\neg F_G(M).
$$

又已知：

$$
\operatorname{LegalEven}(M).
$$

若：

$$
R_G^{-}(M)=0,
$$

則依 failure definition：

$$
F_G(M),
$$

矛盾。

所以：

$$
R_G^{-}(M)>0.
$$

這是 R07 所有 lower-success history 的唯一 canonical source。

---

# 34. Minimality theorem不能偷偷假設 Goldbach

T07只依賴：

$$
\boxed{
N_*
\text{ is least failure}.
}
$$

它不依賴：

$$
\forall N<N_*,
$$

預先知道某個外部 Goldbach theorem。

後續 provenance應標：

```text
source: S4_minimality_history
```

---

# 35. Proof-admissible constraint

定義一個 constraint：

$$
K:
\mathbb N\to\operatorname{Prop}.
$$

稱：

$$
K
$$

為 counterexample-necessary，如果：

$$
\boxed{
\forall N,
\operatorname{GoldbachFailure}(N)
\to
K(N).
}
$$

Lean-oriented：

```lean
def CounterexampleNecessary (K : Nat → Prop) : Prop :=
  ∀ N, GoldbachFailure N → K N
```

---

# 36. Constraint family

最簡單第一版使用：

```lean
Ks : List (Nat → Prop)
```

而不是 set of predicates。

原因：

- finite；
- recursive；
- easier fold；
- easier serialization。

---

# 37. Proof-admissible outer approximation

定義：

$$
\boxed{
\operatorname{ProofAdmissible}(K_1,\ldots,K_m;N)
}
$$

當且僅當：

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

且所有：

$$
K_i(N)
$$

成立。

Lean-oriented：

```lean
def ProofAdmissible (Ks : List (Nat → Prop)) (N : Nat) : Prop :=
  LegalEven N ∧ ∀ K ∈ Ks, K N
```

---

# 38. Proof-admissible set

$$
\boxed{
\mathcal A_{\mathrm P}(Ks)
=
\left\{
N:
\operatorname{ProofAdmissible}(Ks,N)
\right\}.
}
$$

Lean：

```lean
def ProofAdmissibleSet (Ks : List (Nat → Prop)) : Set Nat :=
  {N | ProofAdmissible Ks N}
```

---

# 39. Sound constraint list

定義：

```lean
def SoundConstraintList (Ks : List (Nat → Prop)) : Prop :=
  ∀ K ∈ Ks, CounterexampleNecessary K
```

即：

$$
\boxed{
\forall K\in Ks,
\forall N,
F_G(N)\to K(N).
}
$$

---

# 40. Outer-approximation theorem

## 定理 V1-01-T08

若：

$$
Ks
$$

sound，

則：

$$
\boxed{
\mathcal C_G
\subseteq
\mathcal A_{\mathrm P}(Ks).
}
$$

---

# 41. T08 proof

取：

$$
N\in\mathcal C_G.
$$

所以：

$$
F_G(N).
$$

由 failure definition得：

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

又由：

$$
Ks
$$

sound，

每個：

$$
K\in Ks
$$

都由 failure推出。

所以：

$$
N\in\mathcal A_{\mathrm P}(Ks).
$$

證畢。

---

# 42. Refinement monotonicity

若：

$$
Ks'
=
K::Ks,
$$

則：

$$
\boxed{
\mathcal A_{\mathrm P}(Ks')
\subseteq
\mathcal A_{\mathrm P}(Ks).
}
$$

## V1-01-T09

這不需要：

$$
K
$$

sound。

因為只是多一個 conjunct。

soundness只影響：

$$
\mathcal C_G
\subseteq
\mathcal A_{\mathrm P}.
$$

---

# 43. 為什麼這個 distinction重要

有兩種不同 theorem：

## Structural monotonicity

$$
A_{K::Ks}\subseteq A_{Ks}.
$$

只由 definition。

## Counterexample soundness

$$
C_G\subseteq A_{Ks}.
$$

需要所有 constraints必要。

不能混成一件事。

---

# 44. Empty-admissible closure

## 定理 V1-01-T10

若：

$$
Ks
$$

sound，

且：

$$
\mathcal A_{\mathrm P}(Ks)=\varnothing,
$$

則：

$$
\boxed{
\mathcal C_G=\varnothing.
}
$$

進而：

$$
\boxed{
\operatorname{StrongGoldbach}.
}
$$

---

# 45. T10 proof

由 T08：

$$
\mathcal C_G
\subseteq
\mathcal A_{\mathrm P}(Ks).
$$

右側 empty，

所以：

$$
\mathcal C_G=\varnothing.
$$

再由 T05：

$$
\operatorname{StrongGoldbach}.
$$

這是 reverse closure 的 machine-level core theorem。

---

# 46. Empty finite window 不等於 global closure

若只證：

$$
\mathcal A_{\mathrm P}(Ks)
\cap
[4,B]
=
\varnothing,
$$

只能推出：

$$
\mathcal C_G
\cap
[4,B]
=
\varnothing.
$$

不能推出：

$$
\mathcal C_G=\varnothing.
$$

這個 finite/global distinction應在 formal core有 theorem。

---

# 47. Finite interval predicate

可定義：

$$
\boxed{
\operatorname{InRange}(B,N)
:
\Longleftrightarrow
N\le B.
}
$$

再建立：

## V1-01-T11

若：

$$
\mathcal C_G
\subseteq
\mathcal A
$$

且：

$$
\forall N\le B,
\quad
N\notin\mathcal A,
$$

則：

$$
\forall N\le B,
\quad
N\notin\mathcal C_G.
$$

這是 finite certificate semantics。

---

# 48. Heuristic constraint不得進 ProofAdmissible

如果：

$$
H(N)
$$

只是 fitted relation，

不能直接加入：

```lean
Ks : List (Nat → Prop)
```

除非已證：

```lean
CounterexampleNecessary H
```

所以 formal architecture天然執行：

$$
\boxed{
\text{heuristic cannot enter proof-admissible list without theorem}.
}
$$

---

# 49. Heuristic list另建 namespace

如果未來需要：

```lean
HeuristicCandidateSet
```

應放不同 namespace：

```lean
namespace RGSCP.Discovery
```

不要和：

```lean
RGSCP.Core
```

同 module。

---

# 50. Truth-leakage metadata不屬 kernel theorem

Data-role：

- TruthLabel；
- DiscoveryProbe；
- Diagnostic；

主要是 experiment metadata。

不應把這些 UI / metadata complexity塞進核心數學 definition。

V1-01 的 core只需要：

- target semantics；
- soundness semantics。

Data role可另存在 YAML / manifest。

---

# 51. Canonical Lean dependency graph

```text
Nat.Prime
  ↓
ReducedPrimeInput
  ↓
GoldbachReducedPair
  ↓
GoldbachSuccessReduced
  ↓
RGminus
  ↓
GoldbachFailure
  ↓
CounterexampleSet
  ↓
MinimalCounterexample
```

平行：

```text
CounterexampleNecessary
  ↓
SoundConstraintList
  ↓
ProofAdmissible
  ↓
ProofAdmissibleSet
  ↓
OuterApproximation
  ↓
EmptyAdmissibleClosure
```

---

# 52. 禁止 dependency

本輪 core禁止 import：

- factorization implementation；
- minFac；
- M6；
- wheel；
- AP bounds；
- heuristic models；
- local data files。

這確保：

$$
\boxed{
\text{V1-01 is target semantics only}.
}
$$

---

# 53. Lean-oriented skeleton

```lean
namespace RGSCP

def LegalEven (N : Nat) : Prop :=
  4 ≤ N ∧ Even N

def ReducedPrimeInput (N p : Nat) : Prop :=
  Nat.Prime p ∧ 2 * p ≤ N

def GoldbachReducedPair (N p : Nat) : Prop :=
  ReducedPrimeInput N p ∧ Nat.Prime (N - p)

def GoldbachSuccessReduced (N : Nat) : Prop :=
  ∃ p, GoldbachReducedPair N p

def GoldbachSuccess (N : Nat) : Prop :=
  ∃ p q, Nat.Prime p ∧ Nat.Prime q ∧ p + q = N

def GoldbachFailure (N : Nat) : Prop :=
  LegalEven N ∧ ¬ GoldbachSuccessReduced N

def CounterexampleSet : Set Nat :=
  {N | GoldbachFailure N}

def CounterexampleNecessary (K : Nat → Prop) : Prop :=
  ∀ N, GoldbachFailure N → K N

def ProofAdmissible
    (Ks : List (Nat → Prop))
    (N : Nat) : Prop :=
  LegalEven N ∧ ∀ K ∈ Ks, K N

def ProofAdmissibleSet
    (Ks : List (Nat → Prop)) : Set Nat :=
  {N | ProofAdmissible Ks N}

end RGSCP
```

注意：

這是 Lean-oriented specification，

不是宣稱已 compile。

---

# 54. Count implementation skeleton

可後加：

```lean
def GoldbachReducedFinset (N : Nat) : Finset Nat := ...

def RGminus (N : Nat) : Nat :=
  (GoldbachReducedFinset N).card
```

再證：

```lean
theorem rgminus_pos_iff :
  0 < RGminus N ↔ GoldbachSuccessReduced N := ...
```

---

# 55. Failure predicate建議最終形式

有兩種 equivalent implementation。

## Prop-first

```lean
def GoldbachFailure (N : Nat) : Prop :=
  LegalEven N ∧ ¬ GoldbachSuccessReduced N
```

## Count-first

```lean
def GoldbachFailure (N : Nat) : Prop :=
  LegalEven N ∧ RGminus N = 0
```

V1-01 建議：

$$
\boxed{
\text{Prop-first}.
}
$$

理由：

- 少依賴 Finset；
- theorem更抽象；
- count later bridge；
- computational layer與 logical layer分離。

再證：

$$
F_G(N)
\Longleftrightarrow
\operatorname{LegalEven}(N)\land R_G^{-}(N)=0.
$$

---

# 56. Canonical theorem statements

本輪 formal core應最終提供以下 theorem names。

```text
goldbach_success_iff_reduced_success
rgminus_pos_iff_reduced_success
failure_iff_legal_and_rgminus_zero
strong_goldbach_iff_counterexample_empty
minimal_counterexample_exists
minimal_counterexample_lower_success
proof_admissible_outer_approx
proof_admissible_refinement
empty_proof_admissible_implies_goldbach
finite_empty_proof_admissible_implies_finite_goldbach
```

---

# 57. Boundary test：$N=4$

$$
4=2+2.
$$

reduced input：

$$
p=2,
$$

且：

$$
2p=4.
$$

所以：

$$
R_G^{-}(4)=1.
$$

因此：

$$
F_G(4)=0.
$$

E0 unit test必須包含。

---

# 58. Boundary test：$N=5$

不是 legal even。

即使某些 pair predicate有自己的 truth，

$$
F_G(5)
$$

依 canonical typed failure定義：

$$
\boxed{
\text{false}.
}
$$

這避免 odd number被誤收 counterexample universe。

---

# 59. Boundary test：$N=6$

$$
6=3+3.
$$

reduced witness：

$$
p=3.
$$

所以：

$$
R_G^{-}(6)=1.
$$

---

# 60. Boundary test：$N=8$

$$
8=3+5.
$$

reduced witness：

$$
p=3.
$$

所以：

$$
R_G^{-}(8)=1.
$$

---

# 61. Boundary test：$N=10$

reduced representations：

$$
3+7,
$$

$$
5+5.
$$

所以：

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

這同時是 V1-04 two-channel boundary的重要 control。

---

# 62. Odd target safety test

例如：

$$
9=2+7.
$$

`GoldbachSuccessReduced 9` 可以為 true。

但：

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

false。

因此：

$$
\operatorname{GoldbachFailure}(9)
$$

false。

這正是 success relation與 conjecture domain分離的理由。

---

# 63. Why odd success is allowed

GoldbachSuccess本質是：

> 是否可寫成兩 primes。

odd $N$ 仍可能有：

$$
2+\text{odd prime}.
$$

所以 success relation本身不應被限制到 even。

Strong Goldbach才限制：

$$
LegalEven.
$$

這讓 formal semantics更一般且自然。

---

# 64. Test：$N=1,2,3$

全部：

$$
\operatorname{LegalEven}(N)=\mathrm{false}.
$$

所以：

$$
N\notin\mathcal C_G.
$$

counterexample universe自動乾淨。

---

# 65. Counterexample-set decidability

如果使用：

$$
Nat.Prime
$$

與 finite existential，

則對固定：

$$
N
$$

GoldbachFailure是 decidable。

可後續建立：

```lean
instance : Decidable (GoldbachFailure N)
```

若 Mathlib自動推導則不需手寫。

這對 finite certificates與 E0很重要。

---

# 66. MinimalCounterexample structure 不應全域 instantiate

只有在 assumption：

$$
\mathcal C_G\neq\varnothing
$$

的 proof branch中，

才建立：

```lean
mc : MinimalCounterexample
```

不能在 global namespace假設它存在。

這避免 formal environment偷偷假設：

$$
\neg G.
$$

---

# 67. Contradiction-mode namespace

可考慮：

```lean
namespace RGSCP.AssumeCounterexample
```

其中 parameter：

```lean
(mc : MinimalCounterexample)
```

R07 transport等 theorem放這裡。

這樣 dependency圖清楚標：

> theorem成立於 counterexample-existence contradiction branch。

---

# 68. Proof-admissible constraints不能依賴 current $N$ target oracle

形式上：

$$
K(N)
$$

可以任意依賴 $N$。

但若：

$$
K(N)
:=
\neg\operatorname{GoldbachSuccessReduced}(N),
$$

雖然確實 counterexample-necessary，

卻完全沒有 proof compression。

所以 formal kernel允許，

但 source/proof-compression audit要另外標記。

---

# 69. Kernel correctness vs research usefulness

這是 V1 之後要一直分開的兩件事：

## Kernel correctness

statement有沒有嚴格成立。

## Research usefulness

statement有沒有降低 proof burden。

例如：

$$
K(N)=F_G(N)
$$

作 constraint是 sound，

但無用。

所以：

$$
\boxed{
\text{Sound}
\neq
\text{Compressing}.
}
$$

---

# 70. Constraint metadata

Formal theorem外，manifest可加：

```yaml
constraint:
  id:
  theorem_name:
  sound: true
  target_equivalent: false
  source_class:
  proof_compression_gain:
  truth_leakage_risk:
```

這不進 Lean kernel，

但進 sync ledger。

---

# 71. V1-01 Formal Acceptance Gate

本輪只有以下全部 PASS 才算 kernel ready：

### G1

`LegalEven` domain固定。

### G2

Reduced prime input不用 Nat division作 primitive。

### G3

Standard success與 reduced success equivalence證完。

### G4

Reduced count positivity equivalence證完。

### G5

Failure predicate不把 odd / small $N$ 收進來。

### G6

Counterexample emptiness equivalence證完。

### G7

Minimal counterexample structure可由 nonempty assumption建立。

### G8

Lower-success theorem證完。

### G9

ProofAdmissible不含 $F_G$。

### G10

Outer approximation theorem證完。

### G11

Empty admissible closure theorem證完。

### G12

No `sorry`.

---

# 72. V1-01 Falsification / Bug Checklist

若任何 implementation出現：

1. odd $N$ 被列為 counterexample；
2. $N=4$ failure；
3. standard success但 reduced success false；
4. reduced witness卻有 $p>N/2$；
5. `ProofAdmissible` definition直接包含 `GoldbachFailure`；
6. empty finite window被推成 global theorem；
7. minimal counterexample無 nonempty assumption；
8. lower-success theorem用 global Goldbach作 premise；

立即停止。

---

# 73. V1-01 Machine-Readable Contract

```yaml
module: RGSCP.Core.Foundation
version: 0.1

carrier:
  type: Nat

target_domain:
  LegalEven:
    min: 4
    parity: even

primary_success:
  name: GoldbachSuccessReduced
  witness:
    p_prime: true
    twice_p_le_N: true
    complement_prime: true

primary_count:
  name: RGminus

failure:
  typed_to_legal_even: true

counterexample:
  set: CounterexampleSet

minimality:
  requires_nonempty_counterexample_set: true

admissibility:
  proof_outer_approximation: true
  embeds_failure_predicate: false

forbidden_dependencies:
  - lpf
  - factorization
  - M6
  - wheel
  - analytic_prime_bounds
  - heuristic_models
```

---

# 74. Expected theorem dependency

```text
L01 arithmetic subtraction safety
  ↓
T01 reduced success iff standard success
  ↓
T02 RGminus positivity iff success
  ↓
T03 failure iff legal and count zero
  ↓
T05 StrongGoldbach iff C_G empty
  ↓
T06 minimal counterexample existence
  ↓
T07 lower-success from minimality
```

以及：

```text
CounterexampleNecessary
  ↓
SoundConstraintList
  ↓
T08 outer approximation
  ↓
T09 refinement
  ↓
T10 empty admissible closure
```

---

# 75. V1-01 完成後才允許什麼？

只允許進：

# V1-02
## Obstruction / Reduced GFOC Kernel

建立：

- proper factor witness；
- reduced pointwise small-factor theorem；
- exact GFOC；
- proper obstruction map；
- canonical lpf partition。

---

# 76. 不允許直接跳什麼？

V1-01 尚未 machine-check前，

不應直接形式化：

- M6 shadow；
- demand / capacity；
- transport graph；

因它們都依賴 reduced target semantics。

---

# 77. 本輪的 proof-compression status

V1-01 本身不提供 Goldbach-specific compression。

它提供：

$$
\boxed{
\text{semantic compression / dependency normalization}.
}
$$

也就是：

> 後續所有 theorem只需對一份 canonical target定義負責。

---

# 78. 本輪 Verdict

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

但必須誠實區分：

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

下一個真正 gate是：

> 在 cloud / local formal environment中，把本文件 skeleton 轉成可編譯 theorem file，直到無 `sorry`。

---

# 79. 下一輪

若依「一輪一篇」繼續，

下一篇建議：

# RG-SCP Validation V1-02
## Obstruction / Reduced GFOC Kernel

但只有兩種模式：

### Mode A — 先寫 formal specification

像本輪一樣先產 MD contract。

### Mode B — 有可用 Lean environment時

直接同步產：

```text
Foundation.lean
```

與：

```text
V1-01_FORMALIZATION_REPORT.md
```

目前雲端驗證線可以先用 Mode A，等正式 code runtime / repo ready 再 machine-check。

---

# 80. 最短版本

V1-01 將 RG-SCP 的 machine target壓成：

$$
\boxed{
\operatorname{LegalEven}
}
$$

$$
\boxed{
\operatorname{GoldbachSuccessReduced}
}
$$

$$
\boxed{
R_G^{-}
}
$$

$$
\boxed{
\operatorname{GoldbachFailure}
}
$$

$$
\boxed{
\mathcal C_G
}
$$

$$
\boxed{
N_*
}
$$

以及：

$$
\boxed{
\mathcal A^{\mathrm P}.
}
$$

最重要 theorem：

$$
\boxed{
\operatorname{GoldbachSuccess}
\Longleftrightarrow
\operatorname{GoldbachSuccessReduced}
}
$$

$$
\boxed{
\operatorname{StrongGoldbach}
\Longleftrightarrow
\mathcal C_G=\varnothing
}
$$

$$
\boxed{
\mathcal C_G\neq\varnothing
\Longrightarrow
\exists N_*
}
$$

$$
\boxed{
M<N_*
\land
\operatorname{LegalEven}(M)
\Longrightarrow
R_G^{-}(M)>0
}
$$

以及：

$$
\boxed{
\mathcal C_G
\subseteq
\mathcal A^{\mathrm P}
}
$$

只要：

$$
\mathcal A^{\mathrm P}
$$

中的 constraints全是 counterexample-necessary。

這就是 V1 Formal Core 的第一層 kernel。

---

# 附錄 A：Lean-Oriented Full Skeleton

```lean
namespace RGSCP

def LegalEven (N : Nat) : Prop :=
  4 ≤ N ∧ Even N

def ReducedPrimeInput (N p : Nat) : Prop :=
  Nat.Prime p ∧ 2 * p ≤ N

def GoldbachReducedPair (N p : Nat) : Prop :=
  ReducedPrimeInput N p ∧ Nat.Prime (N - p)

def GoldbachSuccessReduced (N : Nat) : Prop :=
  ∃ p, GoldbachReducedPair N p

def GoldbachSuccess (N : Nat) : Prop :=
  ∃ p q,
    Nat.Prime p ∧
    Nat.Prime q ∧
    p + q = N

def GoldbachFailure (N : Nat) : Prop :=
  LegalEven N ∧ ¬ GoldbachSuccessReduced N

def CounterexampleSet : Set Nat :=
  {N | GoldbachFailure N}

structure MinimalCounterexample where
  N : Nat
  fail : GoldbachFailure N
  minimal : ∀ M < N, ¬ GoldbachFailure M

def CounterexampleNecessary (K : Nat → Prop) : Prop :=
  ∀ N, GoldbachFailure N → K N

def ProofAdmissible
    (Ks : List (Nat → Prop))
    (N : Nat) : Prop :=
  LegalEven N ∧
  ∀ K ∈ Ks, K N

def ProofAdmissibleSet
    (Ks : List (Nat → Prop)) : Set Nat :=
  {N | ProofAdmissible Ks N}

end RGSCP
```

---

# 附錄 B：Canonical Theorem Queue

```yaml
V1_01:
  - id: T01
    name: goldbach_success_iff_reduced_success
    status: to_formalize

  - id: T02
    name: rgminus_pos_iff_reduced_success
    status: to_formalize

  - id: T03
    name: failure_iff_legal_and_rgminus_zero
    status: to_formalize

  - id: T05
    name: strong_goldbach_iff_counterexample_empty
    status: to_formalize

  - id: T06
    name: minimal_counterexample_exists
    status: to_formalize

  - id: T07
    name: minimal_counterexample_lower_success
    status: to_formalize

  - id: T08
    name: proof_admissible_outer_approx
    status: to_formalize

  - id: T09
    name: proof_admissible_refinement
    status: to_formalize

  - id: T10
    name: empty_proof_admissible_implies_goldbach
    status: to_formalize

  - id: T11
    name: finite_empty_proof_admissible_implies_finite_goldbach
    status: to_formalize
```

---

# 附錄 C：Unit Test Vector

```yaml
targets:
  - N: 1
    legal_even: false
    counterexample: false

  - N: 2
    legal_even: false
    counterexample: false

  - N: 3
    legal_even: false
    counterexample: false

  - N: 4
    legal_even: true
    reduced_pairs:
      - [2, 2]
    RGminus: 1
    failure: false

  - N: 5
    legal_even: false
    counterexample: false

  - N: 6
    legal_even: true
    reduced_pairs:
      - [3, 3]
    RGminus: 1
    failure: false

  - N: 8
    legal_even: true
    reduced_pairs:
      - [3, 5]
    RGminus: 1
    failure: false

  - N: 9
    legal_even: false
    standard_prime_pair_exists: true
    counterexample: false

  - N: 10
    legal_even: true
    reduced_pairs:
      - [3, 7]
      - [5, 5]
    RGminus: 2
    failure: false
```

---

# 附錄 D：Source Signature

```yaml
RG-SCP-V1-01:
  S0_elementary: primary
  S1_factor_lpf: forbidden_dependency
  S2_wheel: forbidden_dependency
  S3_fixed_point: forbidden_dependency
  S4_minimality: only_after_MinimalCounterexample_structure
  S5_analytic: forbidden_dependency
  S6_heuristic: forbidden_dependency

proof_role:
  target_semantics: true
  proof_compression: semantic_only
```

---

# 附錄 E：Commit Decision

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

formal_status:
  machine_checked: false
  lean_compiled: false
  sorry_free: not_yet_tested

canonical_decisions:
  - reduced_domain_primary
  - multiplication_bound_2p_le_N
  - prop_first_failure_definition
  - typed_failure_includes_legal_even
  - minimal_counterexample_requires_nonempty_assumption
  - proof_admissible_outer_approximation_excludes_failure_predicate
  - heuristic_constraints_forbidden_without_promotion

next_round:
  V1-02_Obstruction_Reduced_GFOC_Kernel

commit_to_sync_core: true
```