Operator-Native RDSS：有限 hp/hhp-like Branch Quotient Checker

Configuration Triples, History Isomorphism, Hereditary Closure, and Versioned Quotient Certificates

版本： v0.11 Working Proof/Checker Draft
日期： 2026-08-10
作者：Neo.K
機構：EveMissLab／一言諾科技有限公司
定位： ON-RDSS Branch Quotient Certificate 由 bounded-signature proxy 升級為有限 configuration-relation checker
前置： ON-RDSS v0.9–v0.10

摘要

v0.10 的 Branch Quotient Safety 使用：

current observation；
history profile；
bounded future signature；

作為有限 proxy。

本版進一步改用 event-structure concurrency theory 中更標準的 configuration-triple 形式：

\boxed{ (C_1,f,C_2) }

其中：

f:C_1\cong C_2

必須保存：

event profile；
causal order；
configuration history structure。

本文在 finite prime-event-structure 子域上實作：

hp-like greatest-fixed-point checker；
hhp-like checker，額外要求 relation 對 matched subconfigurations hereditary downward closed；
ON-RDSS profile equality，把 label 之外的 type / authority / residual 一起納入 matching。

本版不宣稱已得到 general CEES / general event structure 的完整 hp/hhp solver。

1. 為什麼從 Signature Proxy 升級？

v0.10 toy criterion：

CurrentSig(C_1)=CurrentSig(C_2),

HistorySig(C_1)=HistorySig(C_2),

FutureSig_k(C_1)=FutureSig_k(C_2)

可以抓到很多反例，

但它仍可能：

因 bounded depth 漏掉遠期差異；
沒有明示保存歷史事件對應；
沒有真正以 configuration extension 做 back-and-forth；
無法表達 hereditary closure。

所以：

\boxed{ SignatureSimilarity \neq HistoryPreservingBisimulation. }

2. 有限 Prime Event Structure 子域

本 checker 暫時使用：

\boxed{ P = (E,\le,\#,\Lambda). }

其中：

$E$ ：有限事件；
$\le$ ：causal partial order；
$\#$ ：conflict；
$\Lambda$ ：ON-RDSS event profile。

Configuration：

C\subseteq E

需：

conflict free；
downward closed。

3. ON-RDSS Event Profile

傳統 hp/hhp matching 常首先要求 label-preserving。

本版將 label 擴充為 profile：

\boxed{ \Lambda(e) = ( Label, Type, Authority, Residual ). }

因此兩事件只有：

\Lambda(e_1)=\Lambda(e_2)

才可直接匹配。

這是 ON-RDSS-specific strengthening，不是 hp/hhp 的普遍定義。

4. History Isomorphism

給：

C_1\in Conf(P_1), \qquad C_2\in Conf(P_2).

映射：

\boxed{ f:C_1\to C_2 }

必須為 bijection，並滿足：

Profile preservation

\Lambda_1(e) = \Lambda_2(f(e)).

Causal-order preservation and reflection

\boxed{ e\le_{C_1}e' \iff f(e)\le_{C_2}f(e'). }

因此：

(C_1,f,C_2)

保存的是 configuration history 的 labeled poset structure。

5. Posetal Product State Space

定義候選 triple space：

\boxed{ \mathcal T(P_1,P_2) = \{ (C_1,f,C_2) \mid f:C_1\cong C_2 \}. }

有限 checker 先枚舉所有合法 triples。

6. Event Extension

若：

C\xrightarrow{e}C'

表示：

C'=C\cup\{e\}

且 $C'$ 仍是 configuration。

對 triple：

(C_1,f,C_2)

若：

C_1\xrightarrow{e_1}C_1',

希望找到：

C_2\xrightarrow{e_2}C_2'

使：

\Lambda_1(e_1)=\Lambda_2(e_2)

並延伸：

\boxed{ f' = f[e_1\mapsto e_2]. }

要求：

(C_1',f',C_2')

仍在 relation。

反向亦然。

7. hp-like Greatest Fixed Point

令初始：

R_0 = \mathcal T(P_1,P_2).

反覆刪除無法滿足 forward/back extension matching 的 triples：

R_0 \supseteq R_1 \supseteq R_2 \supseteq\cdots

直到固定：

\boxed{ R_{hp}^{\ast}. }

若：

(C_1,f,C_2)\in R_{hp}^{\ast},

本 checker 稱它們 hp-related。

8. hhp-like Hereditary Closure

在 hp 條件外，再要求：

對：

(C_1,f,C_2)\in R

以及任意 matched subconfiguration：

D_1\subseteq C_1,

令：

D_2=f(D_1),

以及 restricted map：

f|_{D_1}.

只要 $D_1,D_2$ 都是 configurations，就要求：

\boxed{ (D_1,f|_{D_1},D_2)\in R. }

因此 relation 對歷史刪除保持 hereditary closure。

9. hhp-like Greatest Fixed Point

同樣從全部 history-isomorphic triples 開始，

同時反覆施加：

forward matching；
backward matching；
hereditary subconfiguration closure。

固定點：

\boxed{ R_{hhp}^{\ast}. }

10. BQCert 的新核心

v0.10：

BQCert = Observation + HistoryProxy + FutureProxy + Authority + Residual + Version.

v0.11 改成：

\boxed{ BQCert_{Q,v}^{hhp} = ( TripleRelation, HistoryIso, BackForthWitness, HereditaryWitness, ONProfileScope, Version ). }

工程上仍可額外帶：

authority review；
residual review；
scope；
evidence refs。

11. Branch Quotient Rule

如果存在：

f

使：

\boxed{ (C_1,f,C_2) \in R_{hhp}^{\ast} }

並且 ON-RDSS 的 version/scope certificate 成立，

才允許：

\boxed{ [C_1]_{Q,v} = [C_2]_{Q,v}. }

12. hp 與 hhp 的角色差異

hp 要求：

當前歷史 correspondence 可被未來事件 forward/back 延伸。

hhp 再要求：

這個 correspondence 往回限制到可匹配的過去 configurations 時仍保持 relation。

因此 hhp 對：

\boxed{ \text{history-preserving folding} }

更適合作為保守 reference。

這不表示 ON-RDSS 永遠必須用最強 hhp；

可依 domain 提供：

\boxed{ QuotientMode \in \{ Obs, Future, HP, HHP \}. }

13. Quotient Mode

Obs

只比較 current projection。

最便宜、最危險。

Future

比較 bounded / symbolic future capability。

HP

保留 configuration history isomorphism 與 forward/back extension。

HHP

再加入 hereditary historical restriction。

治理關鍵 parent state 預設應偏向 HHP 或更強 ON-specific profile equivalence。

14. ON-specific Strengthening

即使兩事件普通 label 相同：

label(e_1)=label(e_2),

若：

Auth(e_1)\neq Auth(e_2),

則 ON profile 不同。

同理：

Residual(e_1)\neq Residual(e_2)

也阻止直接匹配。

所以：

\boxed{ BehaviouralLabelEquality }

與：

\boxed{ GovernedProfileEquality }

分離。

15. Experiment A — Symmetric Branches

結構：

a\to r_a\to f_a,

b\to r_b\to f_b

且兩條 branch profiles 對稱。

比較：

C_A=\{a,r_a\},

C_B=\{b,r_b\}.

Checker 找到 history map：

\boxed{ f(a)=b, \qquad f(r_a)=r_b. }

結果：

\boxed{ HP=true, }

\boxed{ HHP=true. }

16. Experiment B — Same Present, Different Future Profile

保留：

C_A,C_B

當前 history profile 對稱，

但把：

f_b

改成不同：

label；
authority。

Checker：

\boxed{ HP=false, }

\boxed{ HHP=false. }

因為 branch A 的 future extension 找不到 profile-preserving match。

17. Experiment C — Meta Breaks Equivalence

v1：

C_A \sim C_B.

v2 只對 branch A 新增：

r_a\to x_a

且：

Auth(x_a)=special.

結果：

\boxed{ HP_{v2}(C_A,C_B)=false, }

\boxed{ HHP_{v2}(C_A,C_B)=false. }

這再次驗證：

\boxed{ BQCert^v }

必須版本化。

18. Experiment D — Structure Renaming

兩個 event structures：

x\to y

與：

u\to v

profiles 分別對應：

x\leftrightarrow u,

y\leftrightarrow v.

Checker 從空 configurations 找到：

\boxed{ HP=true, \qquad HHP=true. }

表示 event identifier 不必相同，只要 history structure / profile 可對應。

19. Checker 實作方式

有限演算法：

枚舉 configurations；
對等 cardinality configurations 枚舉 bijections；
保留 profile + causal-poset isomorphisms；
得到所有 triple candidates；
greatest-fixed-point elimination 求 hp；
再加入 hereditary subconfiguration elimination 求 hhp。

因此是 exponential / combinatorial toy checker，不是大型 Runtime 解法。

20. 複雜度警告

Configuration 數量本身可能指數成長，

配置間 bijection 還有 factorial factor。

所以：

\boxed{ \text{exact HHP checking} }

不適合作為所有大型 RDSS parent-state comparison 的即時計算。

工程上需要：

bounded scope；
local quotient candidates；
signatures / invariants 預篩；
incremental certificates；
cached fold registry。

21. Two-Tier Quotient Checking

建議：

Tier 1 — Cheap Candidate Filter

使用：

current profile；
boundary contract；
bounded future signature；
authority/residual hash。

只有通過才進 Tier 2。

Tier 2 — Exact / Strong Checker

對小型局部 event substructure 執行 hp/hhp-like checker。

所以：

\boxed{ FastIndex \neq StrongQuotientAuthority. }

22. BQCert 作為可重建 Authority

真正 parent-state merge authority：

\boxed{ BQCert }

可包含：

candidate pair；
event semantics version；
hp/hhp mode；
relation triples；
history maps；
proof/checker version；
scope；
profile equality regime。

快速：

QuotientIndex

可以由它生成。

23. Meta Revalidation

若：

\mathfrak E_v \to \mathfrak E_{v+1},

所有受影響：

BQCert^v

標記：

\boxed{ Stale. }

重新 checker：

Recheck_{v+1}(C_1,C_2).

若失敗：

\boxed{ SplitRequired. }

24. State Merge / Split 現在有更正式的依據

State merge：

\boxed{ C_1 \stackrel{HHP/ON}{\sim} C_2 \Rightarrow MergeCandidate. }

State split：

\boxed{ BQCert^v \text{ valid} \land BQCert^{v+1} \text{ invalid} \Rightarrow SplitRequired. }

25. Folding Map Verification

事件 folding：

F:E\to\widehat E

可以轉化成：

folding 前後 event structures 是否由 hp/hhp-like relation 連接？

因此 bounded checker 可成為 fold regression tool。

但完整 event-structure minimisation 仍應優先利用既有 folding 理論，而不是 ON-RDSS 自行重建全部 minimisation mathematics。

26. hhp 與 General CEES 的缺口

本 checker 是 finite PES。

v0.9 General CEES：

(E,Con,\vdash,\ldots)

允許：

disjunctive enabling；
general consistency；
dynamic causality。

其 history poset 不一定像 prime event structure 一樣由一個固定全域 causal order直接取得。

因此要做 general CEES 的 hhp，需要先明確定義：

\boxed{ HistoryOrder(C,\pi) }

或 configuration-specific causal witness。

27. General CEES 下一版候選

一個 configuration 可能需要攜帶 proving sequence / enabling witness：

\boxed{ \widehat C = ( C, \pi, \le_\pi ). }

然後 hp/hhp 比較的不是裸：

C

而是：

\widehat C.

這才能處理同一 event set 具有不同 causal history 的系統。

28. Causal Ambiguity

若同一 configuration：

C

可由不同 enabling choices 得到不同 causal explanations，

則：

\boxed{ SetOfEvents }

本身不足以代表 history。

ON-RDSS 必須保留：

\boxed{ Configuration + EnablingWitness. }

這和 v0.9 disjunctive causation 的問題直接相連。

29. 對 Parent State 定義的再精化

v0.10：

State = VersionedHistoryPreservingQuotient(Configuration).

v0.11 更精確：

\boxed{ State_{parent}^{Q,v} = Quotient( \text{History-Decorated Configurations} \mid BQCert_{Q,v} ). }

在 prime 子域，history decoration 可由 causal configuration poset 隱式給出。

在 general CEES，可能需要 explicit enabling witness。

30. 第一個正式 BQCert Verification Rule

Prime finite 子域暫定：

\frac{ (C_1,f,C_2)\in R_{hhp}^{\ast} \qquad Version(C_1)=Version(C_2)=v \qquad Scope(f)\subseteq Q }{ \boxed{ BQCert_{Q,v}(C_1,C_2)\downarrow } }

實際 ON-RDSS 還要加入：

certificate checker version；
authority regime；
residual policy。

31. No Silent Merge

即使 checker 找到：

HHP(C_1,C_2),

也不代表 Runtime 必須自動 merge。

應區分：

\boxed{ MergeSafe }

與：

\boxed{ MergeAuthorized. }

前者是形式判定，

後者是治理決策。

32. No Silent Split

同樣：

BQCert

失效表示：

SplitRequired.

不表示 Runtime 必須立即破壞所有 live references。

還需要：

migration；
aliases；
versioned routing；
graceful split。

33. hp/hhp Checker 與 Certificate

Checker 結果不是數學證明助理證書。

第一代只能產生：

\boxed{ FiniteModelCheckCertificate. }

其中包括：

model hash；
relation size；
matching maps；
checker version；
exact finite scope。

未來若 Lean / Coq formalize，再提升證書級別。

34. 有限結果

本版實測：

Symmetric branch

HP=true, \qquad HHP=true.

Different future / authority

HP=false, \qquad HHP=false.

Meta-added one-sided future

HP=false, \qquad HHP=false.

Isomorphic renamed structures

HP=true, \qquad HHP=true.

35. 本輪沒有找到 hp / hhp 分離案例

本輪幾個有限模型中：

R_{hp}^{\ast} = R_{hhp}^{\ast}

在測試案例上恰好相同。

這不代表兩種 equivalence 一般相同。

它只表示目前 toy cases 沒有命中需要 hereditary condition 才能區分的結構。

後續應特別構造或搜尋：

\boxed{ HP=true, \qquad HHP=false }

的最小反例，作為 checker regression。

36. 下一步

找 hp / hhp 最小分離模型；
把 checker 從 PES 推到 stable / general configuration structures；
加入 proving-sequence / enabling witness；
定義 hp/hhp over dynamic-version snapshots；
加入 fold-map validator；
BQCert 生成完整 witness package；
接 StateSplit / StateMerge Runtime；
對大型模型加入 quotient candidate index；
研究 exact checker 的 complexity boundary；
Lean formalize prime finite core。

37. 暫定結論

ON-RDSS 的 Branch Quotient 已經從：

\boxed{ \text{看起來一樣} }

逐步推進到：

\boxed{ \text{bounded future/profile same} }

再推進到：

\boxed{ \text{configuration-history isomorphism} + \text{forward/back matching} + \text{hereditary closure}. }

因此 parent state 越來越不應被理解成「同值」。

更合理的是：

\boxed{ State_{parent} = \text{Governed Quotient Class under a Versioned History-Preserving Behavioural Relation}. }

而 ON-RDSS 在既有 hp/hhp/folding 理論上真正新增的責任是：

\boxed{ Authority + Residual + Certificate + Version + MetaRevalidation. }

ON_RDSS_HP_HHP_Branch_Quotient_Checker_v0.11