# RG-SCP Validation V1-04
## M6 Fixed-Point / Exact Fiber Kernel
### $M6^*$、$T_{\mathrm{top}}=\operatorname{lpf}$、Fixed-Point Set、Exact Fiber Multiplier 與 Additive Candidate Domain

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

---

## 摘要

V1-04 正式建立 RG-SCP 的 M6 fixed-point kernel。

本輪只處理：

1. $M6^*$ domain；
2. $T_{\mathrm{top}}$；
3. $T_{\mathrm{top}}=\operatorname{lpf}$；
4. fixed-point set；
5. exact multiplicative fibers；
6. additive candidate domain；
7. reduced additive candidate domain。

本輪刻意不處理：

- $\Delta_6$；
- pair energy；
- shadow map；
- two-channel Goldbach decomposition；
- boundary-$3$；
- demand / capacity；
- transport。

這些留給 V1-05 之後。

核心 domain：

$$
\boxed{
M6^*
=
\left\{
n\in\mathbb N:
n>1,
\quad
\gcd(n,6)=1
\right\}.
}
$$

對：

$$
n\in M6^*,
$$

定義：

$$
\boxed{
T_{\mathrm{top}}(n)
=
\min
\left\{
d\in M6^*:
d\mid n
\right\}.
}
$$

本輪首先形式化：

$$
\boxed{
T_{\mathrm{top}}(n)
=
\operatorname{lpf}(n)
}
$$

對所有：

$$
n\in M6^*
$$

成立。

因此：

$$
\boxed{
T_{\mathrm{top}}(n)=n
\Longleftrightarrow
n\in\mathbb P.
}
$$

而：

$$
\boxed{
\operatorname{Fix}(T_{\mathrm{top}})
=
P^*
=
\mathbb P_{>3}.
}
$$

這個結果的 source status 必須固定：

$$
\boxed{
T_{\mathrm{top}}
\text{ 與 }
\operatorname{lpf}
\text{ 在 element level 同源。}
}
$$

也就是：

$$
\mathcal S_1.
$$

fixed-point language的價值是 relational organization，不是新 primality oracle。

本輪第二個核心是 exact fiber。

對：

$$
p\in P^*,
$$

定義：

$$
\boxed{
F_p
=
\left\{
n\in M6^*:
T_{\mathrm{top}}(n)=p
\right\}.
}
$$

V0-R04 已修正原先過寬的：

$$
F_p\sim pU_6.
$$

正確 multiplier set 為：

$$
\boxed{
U_p
=
\left\{
u\in\mathbb N:
\gcd(u,6)=1,
\quad
\forall r\in\mathbb P,
\ r\mid u
\Rightarrow
p\le r
\right\}.
}
$$

其中：

$$
u=1
$$

自動允許。

本輪要 formalize exact theorem：

$$
\boxed{
n\in F_p
\Longleftrightarrow
\exists u\in U_p,
\quad
n=pu.
}
$$

等價 set form：

$$
\boxed{
F_p
=
\{pu:u\in U_p\}.
}
$$

第三個核心是 additive candidate domain：

$$
\boxed{
\mathcal A_N^{(6)}
=
\left\{
a\in M6^*:
N-a\in M6^*
\right\}.
}
$$

V0-R04 已給 elementary explicit witnesses。

對所有 even：

$$
N\ge10,
$$

有：

$$
\boxed{
\mathcal A_N^{(6)}\neq\varnothing.
}
$$

而且 reduced half：

$$
\boxed{
\mathcal A_N^{(6),-}
=
\left\{
a\in\mathcal A_N^{(6)}:
2a\le N
\right\}
}
$$

也非空。

這一 theorem 只需要：

$$
N\bmod6
\in
\{0,2,4\},
$$

並可用：

- $a=5$；
- $a=7$；

作 explicit witnesses。

因此 V1-04 的 formal kernel最終形成：

$$
\boxed{
M6^*
\to
T_{\mathrm{top}}
\to
P^*
\to
F_p
\to
U_p
\to
\mathcal A_N^{(6)}.
}
$$

這將作為 V1-05 的唯一 fixed-point dependency。

---

# 1. V1-04 dependency boundary

允許：

- V1-01 Foundation；
- V1-02 Composite / minFac；
- elementary gcd / divisibility；
- finite sets / subtypes。

不允許：

- V1-03 wheel hard set作 theorem premise；
- $\Delta_6$；
- shadow；
- boundary-$3$；
- capacity；
- minimality；
- heuristic。

---

# 2. M6-star predicate

定義：

$$
\boxed{
\operatorname{M6Star}(n)
:
\Longleftrightarrow
1<n
\land
\gcd(n,6)=1.
}
$$

Lean-oriented：

```lean
def M6Star (n : Nat) : Prop :=
  1 < n ∧ Nat.Coprime n 6
```

---

# 3. Residue characterization

## Theorem V1-04-T01

對：

$$
n>1,
$$

有：

$$
\boxed{
\operatorname{M6Star}(n)
\Longleftrightarrow
n\equiv1\pmod6
\lor
n\equiv5\pmod6.
}
$$

這不是 fixed-point theorem必要依賴，

但對 additive candidate construction與 human-readable bridge很有用。

---

# 4. Prime-star predicate

定義：

$$
\boxed{
\operatorname{PStar}(p)
:
\Longleftrightarrow
\operatorname{Prime}(p)
\land
\operatorname{M6Star}(p).
}
$$

Lean-oriented：

```lean
def PStar (p : Nat) : Prop :=
  Nat.Prime p ∧ M6Star p
```

---

# 5. $P^*=\mathbb P_{>3}$

## Theorem V1-04-T02

對 prime：

$$
p,
$$

$$
\boxed{
\operatorname{PStar}(p)
\Longleftrightarrow
3<p.
}
$$

因 prime若：

$$
p>3,
$$

就不被：

$$
2,3
$$

整除。

反方向：

$$
p\in M6^*
$$

排除：

$$
2,3.
$$

---

# 6. $T_{\mathrm{top}}$ 的 formal representation

原始數學定義：

$$
T_{\mathrm{top}}(n)
=
\min
\left\{
d\in M6^*:
d\mid n
\right\}.
$$

若直接 formalize finite minimum，

需要：

- nonempty divisor set；
- order minimum；
- membership proof。

但 V0 已證：

$$
T_{\mathrm{top}}
=
\operatorname{lpf}
$$

on：

$$
M6^*.
$$

所以 V1-04 有兩種 implementation strategy。

---

# 7. Strategy A — Definitional minFac

直接定義：

```lean
def TTop (n : Nat) : Nat :=
  Nat.minFac n
```

但所有 theorem只在：

```lean
M6Star n
```

下使用。

優點：

- implementation簡單；
- source identity顯式；
- 不重造 divisor minimum。

缺點：

- 與原始「minimum in $M6^*$」定義不是 definitional equality；
- 需要一個 bridge theorem說此 implementation faithful。

---

# 8. Strategy B — Native M6 minimum

定義：

```lean
def TTopNative (n : Nat) : Nat :=
  min {d | M6Star d ∧ d ∣ n}
```

再證：

$$
T_{\mathrm{top}}^{\mathrm{native}}
=
\operatorname{minFac}.
$$

優點：

- 完全保留原始 operator semantics。

缺點：

- formalization成本較高。

---

# 9. V1-04 建議

第一階段採：

$$
\boxed{
\text{Strategy A}
}
$$

但保留 theorem：

$$
\boxed{
\text{TTopSpec}
}
$$

表達它等價於 native minimum。

也就是：

```text
implementation:
  minFac

mathematical_spec:
  least M6Star divisor
```

---

# 10. TTop implementation

Lean-oriented：

```lean
def TTop (n : Nat) : Nat :=
  Nat.minFac n
```

注意：

不得在：

$$
n=0,1
$$

上使用其 primality語義。

所有 fixed-point theorem都要求：

$$
M6Star(n).
$$

---

# 11. Prime divisors of M6-star are also M6-star

## Lemma V1-04-L01

若：

$$
\operatorname{M6Star}(n),
$$

$$
r\in\mathbb P,
$$

且：

$$
r\mid n,
$$

則：

$$
\boxed{
\operatorname{M6Star}(r).
}
$$

---

# 12. L01 proof

若：

$$
2\mid r,
$$

因：

$$
r\mid n,
$$

則：

$$
2\mid n,
$$

與：

$$
\gcd(n,6)=1
$$

矛盾。

同理：

$$
3\nmid r.
$$

所以：

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

且 prime給：

$$
r>1.
$$

---

# 13. Least prime factor lies in M6-star

## Lemma V1-04-L02

若：

$$
\operatorname{M6Star}(n),
$$

則：

$$
\boxed{
\operatorname{M6Star}(\operatorname{minFac}(n)).
}
$$

由：

- minFac prime；
- minFac divides；
- L01。

---

# 14. TTop specification theorem

## Theorem V1-04-T03

若：

$$
\operatorname{M6Star}(n),
$$

則：

$$
\boxed{
T_{\mathrm{top}}(n)
=
\min
\left\{
d:
\operatorname{M6Star}(d)
\land
d\mid n
\right\}.
}
$$

這是 mathematical-spec theorem。

如果 formal minimum notation麻煩，

可以拆成兩條 characterization。

---

# 15. Least-M6-divisor characterization

## Theorem V1-04-T03a

若：

$$
\operatorname{M6Star}(n),
$$

則：

$$
\boxed{
\operatorname{M6Star}(T_{\mathrm{top}}(n))
}
$$

且：

$$
\boxed{
T_{\mathrm{top}}(n)\mid n.
}
$$

---

# 16. Minimality characterization

## Theorem V1-04-T03b

若：

$$
\operatorname{M6Star}(n),
$$

以及：

$$
\operatorname{M6Star}(d),
$$

$$
d\mid n,
$$

則：

$$
\boxed{
T_{\mathrm{top}}(n)\le d.
}
$$

T03a + T03b 就完整表示原始 minimum operator語義。

---

# 17. TTop equals lpf

因 implementation採 minFac，

machine上可能是 definitional。

數學 statement仍正式記：

## Theorem V1-04-T04

若：

$$
\operatorname{M6Star}(n),
$$

則：

$$
\boxed{
T_{\mathrm{top}}(n)
=
\operatorname{lpf}(n).
}
$$

source：

$$
\mathcal S_1.
$$

---

# 18. TTop output prime

## Corollary V1-04-C01

若：

$$
\operatorname{M6Star}(n),
$$

則：

$$
\boxed{
\operatorname{PStar}(T_{\mathrm{top}}(n)).
}
$$

也就是：

$$
T_{\mathrm{top}}
:
M6^*
\to
P^*.
$$

---

# 19. Fixed-point predicate

定義：

$$
\boxed{
\operatorname{TTopFixed}(n)
:
\Longleftrightarrow
\operatorname{M6Star}(n)
\land
T_{\mathrm{top}}(n)=n.
}
$$

Lean-oriented：

```lean
def TTopFixed (n : Nat) : Prop :=
  M6Star n ∧ TTop n = n
```

---

# 20. Fixed-point theorem

## Theorem V1-04-T05

$$
\boxed{
\operatorname{TTopFixed}(n)
\Longleftrightarrow
\operatorname{PStar}(n).
}
$$

這是 V1-04 核心 theorem之一。

---

# 21. T05 proof：prime推 fixed

若：

$$
n
$$

prime，

則：

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

又：

$$
n\in M6^*.
$$

所以 fixed。

---

# 22. T05 proof：fixed推 prime

若：

$$
T_{\mathrm{top}}(n)=n,
$$

即：

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

對：

$$
n>1,
$$

這等價於：

$$
n
$$

prime。

---

# 23. Fixed-point set form

定義：

$$
\operatorname{Fix}(T_{\mathrm{top}})
=
\left\{
n:
\operatorname{TTopFixed}(n)
\right\}.
$$

則：

$$
\boxed{
\operatorname{Fix}(T_{\mathrm{top}})
=
P^*.
}
$$

這是 set-level corollary。

---

# 24. Source de-duplication metadata

formal manifest必須記：

```yaml
TTop:
  implementation_source: Nat.minFac
  arithmetic_source: S1_factor_lpf
  independent_primality_oracle: false
```

避免之後把：

$$
T_{\mathrm{top}}
$$

與：

$$
\operatorname{lpf}
$$

當兩個證據來源。

---

# 25. Multiplicative fiber predicate

對：

$$
p\in P^*,
$$

定義：

$$
\boxed{
\operatorname{FiberOf}(p,n)
:
\Longleftrightarrow
\operatorname{M6Star}(n)
\land
T_{\mathrm{top}}(n)=p.
}
$$

Lean-oriented：

```lean
def FiberOf (p n : Nat) : Prop :=
  PStar p ∧
  M6Star n ∧
  TTop n = p
```

也可把：

$$
PStar(p)
$$

放 theorem premise而不塞 definition。

---

# 26. Fiber partition

## Theorem V1-04-T06

若：

$$
\operatorname{M6Star}(n),
$$

則存在唯一：

$$
p
$$

使：

$$
\boxed{
\operatorname{PStar}(p)
\land
\operatorname{FiberOf}(p,n).
}
$$

由：

$$
p=T_{\mathrm{top}}(n).
$$

因此：

$$
M6^*
=
\bigsqcup_{p\in P^*}F_p.
$$

---

# 27. Basic multiplier form

若：

$$
\operatorname{FiberOf}(p,n),
$$

則：

$$
p\mid n.
$$

所以存在：

$$
u
$$

使：

$$
n=pu.
$$

而：

$$
\gcd(u,6)=1.
$$

但這只是必要條件。

---

# 28. 為什麼 $u\in U_6$ 不夠

反例：

$$
n=35,
\quad
p=7,
\quad
u=5.
$$

$$
\gcd(5,6)=1,
$$

但：

$$
T_{\mathrm{top}}(35)=5.
$$

所以：

$$
35\notin F_7.
$$

因此 old：

$$
F_p=pU_6
$$

不能進 formal core。

---

# 29. Canonical multiplier predicate

定義：

$$
\boxed{
\operatorname{FiberMultiplier}(p,u)
}
$$

當：

$$
\gcd(u,6)=1
$$

且：

$$
\forall r\in\mathbb P,
\quad
r\mid u
\Rightarrow
p\le r.
$$

Lean-oriented：

```lean
def FiberMultiplier (p u : Nat) : Prop :=
  Nat.Coprime u 6 ∧
  ∀ r, Nat.Prime r → r ∣ u → p ≤ r
```

---

# 30. $u=1$ 自動合法

因：

$$
1
$$

沒有 prime divisors，

所以：

$$
\operatorname{FiberMultiplier}(p,1)
$$

只需：

$$
\gcd(1,6)=1.
$$

因此 fixed point：

$$
n=p
$$

正好對應：

$$
u=1.
$$

---

# 31. Fiber implies multiplier constraint

## Theorem V1-04-T07

若：

$$
\operatorname{FiberOf}(p,n),
$$

則存在：

$$
u
$$

使：

$$
\boxed{
n=pu
}
$$

以及：

$$
\boxed{
\operatorname{FiberMultiplier}(p,u).
}
$$

---

# 32. T07 proof

因：

$$
T_{\mathrm{top}}(n)=p,
$$

所以：

$$
p=\operatorname{lpf}(n).
$$

寫：

$$
n=pu.
$$

若：

$$
r\mid u
$$

且：

$$
r
$$

prime，

則：

$$
r\mid n.
$$

由 $p$ 是 least prime factor：

$$
p\le r.
$$

又：

$$
n,p
$$

都 coprime to $6$，

所以：

$$
u
$$

也 coprime to $6$。

---

# 33. Multiplier constraint implies fiber

## Theorem V1-04-T08

若：

$$
\operatorname{PStar}(p),
$$

$$
n=pu,
$$

以及：

$$
\operatorname{FiberMultiplier}(p,u),
$$

則：

$$
\boxed{
\operatorname{FiberOf}(p,n).
}
$$

---

# 34. T08 proof

先證：

$$
n\in M6^*.
$$

因：

$$
p,u
$$

都 coprime to $6$。

再證：

$$
\operatorname{minFac}(n)=p.
$$

因：

- $p\mid n$；
- $p$ prime；
- 任意 prime divisor $r$ of $n$：
  - 若來自 $p$，則 $r=p$；
  - 若整除 $u$，則 $p\le r$。

所以沒有更小 prime factor。

---

# 35. Exact fiber multiplier theorem

## Theorem V1-04-T09

對：

$$
p\in P^*,
$$

有：

$$
\boxed{
\operatorname{FiberOf}(p,n)
\Longleftrightarrow
\exists u,
\quad
n=pu
\land
\operatorname{FiberMultiplier}(p,u).
}
$$

set form：

$$
\boxed{
F_p
=
\left\{
pu:
u\in U_p
\right\}.
}
$$

這是 V0-R04 correction正式進 formal kernel。

---

# 36. Fiber fixed point = multiplier one

## Theorem V1-04-T10

若：

$$
\operatorname{FiberOf}(p,n)
$$

且：

$$
n=pu,
$$

$$
\operatorname{FiberMultiplier}(p,u),
$$

則：

$$
\boxed{
n=p
\Longleftrightarrow
u=1.
}
$$

這將成為 V1-05 pair-energy zero theorem的底層。

---

# 37. Composite fiber point multiplier lower bound

若：

$$
n\in F_p
$$

且：

$$
n\neq p,
$$

則：

$$
u>1.
$$

因 $u$ 的所有 prime factors：

$$
\ge p,
$$

可進一步得到：

$$
\boxed{
u\ge p.
}
$$

---

# 38. Theorem V1-04-T11

若：

$$
\operatorname{FiberOf}(p,n),
$$

$$
n\neq p,
$$

並寫：

$$
n=pu
$$

with valid multiplier，

則：

$$
\boxed{
p\le u.
}
$$

原因：

$$
u>1
$$

有某 prime divisor：

$$
r.
$$

由 FiberMultiplier：

$$
p\le r\le u.
$$

---

# 39. Positive fiber inflation lower bound

由：

$$
n=pu,
$$

$$
u\ge p\ge5,
$$

若：

$$
n\neq p,
$$

則：

$$
n-p
=
p(u-1)
\ge
p(p-1)
\ge
20.
$$

這個 theorem可在 V1-04先建立，

V1-05直接重用。

---

# 40. Theorem V1-04-T12

若：

$$
\operatorname{FiberOf}(p,n),
$$

且：

$$
n\neq p,
$$

則：

$$
\boxed{
20\le n-p.
}
$$

這是：

$$
e_6(n)>0
\Rightarrow
e_6(n)\ge20
$$

的更底層 fiber形式。

---

# 41. Additive candidate predicate

對：

$$
N,a,
$$

定義：

$$
\boxed{
\operatorname{M6AdditiveCandidate}(N,a)
:
\Longleftrightarrow
\operatorname{M6Star}(a)
\land
\operatorname{M6Star}(N-a).
}
$$

Lean-oriented：

```lean
def M6AdditiveCandidate (N a : Nat) : Prop :=
  M6Star a ∧
  M6Star (N - a)
```

---

# 42. Candidate subtraction safety

在 candidate theorem中，

explicit witnesses：

$$
5,7
$$

會保證：

$$
a\le N.
$$

若要 general candidate involution theorem，

需從：

$$
M6Star(N-a)
$$

本身無法反推出：

$$
a\le N
$$

因 Nat subtraction若 underflow：

$$
N-a=0,
$$

不會 M6Star。

所以其實 M6Star(N-a) 已排除 underflow。

可證：

## Lemma V1-04-L03

若：

$$
\operatorname{M6AdditiveCandidate}(N,a),
$$

則：

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

---

# 43. Additive candidate set

$$
\boxed{
\mathcal A_N^{(6)}
=
\left\{
a:
\operatorname{M6AdditiveCandidate}(N,a)
\right\}.
}
$$

---

# 44. Complement closure

## Theorem V1-04-T13

若：

$$
\operatorname{M6AdditiveCandidate}(N,a),
$$

則：

$$
\boxed{
\operatorname{M6AdditiveCandidate}(N,N-a).
}
$$

並有：

$$
\boxed{
N-(N-a)=a.
}
$$

由 L03。

這建立 additive involution。

---

# 45. Even target residue cases

若：

$$
N
$$

even，

則：

$$
N\bmod6
\in
\{0,2,4\}.
$$

對：

$$
N\ge10,
$$

三個 case可給 explicit candidate。

---

# 46. Case $N\equiv0\pmod6$

取：

$$
a=5.
$$

則：

$$
5\in M6^*.
$$

且：

$$
N-5\equiv1\pmod6.
$$

若：

$$
N\ge12,
$$

則：

$$
N-5\ge7>1.
$$

所以：

$$
N-5\in M6^*.
$$

---

# 47. Case $N\equiv2\pmod6$

對 even：

$$
N\ge10,
$$

且：

$$
N\equiv2\pmod6,
$$

最小可能其實是：

$$
14.
$$

取：

$$
a=7.
$$

則：

$$
N-7\equiv1\pmod6,
$$

且：

$$
N-7\ge7.
$$

所以 candidate。

---

# 48. Case $N\equiv4\pmod6$

取：

$$
a=5.
$$

則：

$$
N-5\equiv5\pmod6.
$$

對：

$$
N\ge10,
$$

$$
N-5\ge5.
$$

所以 candidate。

---

# 49. Additive candidate nonempty theorem

## Theorem V1-04-T14

若：

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

且：

$$
10\le N,
$$

則：

$$
\boxed{
\exists a,
\operatorname{M6AdditiveCandidate}(N,a).
}
$$

這是 V0-R04 additive-surjectivity的 elementary kernel。

---

# 50. 不依賴 prime distribution

T14只使用：

- parity；
- residue mod $6$；
- constants $5,7$。

所以 source：

$$
\boxed{
\mathcal S_0+\mathcal S_2.
}
$$

不依賴：

- Goldbach；
- lpf distribution；
- analytic theorem。

---

# 51. Reduced M6 candidate

定義：

$$
\boxed{
\operatorname{M6ReducedCandidate}(N,a)
:
\Longleftrightarrow
\operatorname{M6AdditiveCandidate}(N,a)
\land
2a\le N.
}
$$

---

# 52. Reduced candidate nonempty theorem

## Theorem V1-04-T15

若：

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

且：

$$
10\le N,
$$

則：

$$
\boxed{
\exists a,
\operatorname{M6ReducedCandidate}(N,a).
}
$$

---

# 53. Explicit witnesses滿足 reduced bound

### $N\equiv0$

$$
a=5.
$$

最小：

$$
N=12.
$$

$$
2a=10\le12.
$$

### $N\equiv2$

$$
a=7.
$$

最小：

$$
N=14.
$$

$$
2a=14\le14.
$$

### $N\equiv4$

$$
a=5.
$$

最小：

$$
N=10.
$$

$$
2a=10\le10.
$$

所以同一 witnesses足夠。

---

# 54. Reduced candidate domain的意義

V1-05 定義：

$$
\Delta_6(N)
$$

時可以只在：

$$
\mathcal A_N^{(6),-}
$$

取 minimum，

因 complement involution保證 pair symmetry。

這可將 finite search domain減半。

---

# 55. Candidate count不是 Goldbach count

$$
\mathcal A_N^{(6)}
$$

只要求：

$$
a,N-a\in M6^*.
$$

它不要求兩者 prime。

所以：

$$
\boxed{
\mathcal A_N^{(6)}\neq\varnothing
}
$$

對 Goldbach本身幾乎是 background geometry。

不能把 candidate nonemptiness誤當 Goldbach進展。

---

# 56. Fixed-point incidence尚未在本輪定義

本輪到：

$$
M6AdditiveCandidate
$$

為止。

不定義：

$$
\mathcal Z_6(N).
$$

原因：

V1-05 要把：

- fixed-point incidence；
- defect；
- pair energy；
- $\Delta_6$；
- two-channel theorem；

放在同一個 coherent module。

---

# 57. TTop / minFac source firewall

任何後續 theorem若寫：

```text
TTop n = ...
```

source ledger自動標：

$$
\mathcal S_1.
$$

不能另標：

```text
new fixed point source
```

除非 theorem使用的是：

- cross-fiber；
- additive incidence；
- shadow relation；

而不是單點 TTop value。

---

# 58. Fixed-point relational source從哪裡開始？

$\mathcal S_3$ 真正開始於：

- fiber partition；
- additive candidate coupling；
- pair section；
- shadow。

所以本輪：

$$
T_{\mathrm{top}}=\operatorname{lpf}
$$

仍是：

$$
\mathcal S_1.
$$

而：

$$
F_p
$$

與：

$$
\mathcal A_N^{(6)}
$$

開始提供：

$$
\boxed{
\mathcal S_3
\text{ organization}.
}
$$

---

# 59. Canonical theorem queue

```yaml
V1_04:
  - id: T01
    name: m6star_iff_mod6_one_or_five
    status: to_formalize

  - id: T02
    name: pstar_iff_prime_gt_three
    status: to_formalize

  - id: T03a
    name: ttop_is_m6star_divisor
    status: to_formalize

  - id: T03b
    name: ttop_le_any_m6star_divisor
    status: to_formalize

  - id: T04
    name: ttop_eq_minFac_on_m6star
    status: to_formalize

  - id: T05
    name: ttop_fixed_iff_pstar
    status: to_formalize

  - id: T06
    name: m6star_unique_fiber
    status: to_formalize

  - id: T07
    name: fiber_implies_exact_multiplier_constraints
    status: to_formalize

  - id: T08
    name: exact_multiplier_constraints_imply_fiber
    status: to_formalize

  - id: T09
    name: fiber_iff_p_times_Up
    status: to_formalize

  - id: T10
    name: fiber_fixed_iff_multiplier_one
    status: to_formalize

  - id: T11
    name: nonfixed_fiber_multiplier_ge_p
    status: to_formalize

  - id: T12
    name: positive_fiber_inflation_ge_twenty
    status: to_formalize

  - id: T13
    name: m6_additive_candidate_complement_closed
    status: to_formalize

  - id: T14
    name: m6_additive_candidate_nonempty
    status: to_formalize

  - id: T15
    name: m6_reduced_candidate_nonempty
    status: to_formalize
```

---

# 60. Lean-oriented skeleton

```lean
namespace RGSCP

def M6Star (n : Nat) : Prop :=
  1 < n ∧ Nat.Coprime n 6

def PStar (p : Nat) : Prop :=
  Nat.Prime p ∧ M6Star p

def TTop (n : Nat) : Nat :=
  Nat.minFac n

def TTopFixed (n : Nat) : Prop :=
  M6Star n ∧ TTop n = n

def FiberOf (p n : Nat) : Prop :=
  PStar p ∧
  M6Star n ∧
  TTop n = p

def FiberMultiplier (p u : Nat) : Prop :=
  Nat.Coprime u 6 ∧
  ∀ r, Nat.Prime r → r ∣ u → p ≤ r

def M6AdditiveCandidate (N a : Nat) : Prop :=
  M6Star a ∧
  M6Star (N - a)

def M6ReducedCandidate (N a : Nat) : Prop :=
  M6AdditiveCandidate N a ∧
  2 * a ≤ N

end RGSCP
```

---

# 61. Unit test：M6-star

應驗：

```text
5   -> true
7   -> true
11  -> true
13  -> true
25  -> true
35  -> true

2   -> false
3   -> false
6   -> false
9   -> false
15  -> false
```

---

# 62. Unit test：TTop

$$
T_{\mathrm{top}}(5)=5.
$$

$$
T_{\mathrm{top}}(25)=5.
$$

$$
T_{\mathrm{top}}(35)=5.
$$

$$
T_{\mathrm{top}}(49)=7.
$$

$$
T_{\mathrm{top}}(77)=7.
$$

---

# 63. Unit test：fixed points

```text
5  fixed
7  fixed
11 fixed

25 not fixed
35 not fixed
49 not fixed
```

---

# 64. Unit test：fiber correction

For:

$$
p=7,
$$

$$
n=35.
$$

雖：

$$
35=7\cdot5,
$$

但：

$$
5<7.
$$

所以：

```text
FiberMultiplier 7 5 = false
FiberOf 7 35 = false
FiberOf 5 35 = true
```

這是 V0-R04 最重要 regression test。

---

# 65. Unit test：valid fiber multiplier

$$
p=5,
\quad
u=7.
$$

$$
n=35.
$$

所有 prime divisors of $7$：

$$
\ge5.
$$

所以：

```text
FiberMultiplier 5 7 = true
FiberOf 5 35 = true
```

---

# 66. Unit test：square fiber

$$
p=5,
\quad
u=5,
\quad
n=25.
$$

valid。

$$
T_{\mathrm{top}}(25)=5.
$$

且：

$$
n-p=20.
$$

正好達成 positive inflation lower bound：

$$
20.
$$

---

# 67. Unit test：$N=10$

$$
N\equiv4\pmod6.
$$

取：

$$
a=5.
$$

$$
N-a=5.
$$

所以：

```text
M6AdditiveCandidate 10 5 = true
M6ReducedCandidate 10 5 = true
```

---

# 68. Unit test：$N=12$

$$
N\equiv0\pmod6.
$$

取：

$$
a=5.
$$

$$
N-a=7.
$$

candidate成立。

---

# 69. Unit test：$N=14$

$$
N\equiv2\pmod6.
$$

取：

$$
a=7.
$$

$$
N-a=7.
$$

candidate成立。

---

# 70. Unit test：$N=16$

$$
N\equiv4\pmod6.
$$

取：

$$
a=5.
$$

$$
N-a=11.
$$

candidate成立。

---

# 71. Additive candidate theorem不應依賴 primes

注意：

$$
a=5,7
$$

碰巧也是 prime，

但 proof只需要：

$$
a\in M6^*.
$$

不要把 theorem寫成：

> 因 $5,7$ 是 prime，所以 candidate存在。

真正需要的是 residue / positivity。

這可減少不必要 source dependency。

---

# 72. Additive candidate domain包含 composite

例如：

$$
25\in M6^*.
$$

所以 candidate domain不是 prime domain。

這正是 V1-05 要研究：

$$
\text{full candidate}
\to
\text{fixed-point section}
$$

的理由。

---

# 73. Formalization API uncertainty

compile前需核對：

```text
Nat.minFac
Nat.minFac_prime
Nat.minFac_dvd
Nat.prime_iff_minFac
Nat.Coprime
mod-six residue lemmas
prime factor existence for u > 1
```

若 API不同，

只調 proof implementation。

不能修改 theorem semantics。

---

# 74. Alternative to prime-factor-of-u theorem

T11：

$$
u>1
\Rightarrow
\exists r\in\mathbb P,\ r\mid u
$$

如果 Mathlib API難找，

可直接使用：

$$
\operatorname{minFac}(u)
$$

作 witness。

因：

$$
u>1,
$$

minFac prime且 divides。

再由 FiberMultiplier：

$$
p\le\operatorname{minFac}(u)\le u.
$$

這可能是最乾淨 formal route。

---

# 75. Formal acceptance gate

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

### G1

M6Star domain固定。

### G2

TTop implementation / mathematical spec bridge完成。

### G3

TTop = minFac source identity明確。

### G4

fixed points iff PStar完成。

### G5

fiber partition unique。

### G6

old $U_6$ multiplier bug不存在。

### G7

exact $U_p$ multiplier theorem完成。

### G8

nonfixed multiplier：

$$
u\ge p.
$$

完成。

### G9

positive inflation：

$$
n-p\ge20.
$$

完成。

### G10

additive candidate nonempty完成。

### G11

reduced additive candidate nonempty完成。

### G12

no `sorry`.

---

# 76. Bug / Falsification Checklist

若出現以下任一，停止：

1. $35\in F_7$；
2. composite M6 point被判 fixed；
3. prime $>3$ 被判 non-fixed；
4. TTop theorem在非 M6Star domain被無條件使用；
5. multiplier只要求 gcd$(u,6)=1$；
6. $u=1$ 被排除；
7. $25$ 的 positive inflation不是 $20$；
8. additive candidate theorem使用 Goldbach assumption；
9. candidate set被誤當 prime-pair set；
10. V1-05 object提前進 V1-04；
11. TTop與 minFac被記成兩個 independent sources。

---

# 77. Source Signature

```yaml
RG-SCP-V1-04:
  S0_elementary:
    role:
      - gcd
      - divisibility
      - residue
      - additive_candidate

  S1_factor_lpf:
    role:
      - TTop
      - fixed_point
      - fiber_label
      - multiplier_lower_bound

  S2_finite_quotient:
    role:
      - M6Star_domain
      - mod6_candidate_construction

  S3_fixed_point_relational:
    role:
      - fiber_partition
      - additive_candidate_interface

  S4_minimality:
    forbidden_dependency: true

  S5_analytic:
    forbidden_dependency: true

  S6_heuristic:
    forbidden_dependency: true

source_identity:
  TTop_eq_lpf: true
  new_primality_oracle: false
```

---

# 78. Proof-compression status

本輪真正的新 compression不是：

$$
T_{\mathrm{top}}=\operatorname{lpf}.
$$

那只是 source normalization。

真正值得保留的是：

$$
\boxed{
M6^*
=
\bigsqcup_{p\in P^*}
F_p
}
$$

以及：

$$
\boxed{
F_p
=
pU_p.
}
$$

這把 factor structure整理成可與 additive fiber耦合的 relational coordinates。

---

# 79. V1-04 Verdict

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

仍然：

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

本輪完成的是：

> 將 M6 fixed-point line從概念語言壓成可 machine-check 的 exact domain/operator/fiber contract，並徹底修正舊 $F_p=pU_6$ 過寬問題。

---

# 80. 下一輪

下一篇：

# RG-SCP Validation V1-05
## M6 Section / Defect / Shadow / Two-Channel Kernel

只做：

- fixed-point incidence set；
- $e_6$；
- pair energy；
- $\Delta_6$；
- $\Delta_6=0$ iff M6 prime-pair section；
- positive $\Delta_6\ge20$；
- shadow identity；
- shadow gap；
- two-channel count theorem；
- $6\mid N$ clean branch；
- naive shadow descent no-go。

這將是 fixed-point line真正接回 Goldbach target的一輪。

---

# 81. 最短版本

V1-04 的核心是：

$$
\boxed{
M6^*
=
\{n>1:\gcd(n,6)=1\}
}
$$

$$
\boxed{
T_{\mathrm{top}}(n)=\operatorname{lpf}(n)
}
$$

$$
\boxed{
\operatorname{Fix}(T_{\mathrm{top}})
=
P^*
}
$$

以及：

$$
\boxed{
F_p
=
\{pu:u\in U_p\}
}
$$

其中：

$$
\boxed{
U_p
=
\left\{
u:
\gcd(u,6)=1,
\quad
r\mid u,\ r\in\mathbb P
\Rightarrow
p\le r
\right\}.
}
$$

再加：

$$
\boxed{
\mathcal A_N^{(6),-}\neq\varnothing
}
$$

對所有 even：

$$
N\ge10.
$$

這就是 V1-05 建立 $\Delta_6$ 與 shadow geometry所需的完整 fixed-point kernel。

---

# 附錄 A：Lean-Oriented Skeleton

```lean
namespace RGSCP

def M6Star (n : Nat) : Prop :=
  1 < n ∧ Nat.Coprime n 6

def PStar (p : Nat) : Prop :=
  Nat.Prime p ∧ M6Star p

def TTop (n : Nat) : Nat :=
  Nat.minFac n

def TTopFixed (n : Nat) : Prop :=
  M6Star n ∧ TTop n = n

def FiberOf (p n : Nat) : Prop :=
  PStar p ∧
  M6Star n ∧
  TTop n = p

def FiberMultiplier (p u : Nat) : Prop :=
  Nat.Coprime u 6 ∧
  ∀ r, Nat.Prime r → r ∣ u → p ≤ r

def M6AdditiveCandidate (N a : Nat) : Prop :=
  M6Star a ∧
  M6Star (N - a)

def M6ReducedCandidate (N a : Nat) : Prop :=
  M6AdditiveCandidate N a ∧
  2 * a ≤ N

end RGSCP
```

---

# 附錄 B：Canonical Unit Tests

```yaml
TTop:
  5: 5
  25: 5
  35: 5
  49: 7
  77: 7

fixed:
  true: [5,7,11,13]
  false: [25,35,49,77]

fiber:
  - p: 7
    n: 35
    expected: false

  - p: 5
    n: 35
    expected: true

  - p: 5
    n: 25
    expected: true
    inflation: 20

additive_candidates:
  - N: 10
    a: 5
  - N: 12
    a: 5
  - N: 14
    a: 7
  - N: 16
    a: 5
```

---

# 附錄 C：Superseded Claim

```yaml
superseded:
  old:
    fiber_multiplier:
      condition: gcd(u,6)=1

  new:
    fiber_multiplier:
      conditions:
        - gcd(u,6)=1
        - every_prime_divisor_of_u_ge_p

  counterexample:
    35_equals_7_times_5:
      why_old_fails: TTop(35)=5
```

---

# 附錄 D：Formal Dependency

```text
V1-02 minFac / Composite
  ↓
M6Star
  ↓
TTop
  ↓
TTopFixed
  ↓
PStar
  ↓
FiberOf
  ↓
FiberMultiplier
  ↓
Exact Fiber Theorem
  ↓
Positive Inflation >= 20
```

parallel：

```text
M6Star
  ↓
M6AdditiveCandidate
  ↓
ReducedCandidateNonempty
  ↓
V1-05 Section / Delta / Shadow
```

---

# 附錄 E：Commit Decision

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

formal_status:
  machine_checked: false
  lean_compiled: false
  sorry_free: not_yet_tested

canonical_decisions:
  - M6Star_domain_fixed
  - TTop_implemented_via_minFac_with_native_spec_bridge
  - TTop_and_lpf_same_S1_source
  - fixed_points_equal_PStar
  - exact_fiber_uses_U_p_not_U6
  - nonfixed_multiplier_ge_p
  - positive_fiber_inflation_ge_20
  - additive_candidate_nonempty_for_even_N_ge_10
  - reduced_candidate_nonempty
  - Delta_shadow_two_channel_deferred_to_V1_05

next_round:
  V1-05_M6_Section_Defect_Shadow_TwoChannel_Kernel

commit_to_sync_core: true
```