架构裁决、模型与可行性证明

研究总览 · 2026-09-20

当前架构、封存实现和构造性证明；实施步骤只引用现有计划。

• 4. 模型语义与系统结构
• 15. 研究完成度与实施边界
• 22. 收敛方案：统一持久设计图与关系编译器的构造性可行性证明
• 23. 效率目标、架构重审与候选几何复用的条件推导
• 24. 通用 AI CAD 的整体架构裁决

4. 模型语义与系统结构

下图只表示需要搜索的几何候选子流程；已知输入的直接求值和显式构造不经过优化器，完整分工见 §22。失败/未知仅在有合法候选且预算允许时继续，预算耗尽返回 unknown，取消释放候选。

flowchart TD
  A[同一原生 Interface：需求及修改范围] --> B[AMIR 设计关系与语义引用]
  B --> C[关系编译：结构语法、内外近似、约束来源]
  C --> D[HiGHS：离散选择与线性子问题]
  C --> E[CasADi/IPOPT：非线性参数候选]
  D --> F[封存 Realization：数值、结构与具体构造]
  E --> F
  F --> G[OCCT 求值与实际几何检查]
  G -->|通过| H[原子提交：源设计、封存资源、验证与修订]
  G -->|有合法候选且预算允许| C
  G -->|预算耗尽或取消| U[unknown 或 cancelled：不提交]
  D --> I[不可行证据精确核验]
  I -->|前提成立才剪枝| C
  H --> J[离线抽象候选：Stitch]
  J -->|类型、展开与效果核验| C

4.1 一份模型真相

设计问题是语义对象，包含：requirementRefs、带单位变量与范围、结构选择域、锁定角色和软目标。硬要求由 assertions 唯一持有，设计问题通过 ID 引用，不把同样要求在 planner、solver 和 document 中分别维护。实现由 Revision 关联到封存资源；源设计不反向引用本次派生的 realizationHash，以免形成身份循环。

当前 modelHash 包含 assertions 和 semantic extensions，排除 metadata，见 执行规范 §14.1。因此新增求解语义必须进入当前 schema 与规范化投影；不得存 metadata 后宣称具有持久强制效力。

设计要求和允许的选择策略属于源模型语义。basis、临时矩阵、工作句柄与普通运行日志可丢弃；已选结构、数值、具体构造、输入闭包、运行身份及提交所依赖的证据必须作为 Realization/验证资源持久保存。随机性若参与选择，相关策略与可追溯信息须绑定本次求值；仅保存 seed 不能替代具体结果。历史重放读取封存实现，不依靠重新运行求解器恢复结果。

4.2 允许修改不是默认全部解锁

用户可以锁孔数、孔径、安装面、接口位置、材料和某个局部结构，仅开放其余变量。求解器不能为改善目标而删除要求、放宽容差或改变锁定项。多个目标按显式优先级处理；“少改结构”不得压过硬净距要求。

整数选择使用线性/分段线性目标。若需要连续二次位移目标，可在明确授权的分阶段策略下固定离散选择，再使用同一 HiGHS 的连续凸 QP；这只优化已选分支，不保证联合 MIQP 全局最优。若用户要求联合最优，应明确当前能力边界，不能默默改成分阶段目标；也不将 qpsol 名称误读为支持 MIQP。

4.3 结果语义

结果	含义	对历史的作用
solved	有一个已验证实现；另列最优性是否已证	可以进入现有提交流程
infeasible-in-declared-domain	声明域中所有分支有足够不可行证据	不提交替代几何，保留原 Revision
unknown	超时、非凸局部失败、检查不足或证据未通过	不等同无解，不改原 Revision
cancelled	用户/预算控制取消	释放临时资源，保留原 Revision

候选失败和整个域无解是不同事件。几何检查仍保持 pass/fail/unknown；对未知要求不允许静默提交。

15. 研究完成度与实施边界

架构及证明的当前结论统一见 §22；本节只保留同一结构下的求值计划选择，产品实施状态见工作进度。

15.1 选定方案的求值成本取舍

对 AI 的统一入口以稳定概念、可组合关系和可发现契约组织；数值与几何求值计划留在内核。下面的成本优化始终在这一契约内部进行，不能为了降低内部计算成本而把求解器选择、矩阵装配或施工顺序重新交给 AI。

源设计只有一份权威：设计变量、关系、选择域、允许修改范围、原始要求及用户显式指定的构造。求解得到的结构、数值与构造属于派生的封存 Realization。 二者共同持久化，分别绑定 modelHash 与 realizationHash，不能把求解输出覆盖回原关系。临时矩阵、basis 和工作缓存可丢弃；恢复所需实现资源必须保留。

对固定结构 z，在有限候选集 (\Pi(z)) 中选择求值计划：

[ \pi^*\approx\arg\min_{\pi\in\Pi(z)} \widehat T_{compile+solve+geometry+recover+verify}(\pi) \quad\text{s.t. 同域等价、要求保持、误差与内存预算满足。} ]

这里的近似号是明确的工程事实：经验成本模型只在锁定环境与采样范围内可信，不是求出了所有实现的全局最优。结构搜索 z 与同结构的等价求值计划 π 分开；改变对称族是搜索子域，不能冒充纯性能优化。

内核需要完成的事	采用的机制	限制自研复杂度的边界
减少必须求解的自由量	已声明等式、对称/等距参数化、固定值与别名代入	不自研通用符号代数；不偷偷添加对称或锁定
平衡未知数与耦合成本	保留原变量、小块/部分消元、必要时全消元	有限候选、有限编译预算；导数与线性代数复用后端
避免不必要的搜索	能证明时解析判定；否则按结构选 LP/QP/NLP/有界离散搜索	不给普通请求叠加全部 solver，不把局部失败当证明
减少几何工作	已知截面/拓扑直接构造；一般情形使用成熟构造算法	不重写曲面求交/修剪/偏置，不扩大等价律适用域
支持连续编辑	持久模型、basis/参数更新、经检查的局部失效	一条候选—检查—提交路径；缓存必须有净收益

当前库分工已经确定：OCCT 负责实体几何；PlaneGCS 负责草图约束与其诊断；CasADi/IPOPT 负责剩余非线性关系；独立 HiGHS 负责 LP/MILP/连续凸 QP。它们承担不同的必要职责。移除或不发布同类重复插件，按需加载；Manifold 仅属于已声明的网格能力。Stitch 与复杂证书搬运不属于每次编辑必经路径。

本方案真正缩小的是 Aira 必须维护的重复特征求解流程，以及每次任务执行的无效数学/几何工作。维持任意 B-Rep/STEP 接受域时，不能声称已证明 OCCT 可被压成几个短公式，或能显著删除其通用求交代码。保留成熟基础设施与改变内核组织方式并不矛盾。

用户要求研究清楚前不开始实现，本文不把论文支持或隔离探针通过视为开工许可。研究内容由总览统一索引；用户另行明确授权的项目原则契约已经纳入本轮文档修改，产品运行时变更仍未启动。

22. 收敛方案：统一持久设计图与关系编译器的构造性可行性证明

22.1 本次必须证明的命题与最终选择

用户要求“证明一个可行方案”，而不是继续列举可能性。§18–§21 的不足在于，组合论证主要写成“若基础语义正确则整体保持”，没有充分给出基础翻译。这里补齐构造，并作出确定选择：

采用统一持久设计图。AI 描述工程对象、必须成立的关系和允许改变的量；核心将关系编译为直接计算或适用的数学问题，生成并验证实际构造。复杂几何与明确指定的工程程序同样进入这张图，保留通用表达能力。

可行性证明须同时建立三件事：① 该模型可容纳已有有限工程描述，不能因简化 AI 接口退化为孔、板模板；② 在明确而非空的数学域内，确实存在从要求到实现的算法，不能让 AI 自己填矩阵和全部施工参数；③ 编译、求解和几何执行可分工，不要求一个优化器解决所有设计。证明方案可行不要求先证明所有算法全球最快，也不以当前产品已经实现为前提。

“通用”在这里指跨产品类别、可组合的工程表达；“自动设计”指已给定语义与算法域内的求解。整个系统必须容纳前者，不能为了后者的完备性而删掉复杂几何、行为或物理模型。§20 的不可判定性不阻止这个构造。

22.2 模型具体保存什么

以下为研究中的语义结构，不是冒充现有 Interface 已接受的 JSON schema。它落在同一 AMIR 权威状态内：

内容	必须保存的意义	直接执行职责
定义与实例	类型、稳定身份、带单位参数、局部坐标、共享定义与实例路径	同一部件定义可实例化，不复制数值算法
关系	两端对象、参数角色、适用域、硬要求引用、目标与授权选择	编译为表达式、约束或实际结果检查；每项保留来源
构造	曲线/曲面/拓扑数据、已指定的程序、定义域与结果角色	调用同一几何内核；关系生成的程序是有来源的具体实现
连接与行为	端口类型、连接规律、状态、时间、事件守卫、重置和初始化	保留对应方程与事件语义，交给指定执行模型
分析	几何域、材料、工况、边界条件、分析模型及版本、结果对象	执行所指定的模型并绑定结果来源；不得把模型名当分析结果
修改与提交	修改对象、固定/开放量、保持条件、基准修订、具体实现	求值和检查在候选状态进行，通过后进入已有原子提交

要求继续由现有 assertions 持有，关系引用其 ID；不能再复制 planner、solver、document 三份要求。派生矩阵、B-Rep、网格、数值结果和缓存没有各自改写设计意图的权力。显式锁定的构造属于设计要求；未锁定、由编译器生成的构造属于实现。这个区别决定修改时哪些内容可重算。

22.3 通用表达证明：给出逐构造翻译，不依赖产品枚举

先在 Aira 之外确定参照域 P：有限的工程描述，由下列资料和构造组成。几何资料采用公开 B-Rep 的点、曲线、曲面、裁剪域、拓扑关联、位置与方向；计算包含有限表达式、命名绑定、分支、有界重复及声明过的原生调用；产品包含有限部件图和端口连接；行为采用显式状态、方程、事件及初始化；分析调用具有确定的执行模型。参照域不按当前 AMIR 是否已支持来定义，也不按飞机/机器人名称划分。

P 的求值采用明确的事务语义：计算候选，成功验收才提交，失败保留原状态。它不包含在求值中任意修改外部设备或文件的隐式副作用。否则，源程序失败前已部分修改而目标回滚，不能声称失败行为相同。行为/分析调用的外部输入、随机流、数值环境和调度属于执行模型的显式条件。

原子能力集合必须明确：标量/向量与单位运算，直线、圆锥曲线、样条曲线/曲面及裁剪拓扑记录，变换、实例、拉伸、旋转、扫掠、放样、布尔、圆角和偏置等已指定的几何调用；关系表达式包含其支持的算术与函数；行为保留所采用模型的状态转换与求值规则。每个原子绑定具体语义和后端，不允许一个无执行定义的 anything 节点充当覆盖证明。未来新增原子的覆盖取决于它自己的实现，不计入本证明的现有集合。

OCCT BRep 格式明确存储几何、拓扑及位置/方向，这为上述几何参照域提供独立对象；Modelica 方程语义提供连续关系、事件和初始化的独立定义。这里不宣称完整支持 Modelica 语言所有构造，也不把未知物理规律纳入原子集合。

构造翻译 C 如下。定义采用共享引用，重复保留有界生成节点，避免在编译阶段无条件展开：

P 中的构造	C 实际生成什么	为什么保持意义
量 q、变量 x、单位 u	有类型的值/变量节点及单位标签；必要时附显式单位换算	数值、量纲与固定/开放角色不丢；温度等有偏移单位不能仅乘比例
let x=f(a,b)	调用节点 f、输入引用 C(a)/C(b)、命名输出 x	使用相同函数、输入、定义域和数值规则
曲线、曲面与 B-Rep 资料	控制数据、节点向量、权重、参数域、裁剪曲线、关联与方向，以及相应构造节点	保留几何与邻接，不能以距离近似代替拓扑保持
construct(op,args)	绑定同一原子 op 和参数的构造节点	不猜逆函数；直接执行同一已有算法，保留失败语义
部件定义、实例与坐标	共享定义引用、独立实例身份和位置节点	定义相同不合并实例身份；变换作用域明确
connect(p,q)	按端口类型展开的关系及端口到变量的映射	信号、势/流、机械连接采用各自连接规律
if c then a else b	条件节点、两个分支的作用域和输出对应	保留实际选中的分支；不得偷偷算完两支并暴露原先不会发生的异常
repeat(n,body)	有界重复节点、body 定义、迭代键与命名作用域	执行展开有限；实例引用由声明的键解释，不猜面索引
初始状态、连续方程、事件	相同状态变量、初始条件、方程、守卫、重置及事件优先/同时性规则	不把轨迹降为静态快照，不重排有副作用的事件
分析模型调用	模型身份、同一输入/工况/边界/精度和调用节点	复用该模型的执行语义；黑盒仅能获得已声明的前向能力
参数/关系修改	修改被命名的源节点，失效其依赖结果	原设计关系继续存在；不能把一次求解坐标覆盖回关系定义

例如势/流型连接不是泛泛“连一条边”：对同一连接集合，势变量生成相等关系，流变量按端口方向生成带符号的和为零；连接集合合并和符号取自既定端口规则。Modelica 连接规范提供这一具体编译机制。流体 stream 等其他连接不得擅自按同一简单规则处理。

定理 A——构造性表达保持。 对上述原子语义已绑定、类型正确的有限描述 p，C 在有限时间内产生图；以相同原子执行语义解释该图，结果与 p 对应。对应项包括数值与单位、几何与拓扑、部件身份、声明的状态/事件及失败结果。对时间行为，这个结论保持语义允许的轨迹及相同求值规则下的有限执行前缀，不保证任意系统的无限仿真终止。

具体到数值仿真，保持的是相同积分算法、容差、舍入、输入和事件顺序下的数字执行行为，不是已经证明精确微分方程解或真实物理轨迹。浮点代数重排、改变积分器、降低网格精度或重新调度都属于另外的变换，必须有相应误差/语义依据，不能借用此处的直接翻译证明。

证明按上表的语法构造归纳：值直接复制；调用接收归纳假设保证的对应输入；绑定和实例用不冲突的名字替换；条件选择相同分支；有界重复对迭代次数作归纳；连接显式生成对应关系；行为对状态转换作归纳，并保持连续关系、初始条件及事件规则。源中已有的依赖和副作用顺序保留，所以不会凭空增加重排行为。编辑时修改对应源节点并重新解释，得到相同映射。已失效或有歧义的几何引用必须显式报告，不能用“同样形状”证明身份延续。

这给出算法而不只给前提：C 是逐节点建图和连引用，解释器对每类节点执行上表规则。 不需实现一个能理解飞机的神谕。共享定义与有界重复不展开时，建图工作量与显式语法、引用和几何记录的总长度线性相关；类型检查、连接展开、仿真和几何运算的成本另计。保留紧凑重复节点不代表生成百万个实例也只需常数时间。

参照域 P 中已明确语义和绑定的 CAD 构造因此是新语言的可嵌入子域；关系求解增加表达方式而不删掉这个子域。此结论不覆盖未列明的全部 CAD 功能、任意工程程序或所有物理模型。这里的保守扩展是语义包含关系，不是保留两套版本和兼容执行器。生产仍只有一个当前契约和执行路径。复杂外形不必先被改写成孔板模板，通用性也不依赖“恰好十二个算子”。

22.4 数学求解证明：具体的编译与恢复映射

矩阵不是由 AI 填写。编译器对仿射表达式 e 递归计算系数对 (aₑ,cₑ)，使 e=aₑᵀx+cₑ：已知常量 k 对应 (0,k)，未知变量 xⱼ 对应 (单位向量 eⱼ,0)，加减按系数加减，乘已知标量按比例缩放，除已知非零标量同理。未知量相乘、未知分母或非线性函数不得误归为仿射。对 e₁=e₂ 或 e₁≤e₂，把两边系数作差即得到一行。对象关系通过已定义的数学意义展开，例如已知偏移对应 a−b=d，中点对应 2c−a−b=0；先核对量纲，再进入系数收集。这是完整的有限递归算法，不依赖 AI 临时推导每一行。

在单位已规范化的一个固定连续分支上，设编译出的硬关系为

[ Ax=b,\qquad Hx\le h,\qquad x\in X, ]

目标为 J(x)。先检查 Ax=b 的相容性。若相容，求一个特解 x₀，并令 N 的列构成 ker(A) 的完整基；令 r(z)=x₀+Nz。编译出的剩余问题为

[ HNz\le h-Hx_0,\qquad x_0+Nz\in X, \qquad \min_z J(x_0+Nz). ]

定理 B——不丢解的仿射编译。 原问题的可行集合恰为剩余问题经 r 恢复后的集合，且目标值对应。

证明：原问题任一可行 x 满足 A(x−x₀)=0，因此 x−x₀ 在 N 的列空间中，存在 z；代入得到所有剩余约束。反向上，任一剩余可行 z 经 r 恢复后满足 Ax=b，并因其他约束完整代入而可行。目标直接代入，故最优解也对应。rank(A)=r 时，连续自由坐标从 n 变为 n−r；不相容时是这个分支的等式冲突。

这是任意规模仿射关系系统的结论，不是某个孔位样本的经验。固定坐标、相等、固定差、给定权重的中心关系、已知方向的平移配合等都可通过共享语义定义生成矩阵行；AI 不负责填写 A、N 或 r。整数变量不能直接套用连续零空间后放松为实数：整数域须完整保留，或把它们留给混合整数模型。

此证明采用精确代数语义。数值秩判定、浮点零空间和舍入后的 B-Rep 必须使用声明的误差与结果核验，不能直接冒充精确等价。实现也不必总是显式形成稠密 N：优先局部替换、保留分隔变量，或交给 HiGHS 原有 presolve。推导证明可以消去什么，不命令产品重新实现高斯消元或每次全消元。

若一组关系是无环定义 xᵢ=fᵢ(parentᵢ)，且根输入已知、函数在域内单值有定义，便可按拓扑序计算；全部原约束仍须检查。无环本身不消除未知量或目标耦合：例如 x=1−y 在 y 开放时仍需确定 y。其余开放量及耦合约束、目标保留在剩余问题中，不以是否成环作为需要求解的充要判据。剩余线性问题使用 HiGHS，连续凸二次目标仍使用同一 HiGHS，可微非线性片段用 CasADi/IPOPT 产生候选。任意前向程序 f 的存在不证明逆问题 f(x)=0 可由这些后端完整求解。

22.5 非空的结构求解域：任意有限规模的三维箱体布局

为防止“可解片段”仍只是空名，给出一个完整参数族的编译。对象为任意有限 n 个长方体，全部平行于同一公共坐标系的坐标轴且不允许旋转，三边 dᵢₖ>0 已知，最小角位置 xᵢₖ 有已知有限界 lᵢₖ≤xᵢₖ≤uᵢₖ；附加位置/容纳要求为线性关系。要求对指定的每对部件 (i,j)，至少在一个坐标方向留出已知间距 gᵢⱼ>0。所有尺寸、间距、界及附加线性关系/目标系数均为有限有理输入；有限浮点输入可按其精确有理值解释。该语义是轴向分离，不偷换成任意形状的精确最短距离。

对每对部件生成六个二元变量：三个轴上的 i 在 j 前，以及 j 在 i 前。以 i 在 j 前为例：

[ x_{ik}+d_{ik}+g_{ij}\le x_{jk}+M_{ijk}(1-y_{ijk}), \qquad M_{ijk}=\max(0,u_{ik}+d_{ik}+g_{ij}-l_{jk}). ]

每对的六个变量之和至少为 1。反方向用对应交换后的界。M 从输入界严格推导；y=0 时该不等式对所有允许坐标恒成立，y=1 时恰为原来的分离关系。

因此：任一原布局可为每对选一个成立方向得到整数模型的见证；任一整数模型的见证至少保留一个真实分离方向，恢复坐标便得到原布局。两边可行性等价，线性目标也可原样保留。构造输出只是把各箱体按求出的坐标放置为独立有身份的实体；正尺寸保证各箱体合法，正间距保证指定的实体对分离。其他设计关系必须同样保留，不能借“箱体有效”跳过总装要求。

这里的几何保证针对理想欧氏箱体。任意微小的正尺寸或间距不自动落入 OCCT 的可靠接受域；实际交付须满足声明的尺寸、间隙和数值容差，并核验所构造的实体。不能用理想模型可行掩盖有限精度交付失败。

这证明核心能够从关系完成实际的有限结构选择及几何构造，而不要求 AI 枚举六向布局。数学上，有界二元选择加有理 LP 是可判定问题；实现采用成熟 MILP 的求解与剪枝，不用产品逐一试做来验证这个表达结论，也不把 MILP 最坏复杂度宣称为多项式。HiGHS 的浮点结果仍按 §6、§7 与几何容差核验，预算耗尽可返回 unknown。

对任意部件采用包围箱时，这一模型只提供不碰撞的充分条件，可能拒绝实际可嵌套的形状；不得扩大为精确碰撞判定或全 CAD 完备求解。这里选箱体是为了给出无遗漏的代数证明，不把整个语言限制为箱体。复杂部件几何由定理 A 保留，其他精确关系按其实际数学结构编译。

22.6 AI 易操作性的可证明改变

必须区分“减少输入义务”和“某个 LLM 成功率提高”。前者可以在这里证明，后者需要经验数据。

设一个持久关系图生成可逆仿射系统 Ax=b+Bu；u 是设计控制，x 是派生施工量。核心可计算

[ x=A^{-1}b+A^{-1}Bu. ]

实现用成熟分解/求解，不显式计算逆矩阵。A 固定时可复用分解；初始关系及其构造定义保存于模型。在一个明确要求展开赋值的接口中，若改动 k 个设计控制会改变 s 个施工数值，更新这些数值需要提交相应 s 项赋值；在关系接口中只需提交 k 项控制修改，x 由核心重新计算。当 s>k，必填施工赋值严格减少；关系和稳定对象身份同时保留，修改可以重复进行。 这个结论覆盖所有满足条件的矩阵和参数，无须抽样枚举产品。

可接受修改还须处于构造的有效参数域，并满足身份绑定与检查条件；这些保证来自持久模型及实际构造/提交流程，不能单凭 A 可逆推出。域外或检查失败不提交。

不能隐去初始建模成本：若 AI 为一次任务手写同等规模矩阵，省下的坐标可能只是搬到了矩阵里。方案要求通用关系的数学定义由核心保存，领域组合可命名复用，用户只写该设计实际需要的对象与关系。既有参数化程序接口已经做到的自动传播也不算本方案独有收益。新的实施重点是把同一机制贯通可发现的关系、联合求解、持久修改与失败解释。

进一步，两个满足同一要求的实现可能有不同形状或后续行为，不一定可互换。仅有“存在某个实现”的投影不能证明安全隐藏。系统只可隐藏由已知语义确定的量，或根据已授权的设计目标/选择策略确定的量；仍有设计意义的自由度必须显式保留。用户锁定的工艺顺序、拓扑身份或接口位置不能被当作编译细节丢弃。

持久修改还有一个直接保持结论。令 d 为设计状态，L(d) 为上述可计算恢复算法生成的完整候选状态，q 为从该状态读取所保存设计语义的操作；q 不是从任意 B-Rep 猜意图。恢复时原样保存契约，因此 q(L(d))=d。若一次允许修改为 U(d,e)，则重新恢复后的设计语义满足

[ q\bigl(L(U(d,e))\bigr)=U(d,e). ]

对任意有限合法修改序列归纳，关系、控制量与身份继续按设计修改解释。这里的 L 限于已给出恢复算法且构造/检查通过的域；失败则事务保留旧状态。这保证了所述持久语义机制不必靠每次让 AI 重写施工过程维持。构造替换专题进一步以观察保持与双向编辑对应给出充分条件，并完成顺序切孔/批量切孔参数族的证明；它承担这里的 q(L(d))=d 本身不能承担的替换义务。

能力发现也有具体构造：同一关系定义包含输入/输出类型、单位、域、固定/开放角色、编译和检查能力。目录按对象类型与所需关系筛选，再按需展开参数和失败原因；使用可靠的类型兼容筛选时，类型不可能适用的项可排除，无法判定的项须保留或说明未知。这个结构消除“必须先读实现源码”的接口前提，但不宣称自然语言检索或 AI 理解已获完备保证。

22.6.1 可隐藏选择的充分条件与不可省略的信息

以下是本项目的条件推导，不是对当前程序完成形式化验证的声明。令 D 为源设计，S(D) 为合法实现集合，O 为本次承诺的观察集合（形状、接口、要求、身份，以及声明支持的未来编辑行为）。定义 x ≈O y 当且仅当所有 o∈O 都满足 o(x)=o(y)。带容差的检查可作为观察谓词，但不能直接用“距离小于 ε”定义等价关系，因为它通常不满足传递性。

核心无需唯一确定全部内部状态。它能够安全隐藏实现选择的一个充分条件是：S(D) 非空，且 S(D)/≈O 只有一个等价类；选出任意合法实现都保持承诺的观察。证明直接来自等价关系的定义，无须枚举实现。若有多个观察不同的类，源设计必须保留区分类的控制，或明确授权一种选择策略。若既无区分信息也无授权，程序无法知道设计者想要哪一类：两个意图具有完全相同输入，确定性程序必然给出相同输出，随机选择也不能保证符合二者。这是输入信息缺失，不能靠更强求解器弥补。

这不是要求运行时判定任意程序的观察等价。证明由已支持的组合规则及适用前提承担；无法建立时保留显式选择或报告未决，不启动“遍历所有实现”的算法。O 的范围必须随能力公开，不能声称覆盖任意未来编辑。

当前源码的对应边界是：RelationGoal 要求显式 goal；feasible 表示授权在已声明约束内选择一个可行实现，minimize 的 feasible-incumbent 也不承诺最优。二者均不证明解唯一，更不证明未声明的工艺意图受到保护。数值初值、Worker 缓存和遍历顺序不是额外授权。Realization 保存一次已检查的选择，使恢复不重新选择；它解决历史稳定性，不替代源设计的选择授权。这里不增设“必须唯一解才能提交”的限制。

因此，AI 原生接口的必要内容可由职责推出：对象及其稳定身份、要求与适用域、固定/开放角色、选解授权、观察结果与失败来源。派生矩阵、坐标展开、后端编号和施工调度不应成为普通关系任务的必填信息。首次定义新关系仍有不可消除的建模成本；成熟关系的展开由核心承担。可证明的收益是删除这些输入与维护义务，不是从公式推出某个模型的理解率。

这给出实施优先级而非新的功能清单：先让现有语义定义贯通发现、编辑、编译、检查、封存和公开读取；只有当前义务因实际资源成本无法交付时，才把局部性能优化提升为阻塞项。Worker 复用或更多解析数值成功，都不能代替尚未接通的语义边界。

22.7 复杂度与效率为何可以同时控制

采用固定编译流程：绑定类型与身份 → 按需展开定义 → 已知量求值 → 保留语义的局部消元 → 剩余问题分类求解 → 具体构造 → 实际结果与保持条件核验 → 原子提交。这是一条执行路径的阶段，不是新增八个框架。

1. 前向依赖图可在 O(V+E) 的图遍历工作内确定计算顺序；实际函数、几何和分析成本另计。不能把已知的全部量重新放入 NLP。
2. 环、共享变量和跨组件约束进入联合问题；独立子问题只有在边界条件及目标分解成立时才分开。稀疏矩阵保持稀疏，消元导致耦合变密时可以停止消元。
3. MILP 只承担已声明的离散决策；几何构造直接调用已有内核，不在布尔 builder 内外再包无边界搜索。求解失败保留语义原因，不能无休止重试。
4. 修改沿完整依赖传播。几何相互作用、查询成员变化、工况和分析参数都计入依赖；只按显式数值边传播不足以保证正确。
5. 已验证具体构造随修订保存，历史重放不重新搜索；只有新设计修改触发求解。AI 输入减少不表示机器可免除输出 s 个变化量所需的 Ω(s) 工作。

成本仍按

[ T=T_{发现与形式化}+T_{编译}+T_{求解}+T_{构造}+T_{检查}+T_{提交} ]

核对。该构造证明的是不存在“为通用表达而必须把所有任务变成一个庞大优化问题”的架构要求；它不证明任何实例都提速。§12.9 与 §12.11 的链式 QP 成本证据用于选择消元粒度，§12.10 另记录几何构造成本；它们不是完整 CAD 交互的端到端测量，不能用 n−r 小于 n 就宣称更快。MLIR 的多层表示与逐级 lowering是保留高层结构、再映射适用底层执行形式的成熟方法依据；本方案不因此引入 MLIR 依赖。

22.8 落地边界已经确定

职责	采用什么	Aira 实际需要实现什么
实体、曲面、拓扑与几何检查	现有 OCCT 8.0.1 内核	将设计关系的具体见证接到同一构造与检查；保留语义引用和生命周期
草图	唯一 PlaneGCS 1.2.0-aira.1	复用已接线的草图约束域与诊断
LP/MILP/连续凸 QP	独立 highs-js 1.15.3 / HiGHS 1.15.1	从关系生成稀疏模型、行到要求映射、增量更新及候选/证据核验；排除重复插件
非线性连续片段	CasADi 3.8.0 / IPOPT 3.14.19	生成对应符号模型与硬约束，回查实际几何；保留局部求解边界
AI 原生能力	既有 AI SDK 工具和原生 Interface	从同一语义定义派生发现、参数、修改与诊断，不另建 Agent 循环
持久模型与编译	演进现有 AMIR、编译器、断言与事务	实现上表翻译、已知/未知角色、保持条件、恢复映射和语义失效传播
时间行为与领域分析	§22.10 选定本机 OpenModelica / MSL 的方程与状态事件域	保留对象、连接、工况、状态/事件及结果依赖；不以此覆盖未实现的其他分析

这里选择的是 CAD 设计核心方案。§21 的来源先作为方法依据；为使实施计划中的时间行为与分析不止于空接口，§22.10 进一步选定 OpenModelica 本地 CLI 路线。OMPL、SimPy 不随之加入产品。工业设计平台可以保存、编辑并向专用分析系统提交确定模型；CAD 核心不需要把所有 CFD、结构、控制和排程求解器重写在内部。承诺某项分析须有实际后端、接受域与连接，不能由表达定理代替实现。

本轮复核当前 AMIR schema、装配求解和设计编译/保持流程：已有对象身份、操作契约、要求、装配关系及提交设施。当前装配函数把关系残差平方和交给 IPOPT，再检查关系误差，并不是通用关系编译器；不能据它的存在宣称本方案已经接通。实际改动位置与数学职责已经能对应，缺口是产品工程实现，不是再寻找一个万能求解库。

实施边界的进一步源码核查：候选控制器在求值前经 Core 固定 candidate.document 和 modelHash；修订身份目前未纳入施工见证身份。因此不能只在 AI authoring 层求解，也不能在 preview 后改写已冻结文档并继续使用原凭据。采用共享图求值中的关系块：源要求保持不变，选定结构、参数和具体构造形成封存实现（Realization）；其内容哈希同时进入验证绑定、修订身份与同次持久化。modelHash 表示设计语义，realizationHash 表示本次实际选定实现，二者分工明确；封存实现不含它将参与生成的 revisionId，避免哈希循环。历史读取使用封存实现重放与核验，不能再次求解选出另一个合法结果。实现步骤只维护在现有产品实施方案。

工业模块的实际边界：多体实现存在固定激励/载荷与无条件 success 的路径；空间搜索包含端点附近碰撞放行及仅采样的平滑结果；热流模型依赖管段名字、固定网格和固定迭代。这些源码事实不支持历史“通用工业分析已完成”的宣称。它们只能在明确模型前提、误差与真实检查下承担候选或限定近似，不能作为五类工业系统已经能仿真的证据。新核心计划必须让分析从真实对象与工况进入共同模型，替换假成功路径，不能只把现有类名登记到能力目录。

**复杂度、效率与通用性的最终平衡裁决：**把用户有意义的设计信息保留在持久语义层，把重复的施工计算交给编译器，把计算方法按数学结构分配给已有算法；完整构造能力保持可达，常用组合按需发现。正确性、身份和历史保持是硬条件；在这些条件下减少 AI 必填实现细节，再约束编译成本、稀疏度、加载与交互预算。不把多项未知收益任意加权后宣称求得了“全 CAD 完美最优点”。这是已确定、能落实到代码的工程选择，不再以未找到全局最优为理由停止实施规划。

22.9 完成审查与结论

用户要解决的事	本节交付的依据	可以作出的结论
降低 AI 操作负担	定理 B、§22.6 的控制量到施工量映射与持久修改	可计算施工量不再是 AI 必填项；不是成功率提升的实验结论
不丢通用工业表达	独立参照域、逐构造翻译、定理 A	保留该有限工程域的表达与行为，新增关系求解不迫使复杂形状模板化
核心只是程序，如何推导	明确建图、连接方程、仿射恢复与整数编码	所需推理可由程序执行，不需要内核自行发明语义
用数学而非遍历产品	任意规模仿射族、有限布局编码和结构归纳	按规则证明覆盖与正确性，不枚举飞机型号或每个尺寸
兼顾复杂度与效率	无环求值、分块保留、专用求解、成本分解	获得可实现的分工；没有把全 CAD 交给一个优化器
避免冗余库、允许突破	§22.8 的唯一职责与已有选型	成熟算法复用；创新集中在持久语义、关系编译和 AI 操作机制
研究必须独立落文档	本文及其中来源、推导和现有证据	研究按专题分篇并由总览统一索引，未新增产品实现或测试套件

本节完成一个具体架构在参照域 P 内的构造性可行性论证：保留工程描述的表达与行为，对明确数学域主动求得实现，共用一个持久模型与执行系统。 三项更强义务由独立专题补足，不倒改定理 A 的域：

• 工业覆盖证明定义独立目标域 Iμ 与显式扩展 Pᴵ，给出五类系统的逐构造翻译、组合及编辑保持；范围由建模规格 μ 明确。
• 构造替换证明给出观察与编辑模拟条件，以有限规则覆盖整个合法参数族；拓扑角色、工艺和分析消费者都纳入观察闭包。
• 工程有效性证明给出要求余量、误差传播、全时域包络与耦合判据，完成有限热网络及带外部物性前提的工程保证推导。

这些结果确定了实施所需规则与拒绝边界，不再以遍历整机或寻找全局最优为开工前提。当前产品接线、各实际模型的充分性及外部事实真实性分别核验；不能把形式翻译和条件定理写成所有现实整机已经合格。

本结论没有把当前 Aira 写成已完成产品，没有宣称任意自然语言都可自动生成整机，也没有把基础理论称为首次发明。自主突破的位置明确为：让持久设计关系成为 AI 与核心共享的可执行语义，由编译器承担可算法化的施工与修改工作，同时保住复杂工程的表达能力。

22.10 有限域条件的组合编译推导

本节固定接受域：有限数值域未知量与已知有理阈值的比较，经常量、not、and、or 组成有限无环图，作为有界仿射等式的激活条件。连续未知量比较、条件构造与非线性分支不由本结论覆盖。

对未知量 x 的有限域 {v₁,…,vₖ}，引入二值 bᵢ，约束 Σbᵢ=1、x=Σvᵢbᵢ。比较条件 x⋈q 的真值 z 定义为 Σ{bᵢ | vᵢ⋈q}。比较用精确有理数完成；重复数值成员允许多个选择位，但一选一约束保证 z 仍等于该数值条件的真值。没有对不同变量的域取笛卡尔积。

对二值子节点 a、b，引入每个逻辑节点唯一的二值 z：

• not：z+a=1。
• and：z≤a，z≤b，z≥a+b−1。
• or：z≥a，z≥b，z≤a+b。

and 的上界在任一子节点为零时迫使 z=0，在两者均为一时下界迫使 z=1；or 的下界在任一为一时迫使 z=1，在两者均为零时上界迫使 z=0。not 直接成立。由拓扑序归纳，每个节点的辅助值唯一等于源条件值；反过来，任意源赋值的真值扩展满足上述约束。因此投影回原变量后保持条件语义。共享子节点只编码一次，同一行中重复引用须累加系数，不能覆盖。

激活等式 z⇒(aᵀx=t) 由变量盒界推导 m≤aᵀx≤M。令 L=max(0,t−m)、U=max(0,M−t)，编码 aᵀx−Lz≥t−L 与 aᵀx+Uz≤t+U。z=1 时两式合为原等式；z=0 时由盒界恒成立。缺失有限行界时不能任意指定大常数，当前返回未支持。已知恒假条件直接省略行，已知恒真直接使用等式。

图遍历成本为 O(V+E)，逻辑辅助变量及行数为 O(V)。比较叶节点另需扫描其所引用单变量的有限域，成本为这些扫描长度之和；这不是求解复杂度的多项式保证。上述等价性针对精确数学编码；浮点矩阵及 big-M 的数值误差不享有该保证。HiGHS 只提议候选，Core 从候选原变量的精确二进制有理值重算条件和原等式，预算耗尽或非法图返回 unknown。仅凭浮点无解、求解状态或编码可行不能出具源问题不可行/最优证据。

实现采用共享条件 DAG 与等式对节点 ID 的引用；拓扑顺序、缺失引用和重复定义在 Core 核验。编译身份与数值核验身份随代码更新，历史结果不得绕过当前身份核验。静态检查和一次源编译→求解→独立核验→构造物化用于核对实现接线，不以追加工业案例代替本节归纳推导。

22.11 条件构造的需求求值

给定已核验候选 x，构造 c 的存在性由其条件 g(c,x) 决定。先对全部条件求值，再仅对活动集合 A(x)={c | g(c,x)=true} 收集输入表达式和物化节点。未活动构造的输入不属于本次求值义务；例如被排除分支里的除零不应使活动设计失败。活动分支的未定义输入则必须拒绝，不能以条件构造为由忽略。

构造输出的可用性是单独的静态义务：消费 c→p 必须满足 g(c,x)⇒g(p,x)，公开输出视为无条件消费者。链接器以消费者条件为真作为假设，传播已知布尔事实：not 双向反转；and 为真向两个子节点传播真；or 为假向两个子节点传播假；子节点确定合取/析取值时向父节点传播。字面量提供固定事实。每条规则都保持假设下必真的事实，因此推得生产者条件为真即为蕴含的充分证据；假设导致矛盾则消费者不可能活动，蕴含真值为空真。推不出不能算蕴含不成立，仍以 availability-unproven 拒绝；不另建 SAT 求解器。单次假设闭包中每个表达式至多入队一次，每条逻辑边访问常数次，成本 O(V+E)，不枚举布尔赋值；缓存最近消费者的闭包以限制内存。沿构造 DAG 归纳，活动消费者的每个已接受生产者也活动，物化顺序因此不会产生悬空输入。运行时仍复核实际活动集合，缺失来源不能封存为有效结果。

这允许可编译的有限域条件构造参与同一候选求解，取消“未知构造条件一律阻止求解”的旧限制。活动输入通过同一 Core 候选表达式求值器按需计算，使用相同源、变量快照及数值身份；地址、条件值与实际节点仍进入同一 Realization。此结论不声称静态蕴含判定完备；分支输出选择另按下一节的规则组合。

22.12 分支输出选择的组合规则

源配方新增 {select:{condition,yes,no}}，condition 引用 Bool 表达式，yes/no 递归使用同一配方语法。它适用于构造输入与公开输出，不引入新的几何执行器。选择不更改源设计，只改变本次 Realization 中的绑定。

设当前路径前提为 Γ，选择条件为 g，目标类型为 T。两条静态义务分别为 Γ∧g 下 yes 可用且符合 T，以及 Γ∧¬g 下 no 可用且符合 T。每一输出引用要求路径前提蕴含生产者的存在条件，沿用 §22.11 的可靠但不完备传播。对普通构造输入，两支的 literal/port/list 绑定类别还须被锁定端口接受。未选中支也必须具有合法类型和引用，不能把一次运行没有选中当成静态正确性证明。数量按量纲与语义比较，几何输出按锁定模块的值类型匹配；列表内容的完整结构仍由实际模块 Schema 检查，不将本规则冒称所有聚合类型的完备推断。

运行时先求得条件真值，再只沿被选中配方收集数值需求、解析输出引用。由 g 的真假互斥且完备，加上两条分支义务，可推出已支持且检查通过的选择总有一个合法结果；对嵌套选择按配方结构归纳成立。未能求出条件真值时返回未完成，不猜测分支。准备与物化现在共用按路径收集器：仅请求当前可达选择条件，同层缺失条件批量交给 Core；未知父条件停止该路径，候选确定后再恢复。每个访问的配方计入预算，重复条件读取缓存，不因等待条件而重复扣除同一配方的预算。未到达的嵌套条件不触发数值域检查，到达后的错误仍必须拒绝。所有分支仍接受静态引用、类型和可用性检查；惰性求值不允许隐藏非法源结构。配方遍历不展开变量赋值，Core 调用轮数受所达选择层数约束；每轮 Core 的类型/表达式工作另受现有预算限制，不将跨批次重复分析成本宣称为零。

公开输出最终指向所选物化节点，条件值、节点集合、输入及输出映射进入同一封存块。源、候选、数值 Core 和编译身份必须一致，重放重新执行同一选择规则并比对封存块。此处不额外保证两条几何分支拥有相同面边身份；跨分支拓扑对应仍须满足构造替换专题的独立条件。

22.13 非线性执行与设计验收的分工

定义性 law 精确成立，工程容差由原 assertion 拥有。因此 IPOPT 的 tol 只能是数值停止条件，不能改写 law 为带隐式偏差的等式。非线性路线必须分成：源表达式与单位编译、局部候选生成、源域及原要求独立验收。不存在精确可交付浮点解时，局部收敛不构成交付；允许偏差应由设计者在工程要求中明确表达。超越函数的非平凡结果仍需要可信包络，不能拿 Math/求解器的一个浮点值代替。

真实需求是把连续标量目标、变量界及约束界交给已有优化器，复用依据为锁定 CasADi 3.8.0 的 SX.sym/vertsplit/算术算子、nlpsol 的 x/f/g 和 x0/lbx/ubx/lbg/ubg，以及现有装配求解中的 load_nlpsol(‘ipopt’) 与显式 delete 生命周期。已证实差异是现有装配入口只接受刚体配合，不能直接消费关系标量 DAG；不是求解算法缺失。决定增加标量问题编译适配，复用同一 CasADi/IPOPT 运行时，不引入第二个 NLP 库或自研优化器。

当前标量执行器接受拓扑有序算术表（常量、变量、取负及四则运算）、连续变量初值/界、目标和行界。索引只能引用已构建值，先检查规模和初值定义域，再建 SX。求解产生的有限数值仍只标记 unverified，即便状态为 Solve_Succeeded；不出具不可行、最优或唯一性结论。同步优化阶段的强取消仍依赖既有 Worker 生命周期，入口信号检查不冒称能够抢占正在执行的 WASM。

源关系现按数学结构分流：已有线性片段仍交 HiGHS；仅含连续闭区间变量、已确定活动 law/构造且所有待编译项属于支持算术片段时，编译为连续算术表。下述结构化凸二次片段交同一 HiGHS，其余支持的算术表交 CasADi/IPOPT。两种后端共用 relation-solve Worker 的超时、取消与销毁边界，按分支加载依赖。离散混合、非光滑选择、超越函数、严格连续边界和未解析要求不因接入后端而获得准入；退化初值导致的求解失败也不能推断无解。

凸二次分流依据结构推导，不依据工业案例或数值特征值猜测。令仿射表达式为 aᵀx+b；允许目标由仿射项、仿射平方、凸项相加、减去仿射项、非负常数字面量乘凸项或正常数字面量除凸项组成，所有约束行必须仿射。对该语法归纳，目标可写为 f(x)=d+cᵀx+Σᵢwᵢ(aᵢᵀx+bᵢ)²，wᵢ≥0。因此 Q=2Σᵢwᵢaᵢaᵢᵀ，任意 z 有 zᵀQz=2Σᵢwᵢ(aᵢᵀz)²≥0；线性项增加 2Σᵢwᵢbᵢaᵢ，常数项增加 Σᵢwᵢbᵢ²。仿射约束 l≤aᵀx+b≤u 化为 l−b≤aᵀx≤u−b。该等价性在算术表的实数解释下成立；源到浮点算术表的误差仍遵守下段候选/验收分工，不宣称浮点矩阵与源精确可行集相同，也不由凸性推出可行、有界、唯一或已取得最优证据。

实现位置为 relation-quadratic.ts：同一引用的仿射乘积识别为平方，目标共享 DAG 逆拓扑累加权重一次，不展开变量赋值或复制表达式树。系数支持集合的合并和每个平方的非零外积仍有实际成本，外积最坏为 O(k²)，不能宣称一般线性复杂度；20,000 次工作预算、非有限系数或不支持语法使专门化放弃并交既有 NLP。有限行界平移溢出同样放弃，只有原有的开界保留无穷。该语法是凸 QP 的充分识别条件，未识别不代表非凸；整数变量不进入此连续表，不形成 MIQP。

复用依据为锁定 highs 1.15.3 的 ModelData/HessianInput：目标采用 offset+cᵀx+0.5xᵀQx，triangular Hessian 使用下三角 CSC，列内行号唯一且有序。上述 Q 不再乘 0.5；模型创建、时限、候选读取和 finally 释放统一走 relation-highs-model.ts 的 runRelationHighs，不增加求解库。原始关系与端口等式仍由 Core 独立验收，feasible-incumbent 只交付受检候选；certified-gap 缺证据仍不能交付。实施验收只需核对这条生产分流、原谓词检查及共同封存链是否实际接通，不用不同产品名称重复验证凸性。

编译论证分两层。首先，在精确数语义下，对源 DAG 的拓扑序归纳：叶子由 Core 归一到同一单位，未知量一一映射列，派生变量引用其定义；取负、加减乘保持对应值，除法仅在分母非零的定义域内保持对应值。因此活动 law 的左右差、原要求的测量值和目标可对应到同一算术表，遍历按可达节点进行，不枚举变量赋值。其次，交给优化器时常量、界和运算转为浮点近似，不能据此声称精确可行集相等；该表只负责生成候选。数值转换超范围明确拒绝，除法奇点或局部失败保留为失败/未知，不做全局判定。

联合连续问题复用同一编译器，并额外需求连接所用的生产者表达式。合并时分别给变量列和表达式索引加偏移，局部引用先后关系不变；由上述拓扑归纳，每个局部表达式的含义在合并后保持，再追加消费者辅助列减生产者表达式等于零的行。单一显式目标原样映射，未声明的多个目标不合成权重。表达式仅拼接一次，不展开变量赋值；候选恢复仍用来源键。运行时复用 CasADi/IPOPT，验收逐节点用 Core 检查原谓词，再以同一候选检查全部连接等式，之后才恢复原始消费者并封存。当前支持局部表达式有序的连续四则算术片段，节点间标量等式可组成反馈；非有理精确交付、混合整数非线性和未知分支选择不由本次拼接获得保证。

准入重新以候选的精确 binary64 有理值代入源表达式，由 Core 重算 law 与原 assertion 的测量、上下界和显式容差，再检查原变量域；不使用优化器残差或容差作证明。接受蕴含源要求成立的论证依赖现有 Core 精确算术、源类型/单位校验及检查器正确性，并非整个实现已形式化验证。非有理结果保持未知。要求 certified-gap 的目标在缺少最优间隙证据时明确留作 pending，不能降级成 feasible-incumbent。验收值进入已有物化、封存和重放链；此处建立的是点可行性，不是全局最优、解存在性或预算内必能求解的保证。

22.14 联合块的分解条件：有向无环不等于可独立求解

跨关系节点的数值端口不能仅有类型声明。当前 prepareRelationGraph 已对尚未消元的数值标量端口生成编译快照中的辅助未知量，并保留原节点及来源映射；共享候选求值将生产者表达式与辅助量的等式合入同一线性问题。该接线目前受构造 DAG、已支持线性或连续算术片段和明确单目标条件限制；标量反馈按 §22.16 的完整候选及封存见证处理，混合整数非线性和未知输出选择仍未闭合。仅给端口补一个显示单位或把上游局部解改为常量，不补足这项语义。

反例可直接推导，无需运行试验：上游声明 x∈[0,1] 并希望最小化 x，下游声明 y=x 且 y≥1/2。有向引用只有上游→下游，强连通分量全是单点；若先固定上游局部最优 x=0，下游无解，但整体可行且整体最小 x 为 1/2。故 SCC 只识别有向反馈，不能证明独立优化或独立可行性。下游失败不能提升为源设计整体无解。

正确分解的充分条件来自可行集乘积：将每个约束与其依赖的未知量关联，先展开跨节点标量端口定义，使用 (源节点 ID,局部变量 ID) 标识未知量。每个关系 law、变量域、原要求和活动选择条件都属于约束；依赖必须沿源表达式闭包传播，不能只看端口直接指向的节点。在所有约束可分入互不相交的未知量集合 X₁…Xₖ 且边界输入固定时，有 S(D)=S₁×…×Sₖ，各块可行点组合当且仅当整体可行。证明由每个约束仅涉及一个 Xᵢ 逐项代入得到。未知量—约束无向关联图的连通分量提供保守分块；已知量可以前向消去，含义不明的隐式几何/物理依赖不能当作不存在。建立关联图和分量遍历为 O(V+E)，表达式展开须保持共享 DAG，不能复制展开为指数大小树。

这个条件只证明可行性分解。若宣称最优，还须证明全局目标可按独立块分解且采用明确的目标组合策略。多个源节点的目标不能未经授权相加、任意设权或以节点遍历顺序建立优先级；不同量纲相加尤其不合法。没有声明组合策略时，跨节点目标冲突属于未完成的契约，不能通过实验猜测用户偏好。certified-gap 仍需针对同一全局目标的证据。

实现顺序据此确定：先定义跨节点端口的表达式替换与目标组合契约，再形成共同未知量和约束关联块，复用现有问题分类、候选生成与原要求核验，最后将同一联合候选拆回各源节点的封存片段。源节点名称不是求解边界；拆回必须保留跨块输入绑定及共同候选身份，不能把来自不同联合解的局部片段混合恢复。当前实现以未消元标量端口连接组件作保守联合块，尚未细分到约束关联的最小分量。循环数值关系与循环几何构造需分别判定，不能为了接受前者而绕过后者的依赖正确性；现已分离完整语义依赖与构造排序，数值反馈进入联合方程，几何循环仍拒绝。

已知输出消元先复用现有前向依赖顺序与 Core：若生产者源求值证明输出为固定有理数或布尔量，并可通过 materializeRelationScalarsJson 精确往返为同类型常量，则在消费者的编译快照中替换端口。已确定的 select 仅沿选中分支展开；同名义类型的已绑定常量输入可直接转发。这个替换由“对所有源合法赋值，输出均为同一值”得到，不依赖生产者候选、最优点或求解顺序。原源引用与生产者的要求仍保留，所有关系仍须完成检查才可交付；常量替换不是跳过生产者的许可。非终止小数不被浮点近似，依赖未知量的输出不进入此路径。现有接口尚不能物化的精确值继续未解析，属于表示/绑定缺口，不属于已证无解。

22.15 联合 IR 的名称、端口与已知性约束

联合 IR 使用结构化来源键，不把用户字符串拼接后当成全局身份。变量键为 (sourceNodeId, variableId)，表达式键为 (sourceNodeId, expressionId)，两类键具有独立种类标签；端口键为 (sourceNodeId, outputPort)。即使两个节点都声明 x，也默认是两个未知量。序列化使用规范 JSON 元组；后端稠密列号只由排序后的键集合派生，列号不是持久身份。必须保留反向列映射以恢复源候选和诊断。不得改变源局部 ID 来迁就联合矩阵。

数值连接采用边界等式。若消费者 B 的输入 p 指向 A 的输出 q，输出 q 的源语义为 f(X_A)，引入有类型边界量 u_(B,p)，加入 u_(B,p)=f(X_A)，B 中 input(p) 读取此量。多个消费者可引用同一输出表达式 DAG，不递归复制生产者源树。几何对象端口仍属于构造依赖，不能据此变成可供数值优化器任意赋值的标量。

语义保持分两个方向：任意源合法赋值可扩展为 u_(B,p)=f(X_A)，满足所有边界等式；任意满足联合约束的赋值，按来源键投影并删除辅助 u，即满足原端口连接及各节点约束。因此在表达式定义域、类型、单位和活动条件保持一致的前提下，辅助量引入不增加或删除源解。对已知输出，§22.14 的精确消元是此等式的特例。对于数值反馈，等式可以成环，但每个局部计算表达式仍须有合法求值顺序；不能将循环直接展开为无限表达式树。

必须重新检查跨节点已知性。现有 RelationSystem 的 fixed 值、unknown 的域端点与初值要求不依赖未知量；局部 input 节点本身不能证明全局已知。若端口绑定后这些项依赖联合未知量，应在其源位置拒绝该用法，或通过明确的新语义将它改写为联合约束，不能把一次上游候选当作常量绕过原契约。原 assertion 的验收标准同样保持独立，不得随着联合候选变化而变宽。允许的“已知”来自源依赖证明，不来自节点排序。

目标先保留为带来源键的向量，不提前生成任意加权和。一个联合块只有一个 minimize 目标且其余均为 feasible 时，该目标可直接交现有后端；多个 minimize 目标须等正式的优先级/权重/其他选择契约给出后才能生成对应优化问题。每个目标的单位和 accept 条件随来源保留。所有 feasible 目标只合并约束，不凭空创造最优化要求。当前线性合并器实现这一规则，多个 minimize 或 certified-gap 无证据时拒绝，不把返回的可行候选声明为经证明的全局最优。

失败诊断沿相同来源映射恢复到源 JSON 路径：编译阶段给出相关节点、分类与待编译项；缺少目标组合或间隙证据指向各源 goal；候选检查的变量、law、原要求和连接键分别映射到原变量、关系、assertion 或输入端口，辅助列不成为用户需要猜测的变量。candidate-rejected 仅表示该候选未通过，unknown 表示当前证据不能完成判定；二者均明确 infeasibility:not-proven。只有单独核验的无解证据才能改变后者，求解器状态码、超时及精确残差本身不能证明源设计无解。

22.16 联合候选的恢复与交付顺序

局部检查通过不能推出跨节点连接成立。联合结果必须先按 §22.15 的列反向映射恢复完整候选快照，严格检查来源键集合、重复/缺失/多余列及有限数值，再处理局部节点；不能边获取某个局部候选边提交或替换其它节点。后端列号、完成顺序和上一轮缓存不能成为变量身份。

编辑也使用同一原子边界。现有原生计划以 edit-relations 的非空 edits 数组提交完整节点定义及可选完整输入映射，每个源节点只出现一次；外部绑定省略时保留，提供空映射时清空。所有 node.put 与要求修改组装为一个 Patch，在同一源快照上求值，只生成一个提交，不先保存半个关系系统。原单节点 edit-relation 入口已退役，单节点编辑同样使用一个元素的 edits。公共输出声明不在本操作中更换；控制角色在各定义中修改，独立 Parameter 的编辑仍使用其既有契约，不能冒称本操作可同时改变任意文档对象。

对于无环数值连接，可以在同一候选快照下沿源依赖计算生产者输出，使用 Core 精确求值和单位转换生成消费者绑定，然后以这些绑定与对应局部候选重新检查原 law、域和 requirements。只有所有局部检查与端口连接检查均通过，才可物化构造并封存。形式上，各局部谓词的合取还必须加上每条连接的相等谓词；删去后者就允许生产者输出与消费者使用不同数值。全局目标的验收条件也必须单独核验，不能从局部可行性推出。

现有 DesignRealization 已把完整源 modelHash 与所有关系块哈希绑定在同一实现根中，无需再创建平行的修订或提交机制。对于可从源和完整局部候选唯一重算的边界值，不增加一份可独立变化的缓存权威。重放读取全部封存局部候选，重算同一边界绑定并比较局部 boundNodeHash，最终核对同一实现根；不能重新运行优化器。每个哈希都须由相应内容重算，哈希字符串本身不能恢复丢失的绑定值。

循环数值连接不能仅沿 DAG 恢复，但不一定需要新增见证结构。核对当前 RelationRealizationBlock 后，variables 以外的 outputs 已保存物化后的 typed 标量字面量：每条连接的辅助值可由其生产者封存输出取回，与全部局部候选一次组装成完整快照。恢复先检查原始变量键集合、有限值、边界字面量名义类型与规范单位，再由 Core 重算所有原谓词和端口等式，并将重新物化的每个生产者输出与原封存字面量作规范哈希比较。转浮点只生成待验候选，不能证明与字面量精确相等；比较不一致必须拒绝。由此不依赖节点遍历次序、不重新求解、不新增一份边界缓存权威；既有实现根仍绑定所有块与源。

此恢复机制的辅助列不进入源编辑或局部持久变量。图准入按两种关系区分：完整语义图保留每个源引用，用于修改传播、来源和要求独立性；构造排序只对执行依赖取拓扑序。两个 design.relationSystem 之间、引用已注册非布尔数值输出的直接标量 PortRef，由联合边界等式承担，不要求生产者先执行。列表、几何、实例/放置、普通程序和其他引用不适用此规则。若两个节点之间同时存在数值与几何引用，几何执行边仍保留。

这个区分来自执行职责，而非对任意循环的豁免：标量连接的正确性由完整候选下的等式核验建立；构造读取已核验数值后才执行，不能再次搜索。Core validate_module_nodes 仍逐项校验所有引用，只对构造依赖检查环；工作台保存 inputFeatureIds/dependentFeatureIds 的完整语义边，以 executionInputFeatureIds 决定排序。要求标准的未知量传播继续沿完整语义边走带 visited 集合的遍历，不能因排序边被去掉而丢失依赖。物化后的执行投影仍须满足普通构造 DAG；方程循环不授权几何自依赖。数值反馈接线状态与实操证据见现有工作进度，不能仅从此图规则推断所有循环可解。

22.17 备份恢复的并发提交条件（2026-09-21）

备份验证与真实存储更新是两个不同阶段。设导入开始时当前会话 head 为 h₀，验证得到备份 B，最终 IndexedDB 写事务 T 读取 head h。安全条件是 T 内 h=h₀ 才允许写入 B 的修订、证据、资源、历史与新 head；否则 T 中止、全部记录保持不变，原 Session Core 不替换。新建隔离验证存储使用 expectedHead=null，含义是仅当分支不存在才可建立，不能作为无条件覆盖开关。

证明来自同一对象存储集合的读写事务串行性和原子性：并发提交若先于 T 完成，T 的读值改变并拒绝；若 T 先完成，并发提交自身的 expectedHead 核验负责拒绝陈旧更新。事务外验证耗时不影响该次序，因此不需要猜测延时、禁止其他会话或用验证时的一次查询代替事务内比较。比较使用导入开始的会话 head，不能在验证结束后读取新 head 并把它冒充用户已接受的覆盖前提。仍不把导入自动变成分支合并。

共享 importPortableProject 已捕获初始 Core head，AiraProjectStore.importProject 必需显式预期 head，storage-portable 在任何写入前于同一读写事务核对并复用 REVISION_CONFLICT。候选替换 Core 只发生在导入事务成功后；失败会释放预建的新 Core。Chrome 中以真实第二会话在验证后/写入前提交，确认冲突不覆盖持久 head、修订、补丁、证据及资源，也不替换原会话。匹配预期 head 的备份仍在禁止 Worker 下恢复封存结果。核验比较排除每次新生成的 exportedAt，因其不是持久状态；不因时间戳差异修改产品数据。此并发边界验收结束，不据此声称全部 UI 撤销重做或初始源文档求值已完成。

22.18 源状态与已封存历史的区分（2026-09-21）

历史恢复的前提是目标修订已有选定实现。初始源修订 parents=[] 没有候选证据与 Realization，公共读取已将其标为 source-unevaluated，修订列表也标记不可恢复；因此不能把它当作“缺失见证时允许重新求解”的特例。恢复算子 replay(D,W) 的 W 缺失时没有原选择可保持，即使源关系只有一个数值解，也不能据此伪造旧几何、检查或原授权。

共享 proposeRevert 对具有 restoreRevision 的适配器在创建候选前拒绝源目标 REVERT_SOURCE_UNEVALUATED；其余历史目标必须加载原证据，不落入普通求解。WorkbenchHistoryManager 初次恢复撤销栈时只收集已知且非源的祖先，未知祖先处停止；从源状态产生首次提交时不把源加入 past。此规则与已有修订列表和公开读取一致，未更改源文档内容，也未伪造初始见证。它不提供“首次生成结果等同历史恢复”的承诺。

对已封存状态，undo/redo 仍使用同一个 append-only 回退事务，成功后才接纳导航状态，再安装对应求值；失败维持 head 和导航前态。Chrome 实际运行产品 LiveWorkbenchHistoryManager、原生 Session 和几何执行，完成已封存关系编辑的一次 undo/redo，核对两侧 Realization 身份、撤销/重做可用状态及源目标拒绝，期间禁止创建 Worker。UI 上下文回调承接真实求值，但未执行 DOM 按钮点击，因此不能将该结果写为完整 UI 交互验收。该控制器接线核验结束，其他历史/并发及工业能力义务仍按计划保留。

23. 效率目标、架构重审与候选几何复用的条件推导（2026-09-28）

本节重新比较职责分配，不以 §22 的既有裁决、现有 Schema、SDK、工具表或实现投入作为最优性的证明。旧结构可以整体替换；必须保持的是明确的设计语义、几何与工程正确性、授权、原子性及当前历史恢复，而不是文件名或类的边界。下文是条件推导与源码支持的实现方向，不是全 CAD 最优定理或实测加速报告；实施顺序和状态仅由既有 GitHub 计划维护。

23.1 优化对象是完整设计行为

一次合格交付包含从独立需求出发的发现与形式化、候选探索、求解与构造、检查、提交、后续编辑和恢复。成本向量至少记录人的决定与返工、AI/后端费用、端到端时延、峰值内存、持久数据及恢复成本。硬条件先于成本比较：丢失未来编辑语义、跳过检查、放宽容差、减少失败分母或取消必要恢复，都不是效率提升。

给定需求与编辑分布 R、支持域及设备 E、总预算 B，比较满足同一验收义务的完成率与成本分布；不同用途可以选不同 Pareto 取舍。权重或主目标必须来自产品需求，不能在看到结果后调整。减少 AI 必填施工量可以按 §22.6 推导，AI 实际错误率和总任务收益仍须独立验证；Jev/Laya 只能作为待比较的语义判断组件，不预设它们进入每次编辑的关键路径。

不能把“任何任务、设备和工作负载下都最快”作为已获证明的结论，具体阻力包括：

• 首次一次性构造可能以直接程序最便宜；大量局部编辑可能值得支付依赖追踪与缓存成本。冷启动最小和长期会话最快不必由同一配置实现。
• 显式交付 s 个变化对象本身需处理其输出；懒物化可以推迟未请求对象，不能把实际输出的工作量算成消失。若查询具有全局耦合，一次局部参数改动也可能影响全模型。
• 减少未知量不必减少计算：消元可能把稀疏约束变密；前向可执行不等于逆向可高效求解；离散拓扑、结构选择与非凸约束不能统一当作一个光滑低维优化问题。
• B-Rep、网格与隐式表达保留的信息和支持的操作不同。某表示的布尔或渲染便宜，不意味着满足精确引用、工程交换及未来编辑的总成本最低；转换与误差检查必须计入。

这些是选择需要明确前提的理由，不是以“没有统一最优”拖延裁决。对当前明确的任务域，可以选择有充分语义保证、可计算成本及可证伪收益的实现。

23.2 最少必要信息来自未来行为，而非最少字段

令设计状态为 d，承诺观察集合为 O，支持的编辑语言为 E。把编辑拒绝、失败和观察作用域也计入行为。定义 d₁ ≡ d₂：对每个支持的有限编辑序列 w，两者具有相同的合法性，并在各自执行 w 后给出相同的 O 观察。数值容差使用明确的检查谓词，不直接将“距离小于 ε”当作可传递等价关系。

必要信息命题。 若某权威编码 R 把行为不同的 d₁、d₂ 编为相同值，则仅依赖该编码和相同编辑输入的确定性实现不可能正确恢复二者的全部承诺行为。证明：选择使行为不同的编辑/观察，解码器获得相同输入，只能产生相同输出，因此至少一个不符。随机猜测也不能保证同时正确。

这里比较的是必须保持的完整观察语义。若契约仅授权“任选一个合格实现”，两个合法结果集合不同却有交集，并不足以证明必须补充意图；不相交的可接受行为或明确锁定的不同编辑规则才形成上述冲突。授权选择与封存结果可消除实现自由度，不能把“存在多解”变成“任何提交都必须再问用户”的规则。

例如同一圆板上的孔目前位于相同半径，但一项设计保持孔心半径，另一项保持孔边到外缘距离；板径改变后必须不同。因此单独保存当前 B-Rep、网格、隐式场或截图不足以恢复这项区别。反过来，命题不要求保存全部施工历史：若在声明的观察和编辑语言下两种构造等价，历史顺序可以作为派生实现被替换；用户指定的工艺顺序若属于观察，则不得删除。

由此得到的是信息义务，而非固定数据结构：必须保存能区分支持行为的对象身份、关系/编辑规则、固定与开放量、适用域、要求、选择授权及必要来源；能够从这些信息唯一导出或由明确策略选择的矩阵、坐标展开和施工顺序不应成为重复权威。关系图、参数化程序和带设计约束的直接模型都可能满足义务。不能据此声称存在通用可计算的“最短设计编码”，或让运行时判定任意程序的全部未来行为等价。

AI 负责尚未给定的设计选择、开放构造提议和语义歧义；核心负责已定义语义下的推导、计算、检查和事务。新关系的首次形式化成本不可凭架构消除。只有当关系定义、适用域及验证方式实际存在时，才能把其施工推导从 AI 转交核心。

23.3 四条实质路线及裁决边界

路线	如何形成和修改设计	可建立的保证与优势	反例、未知及淘汰条件
A：显式参数化程序／特征计算	源程序规定构造和依赖，编辑源参数后增量执行	支持域内的前向语义明确；复杂已知构造无需搜索；已有良好参数化程序可自动传播大量施工量	开放输入变成未知量时可能需要重新编程；显式程序不自动提供逆向求解。若每次关系变化必须由 AI 重写大量施工及引用，不能作为该关系任务的默认接口；不能把它已有的参数传播算成新关系架构独有收益
B：全局关系／能量／隐式求解	保存约束或目标，把形状及结构作为待求状态，求解后物化	在声明数学域内可以交换已知/未知角色，联合处理耦合目标；专门场或优化任务可能避免冗长构造序列	已知构造也被迫进入搜索会增加成本；局部最优不是全域正确；拓扑离散、奇点和隐式到精确交付转换可能主导成本。若无法保持原域、引用与失败语义，淘汰其作为通用唯一执行方式，但不否定适用的局部求解
C：直接精确模型＋显式编辑约束	直接选择对象/面并修改，保存必要保持规则及关联信息	对导入体与局部几何修改可避免重演长构造历史；效果可直接检查	仅存当前几何会违反 §23.2；拓扑改变后如何保持角色和未来规则必须补足。新增设计约束是必要语义，不能称无需历史便无需意图；无可靠映射时拒绝或显式重绑
D：可编辑设计语义＋按需编译和物化	保存必要语义，按请求消费者与数学结构选择直接构造、局部求解、直接编辑及派生表示	可保留 A/C 的确定构造，只有实际未知量进入适用求解；未请求的派生结果可延迟；完整依赖下可复用未变计算	编译、依赖追踪、失效与资源所有权具有真实成本；错误读依赖会伪造缓存正确性。若不能说明具体省去的工作，或成本超过收益，应收缩/替换该机制；“混合”不是自动最优的证明

裁决：以 D 的职责分工作为当前可实施方向，将 A/C 作为有明确语义的构造方式，B 作为明确问题域的求解方式；不维护四套竞争的产品执行器。 选择理由是它可保留必要的持续编辑信息，同时避免把所有任务强制改成搜索或历史重演；这一包含关系不证明 D 的任意实现更快。它允许替换当前图表示、Schema、Agent 调度和求值组织，不将当前 AMIR JSON 形状作为永久上限。

多层 lowering 的方法依据是 MLIR 官方设计理由：保留高层结构再映射目标执行形式；这不要求引入 MLIR 依赖，也不把其性能结论转移到 CAD。构造等价搜索可借鉴 egg 官方说明，但只能在具有 CAD 域、失败、浮点及未来编辑保持前提的规则内使用。低成本表达式提取不证明曲面拓扑等价、现实计算成本最低或饱和搜索有界；本方向不以增加 e-graph 框架作为前置条件。

23.4 按需物化的内容身份、依赖和证据

对派生计算 f，定义完整输入签名 K，覆盖 f 真正读取的设计值/单位、查询及其成员集合、选择策略、构造/形状身份、配置、版本、运行和容差条件。集合查询还需成员增删及“原先不存在”的依赖：新增零件可能改变“所有零件无碰撞”，即使旧显式引用一条没变。未知依赖只能保守失效，不能按普通 DAG 后继闭包冒充完整语义依赖。

在 f 的声明域内具有确定语义、K 完整、缓存内容未变且资源仍有效的前提下，K’=K 足以复用 f 的值。若 f 是检查，还须保持其完整命题、检查器版本、证据域和外部事实有效性；缓存未知不会变成通过。此结论来自相同函数与相同输入，不来自“看起来一样”或“hash 字符串相同”本身；身份须从所声明内容建立和核验。

必须分开计算内容身份与当前使用资格：候选与 Revision 不同，几何计算内容可以相同；当前 actor、授权、task/head、接受来源、证据期限和提交资格仍需验证。可以复用几何值或检查事实的有效载荷，再由同一证据构造机制绑定新上下文；不能缓存整份授权 certificate 后换 revision 字符串。关系的求解块按约束、共享未知量和目标耦合建立，不把节点 SCC 当作数学可分解性的证明。

若旧执行集合为 V，必须重新执行的集合为 A，只有省去的 V\A 计算成本超过依赖维护、签名、查询、重绑定及额外内存成本，才有实际效率收益。可证明少调用若干 builder/solver，不由调用数直接推出毫秒、p95 或 AI 成功率。恢复零次优化也不等于零次几何重建。

Acar、Blume、Donham 的自调整计算论文证明了其语言语义下的记忆化与变化传播一致性；它说明正确增量计算需要语义条件，不替 Aira 证明原生句柄、副作用和几何缓存正确。OCCT OCAF 官方说明提供文档事务与修改管理设施；不能据这些设施存在就推断 Aira 已完成上述生命周期或复用。

23.5 第一条纵向突破：受检候选到已提交几何的复用

对研究时的源码（Git 基线 f9935a3d）作有界核查：几何图执行对 candidate source 选择 OCAF abort（exact-feature-graph.ts），原生文档的 begin 禁止重叠 command，commit 要求图完成，析构会终止未完成 command；缓存模块已经有 restoreCleanFeature、reidentifyCachedResult 及 artifact graph 重绑定。因此问题不是“新增 DAG 缓存”，而是预览得到的受检构造是否能跨提交边界安全进入同一派生缓存，省去提交后的重复 builder 工作。相应源码：图执行、缓存与身份重建、原生事务。

通用设施直接复用锁定的 OCCT V8_0_1（commit b8f597c677811d1f9f4d8a97f5ae2825c0353a42，见构建锁）及现有绑定的 NewCommand / CommitCommand / AbortCommand；Aira 的差异职责是持久提交与派生文档之间的所有权、身份和失败结算，不是另写事务或几何算法，也不要求新增依赖。

候选复用的充分条件。 候选源内容、封存 Realization、完整几何输入与运行绑定不变；候选结果及 topology/history 映射未被后续写入改变；所有权和句柄仍有效；最终权限、task/head CAS、接受来源及验证有效性成立；复用对象能通过同一当前 Revision 结果/证据构造机制产生合法身份。则没有必要只因候选变为 Revision 而重新执行相同 builder。证明分两部分：完整内容相等使同一确定构造的值不变；新的提交检查和身份构造建立其在当前 Revision 下的使用资格。两部分不能互相替代。

上述为完整目标的充分条件，不是当前实现已具备全部条件的声明。首个构造缓存复用切片只处理派生几何生命周期，不能因此宣称任务/head 联合 CAS 已实现；设计任务与接受事件的原子关联仍由 #365 定义。普通几何复用须保持原有提交保护；依赖任务语义的新自动接受能力须等待其必要保护闭合。

最低风险的首个实现可以只晋升构造缓存：成功候选保留一个有界 pending OCAF command；持久提交成功且随后 Revision 请求的源/实现/运行身份精确匹配，才把该 command 纳入派生缓存，后续仍走正常的 Revision 求值、检查、SemanticRef/history 核验和证书生成，由已有 clean-feature 路径复用实体。它不复用旧许可，也不承诺跳过网格化或全部检查。若完整结果直接晋升能满足更强条件，可以另据事实选择，不能反过来要求首批实现所有证据复用。

这不是把 abort 改成 commit。OCAF 与 IndexedDB 不构成一个跨系统原子事务；必须明确两阶段生命周期：

1. prepare 阶段保留隔离/可回滚的候选与旧 committed 基线，不把 pending 派生状态公开为已提交状态。候选准备执行和权威执行可能不止一次，只有完整受检阶段的结果可进入复用判定。
2. 持久事务最终检查当前 head、适用的任务版本、候选及接受绑定，原子保存权威修订与证据。若失败或冲突，abort 候选并继续原基线。
3. 持久成功后才发布/结算派生缓存；若 native finalize 或显示安装失败，权威模型已经提交，应废弃不可靠派生状态，从真实持久 head 重建并显示恢复未完成。不得谎报未提交、再次提交或伪称全部回滚。

所有可能操作同一 OCAF 图文档的 native evaluate 入口都须处理 pending：不同候选、读回、历史恢复、导入、超时、取消和 Worker 销毁不能越过所有权协议。不访问该图文档的独立 STEP 检查等操作不必仅因运行就丢弃候选。单 pending 与清晰失效路径是可用的有界策略，不要求为每个文本假设复制一个 OCAF 文档。若资源约束或原生副作用无法保持旧基线，应停止该复用方式，选择隔离上下文或原有正确重建；“未发布”不授权破坏当前撤销、重做与恢复。

23.6 反例与停止条件

反例	必须执行的保护／它否定什么
预览后只修改用户意图，模型 head 未变	适用的任务版本仍须最终检查；几何相同不使旧接受有效
同一 source 新增装配成员或改变检查范围	查询成员/负依赖使对应检查失效；仅数值参数相同不能复用全局检查
Worker 重启、句柄已释放、借用 shape 被原生算子修改	原生缓存不能直接晋升；封存历史可恢复但仍需重建/核验
candidate source、Revision source、history 或语义引用上下文不同	使用真实缓存拓扑及共同身份构造机制重建绑定；无法证明映射时正常重算，不能字符串换名
持久提交失败，或提交成功但 native finalize 失败	分别保留旧 head，或恢复真实新 head；不可把两个结果都叫“已回滚”
为保留候选使峰值内存、取消响应或长会话资源超预算	释放或拒绝保留；builder 次数下降不能抵消资源退化

这一突破的可证伪收益是：在身份与输入相同、资源有效的实际 preview→validate→commit→readback 路径上，减少重复的几何 builder 工作，同时保持所有适用检查、来源与历史行为。验收应分别观察 builder/求解调用、复用数、重绑定/检查成本、真实几何、失败原子性及端到端资源；不以 evaluate API 调用次数代替内部成本。若发现来源错绑、陈旧提交、释放错误或检查被跳过，先恢复正确执行，不能放宽条件制造命中率。若收益小于缓存维护及资源成本，停止该优化而保留已经确立的语义边界。

本节作出的裁决是“按完整语义区分必要信息，以实际依赖和生命周期减少重复工作”。它支持自主重构整个执行组织，也要求每次替换说明同域语义和具体省去的计算；不以新架构名称、更多模型或更少代码代替结果。

24. 通用 AI CAD 的整体架构裁决（2026-10-02）

研究对象是完整 CAD：人或 AI 表达目标、定位对象、探索、构造、修改、组合、交付与恢复。裁决采用统一持久设计语义、可组合能力与关系编译、按数学结构执行、同一人机决策协议。Jev 候选绑定是其中的局部语义机制；它不定义 CAD 的表达上限。本节统一此前核心、交互与模型研究的职责，不增加第二套模型、执行器或研究完成所必需的实验任务。详细证明沿用 §22、理论 §18 与通用性 §20。这是架构选择，未将现有实现声明为完成。

24.1 通用的定义与选择准则

目标域由有限可计算的工程描述、几何/拓扑表示、装配连接、带单位属性、要求、编辑和误差契约组成，不按产品类别建立一套执行管线。几何、物理行为与工艺可以组合，但模型充分性、材料和工况证据须分别声明。结构化保存一段物理描述不能替代分析能力。

先满足语义、授权、几何、原子性及恢复义务，再减少从需求到交付的人的必要决定、AI 施工推导、机器计算、等待与返工。没有任务分布、损失和成本模型，不能计算唯一数值最优架构；以下给出明确的责任结构裁决及其原因，不用这个边界推迟选择。

可表达、可检查、预算内可求解是三个不同域。 扩展能力不得把其中一个域的增加冒充另两个域的完成。用户的开放目标不受一次模型调用的候选数限制；某个任务未找到方案也不等于已证明无解。

24.2 权威信息由未来编辑决定

设计状态至少保留以下语义类别；这不是永久固定的 JSON 字段表：

语义	必须承担的职责
对象、实例、连接与端口	稳定身份、装配层级、坐标系、材料/工况适用对象及组合边界
参数、关系与要求	单位、定义域、固定/开放量、硬保持项、目标优先级及选择策略
构造与表示	显式程序、关系定义、直接编辑和导入资产；B-Rep/网格/隐式等表示类型与转换误差
编辑及引用规则	后续修改应保持什么；来源、拓扑角色、允许的重绑和失效语义
来源与使用资格	用户观察、提议、接受/授权、外部事实及其版本；不能从模型结果倒推接受

待决任务保存尚未落实的观察、解释和选择，指向同一设计语义；它不独立拥有几何。封存实现保存本次实际选择的结构、参数、程序、构造及必要运行资源，与源设计绑定。聊天、缓存、AI 工作上下文和 UI 均是派生投影。

必要性由 §23.2 的可辨识性证明给出：若两个状态当前同形，但同一未来合法编辑要求不同结果，权威编码不能合并它们。充分信息不要求全部施工历史；可按已证明的编辑保持规则替换构造。由此允许关系图、参数化程序与直接模型共同表达，不把现有 AMIR 布局作为上限。

导入形状作为有来源和表示契约的设计输入。缺少原始意图/历史时，明确缺失；用户可添加新的保持规则，不能声称恢复了唯一原设计。导入、转换或特征识别不能自动获得无损、唯一引用或未来编辑保持保证。持久引用绑定资产/实例、来源及选择语义，通过真实 history/角色映射和查询解析；裸句柄/下标不能承担身份。面积、法向、邻接等描述只作筛选证据，不保证不变或唯一；零个/多个合法后继时保留失效/歧义并重绑。

24.3 五项共同职责与唯一执行路径

flowchart TD
  U[用户或外部 AI：文字、选择、笔画、参数、程序] --> I[原生 Interface：同一能力与交互契约]
  I --> T[当前任务：观察、待决解释、授权与目标]
  T <--> D[持久设计语义：对象、关系、构造、保持规则]
  T --> C[信息依赖协调：读取、判断、生成、沟通]
  D --> K[能力绑定与关系编译]
  C --> K
  K --> E[直接求值、专用求解、几何与行为执行]
  E --> P[隔离候选、实际差异与检查证据]
  P --> T
  P --> A[当前资格与原子提交]
  A --> R[源设计、封存实现及 Revision]
  R --> D

1. 设计语义保存必要意图、编辑与组合规则，是模型权威。
2. 能力定义及编译将类型、前提、关系、效果、读写范围、诊断和执行关联起来；原生 Interface、内置 AI 与 UI 从同一权威获得契约。
3. 执行复用既有适用的几何、草图、线性/整数与非线性设施，按真实问题结构分工；通用算法选择沿用库选型，本次不引入后端。
4. 交互及协调处理仍缺什么信息、哪些任务可并行、何时展示/询问以及哪些旧结果失效；模型只产生有来源的提议或判断。
5. 提交与恢复核验当前状态、授权、必要不变量与证据，封存实际结果；未知写入先读回，历史读取封存实现。

这些是职责，不能据图机械增加转发层。所有提议汇入同一产品执行与事务路径；原生能力不依赖预装技能、源码、鼠标或私有索引才能发现和使用。内置 Jev/LLM 可替换，CAD 契约仍成立。

24.4 构造、关系与直接编辑怎样统一

对已形式化要求 d，见证 w 包括结构、数值、构造、几何及其语义绑定，求满足 R(d,w) 的实现。已知值直接求值；可可靠消元则消元；真正的未知量才进入对应求解；缺少构造时才生成程序或扩展搜索。 多解按明确授权的策略选择，有设计意义且未委托的分歧留给交互协议。

一个与产品名称无关的计算推导：一致实数线性关系 Ax=b、rank(A)=r，n 个变量的解可写为 x=x₀+Nz，其中 Ax₀=b、N 的列构成 ker(A) 的基、z∈Rⁿ⁻ʳ。原不等式 Hx≤h 转成 HNz≤h−Hx₀，原域和目标仍按 x₀+Nz 保留，恢复映射一一对应可行解。例如六个变量的四个独立关系留下两个自由度，核心承担其余量的恢复；未授权的两个自由度不因消元而获得偏好。实际浮点秩判定与证据域须另行明确；稠密化、整数域或非线性分支不能被该推导删掉。

参数化程序可以保存关系和自动计算，关系系统也可以物化精确 B-Rep；不能据名称将它们分别判为高输入负担或不准确。被排除的是强制所有请求提交施工见证、强制已知构造进入全局搜索、或者只保存几何而丢失编辑规则的责任安排。

能力组合要保留前提、单位、身份、误差、域与未修改部分。顺序程序在支持片段按前后条件组合；联合关系保留交集而非逐步锁死某个解。例如 A 允许 x∈[0,1]、B 要求 x=1，联合问题可行；先永久选 x=0 不能代表联合求解。仅输出类型能连接不足以证明组合成立。

新复合能力可由既有规则/程序组合，必须保留其契约和展开。新增原语、检查器或领域模型需要真实定义及适用边界，AI 写下名称不能创造执行能力。已知前向程序不自动可逆；复杂自由形状、拓扑改变和非凸问题不承诺通用高效反演。单项能力契约可概括为类型/端口、前提、关系/效果、保持项、读写与资源域、诊断及展开；接口从该定义派生。只有可执行/可检查定义实际存在时，才由核心承担相应推导。

精确实体、网格、隐式场和曲面采用显式表示语义；权威属于设计描述，派生表示按消费者需要物化。误差、拓扑、引用或交换要求无法保证时，拒绝该转换或保留未知，不能因“精度优先”将全部工程对象预先排除，也不能将视觉近似冒充精确实体。

派生表示不会自动回写其来源。B-Rep→网格→拟合曲面通常非单射，几何距离界也不保证拓扑、身份或未来编辑保持；采用回写/替换必须显式满足这些独立义务。可保留源表示并单向派生渲染/分析数据，避免无必要的往返同步。

24.5 开放意图与鼠标操作的共同协议

沿用交互研究 §3–§4：观察/引用、意图、授权/采纳和工程证据分别记录。 当前选中对象只提供空间指代；范围、引用过期、面分裂/合并和候选/已提交身份须解析。修改范围与候选接受遵循入口的明确操作契约。

焦点 F、允许的语义效果 A、候选实际效果 E(c) 与读取依赖 D(c) 是不同概念，数值上可相同或重叠。必须核验 E(c)⊆A；A 包含授权契约明确允许的参数传播/派生影响，不能将所有读取对象自动纳入可写范围。选中实例不自动授权修改共享定义及其全部实例。实际效果无法界定时，不能凭预测扩大作用域。

若仍有依据的解释 θ 的允许动作集合 A(θ) 有交集，可在交集中合法推进；交集为空的关键分歧需要增加信息或展示可撤销候选。有限候选不证明穷尽所有意图。因此仅凭模型高分不授予正确性或权限，自动选择须有适用域与已授权自由度。

宽泛目标先结合已知保持项，形成带假设的局部方案并展示实际变化；提问围绕改变结果或允许动作的缺失信息。用户可拒绝、继续探索、改目标或改对象，系统保留未知并使相关旧结果失效。澄清屏障阻止受影响的提交，共同合法读取和隔离预览仍可继续。

当前同形而未来规则不同的候选，优先展示一个有区分作用的合法未来编辑及实际结果，而非仅展示当前几何差分。扰动必须在声明域内；随机微小扰动可能看不出分歧。不能形成几何预览时，可给出规则差异/有依据的符号结果，并说明缺少的能力，不能捏造图形结果或强制所有沟通经过预览。

信息量下界也限制自动理解：若有 N 个必须区分且未委托的互斥结果，固定二进制编码最坏至少需 ⌈log₂N⌉ 位。点选、预览、文字或授权默认均可提供信息；该式不规定界面按钮数、对话轮数或 token 数。

24.6 Jev、生成模型、程序与人的推导分工

LLM 与 Jev 是互补的协作组件。 LLM 提供开放推理、设计分解、构造与沟通；Jev 将当前有依据的局部语义问题变成程序可组合的判断。LLM 的提议可形成 Jev 的判断对象，Jev 的结果也可为下一次 LLM 推理提供选定解释、相关材料和待解决分歧。它们共享同一任务与来源，由协调器按信息依赖组织反馈；判断不自动成为硬约束、用户授权或工程事实。

协作可发生在生成前、生成中与生成后：先从已有状态判定相关对象/解释再生成；对同一已知状态的独立判断与必要生成并行；生成新增候选后进行有针对性的语义比较，再将结果反馈给后续构造或沟通。缺少判断所需状态时先读取或生成，不能把存在答案依赖的问题伪装为并行。两者的判断能力可以重叠，生成调用已能顺带完成的判断可在该调用中承担；额外 Jev 调用应有明确的决策作用。不存在强制的固定串联或互相评分循环。

尚缺的内容	责任
已定义运算的值、几何事实、引用解析	程序/核心计算，不重新生成已绑定量
有依据候选中的自然语言含义与角色	Jev 的有界判断；不完整时允许无匹配、扩展和未知
新解释、分解、关系组合、程序、解释及问题措辞	生成模型提出缺失内容，再由同一能力与核心处理
当前信息不能推出且未委托的设计取舍	可信用户决定；模型不能代替授权来源

此分工符合 TypeSafe 构建指南：代码拥有控制流、确定规则与副作用，模型提供结构化语义判断。一次调用的问题有界不限制整体设计语言；候选由读取、解析、能力检索、关系编译及必要生成持续扩展。模型输出置信度不是工程错误率或权限证明。置信度定义

凡不能证明候选覆盖需要决定的域，保留无匹配/域外出口和继续读取、扩展、开放表达或未知的路径；不强选最高分，也不把所有低置信度无条件转成用户问题。分别处理候选缺失、判断不确定、外部证据缺失与未委托偏好。用户可自由修订需求，不受固定问卷约束。

用户给定 Jev 在适用判断中更快、更便宜，故优先在这些位置使用；准确性与完整性条件先于这个偏好。设计不固定模型调用比例，也不强制每一步都调用两个模型。比例由任务中的缺失信息和有效结果复用决定，缺少开放构造时必须保留生成职责。

24.7 大规模图、长设计链和并行的计算边界

对 N 个实例形成的装配森林，局部变换 T_i 已知时，世界变换 X_i=X_parent·T_i 可按拓扑序计算，矩阵维度固定时为 O(N)。修改使 k 个已请求世界变换改变，完整依赖下传播成本为 O(k) 加查询/追踪成本；输出这些改变本身需要 Ω(k)。闭环连接或全局干涉会增加联合条件，不能据森林计算公式声称整个装配求解线性。

一般关系块保留共享未知量、硬约束及目标耦合。仅当边界变量已固定且条件可行集为乘积、目标可分解时，局部问题才能独立求解再组合；分离最优解集合与完整 Pareto 前沿还须对应目标语义。SCC、任务 DAG 或 AI 问题能同时提问均不证明几何可分。等价消元会导致稠密化，应比较计算与恢复成本，不机械最小化变量数。

重算集合 A 来自完整依赖，包含参数、查询成员增删、原先不存在对象、可见性、单位、规则/后端版本和有效外部事实；未知依赖保守失效。候选内容可复用，当前授权、task/head 与提交资格重新核验。只有省下的计算超过追踪、签名、查询、重绑定与驻留成本才有总收益，参考 §23.4。

长期过程保存查询可恢复的设计/任务与原子检查点，模型只持有有界相关工作集；缺少必要事实时继续读取，不让压缩摘要替代权威。并行 worker 在绑定版本上返回提议及依赖；同一协调器在合并点处理冲突、联合要求和原子提交。声明分步事务的任务保留检查点；承诺单次原子编辑的任务不能偷拆成多个已提交步骤。

head 改变不必丢弃全部计算，但候选必须以当前源重新绑定。只有完整读取/查询依赖、写入及保持语义、外部事实和授权条件仍成立，才能复用结果并经同一路径建立新的候选资格；存在写冲突、引用变化或未知依赖时重算、重绑或保留待决。不以显式读集与新改动不相交作为自动语义合并的充分条件。

若第 i 次受控决策确有适用错误上界 ε_i，则 P(至少一次错误)≤min(1,Σ ε_i)，无需假设独立；只有满足独立/对应条件概率时才可使用乘积可靠性。即使假设每步正确率 0.999 且独立，1000 步全对概率约 0.368；这是数学示例，不是 Jev 实测。封存状态、检查与恢复缩小错误后果，不能声称消灭语义错误、保证无限长链成功或把置信度当 ε_i。

24.8 正确性、未完成设计与失败的出口

核心保证是条件性的：在语义绑定、编译/构造规则、检查器适用域及提交不变量成立时，提交满足相应设计契约；几何合法不推出用户意思被正确理解，更不推出现实产品适用。 对可重算实现保存本次封存结果，撤销/重做不重新咨询模型或重新选择解。

结果区分经核验的实现、声明域内已证不可行、信息不足、能力不支持、预算内未知与取消。求解器局部失败只描述该候选/尝试；模型生成缺失、引用失效和工程检查失败分别提供可恢复诊断，不自动放宽硬要求。

未完成设计可以按明确草稿契约保存/提交，但安全、几何及事务的必要不变量仍成立，未具备的工程证据保持 unknown。几何有效性依表示与对象类型判定：开放曲线、曲面和欠约束草图并非天然非法实体；失败的 solid 构造不能静默改名为合法 solid。待求源语义可持久保存为未实现状态，保留已有有效实现与新候选的身份区别。若某工程要求是本次交付的硬前提，它未知或失败就不能宣称完成该交付。用户确认偏好不能替代载荷、材料或分析证据。

24.9 明确裁决及替代方案边界

选择上述统一设计语义与专门化执行，理由是同时保留未来编辑信息、已有确定构造、导入体局部编辑、联合未知量与开放能力组合，并让全部人机入口共享相同承诺。程序/特征、关系求解和直接编辑均可作为该语义下的实现方式；某一方式已能承担全部相应职责时，不为名称另建等价层。

这项选择不要求所有 CAD 任务经过优化器，也不冻结单一几何表示、工具目录、Schema、Agent 或求解器组织。编译和依赖追踪有成本；局部已有参数化程序可直接执行。承诺的通用性是按明确定义的规则族、表示与组合保持建立覆盖，扩展时增加真实语义义务；详见通用性证明及工业构造覆盖。不能以所有产品逐个试用作为作出架构决定的前提。

并行研究与交叉质询中的以下过强建议没有采用，原因构成最终裁决的一部分：

建议或主张	反例/推导与裁决
必须自动判断所有未来编辑等价，故应将整个 CAD 限制为仿射编辑	信息保持命题不要求运行时判定任意程序等价；保留明确源语义，只有具有证明规则的替换才自动采用。一般等价性不可判定不排除一般程序表达。
依赖不交且空间不交是合并的充要条件	正交编辑仍可能违反总质量等全局要求；重叠的 x/y 平移也可能交换。可复用与合并需完整语义条件及当前联合检查，不使用该充要条件或无必要的合流框架。
全局要求必须分配局部松弛预算；超过某改动比例必定全量更快	全局总和可通过合法聚合增量更新；成本分界取决于真实算法、数据与维护成本，不存在由比例单独推出的通用阈值。保留整体检查及直接重算路径。
浮点检查必有某个正漏检率，长链成功率按多个错误率相加后连乘	无给定事件、检测域及条件概率不能推出该率；重叠错误不能直接相加作为精确概率。采用声明前提的可靠性界，不把任意比例或确定性当正确性证明。
至少三步、特定候选数或某种几何表示即可证明架构优胜	这些阈值不能由责任推导得到。选定职责结构允许直接求值，具体性能与体验收益不冒充已证明结果。

由此同时回答“为什么选择”和“哪些反方理由成立”：保留必要编辑信息与单一权威成立；关系全能、唯一范式、指纹自动稳定、参数不交必可合并及模型分数替代真值均不成立。组合与引用的定义负责结构保证，具体模型的经验准确率不会反向充当架构证明。

对原有研究的修正是层级与统一性：核心决定保存什么、怎样组合和编辑；交互决定怎样获取不可缺少的意图；模型协调决定怎样高效形成有依据的绑定和提议。三者联合设计，Jev 的局部候选编译不能单独充当完整 CAD 架构。实现与经验结论仍分别由既有计划/issues 承载，本节不另建状态或验收清单。