# SDRPC-PRIME-001 Validation Phase I — Round 13
## Counterexample-Guided Adaptive Policy Synthesis

**日期：** 2026-09-23  
**Domain：** odd `3 ≤ n ≤ 2,000,000`

**作者：** Neo.K  
**機構：** EveMissLab／一言諾科技有限公司  
**版本：** 原稿未標註（本次整理版）  

---

## 1. 這次 Policy 不再人工指定

Round 12 是 exhaustive / curated policy search。

Round 13 改成 counterexample-guided synthesis：

```text
start with empty policy
-> find lowest surviving composite witness
-> among atoms that reject this witness,
   choose the best composite-elimination / generation-cost atom
-> append only on the all-pass branch
-> repeat
```

Prime truth 只用於 validation / safety gate；registered atom 不允許誤拒 prime。

## 2. Synthesized Policy

```text
D3 → D5 → D7 → S2 → S7 → S3
```

Depth = **6**  
Average atoms evaluated = **2.955**  
Average probe-generation proxy = **23.000**  
Composite fallback = **0**

## 3. Synthesis Trace

| Step | Witness | Chosen atom | Rejected composites | Remaining composites | Stage avg cost(active) |
|---:|---:|---|---:|---:|---:|
| 1 | 9 | `D3` | 333,332 | 517,735 | 1.000 |
| 2 | 25 | `D5` | 133,332 | 384,403 | 1.000 |
| 3 | 49 | `D7` | 76,190 | 308,213 | 1.000 |
| 4 | 121 | `S2` | 308,144 | 69 | 27.701 |
| 5 | 2,047 | `S7` | 68 | 1 | 27.312 |
| 6 | 314,821 | `S3` | 1 | 0 | 27.312 |

這張表是真正的『policy 生長史』：每個新 atom 都有一個具體 counterexample forcing event。

## 4. Counterexample 在這裡不只是反駁

現在 witness 有三個角色：

1. 證明目前 policy insufficient；
2. 限定下一輪候選 atom 必須真的能分裂它；
3. 成為 policy graph 中新增 node 的 provenance。

所以：

```text
counterexample -> repair obligation -> operator insertion
```

CGPR 在這裡正式變成 synthesis rule。

## 5. 與其他 Policy 比較

| Policy | Sequence | Depth | Avg atoms | Avg probe cost | Fallback | First fallback |
|---|---|---:|---:|---:|---:|---:|
| CG first-witness | `D3 → D5 → D7 → S2 → S7 → S3` | 6 | 2.955 | 23.000 | 0 | None |
| Global greedy | `D3 → D5 → D7 → S2 → S7 → S3` | 6 | 2.955 | 23.000 | 0 | None |
| R12 best-zero example | `S3 → S2 → S7` | 3 | 1.298 | 26.967 | 0 | None |
| Cheap-route + MR | `D3 → D5 → D7 → S2 → S3 → S5` | 6 | 2.955 | 23.000 | 0 | None |

這個比較很重要：counterexample-guided greedy 不保證找到全域最低 burden policy。

它的價值是：

```text
every added operator has a witnessed necessity at insertion time
```

而 exhaustive search 的優勢則是能找到更好的全域排列，但缺少同樣清楚的生成 provenance。

## 6. Greedy Policy 與 Global-Greedy Control

Counterexample-guided：`D3 → D5 → D7 → S2 → S7 → S3`。

Global elimination/cost greedy：`D3 → D5 → D7 → S2 → S7 → S3`。

如果兩者不同，代表『先修眼前反例』和『最大化整體淘汰效率』是兩個不同 objective。

這是 proof-policy synthesis 的第一個真正 control problem。

## 7. Ablation：插入過的 Atom 後來還必要嗎？

- 移除 `D3` → fallback=0, first=None, avg probe=28.963
- 移除 `D5` → fallback=0, first=None, avg probe=25.648
- 移除 `D7` → fallback=0, first=None, avg probe=24.588
- 移除 `S2` → fallback=8, first=703, avg probe=18.946
- 移除 `S7` → fallback=3, first=1373653, avg probe=18.933
- 移除 `S3` → fallback=1, first=314821, avg probe=18.933

這裡故意做 post-hoc ablation。

因為一個 atom 在插入當下可能是必要的，但後續加入更強 atom 後，它可能變成冗餘。

所以：

```text
insertion-time necessity != final-policy necessity
```

這表示 synthesis 後還需要 compression / pruning pass。

## 8. 這就是一個新的 Proof Policy 生命週期

目前完整流程已經變成：

```text
counterexample discovery
-> local repair
-> policy growth
-> new counterexample
-> further repair
-> zero-repair candidate
-> global ablation
-> policy compression
-> certificate handoff
```

它和傳統一次性寫出固定 proof script 很不一樣。

## 9. Policy Graph 已可序列化

本輪輸出 `policy_graph.json`，每個 node 保存：

- atom；
- fail edge；
- pass edge；
- terminal certificate handoff。

而 `synthesis_trace.json` 保存它為什麼長出來。

所以現在不只 proof 可 replay，**proof architecture 的形成過程也可 replay。**

## 10. 對算子本體論的再前進

前面是：

```text
operator set
-> operator order
-> branch semantics
```

現在再多一層：

```text
operator provenance
```

也就是每個 operator 為什麼被加入，必須由某個 unresolved state / witness 支撐。

這使 operator ontology 從靜態 ontology 變成演化 ontology。

## 11. Round 13 的限制

- atom grammar 是人工給定的；
- witness selection 固定為 lowest surviving composite；
- objective 是局部 elimination/cost greedy；
- 沒有證明 synthesized policy globally optimal；
- zero fallback 仍只對 finite domain 有效。

所以這是 synthesis prototype，不是新 primality theorem。

## 12. 下一輪

Round 14 最值得做：

```text
Policy Pruning + Branch-Specific Atom Invention
```

兩部分：

1. 對 synthesized policy 做最小化，刪除被後續 operators 支配的歷史修補；
2. 不只從固定 atom grammar 選，開始允許從 counterexample fiber 自動生成 candidate relational probes。

也就是從：

```text
choose an atom
```

升級成：

```text
invent a probe that splits the unresolved fiber
```

那才真正會開始碰到 SDRPC 原本想要的新搜尋法。

## 13. Round 13 結論

```text
counterexamples can synthesize proof policy structure;
local repair decisions carry provenance;
insertion-time necessity may disappear after later refinements;
therefore synthesis must be followed by pruning;
proof architecture can itself be a replayable evolving object.
```

---

```text
Round 13: COMPLETE
Next: Round 14 — Policy Pruning + Branch-Specific Atom Invention
```