关系编译、证据与几何算法

研究总览 · 2026-09-20

数学变换、求解保证、证书、增量生命周期和几何构造的技术条件。

• 5. 关系编译与混合求解的完整设计
• 6. 不可行证据：生成、核验、修复与复用
• 7. 增量求解、生命周期和事务
• 9. 几何底座与检查边界
• 13. 安装板算例与适用域

5. 关系编译与混合求解的完整设计

5.1 编译器输出应包含什么

每条约束保留 requirement ID、对象角色、单位、原始表达式、使用的近似方向、参数域和行映射。输出片段分为：精确线性约束、离散结构约束、连续非线性约束、只能在实际几何上检查的谓词。

正式的源 AST、SolveIR 数据形状、类型/作用域规则、来源映射和完整 JSON 示例由关系编译器工程规约定义；本节保留算法依据，不再并列维护一份结构定义。

同一数值关系只送到一个适用求解器。涉及欧氏距离、旋转或自由曲面时，编译器先判断接受域，不能依赖后端抛异常来判定模型类别。

直接消去固定变量、共享相同表达式、对等距关系使用参数化表达，例如 (x_i=a+ip)，可减少变量和病态冗余。单位缩放必须同时变换约束和证据来源；不得将显示单位与物理数值混淆。

5.2 结构语法

语法描述组合规律：行数、各行数量、对齐/错排相位、允许方向、有限节距集合、对称关系、操作的类型与连接方式。孔数由计数约束守恒。语法有显式规模上限，避免把无界程序枚举伪装成有限求解。

HiGHS MILP 处理线性的结构决策。使用 big-M 时，M 必须从已声明的有限变量域推导；没有合法界就不得构造一个随意的巨大 M。对于少量结构分支，可以由同一控制器按确定顺序生成条件问题，但不再另写一个整数优化器。

候选优先保持当前结构，然后尝试满足要求的变化。LLM 可以建议结构或修改候选排序；它不能自行确认证书或放宽硬要求。该控制器是同一工具内部的数值规划职责，不是另一套 Agent 循环。

5.3 圆孔错排的内外近似

任意圆孔净距条件：

[ (x_i-x_j)^2+(y_i-y_j)^2\ge D_{ij}^2,\quad D_{ij}=r_i+r_j+g_{ij}. ]

这是非凸圆外区域。固定水平差 (\Delta x_{ij}) 与上下顺序后，条件成为：

[ y_b-y_a\ge c_{ij}=\sqrt{\max(0,D_{ij}^2-\Delta x_{ij}^2)}. ]

用有理数 (L_{ij},U_{ij}) 包围根号，并通过精确平方关系核验。内模型使用 U，外模型使用 L：

[ F_{in}\subseteq F\subseteq F_{out}. ]

内模型中的已核验可行点可以接受；外模型的已核验不可行证据可以排除。内模型无解、外模型可行时，按确定精度预算细化界；仍未决定则进入声明的非线性域或返回 unknown。不得用内模型无解证明真实模型无解。

这里的 F 必须对应带用户容差的实际验收域，而非未放宽的名义尺寸。允许剪枝的必要条件是 (F_{accepted}\subseteq F_{out})。例如允许距离至少 8.999 mm 时，可用距离 8.9995 mm 的设计可以接受；证明它不能达到名义 9 mm 不能排除该设计。设计容差、求解器数值容差、几何测量不确定度分别记录；求解器容差不修改用户要求。对测量区间，只有全区间满足要求才判 pass，全区间违反才判 fail，其余 unknown。不能证明编译模型与最终验收域包含关系时，该模型只用于提案，不用于宣告产品需求无解。

转成 (Ax\le b) 时，外模型右端为 (-L)，内模型右端为 (-U)，不能把方向写反。若放开水平节距，旧固定骨架的证书不能覆盖新连续域。

5.4 数值求解与实际几何分工

IPOPT 使用 g/lbg/ubg 表达硬约束、lbx/ubx 表达变量界、f 表达软目标。当前装配实现的 sumsqr(residual) 及后验检查不能直接复制成“任意设计硬条件”的编译器。CasADi 官方 NLP 接口

先做廉价必要条件与数值检查，再调用几何内核，减少明显无效的 B-Rep 构造。求解器输出仍须经过实际实体检查；不将求解坐标复制为新的要求来自证正确。

接受范围、求解停止阈值、浮点表示与测量误差分别服从数值交付规约。该规约给出数据结构、区间三态判定、NLP 量纲缩放、退化处理及候选失败与全域无解的不同结论。

5.5 按数学结构控制总成本

剩余问题的性质	本方案路径	控制复杂度的边界
固定值、已知对称/等距关系、可证明的单调区间	参数代入、结构参数化、解析判定	在声明的结构域内保持等价；本来开放的自由度不得悄悄删除
仿射关系及线性目标	HiGHS LP；同结构优先更新数值和 basis	通用线性消元与 presolve 交给上游，不再写一个简化 LP 内核
固定离散结构、线性约束、连续凸二次目标	同一 HiGHS 的 QP	不扩张成非凸 QP 或 MIQP 承诺
整数选择与仿射关系	同一 HiGHS MILP，或预算内有限条件问题	所有分支都有明确含义；不把一次局部失败当全域排除
无法安全消去的显式非线性关系	CasADi 稀疏 AD + IPOPT 局部 NLP	硬约束显式建模；局部失败为 unknown；拓扑黑盒不伪装为可微表达式
只能由实际几何判定的性质	OCCT 求值与对应检查器	先做合法廉价筛选，仍保留最终实际验收

关系编译器只维护类型/单位、变量依赖、少量有依据的参数化规则、近似方向和检查映射。避免为每个零件模板写特例，也不引入通用 CAS/SMT 重写系统。一般线性预处理、矩阵排序和数值分解继续复用后端。分段展开、枚举和表达式展开设规模预算；无法在预算内降低总成本时，保留原关系送适用后端，或返回明确的能力/预算边界。

不能盲目全局消元。已知关系中的直接代入通常便宜，但消去共享变量可能使多个原本稀疏的约束相互耦合。应保留有助于稀疏性的中间变量；局部分解必须纳入共享变量和跨区检查，不能只按几何对象分组。可借鉴 iSAM2 的增量稀疏分解研究中的结构与更新成本意识，不能据其 SLAM 结果宣布 CAD 性能，也不因此再引入 GTSAM。符号稀疏结构与导数优先使用 CasADi 现有设施。

证书缓存同样有成本门槛。以一次查询的摊销成本表示，只有预期节省满足下式时，性能上才值得启用：

[ p_{valid}T_{avoided}> T_{lookup}+p_{candidate}T_{check}+T_{maintenance}+T_{generation}/N. ]

这里有效命中概率不大于候选命中概率；N 为生成成本可摊销的查询数，尚未观察到的概率不能当成已知收益。只计入真正避免的计算。缓存收益不足可绕过缓存并正常求解，不能绕过最终正确性检查。所选 HiGHS 的增量 LP 实测中位仅 0.5313 ms、P95 1.17 ms，复杂语义匹配和大整数核验可能比重求更贵。因此同结构连续修改首先复用数值状态，跨大量结构重复出现的冲突才考虑证据复用；Stitch 离线压缩不进入每次求解的必经路径。

5.6 自由度、消元与稀疏性的平衡

设一组等式为 (g(x)=0)。在可行点附近满足恒秩等正则条件时，独立约束秩为 r，可行集局部维数为 n−r。这说明可以使用多少局部坐标，不说明采用最少坐标就是最快。只在单点测得 Jacobian 秩不足，不能推导实际自由度；例如 (x^2=0) 在零点的 Jacobian 为零，可行集却只有一个点。活跃不等式还涉及切锥，不能全当独立等式扣除。约束正则性讲义，§8.4–8.5

若 (x=(y,z))，并且局部独立约束的 (G_y) 可逆，隐函数给出 (y=\psi(z))，其导数为 (D\psi=-G_y^{-1}G_z)。剩余关系的 Jacobian 变成 (J_z=J_xD\phi)，其中 (\phi(z)=(\psi(z),z))。逆矩阵可能稠密或病态；局部坐标图也不自动覆盖其他解分支。对非线性 (\phi)，约化目标的 Hessian 还含 (\sum_i f_{x_i}\nabla^2\phi_i)，不能一般地只计算 (D\phi^T\nabla^2 fD\phi)。这些是消元需要携带适用域与恢复映射的数学原因。

一个能完整推导的同域例子是：

[ \min_{x,u}\frac12\sum_{k=1}^N[(x_k-t_k)^2+u_k^2],\quad x_k-x_{k-1}-u_k=0,\quad x_0=0. ]

保留 x、u 有 2N 个变量，Hessian 为单位阵，等式矩阵 (C=[D,-I]) 有 3N−1 个非零元，D 为一阶差分矩阵。按阶段排序的 KKT 矩阵有固定块带宽。完全消去 x 后，(x=Lu)，L 为下三角全一矩阵；未知数减半，但

[ Q=I+L^TL,\qquad Q_{ij}=\delta_{ij}+N-\max(i,j)+1 ]

完全稠密。由 (1\le\lambda_{min}(Q)\le2)，以及 (1+(N+1)(2N+1)/6\le\lambda_{max}(Q)\le1+N(N+1)/2)，得 (\kappa_2(Q)=\Theta(N^2))。相反，对上述无额外不等式的等式 KKT 矩阵，(I\preceq CC^T\preceq5I)，其特征值由 1 与 ((1\pm\sqrt{1+4\sigma(C)^2})/2) 组成，故条件数不超过 ((1+\sqrt{21})/(\sqrt5-1)<4.52)。这些是本例的直接推导；加 u 的盒约束后实际活跃集系统会变化，不能继续套用 4.52 的界。

这仍不能预判两种表示在 HiGHS 中谁快。稠密公式的特殊结构可以被利用，求解器自己的模型处理也有成本。§12.9 的实测恰好显示，在 N≤128 的这批实例中完全消元更快，虽然非零元更多、上述 Q 的条件数随 N 增长。因此“永不增加非零元”和“总是最少变量”都不成立。

中间选择是部分消元：每 B 个阶段只保留块起点 (s_b)，令块内

[ x_{bB+j}=s_b+\sum_{i=1}^{j}u_{bB+i},\qquad s_{b+1}-s_b-\sum_{i=1}^{B}u_{bB+i}=0, ]

第一个起点固定为零，最后一块按真实长度处理，不添加多余末端状态。变量数变为 (N+\lceil N/B\rceil-1)，等式为 (\lceil N/B\rceil-1)，块内 Hessian 存储为 O(NB)。这在变量数与填充之间提供连续的工程选择；它是既有凝聚方法的应用，不能称数学首创。Axehill，Controlling the level of sparsity in MPC研究的正是这类取舍；CasADi multiple shooting也说明增加辅助变量可能改善稀疏性与收敛。

本研究确定的编译规则：原始关系保留在 AMIR 语义中，数值表示只是可丢弃的求解视图。仅比较保留变量、直接代入、小块/部分消元这几类有限候选；一般 presolve 和数值分解交给求解库。候选先满足声明域内等价、单位一致、原变量及要求可恢复，再以

[ \widehat T=T_{compile}+\widehat N_{iter} (T_{evaluate}+T_{derivative}+T_{linear})+T_{recover}+T_{check} ]

及内存约束选择。迭代次数与缓存命中率属于经验估计；不能装成保证。结构模板的选择可在锁定环境下校准并复用，不要求每次交互重复求解所有表示。编译预算用完就保留可用表示，不递归发展成通用代数搜索器。参数化退化时回到原约束或其他适用坐标图，不能宣判原设计无解。

6. 不可行证据：生成、核验、修复与复用

6.1 精确核验的对象

规范化系统为有理 (Ax\le b)，有限上下界纳入行。标准 Farkas 证书满足：

[ \lambda\ge0,\qquad\lambda^\top A=0,\qquad\lambda^\top b<0. ]

HiGHS 的原生 ray 是数值候选，不是自带精确证明。普通 lam_a/lam_x 也不等于不可行 ray。HiGHS 提供状态、ray、basis 等底层设施；Aira 核验器只做有界的代数检查，不自研 LP 算法。所选 HiGHS 1.15.1 API

原生 getDualRay 返回原模型 num_row 个带符号数，不能直接当作规范系统的非负 λ，更不能先把负数删掉。双边行 (l_i\le a_ix\le u_i) 拆为上界行 (a_ix\le u_i) 和下界行 (-a_ix\le-l_i)。设恢复原行/缩放映射后的有符号候选为 (y_i)，有限尝试整体方向 (\sigma\in{-1,1})：上界行乘子 (\max(\sigma y_i,0))，下界行乘子 (\max(-\sigma y_i,0))。非零乘子对应的界必须有限；不存在的界不能凭空补出。随后才进行精确残差检查和变量界修复。若接口结果不能恢复到原模型行，拒绝候选。最终代数核验决定接受，不依赖猜测符号惯例。所选版本的 C API

数值表示必须明确：输入中的规范化十进制字面量按其声明语义转为有理数；求解器返回 binary64 乘子可以转为该浮点值的精确有理表示。不能静默乘一个倍率后取整。选择复用 Cargo.lock 已锁定的 num-rational 0.4.2 / num-bigint 0.4.8；目前它们只是传递依赖，不是已存在的产品证明 API。使用既有 Rust/WASM 构建边界中的 BigRational 核验，不再引入另一个 JS 分数库或自写任意精度整数。有理数 API

证据核验限制维度、非零数、位长和运行预算；超预算为 unknown。一般 OCCT 曲面并不因此变成精确有理数模型。

当前生产接线以无条件连续线性片段为首个接受域：仅 interval 连续变量、空 guards/pending、无 when 的等式及仿射范围。relation-highs-model 按 ranges 后 equalities 的原模型行顺序请求 getDualRay().values，返回前复制数组；取证仍在可终止 Worker 内，finally 释放模型。宿主在发送前复制精确问题，Core verifyRelationInfeasibilityJson 重新读取这份有理 IR，不读取已舍入矩阵，也不接受后端自行宣称的证明。范围行按乘子符号选上/下界，等式允许任意符号；逐项累加精确残差与右端，按 §6.2 使用声明界修复。两种整体方向共用 20,000 工作预算、既有 4,096 位精确数预算，零残差无需有限界。未取得射线、未建立严格矛盾或范围不支持均保持 unknown。

通过结果绑定完整 problemHash、rayHash 和当前 numericIdentity，保存非零行乘子、原 law/requirement 来源、修复所用变量界及正的有理矛盾裕量。单节点及联合节点均经同一原生错误协议报告 proven-for-bound-linear-problem，不产生提交；来源键映射回原定义或端口。它证明当前绑定线性问题没有实数解，因此不能交付该候选设计；没有证明其它参数、结构、整数搜索节点或几何/物理模型无解。改变源或数值身份后必须重新核验，不把旧结果直接当作跨参数学习规则；当前会话内的重新核验复用见 §6.4。没有射线时的辅助 LP 尚未接入，不以本段代替其余实施义务。

6.2 使用变量界修复对偶残差

将候选乘子精确转为有理数并将负分量截为零，得到 (\hat\lambda\ge0)。精确计算：

[ r^\top=\hat\lambda^\top A,\qquad s=\hat\lambda^\top b. ]

若 (l\le x\le u)，则：

[ r^\top x\ge m(r)=\sum_{r_j>0}r_jl_j+\sum_{r_j<0}r_ju_j. ]

而原约束推出 (r^\top x\le s)。故 精确验证 (m(r)>s) 即证不可行。等价地，对正残差加入下界行，对负残差加入上界行，可恢复左端精确为零的 Farkas 证书。

证明仅使用既有变量界。零残差维度不读取上下界，避免 0 与无穷界相乘。不能为了修复证书添加用户未声明的界；某一所需方向无有限界且残差非零时，该方法不能给出证明。此为 verified-LP 思想的应用，不主张原创。

6.3 原生射线与辅助 LP 的裁决

终态通过 highs-js 上游绑定使用同一份 HiGHS。默认请求原生 ray；没有得到可核验候选时，可以在剩余预算内求归一化辅助问题：

[ \min_\lambda b^\top\lambda\quad s.t.\ A^\top\lambda=0,\ \mathbf1^\top\lambda=1,\ \lambda\ge0. ]

原系统不可行时，非零 Farkas 向量可以归一化；辅助可行域紧且最优值负。最终核验不需要归一化或最优性，只需要证书条件成立。辅助失败/超时不是原问题无解。

这两种是同一求解库中的取证方法，不是两条模型执行权威。本次测量表明原生 ray 不恒定更快：presolve 先发现无解后，获取 ray 可能另解 LP。保留这一事实，不能以“直接 API”推导固定性能优势。

6.4 参数化证书

固定结构 (z) 下，若 (A_zx\le b_z(q)) 且 A 不随 q 改变，证书定义参数域：

[ G_\lambda={q:\lambda^\top b_z(q)<0}. ]

若 (b_z(q)=b_0+Bq)，这就是一个仿射不可行区域。A 改变时重新核验左端；根号外界随孔径变化时重新生成并检查界。缓存对象包括语义、单位、矩阵结构、行来源、前提和乘子；每次使用重新核验当前条件。

上述公式只适用于左端已经精确为零的完整证书。若通过 §6.2 修复，保存包含变量界行乘子的完整证书，或在每次复用时重算 (m(r;q)>s(q))。例如 (x\le-1,x\ge0) 无解，改成 (x\ge-2) 后有解；忽略界只保留第一行及负右端会误剪。临时固定的共享变量、局部信赖域和当前外部对象参数也属于证据前提，不能当作永久要求。

缓存查找采用结构化键和限定的角色槽位映射，不做无界子图同构。采用容量上限与收益淘汰；证书缓存可以完全删除而不改变模型语义或正确性。

当前连续 LP 接线采用原行顺序的角色键：numericIdentity、变量身份/类型/数量及非负约束、范围来源/表达式身份、等式来源。命中只是取回乘子的提示；不缓存可直接返回的 pass。每次在当前精确 IR 上重新计算全部行系数、界及 m(r)>s，因此即使系数改变也不能凭旧哈希或旧裕量宣称无解。通过时返回新 problemHash 和当前来源证据，未通过则丢弃提示并进入正常求解。由核验器的结论直接推出：增加此缓存不会把原本可行的问题判无解；缓存删除、冲突或淘汰仅改变取证成本，不改变模型语义。

relation-infeasibility-cache 当前最多保存 8 个最近核验成功的射线提示，键的 UTF-16 字节量加射线标量负载不超过 2,000,000 字节（不是对 JS 运行时总堆大小的承诺）；无全局图搜索、不保存几何或可提交实现。调用前快照源问题，取消后不更新缓存，核验耗时从随后 Worker 的可用求解时限扣除。Core 同步有理核验仍受工作/位长预算约束，不冒称毫秒级强抢占。该实现是带当前条件重验的会话内复用，不是离线生成完整参数区域、跨会话知识持久化或收益优化已完成。

6.5 允许哪些剪枝

已证不可行的二进制结构赋值 (\bar z) 可以形成 nogood：

[ \sum_{\bar z_i=1}(1-z_i)+\sum_{\bar z_i=0}z_i\ge1. ]

只有证明依赖更小的结构前提集合时，才能缩小该求和范围以排除更多结构。IPOPT 未收敛、B-Rep 构造失败、一次测量失败只能降低候选优先级或解释当前失败，不能直接生成永久剪枝。

局部问题在固定分隔符 s 后无解，只排除该 s 下的局部候选；除非另有覆盖证明，不能据此排除允许 s 改变的整个结构。尺寸变更后旧 nogood 也须重验其证书守卫，不能永久累积无条件禁令。

MILP 仅因整数性不可行时，其 LP 松弛可能可行，例如整数 n 满足 2n=5。不存在可证明其连续松弛不可行的 LP ray。本方案证明契约采用可核验的条件 LP 排除及有限结构覆盖；不宣称拥有一般 MILP 的独立完整证明系统。

7. 增量求解、生命周期和事务

7.1 持久句柄与增量矩阵

固定关系结构时保留 HiGHS model、稀疏矩阵结构、行/列来源和有效 basis。尺寸变化更新 RHS/bounds/cost；局部关系变化使用添加、删除、改系数接口。变量域、行集合和 basis 有效性必须由 API 状态与后验检查确认，不假设所有更新都可复用。

现有 CasADi conic 插件每次求解走 Highs_passModel；复用 CasADi Function 并不等于复用了原生 LP basis。研究也验证了通过同一侧模块 C API 的增量调用，但已有 highs-js 持久 API 可以直接满足需求，且避免 LP-only 冷启动加载 CasADi。最终只接 highs-js createModel 及其增量、basis、ray 接口；模型构造走数值稀疏接口，不反复序列化成 LP 文本。绑定实现

不维护 CasADi/HiGHS 第二条生产接入路径。研究探针的内存 Module._compile、LDSO 或 dlopen/dlsym 仅证明现有构件能力，不进入产品。Aira 只做语义行映射、会话所有权和调用适配；raw 指针、WASM table 与任意符号查找不对 AI/用户程序暴露。

句柄归属于一个受控 Worker 和一次模型会话。新修订或取消使旧结果失效；超时需要可实际中止 Worker 的边界，不能只在同步调用前后检查 AbortSignal。HiGHS/IPOPT 不能持有 OCCT 指针；只交换有类型数值与语义引用。进程退出不是产品释放策略。

原生数组分配和内存增长由上游绑定负责；Aira 不缓存跨调用的 WASM 内存视图。成功、异常、取消各路径统一调用模型释放方法；Worker 被终止后丢弃其全部会话引用。依据本次实验只承诺可复用 LP basis，不推导 MIP 搜索树或 QP 分解也会跨所有修改保留。

锁定 highs-js 中，createModel 持有原生实例，输入/输出数组为复制，修改原 JS 数组不等于更新原生模型；更新必须调用对应 API。dispose() 幂等，销毁后调用抛 HighsDisposedError，不能等待 GC 释放。run() 同步，调用状态与 modelStatus 分开读取；infeasible 不等于绑定错误。getDualRay() 可能附加求解，保存原任务状态再取证。options.set({...}) 逐项生效而非事务，传入完整已校验配置。非平凡求解在可终止 Worker 中执行，普通 postMessage 不能中断正在同步求解的同一线程。锁定类型契约

7.2 局部重求解的正确性条件

设 (H=H_L(x_L,s)\land H_R(x_R,s))，s 为共享分隔符。仅当修改不改变 (x_R,s,H_R) 及其引用集合，且新 (H_L) 已验证，才可沿用右侧证据。这是组合正确性的条件，不是“增量算法总快”的承诺。

依赖包含程序数据流、关系读集、查询对象集合、引用基数和空间排除依据。新增物体会改变“对所有物体无碰撞”的量词范围；两特征没有数据流边仍可能相撞。无法证明独立时扩大求解/检查范围，必要时直到整个模型。

7.3 结构改变中的身份

持久身份指向设计角色与构造来源。支持一个对象的引用不能在面分裂后静默选择任意一面；集合引用需要明确 all/one/谓词和基数。当前 lineage 的空、分裂、合并、歧义拒绝规则必须保留。重新布局时，“孔阵列角色”可以保持，但被删除的个体孔不能将旧 ID 转给另一位置。

7.4 一次最终提交

authoring 的 Patch 只提交源设计修改，包括要求、关系及允许修改域；搜索位于所有入口共享的候选求值链。Core 冻结 candidate.document/modelHash 后不再改写源文档。获选结构、参数和构造封存为 Realization，与验证、revision 身份及资源原子持久化。沿用权限、读修订、CAS、preview、validate、commit/read-back；不能仅在 AI 工具中增加一个 solve 步骤，也不能通过反复提交候选试错。

撤销、重做、恢复重放源要求及封存实现，不重新优化。basis 等数值工作缓存可丢弃；当前修订验证与恢复所依赖的证书、身份绑定和实现资源不可丢弃。完整哈希及事务约定见 §22.8 与现有实施方案。

9. 几何底座与检查边界

9.1 表示权威

采用 AMIR 作为设计语义权威、OCCT B-Rep 作为机械实体求值结果。NURBS 是曲面表示，不是完整的实体拓扑内核；网格适合显示及声明为 MeshSolid 的运算；隐式场适合其声明域中的场建模和采样。不能让三种表示成为同一零件的三个独立权威。

保留已有转换误差语义，特别是 requestedOnly、measuredEstimate 与有证明的误差界的区别。调用方要求有证明的误差界而当前方法不能提供时，返回 ERROR_BOUND_UNAVAILABLE；否则保留估计等级和权威用途限制。不能用网格看起来像或相同体积证明精确尺寸等价。现有转换器

9.2 G2 必须检查实际最终曲面

当前 morph-operators 中的 bridgeProfilesWithContinuity 用网格端点构造 box；zebra-analyzer 存在按请求等级填 G2/Class-A 指标的路径。它们不构成真实曲面连续性证据。此结论针对该模块；本轮未证明该桥接已接入公共 AMIR 执行链，不能扩大成全部产品曲面能力的判定。

锁定 OCCT 的 BRepOffsetAPI_MakeFilling 有支持面上的 G1/G2 约束和误差接口，当前 WASM 已经绑定，优先直接调用。Add(edge,supportFace,order,isBound) 要求相应的边界参数曲线。输入必须有真实边、支持面、边界对应关系、方向和容差，不能只给离散点和一个 continuity 字符串。实际绑定

还必须区分中间求解与最终 B-Rep：MakeFilling 先求 GeomPlate，再近似成 BSpline 面；其 G2Error 不是最终曲面整个边界的认证误差上界。最终接缝需要检查位置、法向/切平面、曲率关系及方向；离散采样报告采样范围与误差，不能自动叫全边界证明或 Class-A。

该结论来自锁定版本 BRepFill_Filling 的构面和误差转发，以及 GeomPlate_BuildPlateSurface 的约束采样。当前已有 BRep_Tool.CurveOnSurface 与 BRepAdaptor_Surface.EvalD1/EvalD2，可用于最终面检查。ThruSections.SetContinuity 或点阵拟合的内部 C2 不等于与外部支持面达到 G2。

9.3 自研与复用边界

OCCT builder、拓扑算子、支持面与句柄生命周期都属于 @aira/geometry-kernel 的维护职责。产品层负责 AMIR 参数、关系、语义引用、事务和诊断，不能复制 builder。

Manifold 的 MeshSolid/场离散用途不与 OCCT 的 B-Rep 交付混同；不新增第二个 mesh 布尔库。ml-matrix 的现有 SVD/秩检查不扩张为第二个优化求解器。模型显示、物理分析或制造检查也不能借“统一内核”绕过各自接受域。

已有 aira-field-runtime 区分 standard Manifold levelSet 与委托 @aira/lane-r 的限定域 certified-isotopy；后者有深度/单元数限制及证书，并非任意场都能认证。当前检索未证明它已接入公共原生工具，不能由包存在或 description 推出产品可调用。现有场运行时

9.4 为什么不能把几何难点藏进十二个名字

Boolean 内部仍需曲面求交、分类、裁剪、退化处理和拓扑重建。一般曲面交线不能无误差地回到同一有限 NURBS 表示族；三维边与二维参数裁剪曲线分别逼近后，还要保持一致性。修剪曲面综述

精确谓词解决部分离散判定，不自动使任意曲面求交成为精确构造。Shewchuk 的原始工作应在它的适用问题中使用。OCCT fuzzy boolean 的附加容差会改变近重合情形的处理，不能自动不断放宽直到成功而仍宣称原需求满足。官方布尔语义

固定程序分支中的 AD 与跨拓扑搜索分开。已有 OCCT 自动微分研究说明这不是首次发现；将 CasADi 连接到一个 OCCT 黑盒并不会自动取得导数。DMTet适合可变拓扑网格提案研究，不能直接提供 STEP/B-Rep 的身份和尺寸权威；BRepNet也说明 AI 可直接学习 B-Rep 结构。因此采用多种有明确用途的表示，避免新增一个承诺覆盖一切的隐式几何内核。

9.5 由数学结构直接构造拓扑，减少三维求交

对于恒厚平板，设外轮廓 R 与孔槽 (H_i) 为规则闭平面区域，孔槽互不相交、严格位于 R 内部，并且所有实体沿相同方向和非零长度区间 I 拉伸。定义规则化差 (A\setminus_r B=\operatorname{cl}(\operatorname{int}(A\setminus B)))，截面使用二维内点，实体使用三维内点，则规则化实体满足

[ \operatorname{Extrude}(R\setminus_r\bigcup_iH_i,I) =\operatorname{Extrude}(R,I)\setminus_r\bigcup_i\operatorname{Extrude}(H_i,I). ]

这来自共同笛卡尔积与集合差的关系。正间隔排除了退化接触边界；有一致方向和容差的 Wire/Face 构造仍需实际检查。于是布局求解之后，可以直接构造带内环的平面 Face，再执行一次 Prism，避免该域内原本不必要的三维 Boolean。当前 makeFace(outer, holes) 和 CompoundSketch.extrude 已提供此能力，不需要新几何库。

对任意已有实体开孔，当前 exact-hole-array 本来就构造复合刀具并只做一次原生 cut，不能虚构成逐孔 N 次布尔来夸大差距。盲孔、不同方向孔和曲面基体不满足上述直接拉伸的前提，继续使用已有专用路径。已有下游面引用或特征历史时，实体点集相同也不证明命名、操作身份与历史相同；该优化首先适用于新候选构造，不能静默改写用户锁定的过程语义。

曲面也有可归约域：固定次数、节点、权重和参数位置时，(S(u,v)=\sum R_{ij}(u,v)P_{ij}) 对控制点 P 线性，位置/参数导数约束与二次平滑目标可归约为线性或二次问题。权重、节点或对应参数一起变化通常恢复非线性；一般几何 G2 不等同于固定参数 C2。先用 OCCT 现成拟合 API；只有上游不能表达的联立关系才进入约束编译。这是由 B-spline 定义与 NURBS 定义得到的结构分析，不是重写样条内核。

不能将这些局部简化推广为“求方程替代全部几何”。(S_1(u,v)=S_2(s,t)) 的一个数值解不包含全部交线分支、裁剪环和内外分类；曲面交线追踪教材区分了这些问题。保留成熟求交、裁剪、偏置、圆角和生命周期机制，是保留接受域所需的真实复杂度。

因此孔、槽、凸台、规则肋和阵列可共享参数关系、有限配方和现有构造族，不为每种特征维护一套求解循环；解析圆柱等专用构造仍保留，不能为了“原语更少”强制转成通用 NURBS。只有实际替代了重复机制或减少了昂贵运算，才计为内核简化。

13. 安装板算例与适用域

孔数 8、直径 6、孔间净距至少 3、孔边到板边至少 4 mm，板高 30 mm。

结构	一个可靠的容纳尺寸	说明
单排 8	77×14 mm	水平跨度 7×9，加两侧半径与边距
两排 4–4	41×23 mm	每排跨度 3×9，两行中心距 9
三排 3–2–3	32×29.6 mm	水平节距 9、交错 4.5、行距 7.8

错排满足 (4.5^2+7.8^2=81.09>81)。这给出 40×30 mm 板的可行构造。它不是最密堆积证明。

80→60→40 mm 可以体现从单排到双排再到错排的必要调整，但实际优化目标可能提前选更紧凑结构，不能强迫所有合理求解器输出唯一相同序列。28/30 mm 时，几个已试结构失败不证明任意排布无解。

一个可独立证明的拒绝例是板宽小于单孔直径与左右边距之和，即 W<14 mm，在要求孔完整位于板内且边距按该定义衡量时，任何此类孔都无法容纳。此证据与枚举过几种结构无关。

13.1 从 16 个坐标变量到解析可行性判定

下面不是新性能跑分，而是可以逐步核对的数学降阶。固定 W、H、孔径、净距与边距，先选择居中对称的 3–2–3 结构分支。外侧两排的坐标为

[ x=W/2+{-p,0,p},\qquad y=H/2\pm h; ]

中间一排为

[ x=W/2\pm p/2,\qquad y=H/2. ]

于是 8 个圆心的 16 个坐标由两个非负参数 p、h 生成。最小中心距 (D=6+3=9)，中心到板边至少 (3+4=7)。所有 28 对孔可以完整分成三类：

类别	孔对数	该类最小距离	等价要求
同排内部	7	p	p≥9
两外排之间	9	2h	h≥4.5
中排与外排之间	12	(\sqrt{p^2/4+h^2})	(p^2/4+h^2\ge81)

每类都存在达到所列最小值的孔对，其他孔对距离不小于它，故没有遗漏远邻约束。全部板边约束由坐标极值归并为 (p\le(W-14)/2)、(h\le(H-14)/2)。该分支的完整可行性系统为：

[ \boxed{p\ge9,\quad h\ge4.5,\quad p^2/4+h^2\ge81, \quad p\le P,\quad h\le T},\qquad P=(W-14)/2,\ T=(H-14)/2. ]

在非负域中 (p^2/4+h^2) 对 p、h 单调递增，因此存在可行 p、h，当且仅当

[ \boxed{P\ge9,\quad T\ge4.5,\quad P^2/4+T^2\ge81}. ]

必要性来自上界与单调性；充分性由选择 p=P、h=T 直接给出。该分支的纯可行性已变成三个标量比较，无须 LP/NLP 搜索。 这仍是数学求解，只是得到了更便宜的解析解。加入偏移最小、固定节距、其他孔组干涉等额外目标/关系后，重新分析剩余问题，不能把这个闭式结果套到变化后的模型上。

对 40×30 mm，P=13、T=8。若偏好保持 p=9，则

[ h\in[9\sqrt3/2,8]=[7.794228634\ldots,8]. ]

取 h=7.8 即满足要求，邻排最短距离平方为 81.09。对 28×30 mm，P=7，约束 p≤7 与 −p≤−9 相加即得 0≤−2，严格排除该结构族。本轮用 Node 核对了 40×30、32×30、28×30 的标量判定分别为 true、true、false；正确性依据是上述推导，不依赖这三个样本。

从自由排布限制到对称族是选择搜索子域，不是保持全部自由排布能力的等价变换；只有在该族内，孔对归并及单调判定才保持等价。用户未锁定这个族时，族内无解不能删除其他结构。上述公式使用名义二维尺寸；若验收带容差，按 §5.3 构建相应接受域，实际 B-Rep 仍独立检查。

可推广的机制是对称/等距关系的参数化、按结构归并约束、在已证明符号范围内利用单调性；不是给“8 孔 3–2–3”添加专用 if 分支。这明确展示了能力与成本的取舍：优先搜索低维且可检查的结构族，必要时在声明域和预算内扩大，而不是一开始就求一个完全自由的非凸排布问题。

求解执行实例的复用边界（2026-09-20）

连续编辑的重复启动成本来自每次提案都创建 Worker 并重新加载 WASM，不属于设计问题本身的数学求解成本。现有 relation-solve 现将成功返回候选的 Worker 独占借出/归还，最多保留一个空闲实例，30 秒空闲后终止；并发请求各自持有实例，不覆盖消息处理器。Worker 内惰性加载的 HiGHS Promise 复用同一运行时，LP/QP 仍使用既有唯一适配器，模型句柄按原 finally 销毁。取消、超时、执行错误或 unknown 返回直接终止实例，不进入空闲缓存。HMR 释放空闲实例；缓存不是源设计、见证或恢复依赖，不跳过 Core 原问题检查。

真实 Chrome 求解调用以两个不同的一元凸二次输入核对执行复用：两个候选对应各自输入，仅创建一个 Worker；取消下一调用时终止实例，随后新建实例成功求解。此检查只证明代码加载复用、当前输入隔离与取消恢复，不声称特定加速倍率，未形成统计性能结论。该检查停止。P3 仍要求 HiGHS 模型的持久增量更新及更完整性能验收；Worker 复用不能替代模型更新，也没有替换原模型生命周期或添加第二求解器。

固定结构模型的增量更新（2026-09-20）

推导前提是当前数值模型的变量顺序、稀疏矩阵、Hessian、整数域布局、目标方向与其他结构字段全部相同。此时完整新模型与旧模型的差异仅为 c、列界、行界及目标常数；逐项更新这些字段就得到相同的新数值问题，不需要重建矩阵或重新创建原生实例。比较采用精确字段序列化及数值相等，不以浮点近似相等推断模型身份；每次输入快照独立拷贝，不能由调用方后续修改改变缓存基准。不同源问题即使数值结构相同也只复用执行状态，仍按各自原问题核验。

锁定 highs-js 1.15.3 的 throwing Model API 提供 changeColsCost、changeColsBounds、changeRowsBounds、changeObjectiveOffset；其 types.d.ts 明确范围选择为闭区间，并明确 dispose 所有权。现有唯一适配器已使用这些上游 API，保留至多一个模型随 Worker 生存。矩阵、Hessian、变量身份/域布局等结构变化时先 dispose 再创建；异常、unknown 或无有效候选时销毁并移除模型。原生 time_limit 使用既有 getRunTime 加本次预算，宿主的墙钟终止仍约束整次调用，避免累计运行时间吞掉后续调用预算。没有复制求解器或增加缓存证据权威。

原生绑定核验依次检查行界、线性目标/常数、列界更新和矩阵变化：三次固定结构求解只建一个模型，结构变化再建一个并销毁前一个，各结果与对应解析最优值一致。浏览器实际 QP Worker 调用确认连续输入隔离、取消终止和新实例恢复仍成立。这些是增量 API 与资源接线检查，不是统计性能或通用最优性证明；检查停止。当前结构变化仍完整重建，尚未承诺稀疏系数/Hessian 原位更新。P3 的更广规模及性能承诺仍须按整体计划核验。

固定稀疏布局的系数更新（2026-09-20）。 上述结构判定现进一步区分“稀疏位置”与“位置上的数值”：矩阵 values 和 Hessian values 不进入布局签名，其余布局与域字段仍精确比较。同一稀疏坐标上的矩阵值用锁定 Model.changeCoefficient 更新，按 CSR 行或 CSC 列正确恢复坐标；同一 Hessian 布局的新值用 passHessian 整体传入，由成熟后端处理状态失效。Hessian 有无变化、布局变化、整数域布局或变量身份变化仍先释放再重建。错误清理和原问题核验规则不变，不手写矩阵求解或猜测 basis 有效性。

原生接线检查确认 changeCoefficient 与 passHessian 均被实际调用，LP 系数变化与 QP 二次系数变化后的结果符合对应解析值；六次调用仅创建两个原生模型，第二个来自线性到二次结构切换，旧模型已释放。数值比较阈值仅用于本次原生接线检查，不是设计验收容差或最优性证明。此检查停止；没有统计整体加速倍率，也不把模型复用作为 P1–P6 完成依据。Web 类型及改动 lint 通过。