构造替换、身份与持续编辑保持

研究总览 · 2026-09-20

本篇解决架构 §22.6留下的更强保证：为什么核心替换构造之后，设计含义、引用、工艺约束及后续编辑仍然成立。交付的是条件明确的数学规则和待实现契约，不把当前 OCCT 操作的成功当作已完成该证明。

1. 替换权限来自设计语义

设 d 为源设计，u 为其设计控制，A、B 为实现同一设计的两种构造。q(A(d))=q(B(d))=d 只说明能读回源设计；两种实现都满足若干尺寸，也不足以证明可互换。

编译器可以自动替换的准确条件是：在源设计声明的参数域 U、观察 O、编辑语言 E 及数值交付规则下，两种构造具有规定的语义关系。O 包含产品和下游模块真正依赖的事实，不只是当前截图；E 包含允许的源编辑规则，不是人工列举几次操作。

必须观察的事实	替换时保持什么
几何	指定实体集合、尺寸/方向和声明的几何误差；不只比较包围箱或体积
拓扑	实体/壳/连通分量、孔与界面等设计拓扑；已明确观察的原生面/边数量另行保持
稳定身份	部件、occurrence、设计特征与角色；每个持久引用的集合、方向、基数和演化策略
关系和选择	源要求、开放量、目标与已选分支的意义；同样合格但有设计差异的另一个解不能冒充等价优化
工艺	工序、中间形状、基准、材料区域及制造要求中已指定的含义
行为与分析	端口、载荷区域、材料/边界和输出到原对象的绑定；几何相同不自动保持离散网格或分析轨迹
编辑	同一源编辑的作用域、前提、结果关系与明确拒绝；不得让客户端改写施工树才能继续操作

观察从 AMIR 要求、SemanticRef、显式构造锁定及已注册下游模块的效果签名提取。存在未声明依赖、外部副作用或无法判断的观察时，不能认为它“不重要”。只能选有完整前提的规则，或保留未优化构造。把用户明确指定的工序改成另一种工艺，属于设计编辑，不属于编译优化。

这借鉴验证编译器的可观察语义与逐变换证明方法。CompCert 的语义保持说明区分行为细化与完全相同；本篇给 CAD 自己的保持条件，没有继承 CompCert 对 C 编译的证明，也不引入该编译器依赖。

2. 对所有合法未来编辑的充分条件

令状态 s=(d,u,r) 包含设计、控制和实现；s —e→ s' 表示执行一个具有明确语义的源编辑。内部建图/布尔调用等步骤不在用户观察中，提交结果、要求状态及必须可见的失败属于观察。对两个实现状态定义关系 R，要求：

1. **初始对应：**同一源设计和选择前提下，A、B 的初始状态满足 R。
2. 观察保持：R(sA,sB) 蕴含 O(sA) ≃ O(sB)；拓扑/身份/工艺为精确的对应，连续量按明确误差关系比较。
3. **编辑步保持：**对于任一 e∈E，只要状态在 U 且该编辑的前提成立，A 的每个允许后继都有 B 的对应后继，后继仍满足 R。若承诺等价而非单向细化，反向也成立。
4. **定义域和终止：**声称能成功执行的步骤须有终止与构造/检查有效性前提，内部步骤须有限或有良基下降量，不能用无限内部运行冒充对应；源未定义、引用歧义或域外的编辑不能被偷换成另一个成功编辑。预算耗尽不是语义上的设计无解。若还承诺同一资源预算内成功，须另证成本界，不能由理想几何等价推出。

**定理 S：**上述四条成立时，对任意有限合法编辑串 e1…ek，最终观察仍对应，并且每步都保留相同的设计编辑含义。

证明：长度 0 由初始对应；假设长度 k 的对应成立，对下一编辑使用第 3 条得到 R 的新状态，再由第 2 条得到新观察对应。反向条件保证不是只保留其中一部分原有设计行为。该归纳对所有满足前提的有限编辑串成立，不需要枚举产品或操作序列。

这里证明的是所定义语义与实现前提下的保持。浮点布尔失败、检查器缺口或资源不足，不能从形式语义中自动消失。产品应区分 family-equivalent、candidate-conformant 与 unknown：一次候选检查通过只能得到第二类；原生运算对整个 U 的可用性未证时，不宣称整个 U 内未来操作必成功。

3. 将全序列义务缩成可检查的参数族规则

常见参数编辑不必直接比较两棵任意施工程序。若 A、B 都从同一源 d 和控制 u 前向构造，且对所有 u∈U 已证明：

[ O(A(d,u))\simeq O(B(d,u)),\qquad resolve_A(d,u)\leftrightarrow resolve_B(d,u), ]

源编辑的解释器又相同，则可取 R 为“同一 d/u、对应角色与观察”。每次编辑仍在 U 时，参数族等价立即给出第 2 节的后继对应。无需为每次尺寸修改重新比较所有操作历史。

U 由符号谓词定义，例如正尺寸、分离裕量、无退化、角色基数和适用材料/工况；不得定义成“已经试过成功的点”。证明规则可携带对整个参数盒/域的界，也可以在每次编辑时核验该编辑是否属于已证明的 U。后者是在检查定理前提，不是用逐点测试建立定理。

若一次编辑离开 U，旧替换证明立刻失效。系统仍按源语义编译该新设计，不能继续套用旧替换、冻结本应变化的量或扩大 U。源码构造规则仍在同一编译器和同一几何底座中，不为此保留第二份库或旧版产品执行器。

若 A/B 只能保证各自到同一理想设计的误差 εA/εB，则两者距离最多 εA+εB，不能擅称 ε。连续多次替换都重新绑定同一源理想模型和总误差预算，禁止把上一次近似结果当成新精确源，使误差无界累积。所有硬要求仍按数值交付规约核验。

4. 一个完整替换族：顺序切孔与批量切孔

下面证明一个任意有限孔数的构造规则，而不是报告若干成功样品。定义板体 B=[0,W]×[0,H]×[0,t]，n 个具有稳定设计 ID 的贯穿圆孔，中心 ci=(xi,yi)，半径 ri。固定分离裕量 δ>0，域 U 满足：

[ W,H,t>0,\quad r_i>0,\quad r_i+\delta\le x_i\le W-r_i-\delta,\quad r_i+\delta\le y_i\le H-r_i-\delta, ] [ |c_i-c_j|\ge r_i+r_j+\delta\quad(i\ne j). ]

工具圆柱 Ci 沿 z 轴延伸到 [-a,t+a]，a>0，避免只在顶底面相切。A 按任意声明的计算次序逐孔 regularized cut；B 对相同工具集合一次求差。这里的“次序”只是计算实现，若用户把中间工序列为要求，则本规则不适用。

设 Di 是孔的平面闭圆盘。严格分离及侧边裕量保证两种理想正则化布尔结果均为：

[ S=\left([0,W]\times[0,H]\setminus\bigcup_i \operatorname{int}D_i\right)\times[0,t]. ]

理由：任一点留下，当且仅当它在板体内且不在任何孔的内部；依次排除和同时排除给出相同集合。正则化只恢复实体边界，当前严格分离前提排除了会改变角色归属的孔相交/贴边退化。几何集合相同，因此质量均匀时体积与质心等集合积分一致；例如 V=t(WH−πΣri²)。不必逐个 n 重新验证集合恒等式。

角色映射也可直接构造：

[ wall(i)={(x,y,z):|(x,y)-c_i|=r_i,\ 0\le z\le t}. ]

topRim(i)、bottomRim(i) 分别是 wall(i) 与 z=t、z=0 的交集，方向由同一源坐标和实体外法向约定决定。外壁按矩形四条边定位。严格间距保证 wall(i) 与 wall(j) 不混同，设计 ID i 始终对应自己的角色；身份不靠内核 face 数组位置。

因此，在此域内，几何实体、孔连接结构、上述角色、体积/质量积分及依赖这些角色的要求均保持。只修改 W/H/t/ci/ri 且仍满足 U 的编辑共享相同角色公式，满足第 3 节，故所有有限合法参数编辑串保持这些观察。这里的 E 不含增加/删除孔；要支持它们，需为稳定 ID 的 creation/delete 另定义编辑步，再用本定理处理两端的有限索引集，并核对被删引用的处置，不能假装旧引用仍然存在。

**没有从集合恒等式推出的内容：**两次 OCCT 结果的 TopoDS 面/边数量、seam 切分、B-Rep 字节、history 记录和中间切割体可能不同。若任何下游明确依赖它们，该观察必须额外证明；没有证明就不能采用此规则。孔重叠、贴边、盲孔、相切、零厚结果不在本规则域内，不使用本证明替它们担保。

这是一个已完成的数学替换规则。其产品执行条件仍是：锁定后端在声明容差下实际生成合格实体，并成功建立以下角色证据。理想集合定理不能替代真实 B-Rep 的检查，不能据此编造本轮已经运行批量 cut 的性能或正确性结果。

5. 几何身份证据：角色稳定不等于原生面稳定

对一个角色，适配器返回覆盖它的面/边集合，证明每个成员位于目标支持曲面/曲线、边界覆盖完整、方向与邻接符合要求。只有“每个点都在圆柱上”不足以证明覆盖整个孔壁，也不能排除漏片或重复片。基数属于作者契约：exactly-one-face 不能被改成“任意多面集合”来让替换通过。

OCCT BuilderAlgo的 Modified/Generated/IsDeleted 与 history 可提供具体演化来源；OCAF 命名维护拓扑演化描述。它们不独自证明两种独立构造在所有未来编辑上相同，也不证明工艺要求。

因此复用当前 SemanticRef 契约与解析器：scope、kind、lineage、topology、predicate、cardinality、ordering 共同核验。保留 split/merge/delete/kind-change 策略，不允许 heuristic 命中进入权威验证，也不取第一个候选。

本文并不另造命名系统。若角色需要多个原生 patch，而源引用要求恰一个原生面，则当前规则拒绝替换；只有源引用本来允许对应集合、且现有解析契约对该演化可发布时才继续。不能因两个集合的面积和接近就认定身份保持。

还须遵守现有形状 history 边界：祖先关系不等于唯一身份，几何相似不能给另一条构造伪造祖先。新构造保留真实 history；跨构造角色对应是另有证明的映射，不覆盖原始 authoring witness。当前单面 lineage 引用拒绝分裂/合并，不能为了优化绕过。已有孔阵列已采用批量 cut，本数学例子不是一项已实测的新增加速。

工艺链独立按源定义保留。计算用的切割调用可以被批处理，但加工次序、装夹基准、刀具、材料与中间状态若属于设计要求，它们不随几何优化重排。以孔壁作为载荷面的分析还必须保持物理区域映射；更换网格/积分方法属于工程有效性规约处理的另一项变换。

6. 规则与见证的最小数据契约

规则属于现有 Operation Module/编译器锁定定义，见证属于候选求值资源，不创建第二套规则目录或独立设计文档。下列是待实现的数据形状；所有 hash 引用真实内容与版本，存在一个字符串不等于证明已成立。

type Id = string;
type Hash = string;
type SourceRef = { node: Id; pointer: string };
type ReplacementRule = {
  ruleId: Id;
  sourceOperationContracts: Hash[];
  targetOperationContracts: Hash[];
  sourcePatternDefinition: Hash;
  targetConstructionDefinition: Hash;
  parameterDomainDefinition: Hash;
  observationDefinition: Hash;
  editGrammarDefinition: Hash;
  semanticProof: Hash;
  roleMappingDefinition: Hash;
  numericalAssuranceRequired: "exact" | "enclosed" | "native-checked";
};
type ReplacementEvidence = {
  ruleHash: Hash; sourceModelHash: Hash; inputClosureHash: Hash; realizationHash: Hash;
  candidateId: Id;
  sourceContextHash: Hash; targetContextHash: Hash;
  sourceRecipeHash: Hash; targetRecipeHash: Hash;
  currentDomainCheck: Hash;
  observationClosure: SourceRef[];
  roleResolutionEvidence: Hash[];
  geometryCheck: Hash;
  scope: "family-equivalent" | "candidate-conformant";
  result: "pass" | "fail" | "unknown";
};

ruleHash 由不可变 ReplacementRule 内容计算，作为外层资源身份及见证引用，不写入它自己的哈希输入。parameterDomainDefinition、observationDefinition 和 editGrammarDefinition 使用同一已登记的类型化谓词/编辑规则，不能是自由文本声称“适用一切”。闭合定义须给出匹配方式、作用域、guard、输出绑定和不可适用原因。注册规则时验证数学推导；每次应用只绑定证据与核对前提，不再寻找一个任意程序等价证明。

semanticProof 是规则层的数学依据；其检查方式和可信基础必须明确。当前为人工可审查推导，不声称已经由证明助理机械核验。工程 native-checked 可以满足已声明的交付策略，但不能把程序提升为全域的形式验证实现；scope 与证据等级必须同时展示。

Realization 保存选定构造、数值和规则身份，不包含随后绑定它的完整检查结果；ReplacementEvidence 作为该次 validation 的资源单独引用，禁止经 geometryCheck/roleResolutionEvidence 间接形成 Realization 的哈希自环。先冻结 Realization，再生成绑定该内容的检查和最终 validation，修订在最后关联这些资源。见证不含自身 hash 或尚未产生的最终 revisionId；源模型不反向引用派生 hash。

现有 SemanticRef 完整 context 以修订/求值/图/manifest 标识。P1/P4 的当前契约调整必须让候选检查绑定真实 candidate 身份、realizationHash 和求值上下文，提交后才关联最终修订；不得填虚构 revisionId 或回写旧见证。命名算法身份、源/目标上下文和全部证据须一致，不能借此偷偷引入跨算法版本迁移。历史重放用封存构造，不重新选择“现在看来更快”的另一个实现。

candidateId 指实际发起替换的候选；两个 contextHash 指向采用同一扩展 SemanticRef 契约的不可变上下文资源，分别包含源和目标的真实模型/构造/求值/manifest 及命名算法身份。对应源若为已提交状态，引用其真实修订；对应源若为候选求值，使用候选上下文。检查器核对 context、recipe、realization 和每份角色证据的绑定一致，不仅比较输入值。历史重放读取原候选证据和提交关联，不把 candidateId 改成新的修订 ID。

7. 实际决策算法与有限职责

1. 从源节点和所有消费者收集观察闭包。下游未提供可靠效果签名时拒绝隐式隐藏该依赖。
2. 匹配一个已登记的变换规则，绑定参数、目标角色、后端/模块身份；不开展任意施工程序等价搜索。
3. 核验 U、编辑语义、工艺锁定、源引用演化策略及误差预算。域外或未知时保留按源语义生成的正常构造；不放宽要求。
4. 对通过前提的候选按既有成本模型选择构造，再实际生成。与旧实现相似的截图或 solver success 不是验收依据。
5. 核验实际实体、角色覆盖、全部源要求与分析绑定。失败或未知不移动 head；不为了通过而改 SemanticRef 基数或容差。
6. 封存选定构造和规则依据。源修改使 guard 或观察闭包改变时失效对应见证；撤销/重做读取原封存结果，不换解。

可优先注册的确定规则只有：保留求值顺序和数值语义的已知量代入；有完整恢复映射的精确仿射参数化；满足 §4 全部前提的几何批处理。浮点重结合、任意圆角/布尔交换、任意曲面近似或工艺重排不自动获得权限。

由此，解决“任意替换无法保证”的方法是让替换权限可推导：核心能自动选择的，是处于已证明语义关系内的实现；设计自由度和物理工艺不能被吞进编译细节。证明一次有限规则、每次核验前提，覆盖任意有限合法参数编辑串，同时把实际数值交付义务保留在共同验收链中。

8. 当前源码的首个可闭合规则：精确输入专门化

源码核对位置为 Web 共同编译器 relation-compiler.ts、relation-port-binding.ts 及 relation-joint-execution.ts。当前 bindExactRelationPort 已把规范单位有理端口值编码为既有字面量/除法表达式，改写该输入的表达式读取和构造/输出配方，再删除私有视图中的输入；源 AMIR PortRef 不变。knownRelationOutput 只从源已知值提前绑定，联合路径则在完整候选选择后绑定。这两种来源不能混作“已经证明该设计值唯一”。

8.1 精确变换及观察边界

给定合法源定义 D、有类型输入 p:T、规范值 q=n/d（d>0），令 D[p:=q] 表示无捕获地替换每个 p 读取。对于任意其余变量赋值 x，若环境将 p 绑定为 q，则 D 在该环境下与 D[p:=q] 的表达式值、定义域、law/when、构造参数及输出配方相同。证明按既有表达式 DAG 与 RecipeValue 的结构归纳：输入叶由前提相等；非输入叶不变；父操作及其求值顺序不变，故值和定义域保持；select 使用相同条件与有效分支，不能利用代数消去抹掉分母非零等前提。构造模块、步骤 ID、guard、输出角色及操作顺序均不变，因此该规则不需要跨两种几何算法发明 history 对应。它也不把候选合格性升级为整个参数域的几何成功保证。

有理数保持为确切 n/d；绝对温度用 0 K 加有理温差，不将绝对温度当普通可除标量。Int/Count 必须保持整数与非负细化。输入外部声明的单位已在源求值时规范化，不能直接将任意外部十进制当作规范值。后续构造叶 binary64 交付仍使用现有独立舍入证据，不能把本规则的精确性转嫁到几何内核。

8.2 前提必须绑定真实来源

前提	当前来源	封存与核验义务
q 的数值、类型与规范单位	Core 已知/候选表达式结果，生产者 exactOutputs	引用该生产者源/输出及对应已知或候选身份，不能仅保存 n/d
代入覆盖全部读取	bindExactRelationPort 与 replaceInputRecipes	覆盖 expression input、构造输入、嵌套 list/select 和输出配方；模板先展开，捕获不形成另一个读取通道
未改变源与设计选择	原源文档与私有 boundNode 分离	源输入、替换前后私有上下文身份、规则身份；候选绑定只能声称“给定此候选”的条件等价
恢复没有重新设计	现有 saved variables/exactOutputs → 同一绑定、核验、lowering → 整块哈希比较	重算本次绑定的前提，不能只信保存的规则名；必须与既有 Realization 验证一起完成
持续编辑	每次从当前源和当前绑定重新编译	旧 q 不得穿过变更继续生效；同一源编辑解释器与规则归纳承担保持性

当前接线状态（2026-09-21 核对）：同一 bindExactRelationPort 已完成读取位置收集、私有节点代入和 inputSpecializations 记录，包含源绑定、类型/规范单位、精确值、表达式/配方覆盖、source-known/selected-candidate 分类及前后节点哈希。relation-lowering 将记录封存到 RelationRealizationBlock；relation-materialization 恢复时重新准备、代入、lowering，并比较整块 blockHash，联合候选路径另核对生产者 exactOutputs。公开读取直接引用同一封存字段。Web 的见证类型现直接引用生成契约，不维护第二份字段定义。

这些代码兑现的是 §8.1 的条件精确代入，不是跨几何算法的完整 ReplacementEvidence。不能再将此项记录与恢复写成“尚未封存”，也不能凭它宣布 P2 完成：§4 的几何角色对应、观察闭包、工艺与编辑限制，及 §6 绑定实际构造检查的替换见证仍须按正式要求实施。后续不重复创建代入台账、规则目录或数值算术，不假造 semanticProof/geometryCheck 哈希。

8.3 几何替换的实际阻断条件

列表组合的引用投影。 AMIR 输入值包含有限 list；如果选择器叶满足原来源、范围和定义哈希前提，则对 list 逐元素应用同一投影，并保持成员顺序、层级和其他叶不变，可由结构归纳得到与叶投影相同的引用保持性质。列表容器不构成新的几何替换规则，也不允许改变基数或 split/merge 策略。当前 projectRelationSemanticReferences 原先只检查顶层输入，现使用可取消的显式栈遍历 list；面和边选择器继续调用原检查及定义生成函数。本改动不扩大任何操作模块所接受的参数类型。2026-09-21 直接调用实际编译投影确认嵌套选择器与顶层选择器生成同一目标定义、源不变、嵌套的错误来源哈希仍拒绝；类型与 lint 通过。该检查只覆盖列表组合接线，不宣称几何替换的其他前提已完成。

§4 的批量 cut 已存在于现有孔阵列实现；不增加一个等价批量入口，也不将既有批量执行报告成新增优化。启用顺序/批量两种构造间的自动替换前，仍需从实际消费者提取完整观察闭包，并以现有 SemanticRef 规则证明孔壁/孔缘的覆盖、方向、基数及工艺限制。当前单面 lineage 对 split/merge 的拒绝不能绕过。在这些前提未能提供确定证据时，沿用源构造是本规则的规定行为；这不是永久删掉 P2 的替换义务。

8.4 精确代入记录的当前接线

共同 bindExactRelationPort 已改为先检查输入存在、类型/整数细化及模板展开阶段，收集所有 expression 读取与嵌套 list/select/output 配方路径，再计算新增表达式与预算；通过后才修改私有节点。符号端口绑定复用同一配方遍历，不保留另一份遍历实现。记录包含条件规则名 exact-input-specialization、input/type/规范 unit、精确 n/d、原 sourceBinding、替换表达式 ID 与全部配方 Pointer、生成根 ID，以及替换前后的私有节点哈希。bindingKind 明确区分 source-known 与 selected-candidate；后者只说明给定该候选的条件专门化，不声称源值唯一。

PreparedRelationNode 沿源已知绑定和联合候选重绑定累积这些记录；当前 relation block 必需 inputSpecializations 保存记录，无代入为 []，不兼容缺失该字段的旧未发布块。整个块恢复仍从源及已封存候选重新计算代入、重做 lowering 并比较哈希，记录不能代替该校验。此记录绑定的是具体精确代入步骤；它不是 §6 所列几何替换的完整 ReplacementEvidence，也不是跨构造角色覆盖证明。规则仍依赖 §8.1 的可审查推导、锁定编译器和实际源/候选核验；没有编造独立 semanticProof 或 geometryCheck 资源。

实际接线核验已完成两个不同绑定前提：源无开放量时的 source-known，以及由完整联合候选确定的 selected-candidate。均以 1/3 m 跨节点，覆盖 expression input、嵌套 select 两分支及直接输出配方，禁止 Worker 后恢复保持实现根；删除覆盖清单的一项并重新封存仍被整块重建拒绝。核验还定位并修复了遍历顺序问题：无环端口依赖现在按生产者优先的拓扑队列准备，循环及其残余保留原联合路径，不靠节点 ID 或已有数组顺序决定一个纯已知输入是否进入求解。本项核验结束，结果不外推为全套几何替换证明。

原生发现/读取已通过公共结果 Schema 引用同一 inputSpecializations 字段，并由同一 SDK model.read 暴露。使用既有 select 路径 evaluation/realization/relations（或更深路径）和 revisionId/分页，无需读取实现源码或增加查询执行器。实际禁止 Worker 的历史重开后，按修订读取的精确分数、覆盖路径及前后上下文哈希与封存记录一致；别名投影只影响原节点标识的显示，不改变内容哈希或数值语义。

8.5 节点消去的语义扩展前提

非语义扩展的一致性。 Core 的 semantic_extensions 只把显式 semantic:true 的扩展纳入模型身份；投影也必须采用同一分界。否则给普通注释增加一个名为 producerNodeId 的数据字段，就会在 modelHash 不变时新增执行拒绝条件。当前保留节点和 Body 的扩展检查已改为仅扫描显式语义 envelope；普通扩展原样保留，不参与来源对应。typed 常量及已声明语义引用的检查未放宽。2026-09-21 实际构造投影确认非语义 Body 扩展中的 producerNodeId/port 数据不改变执行模型身份、内容完整保留；未经支持的 semantic:true 声明仍拒绝。类型及 lint 通过。此项不证明任意 opaque 常量的观察闭包已完成。

若执行投影消去源关系节点 r，则每个声明 semantic:true 的扩展都必须有保持含义的转换；不能仅因投影后的文档合法，就推断被消去的观察仍成立。反例是源上附加一个工艺或物理区域要求，删除整个节点后该要求不再参与最终文档检查。因此节点消去的局部前提是：源语义命名空间集合包含于本转换实际处理的命名空间集合。它是必要条件，不是完整观察等价的充分条件。

现有 projectRelationSemanticReferences 在任何目标扩展写入之前检查全部将被消去的关系节点，当前只接受已实现转换的 exact-lineage 命名空间；其他 semantic:true 扩展以 RELATION_SEMANTIC_EXTENSION_UNSUPPORTED 和源 Pointer 拒绝。按现有 AMIR canonical/projection.rs 规则，未声明 semantic:true 的扩展不构成语义观察，不新增更严的声明协议。已支持的 lineage 仍走原定义哈希、scope、基数及演化策略检查。

Core 当前本身拒绝未知语义命名空间，故不声称发现了正常源准入可绕过的已复现漏洞。这一前提防止 Core 支持域扩大后，旧关系转换静默丢弃新语义；Core 准入与转换保持承担不同义务。Chrome 执行实际投影函数已确认语义扩展在目标写入前拒绝、源 Pointer 转义正确，非语义扩展接受。该边界核验结束，不代表 §6 的完整几何替换证据或所有消费者观察闭包已经实现。

8.6 联立仿射等式的精确恢复（2026-09-21）

缺口与职责。 原 Core reconstruct 只从含一个未知量的无条件等式开始传播；例如 x+y=1、2x−y=0 没有这种起点，两个精确解 1/3、2/3 又不能由 binary64 精确表示。要求客户端先手工解出它们与 P2 的目标相悖。当前复用锁定 num-rational/num-bigint 的精确算术，在既有 reconstruct 入口扩展稀疏行化简与回代，不新增优化器或通用矩阵库。HiGHS 仍负责自由坐标、离散选择与优化候选；此处只解释无条件线性等式的恢复映射，不搜索最优点。原构造、几何算法和 SemanticRef 不改变。

保持性推导。 将无条件等式写成 Ax+b=0。每一步仅执行 rᵢ←rᵢ−λrⱼ，λ 为已有非零主元的精确有理商；逆变换为 rᵢ←rᵢ+λrⱼ，故解集不变。按有序变量 ID 存储不同首变量的稀疏行，后续消去只留下更大的变量。反序回代唯一确定主元坐标 p=R(z)，z 为非主元自由坐标。不构造稠密零空间矩阵。对完整源谓词 P（含定义域、整数性、条件关系、范围与目标接受条件），合法实现仍由 P(R(z)) 决定，等式满足本身不等于 P 成立。源定义和全量变量保留，实际接受仍调用原检查器；本次不将优化问题缩成自由坐标问题，也不声称已完成所有仿射消元优化。

没有候选时，仅在全部变量都有主元、无矛盾行且预算内完成时产生源唯一确定的候选；其通过原问题检查后才可省略数值求解。存在自由变量则返回 unknown，不擅自把自由度设为零。有候选时，所有输入见证先按当前契约解码，非主元保留原精确值，主元通过 R 恢复。恢复可能违反整数域、激活不同条件或不满足边界，这些仍由完整源检查拒绝，不能据此说设计无解或保留原最优性证书。条件等式不参与本恢复，避免用它决定自身成立条件。

身份、失败与成本。 全部恢复数值仍经既有候选检查、lowering、Realization 和恢复链封存；numericIdentity 绑定当前 Core 算法。没有独立可编辑的恢复权威或第二份缓存。矛盾行、缺失自由值、位数或工作预算耗尽均返回 unknown；此入口不签发不可行证据。解析、消去的每个稀疏项更新与回代都消费原 20,000 工作预算，有理分子/分母仍受原位数界约束。消去可能填充，不能从稀疏输入保证线性复杂度；超限继续按既有 unknown 路径处理，不无限扩大预算，也不把候选采样当作证明。

8.7 单点域作为无条件等式

对于规范单位下的精确有理数 a，x∈{a} 与 x=a 等价；闭区间 a≤x≤a 同样等价。有限集合允许重复表示同一有理数时，其集合语义仍为单点。由此单点域可以提供 §8.6 稀疏消元的初始主元，无需调用优化器猜测已被源约束确定的量。初值不具备这种含义；包含两个不同值的集合、缺失端点或任一端点开放的区间不能按此规则固定。尤其 [a,a) 是空域，不能被替换为 x=a。

历史归纳的空白起点（2026-09-21）。 无节点、Body、root、assertion 且无 product 的源文档没有求解变量、构造或行为执行，因此需要恢复的选解集合只有空见证。恢复该源不需要伪造旧 Realization：以原源语义提出新候选，现有空模型求值器封存当前运行时下的空实现，再执行既有检查和原子提交。参数与设置仍由源保存并进入模型身份；“没有选解”不表示可以省略源身份。此证明不能推广至非空源，也不能免除已封存修订的证据完整性检查。

备份历史的全称义务。 若导入保留有限修订集合 H，并允许这些修订成为恢复目标，则其恢复有效性义务是对每个非源 h∈H 检查源与封存实现，而非只检查 head。哈希和收据一致只能建立内容关联，不能替代源关系的重算。现有导入隔离库内复用 evaluateRevision 顺序重放非 head 历史，再重放 head，全部通过后才执行原比较交换事务；源起点保留原未求值语义，不伪造候选收据。该实现检查备份实际携带的有限对象，不枚举可能的设计。工作量为各历史恢复成本之和，不承诺常数时间或免几何重建；不得重新搜索设计解。

取消与持久化边界。 验证尚未改变目标存储，因此可在异步阶段之间及重放内响应 AbortSignal，并释放验证库。最终 importProject 比较交换事务开始后，取消不能被解释成“操作未生效”：成功则必须交接新 Core，失败则保留原 Core；不能在持久提交与交接之间再次抛取消异常。当前入口在创建替代 Core 后、进入存储事务前作最后一次取消检查，提前取消会释放替代 Core；历史恢复收到同一信号。2026-09-21 原生链核验验证阶段取消不改项目，持久写入成功后注入取消仍交接 Core，无 Worker 启动。此边界不意味着同步解析或不可中断的原生调用可立即抢占。

2026-09-21 接线核验：含空白恢复历史的实际备份中，两个非 head 已提交修订各重放一次，head 一次，全程禁止 Worker；历史重放入口注入失败后，当前 head、持久 head 与导出项目内容保持原值。此失败注入只证明导入路由和失败原子性，不冒充对任意伪造内容的穷尽验证。Web 类型和相关 lint 通过，该项验证结束。

共享 Session 的源恢复能力由适配器给出上述充分条件；工作台历史列表和撤销栈复用相同空模型判定。原生历史管理器检查已确认首次关系建模可撤销到空白并重做，空白提交持久化且重开可读，整个历史操作期间禁止 Worker；类型及相关 lint 通过。此项验证结束，非空初始源的免搜索恢复仍未由本规则覆盖。

当前 reconstruct 复用已有精确分数解码、位数限制和工作预算提取这些等式，保留全部源域、整数/非负细化和要求。后续等式照常与单点主元一起消去，因此冲突不会被覆盖。完整变量均确定且原问题独立检查通过后，才允许现有 source-determined 路径直接交付；没有固定的自由变量仍须由求解器提供候选。结果继续进入同一 Realization 与恢复链，没有新增固定值权威。该规则不声称识别全部单点可行域，也不为一般非线性问题提供唯一性判定。

原生接线核验使用单值有限域 x=1/3 m 与闭单点区间 y=2/3 m，创建真实实体、提交，再修改共同控制量得到 x=1/4 m、y=1/2 m；创建、修改和保存重开全过程禁止 Worker，实际求解器启动数为零，重开保持 Realization 哈希。原检查器拒绝域外值；将有限域扩大为两个不同值或将单点区间上端点改为开放，精确恢复返回 unknown，不代选。Rust fmt/clippy、WASM 构建与 diff 检查通过；验证限定为该编译规则及其既有事务接线，不外推一般域唯一性。

8.8 角色投影的可定位拒绝（2026-09-21）

替换受某个源观察阻止时，只有错误码而没有观察位置不足以让客户端修正绑定，也不足以追踪观察闭包。现有 projectRelationSemanticReferences 对源 lineage scope、目标输出类型、面/边选择器 basis 与来源绑定的拒绝统一使用 RelationDefinitionError，指针定位实际 definitions 成员或下游 inputs 的选择器 basis。有限 list 递归以显式栈保留路径，键遵循 JSON Pointer 转义，保留现有取消检查。源 AMIR、基数与 split/merge/delete/kind-change 策略均不改变，不将这项诊断记录冒充 ReplacementEvidence。

Chrome 调用真实投影：两层 list 的面选择器正常映射到原构造目标，exactly-one 与 onSplit:reject 保持；通过现有定义工厂创建错误来源哈希的选择器，返回 RELATION_SEMANTIC_SELECTOR_BINDING_MISMATCH 与 /nodes/consumer1a0b/inputs/faces~1x/list/0/list/0/const/value/definitions/0/basis。初始核验输入的 lineage origin 未使用契约要求的 origin: 前缀，改正脚本后通过，未放宽产品校验。Web 类型及相关 lint 通过。跨几何算法的完整角色覆盖和观察闭包仍须接线，未启用未经证明的顺序切孔替换。

8.9 角色投影的准备与应用边界（2026-09-21）

已有执行投影使用私有文档，但内部角色投影先写目标扩展再检查全部消费者，后部错误会留下部分转换结果。为让规则检查自身具备失败隔离，现暂存按目标节点合并的 lineage 扩展及具体选择器替换，全部异步定义校验与构造完成后检查取消，再同步应用全部写入；不复制整个文档、不引入持久事务层。准备阶段的异常和取消保持传入目标不变。此结论以调用方持有的普通私有 JSON 图为前提，不宣称可抵抗外部并发修改或恶意属性 setter。

实际 Chrome 投影验证同一嵌套列表先有效后错误的两个选择器：错误指向 definitions/1/basis，传入目标 JSON 完全不变；在 resolve 后触发取消，按既有 EXACT_GRAPH_COMPILATION_CANCELLED 拒绝且目标不变；成功路径保持基数和演化拒绝策略。首次脚本误将本项目取消错误假设为 DOM AbortError，修正判定后通过，产品取消契约不变。Web 类型及相关 lint 通过。该工作加强共同转换机制，不证明跨算法角色覆盖，也不声称此前存在已提交文档污染。

9. 构造替换接线审计：现有身份不能代替缺失的观察证明

2026-09-21 以当前源码核对，后续实现应从下表接续，不重新建立一套权威图或证明存储。

义务	可复用的真实数据与核验	仍缺少的内容
源与选解绑定	RelationRealizationBlock 的 sourceNodeId、boundNodeHash、candidateHash、numericIdentity；relation-construction-graph 从源重新 prepare/rebind，再比 boundNodeHash	此绑定不说明某个几何替换规则适用，不能充当 currentDomainCheck
当前实际施工	同块 nodes、nodeIds、constructionSources、outputs，以及编译器身份；relation-materialization 重建 lowering 并比较完整 blockHash	尚无两种构造的规则匹配、参数域与对应角色定义；不能把同一块哈希标为 sourceRecipeHash 与 targetRecipeHash 来伪造替换
要求保留	requirements 中的源断言哈希/精确范围，preservedAssertions 的原断言哈希；共同断言投影及求值	端口依赖闭包不是观察闭包：下游程序可能观察原生面数、顺序、history 或中间形状
身份与角色	Operation Module.authoringRoles、semanticRefPolicy；lineage 定义、选择器基数/演化策略；实际 history 与面/边查询证据	authoringRoles 声明来源与基数，没有声明每个消费者观察哪些事实。两个独立构造没有原生祖先关系时不能复用 history 来声称对应；须建立规则专属覆盖、方向和邻接证据
当前检查与恢复	exact-feature-graph-evidence-assertions 核对实际拓扑/选择器的来源身份；exact-graph-realization 核对当前内容闭包，恢复重建执行文档	现有旋转、边选择等专用证据不能转换为任意替换的 geometryCheck。须针对真实候选生成角色映射与几何检查，并按 §6 在冻结 Realization 之后绑定

9.1 下一实现必须满足的接口边界

观察闭包应从已校验源契约提取，而不是遍历任意 JSON 键猜语义。起点包括被替换构造输出、显式导出的中间构造、持久选择器和源断言；沿实际消费者传播。节点存在依赖只说明要读取某值，不能推出它只观察实体点集。对没有受锁定契约描述的观察效果，结果应是 unknown 并保留原构造，而不是假定没有观察。

现有 ExactProgram 可在其声明的输入形状上运行显式程序。仅凭它输入类型是 ExactSolid，不能证明它不枚举面、读取 history 或依赖拓扑分割。因此一般程序消费者不能仅靠实体集合等价自动越过；应保留原构造，或者由今后的受约束程序效果契约明确给出可验证限制。不能要求 AI 自己声称“程序不观察拓扑”来获得替换权限。

对 §4 的贯穿圆孔规则，角色覆盖证明的具体义务仍是：每个稳定孔 ID 的全部孔壁 patch 覆盖完整圆柱区间、方向一致、上下边界与邻接对应，并满足源引用原有基数；仅在同一圆柱上、面积相近或 volume 相等都不充分。原生 builder history 用于同一执行链演化，不连接独立执行结果的虚构祖先。现有批孔能力已经是批量执行，不再为它建立一份等价几何算法；真正替换的是源施工选择，规则适用性与角色检查须先落实在共同链。

9.2 本轮结论与停止条件

此次审计没有启用新的几何替换，也没有新增空壳 ReplacementEvidence。下一功能实现应闭合“受类型约束的消费者观察声明 → 规则适用性检查 → 真实角色覆盖 → 冻结实现后的检查绑定”这一条链；不得继续把增加错误码、规则字符串、哈希字段或相似几何案例算作该链完成。精确输入专门化及其恢复已有实现，不列为重复待办。首个几何规则无法获得完整观察/角色证据时，原构造仍是当前执行路径；这不是对长期构造优化目标的放弃。

9.3 锁定消费者的观察契约

当前 Operation Module 的 InputDescriptor 增加 observation：unknown、value、geometry-set、native-representation。缺省为 unknown；value 要求完整 typed value 保持，geometry-set 只承诺规则化定向几何集合的观察，native-representation 还允许读取原生拓扑、顺序、序列化与 history。声明属于锁定执行器的上界契约，不是 AI 可自行填写的候选证明，也不是自动替换授权。目前只为 ExactProgram.shapes 声明 native-representation，不凭参数类型替其他算子声明 geometry-set。

共同 construction graph 在合并引用预算和 DAG 校验后，从同一锁定目录读取真实消费者输入，返回 producer、consumer/input、moduleHash 和 observation。源关系别名只承担编译接线，不冒充原生消费者。此处得到的是直接输入观察；导出角色、断言、选择器和传递观察的完整证明仍未闭合，不能因该图 status:pass 而启用几何替换。该状态的 scope 仍为 relation-construction-port-closure。

当前模块、schema、目录及 Core 的哈希同步更新，沿用单一当前契约。公开 catalog.describe 通过 canonicalModule 返回同一声明，无第二份工具描述。真实 SDK 关系建模与提交后，未声明的拉伸 profile 输入保持 unknown；禁止 Worker 后重开保持实现根和直接观察记录。Core WASM 构建、Web 类型和相关 lint 通过。这项接线不改变 §9.2 的完整链完成条件。

持久选择器的依赖边（2026-09-21）。 ExactFaceSelectorSet / ExactEdgeSelectorSet 的定义 scope 明确绑定 producerNodeId/outputPort；即使消费者的实体输入指向另一个后继构造，这个源角色仍被观察。因此共同 collectWorkbenchValuePortRefs 现在从这两类注册常量的 definitions 提取生产者引用，有限 list 继续递归；同一引用进入执行 DAG、关系构造引用检查及直接观察提取，不另建角色依赖图。普通常量中的同名 JSON 字段不具有该含义。scope 的边只说明依赖，定义哈希、基数、方向、演化与几何对应仍由原检查链核验，不据此推导几何可替换。

实际浏览器调用共同提取器与 DAG 构建器，确认面/边选择器的源依赖和另一个实体输入同时保留，悬空生产者及经选择器形成的环明确拒绝，普通常量不产生依赖；既有真实 SDK 关系建模、提交与免求解重开通过。类型和 lint 通过。该修复补上已注册持久引用的可达性，尚不等于全部观察的语义等价证明。

9.4 传递观察必须使用算子的保持规则

输入 observation 不能直接作为“这个算子的所有输出也等价”的证明。设两个输入具有相同实体集合，但采用不同面分割；一个构造可以在集合意义上得到相同结果，却保留不同输出分割。其下游程序若读取面数，就能区别这两个结果。即使算子的理想数学定义只涉及集合，实际原生输出及失败行为仍需另外约束。因此不能把 geometry-set 标签沿依赖边原样传播，也不能把 value、geometry-set、native-representation 当作适用于所有类型的同一强弱全序。

组合义务。 对锁定算子 M、输出观察要求集合 Q、固定环境 k，规则必须提供输入关系 P 及适用前提 U，使下式成立：

[ U(x,x’,k)\land P(x,x’)\Longrightarrow Q(M(x;k),M(x’;k)). ]

这里 P 同时覆盖全部会变化的输入；不能只逐输入保持、却遗漏输入间共享角色或别名关系。k 包含其余输入、资源、运行时及规则声明的上下文。Q 包含被要求保持的输出角色、允许误差和可见失败；原生浮点构造仅有候选检查时，不据此提升为整个参数域的双向成功保证。此传递规则按实际算子逐项证明并锁定；无规则时返回 unknown，不从输入描述猜输出保持性。

有限图上的推导。 从源要求、持久引用、已声明中间输出及工艺/分析绑定生成观察义务，以端口为索引逆向传播。普通算子使用上述规则把输出义务变成输入义务；关系输出别名只重定位同一义务，不能消除它。共享后继的义务取合取，保留来源引用；规则复用同一已处理义务，不展开所有路径或所有参数赋值。执行构造 DAG 已检查无环，故按逆拓扑顺序处理；必要的参数域证明和角色证据由匹配规则提供，不由图遍历生成。域检查、义务数量和角色解析受既有预算约束，耗尽保持 unknown。

实现边界。 当前 inputObservations 与依赖图只提供上述算法的读取位置和直接观察，尚没有 M 的传递规则或完整 Q 的提取。不能因全部直接输入声明已知便返回“观察闭包通过”。下一条几何替换的完整接线必须同时落实特定源/目标模式、U、输出保持规则、真实角色覆盖与 §6 的冻结后证据绑定；不先新增一套通用效果系统、第二份图或只有哈希的证明外壳。实际公开读取原生面数不等同于源承诺所有未来构造的面数不变；持久下游程序或明确要求读取该事实时才形成相应保持义务，每次源编辑重新推导。

9.5 原生圆柱孔壁的裁剪边界前提

2026-09-21 核对 exact-hole-array 发现，施工检查仅观察圆柱支持和 U 参数跨度，独立要求另有面积与贯穿检查。参数包围为完整 2π 并不蕴含实际面没有内部孔洞，面积接近也不能替代原生边界拓扑。对当前单一完整圆柱孔壁接受域，现复用锁定 OCCT 的 TopExp 遍历、BRep_Tool.IsClosed/Degenerated 和 BRepAdaptor_Curve 检查真实边界：非 seam 边必须恰为两条完整闭圆，wire 为一条带 seam 的环或两条闭环；额外裁剪边、内环、退化或不完整圆明确拒绝。此检查同时进入施工与独立孔要求，原有效实体、圆柱支持、参数跨度、直径/位置、面积及贯穿检查继续各自承担职责。

所有查询使用既有 withOC 和句柄释放机制，不重复实现曲线求交或原生拓扑库。初次接线暴露施工调用处缺失 OCCT 上下文，已修正，未通过设置全局常驻运行时规避生命周期。实际 SDK 普通孔建模与重开通过；在含水平通道的有效基体上新增竖直圆孔，因侧壁被通道穿破而返回 EXACT_HOLE_ARRAY_INVALID，未提交且 head 不变。验证使用真正的隔离 program worker 生成基体与共同 hole-array 执行器，不采用假 history。

结论仅为 native-checked 候选边界检查加强。该检查没有连接两个独立构造的角色，尚未生成跨构造的覆盖、方向/邻接对应或冻结后的 ReplacementEvidence，不能据此启用顺序切孔与批量切孔替换。内核 build:aira、类型及相关 lint 通过；原生 OCCT 绑定未改动。

9.6 已检查孔角色与具体候选面的绑定

仅保存 checkedCylindricalWalls 数量无法表达“哪个孔的哪个面接受了检查”。现用当前结果中的 cylindricalWalls 取代该冗余计数，每项为稳定孔 origin 与同次 ArtifactGraph 的 artifactSubEntityId。原生结果在每个孔完成单面、圆柱支持及实际裁剪边界检查之后，按真实 lineage 建立一一对应；缺失、多匹配或不同孔共用一面均拒绝，不用相似几何补全身份。没有新增持久设计权威，条目数量直接由数组导出。

共同候选/修订 evidence checker 核对实体内容哈希、生产者节点/操作/solid 端口、声明孔数、两侧唯一性及每个 Face 包含对应 origin。该数组属于同次 node result，沿已有 resultHash→geometryEvidenceHash→certificate/evidence 及绑定 Realization 的 execution manifest 封存，不向 Realization 反向写入检查结果，避免哈希环。恢复仍执行原生几何与共同检查。当前结果结构直接更新，无旧字段兼容分支。

实际 SDK 的正常孔提交、重开及破壁拒绝通过；将绑定改为同一实体的另一张面，同时重算 node result、geometry、certificate 和 evidence 哈希，仍返回 EXACT_GRAPH_HOLE_WALL_BINDING_MISMATCH。因此此检查不只依赖外层内容哈希，而核对角色与真实面记录的关系。内核 build:aira、Web 类型、改动 lint 与 diff 检查通过。

这仍是单次构造的实际角色绑定，不建立独立构造之间的 history，也不证明两构造间方向、邻接与观察等价。后续替换检查须消费双方的真实数据并建立规则专属对应，不能把此数组本身命名为完整 ReplacementEvidence。

方向与边界邻接的实际数据（2026-09-21）。 孔壁施工现在同时检查圆柱轴系的 Direct 与原生面方向，二者共同确定材料位于圆柱外侧，不能只看 REVERSED。复用现有 AiraTopologyIndex（TopExp incidence）和 bindExactFaces，将每条非 seam 圆边界绑定到恰一个其他非孔壁面；每孔保存 materialSide=outside-cylinder 及按 Z 排序的两个 rims（圆心、相邻面的 artifactSubEntityId）。原生索引只用于此次求值，ordinal 不进入结果，句柄在 finally 中释放。相邻面不强制为平面，不能由本结果声称源体为平板。周期 seam 不属于物理边界；多邻接、孔壁互邻或没有两个不同高度的圆边界均拒绝。

真实需求是为后续规则提供方向和邻接事实；上游设施是锁定 OCCT 8.0.1 的既有原生拓扑索引、曲线适配和当前面身份绑定。已证实的差异是旧 cylindricalWalls 只有孔—面身份，没有邻接数据。Aira 仅组装受检角色记录，不新增几何或命名算法。共同 evidence checker 额外核对方向标签、两项有限圆心、上下顺序及相邻面身份/非自邻接；这只是结构一致性检查，不能独立证明任意重新伪造的邻接关系。真实几何依据来自原生求值和恢复重建，不把外层哈希称为几何证明。

实际 SDK 验证 10 mm 厚实体贯穿孔得到 Z=0/10 的两圆边界和对应邻面，提交、保存重开保持实现根；把相邻面改为孔壁自身并重算外层哈希仍被拒绝，破壁孔拒绝且 head 保持。内核 build:aira、Web 类型检查及相关 lint 通过。此项提供单次构造的方向/邻接数据，源目标模式匹配、双方角色对应及传递观察证明仍待完成。

原生发现接线。 model.read 的既有 faces 分页条目现可带 holeWall={nodeId,origin,resultHash}，直接读取同一已验证当前权威孔阵列的角色绑定，不按圆柱半径/面数猜孔。匹配 artifactId 与内容哈希；下游构造即使含相似孔壁也不继承该标记。schema 由原生成链更新，SDK 描述明确缺省表示当前无此检查声明，不表示不存在孔；origin 本身不是可直接提交的选择器，持久捕获沿现有 revisionId/faceId 路径。实际公开 SDK 读取得到对应孔角色，contracts/SDK 构建、Web 类型及相关 lint 通过。

公开读取现从同一孔结果继续投影 materialSide 与 rims={adjacentFaceId,centerMm}，上下顺序按 Body 定义 Z；相邻面 ID 与返回的 revisionId 配对使用，跨分页仍保留。圆心使用原生圆几何值，不用面积质心推测，不应用产品放置；不增加边选择器协议。实际公开 SDK 全页和单面分页的角色数据一致，邻面可在同次完整面列表中定位，保存重开保持。此数据仅表示当前受检构造的边界邻接，不承诺后继或替代构造仍保留它。

9.7 源关系面引用到原生程序输入

发现面与捕获面必须使用同一修订绑定的实现端口。原程序输入捕获按源关系节点直接检索施工 artifact，因二者身份不同而失效；现复用面查询的实现见证解析。捕获时在实际生产者作用域运行既有 resolveExactSubEntity，持久引用保存源关系的 producerNodeId、operationRef 和输出端口，以及原始完整 lineage 与显式 policy。

执行投影对 LineageShapeReference 校验源操作、输出类型和解析后的实际实体端口，只改变生产者作用域，不改变 lineage 或拒绝策略。所有写入与既有语义选择器一起暂存，准备失败或取消不留下部分投影。原生解析器继续决定唯一性、删除及来源跟随是否合法；端口解析并不产生跨构造等价证明。未新增库、匹配器或历史系统。

真实浏览器公开 SDK 完成关系板建模、faces 查询、捕获开口面作为程序抽壳输入、上游高度 40→50 修改以及保存重开。源引用仍指向 design.relationSystem，重开实现哈希一致；类型与改动 lint 通过。该有限操作验证源捕获/执行/恢复的接线，不扩大独立构造替换的接受域。

9.8 首条批处理规则的真实匹配域与失败语义

2026-09-21 对照 design-relation-linking.ts、relation-lowering.ts、exact.boolean.difference 的锁定模块、profile-exact-boolean-difference.ts 及 exact-hole-array.ts，不能直接把 §4 的任意有限孔集映射成现有 exact.holeArray。后者只有一个直径和两个规则轴，数量上限 4096，目标不是任意位置/半径工具集合。首条使用该执行器的规则必须明确限定为等直径笛卡尔积网格；一般有限孔集仍是原计划的表达/构造能力，不因首条规则的接受域有限而删除。

义务	可执行匹配与拒绝条件
源模式	在当前 relation construct DAG 中匹配锁定 exact.boolean.difference@1.0.0 的 base 链；每步 tool 须有可解释的圆柱构造和同一源坐标系。程序文本、任意外部 B-Rep 或仅圆柱包围箱不能充当圆柱构造证明。构造守卫必须在本次选解下成立，数值输入来自同一次绑定和交付记录。
初始板体	需要可解释的矩形板构造及其尺寸/坐标变换，不能从最终 AABB 反推“实体等于长方体”。孔中心/半径与板边的严格裕量须由源量和交付误差共同建立。
目标模式	单个现有 exact.holeArray；所有源工具对应同一已交付直径，中心集合与两个有序轴的乘积一一对应，目标数量与源工具数量相等且不超过现有上限。没有这一对应则不匹配，不拟合近似网格，不增加第二个批切入口。
数值对应	源圆柱的实际交付中心/半径与目标 solveExactHoleArray 派生中心必须按当前交付规约比较。数学上相同的表达式可能有不同 binary64 求值顺序；不能只比源十进制文字或 nominal pitch。每个实际源工具核对一次是有限输入验证，不是枚举设计空间。
中间观察	每个被消去中间 solid 的全部消费者、导出、要求、工艺/分析绑定和持久引用都必须被处理。只检查最终 solid 的消费者不足以授权消去。未声明效果保持 unknown。
源角色到目标角色	源 key 使用原构造作用域及稳定设计成员地址；目标 exact.holeArray 的 x/y 归一化位置只是目标实现角色。显式建立双射，不能把两侧 origin 字符串改成相同、伪造 Modified/Generated 或将遍历下标当作设计 ID。
编辑边界	固定成员集、保持模式及域的参数修改重新匹配与核验。增删孔、更换坐标系、改变守卫或观察集合使旧见证失效；需要相应编辑规则，不能沿用旧双射。

源失败谓词是不能消去的设计语义。 当前 difference 在每一步要求 removedVolume > max(1e-9, baseVolume·1e-9)，还要求单个非空有效实体和完整 history。批孔执行器没有这个逐步体积阈值。因此“理想最终集合相同”不足以证明两个现有操作的接受域相同。例如理想板体体积 10⁹ mm³ 时阈值约为 1 mm³；多个彼此严格分离、每孔移除 0.5 mm³ 的贯穿孔符合 §4 的正半径和间距条件，但顺序 difference 的首步不满足其移除量契约。不能因为批处理可生成实体就把源本应拒绝的操作变成成功。这是代码谓词的反例推导，不是本轮已运行的几何结果。

对于等半径、等深度且严格分离的族，每孔理想移除量 v=πr²t，任意前缀的理想基体体积 Vₖ=WHt−kv。由此可以推导逐步材料移除条件；工程检查还必须计入半径/厚度交付误差与积分误差，不能把理想 v 直接当作原生测量值。阈值随前缀体积单调不增，所以在已证体积上下界下，可用初始体积的保守上界统一证明各步阈值，无需执行每一种孔次序。这只消去材料阈值的重复义务，不证明原生 builder 在全域的终止、成功或 history 完整性。

接线位置及停止错误路径。 规则匹配以 prepared.linked.constructModules 的实际锁定模块为依据，在 relation-lowering 封存前产生真正不同的目标 nodes/outputs 与来源对应；不能先改封存块再补一份声明。恢复必须从源、原选解与原规则重建同一选择，现有 read/seal/inspect 和整块哈希检查继续承担绑定。冻结后几何/角色检查消费真实候选，再进入共同验证，不能反向写入 Realization 造成哈希环。仅有当前孔壁方向和 rims，不足以开启该替换：仍需上述源模式、板体/网格域、源失败谓词、完整观察及双方角色证明。当前没有注册或启用此几何替换，本节把缺失项落实到真实操作契约，不将研究规则描述计为实现完成。

源模式的构造类型接续（2026-09-21）。 对锁定模块输入的 ExactBRep，ExactSolid 是可供原生检查的边界表示；其准入不意味着输入已经满足单实体、有效性或相交条件。当前 relation linker 在构造输入上下文接受该单向关系，递归传入 select/list，并同时处理外部 input 与内部 output 配方。公共关系输出不沿用此放宽，保留实际类型与别名投影一致；ExactBRep→ExactSolid 也不作为静态隐式提升。依据是现有 exact.boolean.difference 等模块的明确双类型接受契约，几何检查仍交给原执行器，无新增转换节点或复制实体。真实 SDK 关系拉伸→相减此前被 linker 拒绝，现提交与保存重开成功；外部关系实体输入能到达原生无材料移除拒绝，错误公共输出类型继续拒绝且 head 保持。这是批切源模式可组合的必要修复，不是批切规则已经启用。

持久捕获本身的依赖（2026-09-21）。 LineageShapeReference 读取其声明的 producerNodeId/outputPort，不能因为程序另有一个形状输入就假定来源边必然被那个输入覆盖。共同 collectWorkbenchValuePortRefs 现识别该注册常量，与已有选择器依赖一起进入执行 DAG 和构造观察提取；普通 opaque 常量不扫描同名字段。这个规则只确定读取位置，不证明被捕获面存在、唯一或跨构造对应。实际 SDK 捕获、续改和重开通过；真实源文档上的共同图函数核验了捕获单独形成依赖及自引用循环拒绝。此为补齐观察起点，不等于已经有算子观察传递定理。