# SECV Paper 01｜符號對等約束變量法：母方法與形式基礎

**English Title:** Symbolic Equivalence-Constrained Variable Method: Foundational Definitions and Formal Basis  
**Series:** Symbolic Equivalence-Constrained Variable Method  
**Paper:** 01 / 10  
**Version:** v0.1  
**Author:** Neo.K  
**AI Collaboration:** Aletheia (GPT-5.6 Sol)  
**Status:** Foundational Draft

---

## 摘要

本文提出「符號對等約束變量法」（Symbolic Equivalence-Constrained Variable Method, SECV），作為一種以合法域、符號等價、約束保存、對偶映射與變量消除為核心的形式方法。其基本立場不是直接求解所有變量，而是先判定哪些符號在既定約束與證明義務下並非獨立自由度，並以可驗證的等價、對偶、商化、殘差化與不變量保存規則將其消除或壓縮。

SECV 的核心不是「允許任意消符號」，而是建立一套 legality-first 的演算規則：所有定義域、合法性判定、等價關係、允許變換與閉合條件必須在目標推演前明確給定；任何消除步驟都必須攜帶可檢查的保真見證；任何事後新增規則都必須重新啟動驗證，而不能直接插入原有證明鏈。

本文定義符號域、合法域、證明義務、語義等價、對偶算子、消除算子、殘餘域、生成歷史與規則凍結原則，並提出 SECV 的基本 soundness contract。本文不主張單靠本方法即可解決特定未解數學問題；其目的在於提供一個可審計、可演算法化、可擴展到有限階與無限階消元、以及後續生成種子理論的母框架。

---

## 關鍵詞

符號消元、約束推理、等價類、商空間、對偶、自指、形式證明、殘餘域、變量降維、生成種子、符號計算。

---

# 1. 問題：為什麼一定要把所有變量都求出來？

傳統求解通常以未知量的顯式值為目標。給定問題

$$
P(x_1,x_2,\ldots,x_n),
$$

常見策略是尋找一組

$$
(x_1,x_2,\ldots,x_n)
$$

使全部約束成立。

SECV 採取不同的第一問題：

$$
\boxed{
\text{在目前證明義務下，哪些 }x_i\text{ 仍然具有獨立符號自由度？}
}
$$

若兩個符號在既定約束下對所有相關命題具有相同行為，則沒有必要同時保留其完整表示。若兩個符號形成可證明的對偶、相消、商化或殘差關係，也可以將其轉換為更小的不可約符號表示。

因此，SECV 的計算目標不是單純：

$$
\text{Solve all variables},
$$

而是：

$$
\boxed{
\text{Prove which variables no longer need to exist independently.}
}
$$

這使問題求解從「值搜尋」擴展為「符號自由度削減」。

---

# 2. 基本形式系統

定義一個 SECV 規格：

$$
\mathfrak M
=
(
\Sigma,
\mathcal X,
\Gamma,
\mathcal Q,
\mathcal T,
\mathcal I,
\mathcal C
).
$$

其中：

$$
\Sigma
$$

為基礎符號字母表；

$$
\mathcal X
$$

為由 $\Sigma$ 構造出的允許符號狀態空間；

$$
\Gamma
$$

為問題約束集合；

$$
\mathcal Q
$$

為本輪推演必須保存的證明義務集合；

$$
\mathcal T
$$

為允許使用的符號轉換規則族；

$$
\mathcal I
$$

為必須保持的不變量族；

$$
\mathcal C
$$

為閉合與停止條件。

這七個元素共同決定一個 SECV 遊戲的合法規則。

---

# 3. 合法域

對任意符號狀態 $x\in\mathcal X$，定義合法性判定：

$$
\mathsf{Adm}_\Gamma(x)\in\{0,1\}.
$$

若

$$
\mathsf{Adm}_\Gamma(x)=1,
$$

則稱 $x$ 為相對於 $\Gamma$ 的合法狀態。

合法域定義為：

$$
\mathcal X_\Gamma
=
\{
x\in\mathcal X:
\mathsf{Adm}_\Gamma(x)=1
\}.
$$

SECV 不允許在未證明合法性的對象上直接執行消元。因此任何轉換

$$
T:x\mapsto y
$$

都必須先滿足：

$$
x\in\mathcal X_\Gamma,
$$

並證明：

$$
y\in\mathcal X_\Gamma
$$

或證明 $y$ 落入事先定義的另一合法型別。

此原則稱為：

$$
\boxed{
\text{Legality Before Reduction}.
}
$$

---

# 4. 證明義務與相對語義

兩個符號是否「相同」不能只由字面形式決定。

設

$$
\mathcal Q
=
\{Q_1,Q_2,\ldots,Q_m\}
$$

為當前證明義務。

定義相對語義等價：

$$
x\equiv_{\Gamma,\mathcal Q}y
$$

若且唯若對所有

$$
Q\in\mathcal Q,
$$

有：

$$
Q(x\mid\Gamma)
=
Q(y\mid\Gamma).
$$

因此：

$$
x\neq y
$$

在表面語法上完全可能成立，同時：

$$
x\equiv_{\Gamma,\mathcal Q}y.
$$

SECV 所消除的首先不是「不同字串」，而是「對當前證明義務而言不再獨立的表示」。

---

# 5. 商化消除

若

$$
x\equiv_{\Gamma,\mathcal Q}y,
$$

可將兩者映射至同一等價類：

$$
x,y
\longmapsto
[x]_{\Gamma,\mathcal Q}.
$$

此時原本兩個符號自由度被壓縮為一個代表元。

定義商化算子：

$$
\mathcal E_{\mathrm{quot}}
(x,y)
=
[x]_{\Gamma,\mathcal Q}.
$$

合法商化必須滿足：

$$
\forall Q\in\mathcal Q,
\qquad
Q(x)=Q(y)=Q([x]).
$$

因此商化不是刪除資訊本身，而是刪除對當前任務無效的表示差異。

---

# 6. 對偶算子

定義一個或多個對偶算子：

$$
D_j:\mathcal X_\Gamma\rightarrow\mathcal X_\Gamma.
$$

其用途不是預設 $x$ 與 $D_j(x)$ 必然相等，而是產生一個可比較的符號像。

最一般的比較形式為：

$$
x
\leftrightarrow
D_j(x).
$$

若某個 $D$ 為 involution，則：

$$
D^2=I.
$$

此時可進一步定義對稱與反對稱分量：

$$
P_+
=
\frac{I+D}{2},
$$

$$
P_-
=
\frac{I-D}{2}.
$$

因此任意可線性表示的 $x$ 可以拆為：

$$
x=P_+x+P_-x.
$$

後續若證明某個 sector 對證明義務完全冗餘，便可以合法消除該 sector。

---

# 7. 符號對角性

本文將「符號對角性」定義為：將一個符號與其在某個合法轉換下的像放入同一比較槽。

對符號集合

$$
X=(x_1,x_2,\ldots,x_n),
$$

定義：

$$
D(X)
=
(D(x_1),D(x_2),\ldots,D(x_n)).
$$

對角比較為：

$$
(x_i,D(x_i)).
$$

定義關係矩陣：

$$
M^D_{ij}
=
R_\Gamma(x_i,D(x_j)).
$$

其中最重要的是對角項：

$$
M^D_{ii}
=
R_\Gamma(x_i,D(x_i)).
$$

SECV 可依照對角關係將 $x_i$ 分為：

$$
\begin{cases}
\text{完全可消除},\\
\text{可商化},\\
\text{可殘差化},\\
\text{不可約}.
\end{cases}
$$

因此「對角性」不是傳統線性代數中的矩陣對角化，而是符號與其合法自映射像之間的結構比較。

---

# 8. 殘差化

若 $x$ 與 $y$ 並不完全等價，但存在共同結構 $c$：

$$
x=c+r_x,
$$

$$
y=c+r_y,
$$

則沒有必要同時保存 $x$ 與 $y$ 的完整形式。

可定義殘差：

$$
\Delta(x,y)
=
r_x-r_y.
$$

並施行：

$$
(x,y)
\longmapsto
\Delta(x,y).
$$

但此轉換只有在 $\Delta$ 足以保存 $\mathcal Q$ 所需資訊時才合法。

形式上需要：

$$
\forall Q\in\mathcal Q,
$$

存在可計算的

$$
\widehat Q
$$

使：

$$
Q(x,y\mid\Gamma)
=
\widehat Q(\Delta(x,y)\mid\Gamma).
$$

此時稱 $\Delta$ 為相對於 $\mathcal Q$ 的充分殘差。

---

# 9. 消除算子與見證

定義部分消除算子：

$$
\mathcal E_\Gamma:
\mathcal X_\Gamma
\rightharpoonup
\mathcal X_\Gamma.
$$

每一個消除步驟都必須附帶見證：

$$
w:
\mathsf{ValidElim}_\Gamma(x\rightarrow y).
$$

見證至少要證明：

$$
\mathsf{Adm}_\Gamma(x)=1,
$$

$$
\mathsf{Adm}_\Gamma(y)=1,
$$

以及：

$$
\forall I\in\mathcal I,
\qquad
I(x)=I(y),
$$

或在明確允許的情況下：

$$
I(y)
=
F_I(I(x))
$$

且 $F_I$ 已在規則集中預先定義。

因此 SECV 的基本 soundness contract 為：

$$
\boxed{
x
\xrightarrow[\;w\;]{\mathcal E_\Gamma}
y
\quad
\Longrightarrow
\quad
\mathcal Q(x\mid\Gamma)
\equiv
\mathcal Q(y\mid\Gamma).
}
$$

---

# 10. 規則先於推演

SECV 最重要的認識論約束之一是：

$$
\boxed{
\text{Rule Before Derivation}.
}
$$

若目標命題為 $P$，則在正式推演前必須凍結：

$$
\mathfrak M_0
=
(
\Sigma,
\mathcal X,
\Gamma,
\mathcal Q,
\mathcal T,
\mathcal I,
\mathcal C
).
$$

正式推演期間要求：

$$
\mathfrak M_t
=
\mathfrak M_0.
$$

若推演中新增規則 $T_{\mathrm{new}}$，則原推演不得直接繼續視為同一證明，而應建立：

$$
\mathfrak M_1
=
\mathfrak M_0
\cup
\{T_{\mathrm{new}}\},
$$

並重新驗證先前所有依賴步驟。

因此：

$$
\boxed{
\text{No Post-Hoc Cancellation Rules}.
}
$$

此規則用來防止因目標結論而事後設計消除規則，使方法退化為結論導向的符號過擬合。

---

# 11. 不變量保存

設：

$$
\mathcal I
=
\{I_1,I_2,\ldots,I_r\}.
$$

每一步：

$$
X_k
\rightarrow
X_{k+1}
$$

必須滿足：

$$
I_j(X_k)
=
I_j(X_{k+1})
$$

對所有需要嚴格保存的 $I_j$ 成立。

若某些量允許單調變化，則必須預先聲明，例如：

$$
J(X_{k+1})
\le
J(X_k).
$$

因此不變量可分為：

$$
\mathcal I
=
\mathcal I_{\mathrm{strict}}
\cup
\mathcal I_{\mathrm{mono}}
\cup
\mathcal I_{\mathrm{tracked}}.
$$

其中：

$$
\mathcal I_{\mathrm{strict}}
$$

要求精確保存；

$$
\mathcal I_{\mathrm{mono}}
$$

允許事先規定方向的單調變化；

$$
\mathcal I_{\mathrm{tracked}}
$$

可變化但必須完整記錄。

---

# 12. 殘餘符號域

令初始符號狀態為：

$$
X_0.
$$

反覆施行合法 reduction：

$$
X_{n+1}
=
\mathcal R_{\Gamma}(X_n).
$$

若存在有限 $N$ 使：

$$
X_{N+1}
\cong
X_N,
$$

則稱：

$$
X_\star=X_N
$$

為有限閉合殘餘域。

若不存在有限停止階，但存在一個穩定極限意義下的不可再約域，則記為：

$$
X_\star
=
\operatorname{Residual}_{\Gamma,\mathcal Q}(X_0).
$$

其核心條件是：

$$
\mathcal R_\Gamma(X_\star)
\cong
X_\star.
$$

本文不預設 $X_\star$ 必為空集。

相反地：

$$
\boxed{
X_\star
}
$$

就是所有合法消除完成後仍然存活的不可約符號域。

---

# 13. 符號自由度

對有限符號系統，可定義相對符號自由度：

$$
\operatorname{sdf}_{\Gamma,\mathcal Q}(X)
=
\left|
X/\equiv_{\Gamma,\mathcal Q}
\right|.
$$

若 reduction 有效，期待：

$$
\operatorname{sdf}(X_{n+1})
\le
\operatorname{sdf}(X_n).
$$

嚴格消元時：

$$
\operatorname{sdf}(X_{n+1})
<
\operatorname{sdf}(X_n).
$$

因此 SECV 可被看成尋找：

$$
\boxed{
\min
\operatorname{sdf}_{\Gamma,\mathcal Q}(X)
}
$$

但前提是所有 $\mathcal Q$ 與必要不變量都被保存。

這不是單純資料壓縮；它是帶有證明義務的符號自由度降維。

---

# 14. 演算法形式

對有限問題，可以使用 worklist 形式。

初始：

$$
W_0
=
\Sigma_0.
$$

每次從 $W$ 取出一個符號 $x$，依序執行：

$$
\text{GenerateDuals}(x),
$$

$$
\text{CheckEquivalence}(x,D_j(x)),
$$

$$
\text{ValidateInvariants},
$$

$$
\text{ReduceOrResidualize}.
$$

若某個符號被改寫，則只將受其影響的依賴節點重新加入：

$$
W
\leftarrow
W
\cup
\operatorname{Dependents}(x).
$$

核心迭代可寫為：

```text
Input:
    Symbol state X
    Constraints Gamma
    Proof obligations Q
    Transform family T
    Invariants I

Freeze rule set M0

repeat:
    choose candidate x
    generate legal transforms D_j(x)

    for each candidate pair:
        test admissibility
        test equivalence or residual sufficiency
        verify invariants
        if certified:
            apply reduction
            record witness and provenance
            enqueue affected dependents

until no certified reduction remains

return residual symbolic domain X_star
```

任何沒有 witness 的縮減只屬於 heuristic，不得進入正式 proof layer。

---

# 15. 終止與循環

若存在複雜度測度：

$$
\mu(X)\in\mathbb N
$$

使每次正式 reduction 都有：

$$
\mu(X_{n+1})
<
\mu(X_n),
$$

則有限問題必然終止。

若某些合法轉換不保證嚴格下降，則必須加入狀態循環檢測：

$$
X_i\cong X_j
\quad
(i<j).
$$

一旦形成 cycle：

$$
X_i
\rightarrow
X_{i+1}
\rightarrow
\cdots
\rightarrow
X_j
\cong
X_i,
$$

該 cycle 不得被誤認為進一步證明，而應壓縮為 orbit 或 fixed-cycle object，交由更高層規則處理。

---

# 16. 合流性

不同消除順序可能產生：

$$
X
\rightarrow
Y_1,
$$

以及：

$$
X
\rightarrow
Y_2.
$$

若最終存在：

$$
Z
$$

使：

$$
Y_1
\rightarrow^\ast
Z,
$$

且：

$$
Y_2
\rightarrow^\ast
Z,
$$

則稱此 reduction 局部可合流。

若所有合法路徑最終得到同一等價類 normal form：

$$
X_\star^{(1)}
\equiv_{\Gamma,\mathcal Q}
X_\star^{(2)},
$$

則 SECV 的殘餘域具有 canonical 性。

若無法證明合流性，則輸出不能稱為唯一 canonical residual，只能稱為某一條合法 reduction path 的 residual representative。

---

# 17. Provenance：每個符號為什麼消失？

SECV 要求每次 reduction 都保留來源：

$$
\pi_k
=
(
\text{input},
\text{rule},
\text{witness},
\text{invariants},
\text{output}
).
$$

完整推演形成：

$$
\Pi
=
(\pi_1,\pi_2,\ldots,\pi_N).
$$

因此對任何被消除的符號 $x$，都可以回答：

$$
\boxed{
\text{為什麼 }x\text{ 不再需要作為獨立變量存在？}
}
$$

這使 SECV 不只可執行，也可重播、審計與形式驗證。

---

# 18. 一個最小示例

考慮：

$$
x=a+c,
$$

$$
y=b+c.
$$

若證明義務只與差值相關：

$$
Q(x,y)=x-y,
$$

則共同符號 $c$ 對 $Q$ 是冗餘的：

$$
x-y
=
(a+c)-(b+c)
=
a-b.
$$

因此：

$$
(x,y)
\longmapsto
a-b.
$$

合法性的關鍵不是「看起來可以把 $c$ 消掉」，而是已證明：

$$
Q(x,y)
=
\widehat Q(a-b).
$$

若證明義務改為：

$$
Q'(x,y)=x+y,
$$

則：

$$
x+y=a+b+2c,
$$

此時 $c$ 不能被消除。

所以同一個符號是否可消，取決於：

$$
(\Gamma,\mathcal Q),
$$

而不是取決於符號本身。

---

# 19. 方法邊界

本文特別排除以下錯誤推論。

第一，語法相似不代表可消：

$$
x\approx y
\not\Rightarrow
x\equiv_{\Gamma,\mathcal Q}y.
$$

第二，對稱出現不代表各自為零：

$$
x+(-x)=0
\not\Rightarrow
x=0.
$$

第三，兩個無限標記相同不代表可以相減：

$$
\infty-\infty
$$

本身不構成合法 SECV 操作。

第四，有限樣本全部成功不等於已證明全域：

$$
\forall x\in S_{\mathrm{finite}},
\ P(x)
$$

不能在沒有覆蓋定理時推出：

$$
\forall x\in\mathcal X,\ P(x).
$$

第五，演算法產生 residual 不代表 residual 已具有生成能力；生成種子的充分條件屬於後續論文。

---

# 20. 與既有方法的關係

SECV 與下列已有思想具有交集：

- term rewriting；
- symbolic algebra；
- constraint propagation；
- quotient construction；
- symmetry reduction；
- compiler optimization；
- theorem-prover normalization；
- graph reduction；
- abstract interpretation。

本文不主張上述概念均為新發明。

SECV 的研究重點是將它們統合到一個以：

$$
\boxed{
\text{合法域}
+
\text{相對證明義務}
+
\text{對偶生成}
+
\text{符號消除}
+
\text{殘餘域}
+
\text{可審計見證}
}
$$

為中心的統一方法，並進一步研究其有限階、無限階、生成種子與問題域再展開版本。

---

# 21. 核心命題

本文將 SECV 的母命題濃縮為：

$$
\boxed{
\text{在既定合法域與證明義務下，
計算不必求出全部變量；
它可以先證明哪些符號不再具有獨立存在的必要性。}
}
$$

其形式目標為尋找：

$$
X_\star
=
\operatorname{Residual}_{\Gamma,\mathcal Q}(X_0),
$$

使：

$$
\mathcal Q(X_0\mid\Gamma)
\equiv
\mathcal Q(X_\star\mid\Gamma),
$$

同時：

$$
\operatorname{sdf}(X_\star)
\le
\operatorname{sdf}(X_0).
$$

若達到最小不可約狀態，則：

$$
\boxed{
X_\star
}
$$

代表該問題在當前證明義務下的最小必要符號域。

---

# 22. 後續系列接口

本文只建立母方法。

後續將依序處理：

1. 符號對角性與對偶自指；
2. 符號自由度降維；
3. soundness、termination 與 confluence；
4. 生成種子；
5. 消除—生成對偶；
6. 問題域再展開與完備性；
7. 無限階對等差作為 SECV 子類；
8. 四色問題的合法配置二階壓縮；
9. NS、RH 與 symbolic runtime 的跨域壓力測試。

---

# 結論

SECV 的核心不是「消掉越多符號越好」，而是：

$$
\boxed{
\text{只消除那些已被證明不再承載獨立證明義務的符號自由度。}
}
$$

因此，一個合法 SECV 系統必須同時回答四個問題：

$$
\boxed{
\begin{aligned}
&\text{這個符號為什麼合法？}\\
&\text{它為什麼與另一符號等價、對偶或可殘差化？}\\
&\text{消除後保存了什麼？}\\
&\text{如果規則改變，哪些步驟必須重新驗證？}
\end{aligned}
}
$$

只有在這四個問題可被形式回答時，符號消除才從直覺技巧升格為可審計的證明與計算方法。

SECV 因而將問題求解的基本動作從：

$$
\boxed{
\text{求出未知量}
}
$$

擴展為：

$$
\boxed{
\text{識別自由度}
\rightarrow
\text{證明對等}
\rightarrow
\text{合法消除}
\rightarrow
\text{提取不可約殘餘域}.
}
$$

本文以此作為整個系列的形式起點。