关系编译器 AST 与 SolveIR 规约

研究总览 · 2026-09-20

本文把算法 §5落实为数据结构、类型规则、编译步骤和失败语义。源 AST 的权威结构现已进入生产 schema，经现有生成链导出类型；解析器已实现结构、内部引用与依赖检查，类型推导已处理量纲、单位转换描述及数值域检查义务。关系源模块已登记，完整词汇身份、外部对象/要求接线、SolveIR 与执行仍未完成，不表示当前 AMIR 已能提交或执行这些节点。实施位置与状态分别见现有计划 P1–P4和工作进度。

1. 权威边界与现有契约接合

源 AST 保存设计，SolveIR 是可丢弃的求解视图，Realization 保存已经选择并核验的实现。这三者不能合并成一个会被求解器修改的文档。

新增一个注册的 design.relationSystem Operation Module，沿用现有 ModuleNode 的 op/opVersion/operationContractHash/inputs/outputs/extensions 外壳。inputs.definition 使用 {const:{type:"RelationSystem",value:RelationSystem}}，其余输入沿用 AMIR Value。当前节点 schema与结构解析已进入生成链，模块已登记当前目录，Rust 校验器加载相同 schema 并识别结构编码。完整语义/执行/封存未接通前，Core 明确返回 RELATION_EXECUTION_UNAVAILABLE，目录不声明已可执行。RelationSystem 是同一模块契约中的新结构类型；不是把任意 JSON 塞进 extensions。源 schema、目录和生成类型保持同源，不维护本文草案与生产 schema 两份独立权威。

外部值只经节点 inputs 引用 Parameter、typed producer 或常量，表达式用输入名读取，禁止按字符串路径访问任意工程状态。输出由模块声明的同一端口提供。当前 Parameter 仍是有值的参数，不能把 value:"0" 当成“未知”。源码依据：ModuleNode / Value / Parameter、Operation Module、模块值词汇。

下列 TypeScript 是 JSON 数据形状的说明写法；源 AST 的字段权威以生产 schema 及其生成类型为准，语义校验规则同样强制。所有对象拒绝未声明字段；map 的键及引用服从现有 StableId 规则，输入/输出端口服从现有 PortAddress 规则。可选字段缺省表示不存在，不接受 undefined 作为序列化值。number 仅用于有上界的整数索引/预算，工程标量不用 JSON number。

2. 源 AST：表达式、变量、要求与构造

type Id = string;
type ExprId = Id;
type Decimal = string; // AMIR canonical decimal，不接受指数、-0、冗余末尾零
type ScalarAtom =
  | { type: Id; value: Decimal; unit?: string }
  | { type: "Bool"; value: boolean };
type Expr =
  | { op: "lit"; atom: ScalarAtom }
  | { op: "input"; name: string }
  | { op: "var"; id: Id }
  | { op: "neg" | "sqrt" | "sin" | "cos" | "exp" | "log"; arg: ExprId }
  | { op: "add" | "sub" | "mul" | "div"; left: ExprId; right: ExprId }
  | { op: "cmp"; cmp: "eq" | "le" | "lt" | "ge" | "gt";
      left: ExprId; right: ExprId }
  | { op: "and" | "or"; left: ExprId; right: ExprId }
  | { op: "not"; arg: ExprId }
  | { op: "select"; condition: ExprId; yes: ExprId; no: ExprId };
type Bound = { value: ExprId; inclusive: boolean };
type Domain =
  | { kind: "interval"; lower: Bound | null; upper: Bound | null }
  | { kind: "finite"; values: ExprId[] };
type Variable = { type: Id; unit?: string } & (
  | { role: "fixed"; value: ExprId }
  | { role: "unknown"; domain: Domain; initial?: ExprId }
  | { role: "derived"; value: ExprId }
);
type Law = { left: ExprId; right: ExprId; when?: ExprId };
type RequirementUse = {
  assertion: Id; bindings: Record<string, ExprId>;
};
type RecipeValue =
  | { expression: ExprId }
  | { input: string }
  | { output: { step: Id; port: string } }
  | { list: RecipeValue[] };
type Construct = {
  operationRef: string; operationContractHash: string;
  inputs: Record<string, RecipeValue>; when?: ExprId;
};
type RelationSystem = {
  expressions: Record<ExprId, Expr>;
  variables: Record<Id, Variable>;
  laws: Record<Id, Law>;
  requirements: RequirementUse[];
  goal:
    | { kind: "feasible" }
    | { kind: "minimize"; expression: ExprId;
        accept: { kind: "feasible-incumbent" }
          | { kind: "certified-gap"; absoluteGap: ScalarAtom } };
  continuation: "fresh" | "prefer-current";
  constructs: Record<Id, Construct>;
  outputs: Record<string, RecipeValue>;
  scope: { writable: Id[]; preservedAssertions: Id[] };
  budget: { compileNodes: number; branchCases: number; solveMilliseconds: number };
};

laws 只表达定义性等式，例如坐标构造或材料模型恒等式，默认精确，不添加隐式 epsilon。可接受偏差、间距、限位等工程要求通过 requirements 引用现有 assertion：比较符、目标值、容差、检查器和证据策略由该 assertion 唯一拥有；bindings 只绑定模块契约明确标记为可绑定的受检量角色。minimum/maximum/tolerance 等判据输入始终从源 assertion 的 Value 解析，禁止重绑定为候选或候选的函数。不能在关系节点复制一份不一致的要求。preservedAssertions 必须完整进入同一候选验收，不能只保存名字。

跨节点组合时，每个 (关系节点, assertion) 的绑定构成独立检查义务；多个关系引用同一 assertion 不采用后写覆盖。任何关系要求保留原 assertion 或以空 bindings 引用它，都保留原受检对象的独立义务。仅在没有此类保留义务时，求值图才用绑定检查替换原目标检查；源 assertion 的判据和源 AMIR 均不改写。当前封存块记录受检常量及源 assertion 哈希，验收投影重新核对当前源内容，并将派生检查身份映射回关系和原要求；这不是完整修订交付已接通的声明。

当前要求链接保留有效配置中的原始 assertion，数值范围仅开放 value 角色，原始保持要求作为独立检查义务保留。该实现拒绝判据字段重绑定；判据依赖检查使用共享特征图检查判据是否依赖本次待求生产者，完整来源集合仍须由联合编译器提供并实际接线。此处的字段保护、要求查找与静态依赖检查不等于求值、权限或数值验收已经完成。

结构选择用有限整数域或有界 Int/Count 域表达，when 启用明确分支，select 选择标量结果。无界结构递归、任意字符串函数、外部宿主代码不在此语法内。更多数学算子通过同一锁定模块的类型签名、定义域、求值/导数与检查规则扩展；未绑定规则前只能报告不可执行，不能退回 eval()。复杂显式程序、曲面和 B-Rep 仍使用已有构造模块，不必都成为数值未知量。

constructs 引用现有目录中的构造模块，禁止递归调用本关系系统。它们在选解后实例化为普通 typed producer 图；不是另写一套 builder。构造顺序来自输入依赖；禁用步骤不能被启用步骤或必需输出引用。条件输出须由带相同守卫的已声明角色或总定义的选择模块汇合，不能暗用“第一个存在的结果”。

当前构造链接实现复用已锁定目录验证模块身份、端口与标量输入。守卫蕴含仅接受无条件生产者、相同表达式 ID 或字面真守卫；其他情况返回 RELATION_CONSTRUCT_AVAILABILITY_UNPROVEN，不冒称无解，也不新增布尔求解后端。完整输入值校验、实例化和几何求值尚未接通，此链接结果不构成可执行或可提交凭证。

2.1 有限索引与记录：从乘积语义推导编译职责

本节是 P1 结构扩展的实施规约。依据是工业覆盖 §3，实现继续扩展同一源契约和共享编译链，不增加求解器。当前源 Schema 已增加可选 structures 映射：成员为 {expression}、{fields} 或 {element,items}；数组的 element 用已注册数量类型、记录字段类型或定长数组类型声明，包括空数组。parseDesignRelationSystem 检查全部叶引用并将容器和类型节点计入既有编译预算，typeDesignRelationSystem 检查字段、数组形状和量纲/标量种类。共享叶仍引用同一表达式，不生成变量副本。Count 的非负细化目前仅接受有直接来源依据的 Count 变量或非负整数字面量，不以相同量纲认定任意 Int 表达式满足 Count。RecipeValue.list 仍只组合构造参数。固定成员访问和有序折叠已按本节末的规则接通；未知索引和有界模板尚未完成，不能把源容器准入当成完整工业结构能力。

当前结构值沿共享候选物化执行：对全部结构叶按表达式 ID 去重，复用 Core 候选表达式求值得到有理数或 Bool；未决值阻止本次物化，不用零或显示舍入值填充。关系块必需的 structures 保存源形状快照，structureValues 按表达式 ID 保存规范数量类型与精确值，两者随块哈希封存；无结构时均为空映射。封存检查叶集合恰好闭合、数值/布尔种类和规范单位一致，完整恢复仍从源重算整个块并比较哈希，不能靠内容哈希自证值正确。公共 evaluation.realization.relations 投影同一结构与叶值；没有另一份可编辑结构结果。类型生成对共享结构引用导入同一源类型，运行时 Schema 保留正式引用。

固定的原生修改链已确认：同一记录两个字段共享 x，x 从 1/3 m 修改为 2/5 m，Bool 叶和空数组形状保留，公开读取对应当前封存结果；禁用求解 Worker 重开保持实现根，重哈希伪造旧叶值仍被源重建拒绝。这是本次结构值接线证据，不证明索引访问、有限折叠、场或任意结构替换已经实现；该检查停止。

表示与身份。 结构类型由已注册的标量叶、有限记录和定长同型数组递归组成；类型定义不得递归成无限对象。记录字段以稳定键标识，数组位置有显式顺序。位置不是工程对象身份：需要增删重排而保持身份的集合，用稳定成员 ID 加显式顺序引用表达。结构叶引用现有标量表达式或变量，不复制其值、域或固定/开放角色；两个字段引用同一变量时仍是一个自由度。结构不能通过字符串路径越权读取工程状态。

令结构 T 的叶路径集合为 L(T)。标量的 L 只有空路径；记录是各字段带键前缀的互不相交并；数组是各位置带索引前缀的互不相交并。扁平化 F 按路径读取标量引用，重建 U 按原形状装回，因此由结构归纳得 U(F(v))=v。共享叶另保留引用等价类，不能因路径不同生成独立未知量。此结论证明有限组合的表示保持，不证明这些叶的关系有解，也不允许删除源形状后从求解矩阵猜回结构。

访问与选择。 固定成员访问只解析引用，不做数值求解。未知索引 i 必须为 Int/Count，并保留 0≤i<n 的原始约束；非空同型数组的读取生成逐项相等守卫与惰性选择，越界无结果，禁止最后一项充当默认值。每个合法 i 恰好选中一项，因此结果等于源数组读取；证明按索引规则成立，不需要运行所有工程数组。选择不改变未选分支的定义域语义。非光滑/离散选择沿现有后端接受域分派，不因可标量化便宣称 NLP 或 MILP 均可执行。

有限组合。 有限和按源顺序左折叠，固定展开次数来自结构形状，不能来自尚未求解的连续值；空和要求显式有类型的单位元，绝对温度等没有该加法单位元的类型拒绝。全称、存在有限量词分别降低为合取、析取，空集结果分别为真、假。连续空间/时间量词不适用此规则。固定形状的逐成员关系按相同稳定路径实例化，约束及诊断均保留模板来源和成员路径；不让 AI 手写每个标量方程。

复杂度与停止边界。 设源结构大小为 S、实际展开的叶及表达式/约束引用数为 E，形状解析与共享引用展开按 O(S+E) 工作量组织；规范键排序的成本另计。未知索引一次读取最多生成 O(n) 选择结构，k 次读取最多 O(kn)，不能把它描述为 O(1)。多重展开的乘积必须在分配前用有界计数检查，统一消费现有 compileNodes 与宿主上限；超过预算返回明确的编译预算诊断，不截断、不抽样、不把规模限制当作数学无解。编译成本有界不意味着求解成本线性，离散求解的困难仍由现有时间/分支预算约束。

同一纵向能力的实现边界。 源 Schema/生成类型保存结构及引用；解析器检查形状、类型和别名；共享编译器产生带成员来源的标量视图；候选核验消费全部展开约束；Realization 绑定源结构与选定索引；原生发现和读取从源形状与同一封存叶值重建记录，连续编辑沿原依赖使旧结果失效。私有展开 ID 采用结构化路径的无碰撞编码，不能拼接未转义的成员名。公共编辑仍修改源定义，不暴露一次展开生成的内部 ID 作为可持久编辑身份。

完成判据是上述归纳规则在同一源修改—编译—检查—封存—读取/恢复路径中兑现。实现后只核对类型/生成一致性以及该跨边界接线、越界拒绝与共享叶身份，不按数组长度、工业名称或参数组合追加试验。记录容器本身不完成 P1 的离散场、事件和连接语义；这些义务继续保留。

当前固定访问与有序折叠实现。 源 structureExpressions 以稳定结果 ID 声明 {op:"member",structure,path} 或 {op:"fold",structure,path,reducer,initial}；path 的字符串选择记录字段，非负整数选择数组位置。结果与普通 expressions 共用引用空间，同名重复定义拒绝。member 必须落在标量叶；fold 必须落在标量数组，reducer 为 add/and/or，initial 是显式表达式引用。这里 fold 的含义为 fold(op,z,[a₀,…,aₙ])，不隐含零或其他单位元；要表达求和或有限量词，调用者须提供相应有类型的单位元。空数组返回 initial，非空严格左折叠。

共享解析器只在规范克隆上展开：member 和空 fold 用常真惰性选择保留对原叶/初值的引用，非空 fold 生成既有二元操作链。由 fold(op,z,[]) = z 和 fold(op,z,a::xs) = fold(op,op(z,a),xs) 的定义归纳可得源与展开求值相同；没有添加待求变量、改变自由度或重排加法。生成辅助 ID 避开全部已用名称，展开前/生成时检查预算，固定越界、非标量成员、重复定义和引用环明确拒绝。源文档保留 structureExpressions；解析返回的 node 是供编译使用的私有标量视图，不能作为源编辑结果写回。解析的 expressionOrigins 保留展开结果的源声明位置。

Core 的源级静态数值检查将尚待展开的结果标为 structure-expansion-required，不误报成普通缺引用，也不签发数值结果；候选求值必须消费共享编译器展开后的 AST。后端、精确候选检查、构造与封存恢复继续使用原有标量链。实际原生链已确认 member 驱动几何宽度，fold 在连续修改中得到正确精确结果，空 fold 保持初值，越界编辑保持 head，源未被辅助表达式覆盖，公开读取与免求解重开一致；该接线核验结束。未知索引、有界模板实例化以及更完整的细化类型推导仍未完成，不由固定位置访问冒充动态结构选择。

2.2 未知索引：等价编码、接受域与辅助量责任

本节给出未知索引的等价规则；当前已接入数值标量源声明与编译，数值选择的公开投影与限定原生编辑/恢复链已核验，无环仿射组合索引界传播及 Bool 选择已接通，一般循环/非线性界仍未闭合。源码依据为 relation-guards.ts 的有限变量比较、relation-highs-model.ts 的 one-hot 有限域和有界守卫行、relation-problem.ts 的原等式/域保留，以及共同 Core 候选检查。现有固定访问不能通过尝试各个数组位置扩充成未知索引算法。

令已声明同型标量数组为 a₀,…,aₙ₋₁，索引 i 是 Int/Count，读取结果为 y。其语义恰为 i∈{0,…,n−1} 且 y=aᵢ，并保留源中关于 i、数组成员和 y 的全部关系。n=0 没有合法读取，不能选默认值；固定索引仍走 §2.1，不启动求解。位置只表达当前数组顺序，不成为成员工程身份。

逻辑编码与证明。 引入私有有限整数 k∈{0,…,n−1}，保留等式 k=i；对每个 j 生成守卫 (k=j) ⇒ (y=aⱼ)。k 的域通过既有 one-hot 编码：二元 zⱼ 满足 Σzⱼ=1、k=Σjzⱼ。若源读取合法，令 k=i、zᵢ=1、其余为零、y=aᵢ，扩展关系成立；反之，由有限域和恰一选择得唯一 j=k=i，激活等式强制 y=aᵢ。故消去辅助量后与源读取等价。不能用私有 k 的域覆盖源 i 的原域；两者通过等式相交。辅助量不增加设计自由度，不由 AI 提供初值或选择。

数值专门化的前提。 源读取语义不依赖 MILP，但当前 HiGHS 守卫等式以有限行界生成松弛，不能直接承接无界行。仿射成员 aⱼ=cⱼ+Σₜ bⱼₜxₜ，在源已知盒界 xₜ∈[lₜ,uₜ] 下具有包含界：

Lⱼ=cⱼ+Σₜ min(bⱼₜlₜ,bⱼₜuₜ)，Uⱼ=cⱼ+Σₜ max(bⱼₜlₜ,bⱼₜuₜ)。

系数与界均由现有 Core 有理值/仿射值和原变量域取得，使用同一 BigRational 算术；不得再写 JS 有理运算库。有限域取实际值的最小/最大值，开放整数界先按整数域规则收紧，未知/无穷界如实保留。由逐项区间包含和求和得 aⱼ∈[Lⱼ,Uⱼ]，因此 y∈[minⱼLⱼ,maxⱼUⱼ]；源约束间的相关性可能使此界不紧，但不影响包含性。初值、当前候选或采样极值不是源域界，不能参与此推导。

令 dⱼ=y−aⱼ，在这些已证明的盒界上得 dⱼ∈[D⁻ⱼ,D⁺ⱼ]。守卫 zⱼ=1 时强制 dⱼ=0，zⱼ=0 时放松到包含原行的范围，所需松弛量分别由 max(0,−D⁻ⱼ)、max(0,D⁺ⱼ) 导出。这个推导给出现有守卫行接口的输入，不新增求解器。后端 binary64 转换后的模型仍只产生候选；共同 Core 重验原域、索引及激活等式。浮点模型的不可行状态不能冒充该混合整数源问题的精确不可行证明。

缺少可靠有限界、非仿射耦合或超出后端接受域时，不填任意 M、不丢弃分支、不分别求解上游和下游。保持源语义与原因诊断，交给已经支持且满足同一语义的路径；没有这样的路径时返回未完成/unknown。Bool 成员的读取保留布尔语义，不能隐式把 Bool 输出当作长度或实数；其布尔选择编码和数值成员的守卫等式需要分别接线。此边界是算法接受域，不是源系统已证无解。

求值需求与结构语义。 当前 structures 是完整值记录，候选会核对全部声明叶；本项沿用该契约，不把未知索引悄悄改为能够容纳未定义成员的惰性数组。成员表达式内部既有 select 的惰性语义仍保留。若要表达只有选中成员才存在或有定义的结构，必须显式建模守卫及其存在性，不能通过省略封存叶来改变当前结构契约。

来源、封存与预算。 生成的 k、y、守卫和等式必须关联源索引声明及成员路径；用户编辑和公开设计自由度仍以源变量为准。辅助候选量不是独立可编辑变量，恢复必须由源索引和成员值重建或经原激活关系重新核验，不能相信缓存值。数组成员或顺序变化使原读取实现失效，即便数组长度没有变化；源模型身份、boundNodeHash 和整个块的恢复比较共同保留这项责任。联合依赖分析必须包含索引、所有可选成员及其消费者，不能因源图有向无环便提前固定索引。

对一个 n 项读取，编码规模是 O(n) 个选择/守卫/等式，加上成员仿射表示的实际非零项数；多个读取按各自规模相加，不构造它们的笛卡尔积。源共享依赖保持 DAG，索引集及生成节点在分配前计入现有 compileNodes、分支和求解预算。这个编译规模结论不承诺 MILP 在多项式时间内求解。实施必须一次贯通源准入、精确界推导、共同求解、原关系检查、来源读取及免搜索恢复，再进行对应边界的定点核验；不能先靠若干成功索引案例宣称动态选择完成。

精确界计算的当前实现。 Core relation_numeric/bounds.rs 复用 BigRational 及现有分数解码、位长/工作预算，encloseRelationAffineJson 消费数值身份、既有代数 IR 的变量域和有理/仿射表达式，返回规范有理上下界；null 表示对应方向无界，非仿射或无法解释的输入返回 unknown。开放实数端点取包含闭包，整数端点按 ceil/floor 收紧，有限域与整数/非负细化取交后求包含界；零系数不会把无界变量传播成无界结果。输出绑定请求哈希和数值身份，只证明相对于该输入域的包含，不证明输入已与工程源绑定，也不声明约束系统可行。空域返回 unknown 原因，不签发新的全局不可行凭证。LP 射线检查已复用同一域解释，仍保留其连续闭区间接受域；没有新增有理库或保留第二份等价域解析。该入口是未知索引编译的依赖，索引 AST、界的源绑定和完整选择/恢复仍待接通。

数值索引编译接线。 源 structureExpressions 现接受 {op:"index",structure,path,index}，index 引用原 Int/Count 变量；共享展开器创建私有有限 k、结果 y、k=i 及各成员守卫等式。生成前计入变量/表达式/law 预算，名称避开源 laws，解析返回 indexBindings 和来源位置。空数组与非标量数组明确拒绝，Bool 选择按下述独立布尔展开处理，不能把不支持冒称无解。编译器从原源重新取得确定性辅助映射，对当前绑定问题的成员仿射式请求 Core 精确 hull，校对数值身份及请求哈希后只收紧私有求解列；原源域和候选核验等式保持。无有限仿射界保留 pending，不填任意 M。Core hull 对各成员包含区间取并集包络，沿用同一预算和 BigRational。联合诊断将生成变量/law 映射回索引源声明。依赖其他索引结果的无环仿射成员按下述拓扑规则传播界；循环或一般非线性成员仍可能 pending。公开源变量投影与数值选择/编辑/免搜索恢复已按下述边界接通。实际原生链完成 3/8→1/16 m 的索引几何编辑、禁止 Worker 的重开及重哈希分类伪造拒绝；此链核验结束，组合接线随后沿同一链核验外层读取内层、声明顺序与依赖顺序相反的情形，结果保持；不外推到 Bool 选择、循环索引或非二进制可表示未知量的候选完备性。

源变量与辅助见证的封存边界。 当前 relation block 必需字段 sourceVariables 是从原始源 unknown 声明重建的有序 ID 集；variables 仍保存全部求解见证并由 candidateHash 绑定。TS/Core 块检查要求清单有序、唯一且包含于见证键集；这仅是结构检查，不替代源真实性核验。恢复沿现有流程重新核验变量、重做 lowering，再比较整个块，因此把辅助量伪装成源变量并重哈希不能得到相同恢复块。原生 evaluation.variables 只投影 sourceVariables，编辑继续修改源定义，不以名称前缀猜测哪些量是内部量。当前未发布封存格式同步替换，旧块缺少该必需字段会拒绝，不保留旧契约兼容分支。

组合索引的界传播推导。 若结果 y 的成员仿射式含另一索引结果 z 的非零系数，建立 z→y 的依赖；与当前 hull 集无关的未知量保留原域。对无环依赖按拓扑序处理：基础成员包含于源域推导的包络；假设前驱包络均包含实际值，则仿射区间运算及成员包络并集同样包含 y 的实际值；与原 y 域取交仍保留全部满足源域的设计。由拓扑序归纳得全部结果的包含性。Core 请求的 hulls 是显式补充约束 y 属于成员值的并集，不能由任意调用者提供的 hull 冒充源证明；编译器只能从本次共享展开的 indexBindings 与绑定成员仿射值构造它，并核对整个请求哈希。输出 scope 区分仅声明域与声明域加 hull 约束。

Core 每个 hull 处理一次，用反向邻接和未完成依赖计数排序；BTreeMap/BTreeSet 带对数查找成本，工作量随声明成员及实际非零依赖增长，不形成选择组合笛卡尔积。零系数不建立依赖；无穷端点保持，空交、非仿射和预算耗尽返回 unknown。循环返回 RELATION_CYCLIC_ENCLOSURE_DEPENDENCY，本规则不做固定点迭代，也不据此声称循环系统无解。源变量域、守卫等式和精确候选检查不因此改变。

Bool 索引的等价展开。 仍以私有有限 k 和 k=i 保留位置合法性与源索引域；Bool 结果展开为 ∨ⱼ((k=j)∧aⱼ)，不创建布尔未知量，不隐式转换为数值。由合法索引恰有一个位置相等，其余合取为 false，析取恰等于选中成员，故该表达式与源读取等价；空数组仍拒绝。实现复用现有 Bool DAG、有限比较守卫、候选求值和封存，不展开 DNF 或选择组合。n 项编码在分配前计入 5+4n 个变量/表达式/law 节点，来源映射及源变量投影沿用数值索引规则；没有数值结果列，因此不请求 hull。完整值数组仍要求所有叶有定义，不借布尔短路放宽数组契约。

固定成员或现有有限比较组成的 Bool 读取可进入已有守卫编译；一般连续比较及尚不支持的布尔等式求解不由此自动获得支持，仍沿原 pending 诊断。一次原生链确认 Bool 索引随源位置编辑 true→false，参与关系守卫及构造配方选择，几何宽度 3/8→1/16 m、源/辅助变量区分、免求解重开及分类伪造拒绝保持；该链验收结束。

有限布尔表达式的 law 等式。 对 when g: a=b，其中 a、b 由既有有限比较与 Bool DAG 可编译，令 m=(a∨b)∧¬(a∧b)。布尔真值定义直接给出 m 当且仅当 a≠b，故原关系等价于禁止 g∧m；无 when 时禁止 m。编译器生成带该守卫的精确常数等式 0=1，复用原条件行与 Core 布尔图核验，不另造 SAT 求解器、不将 Bool 值充作尺寸。每个等式新增四个布尔节点，有 when 时再增加一个，保留共享子图、不展开 DNF；生成 ID 避开源名称并计入现有编译上限，原 lawId 保留。已知相等常量仍消除，已知无条件冲突仍直接拒绝。不支持的连续比较或 Bool 未知量域仍 pending；此处支持的是有限布尔表达式等式，不等于任意布尔理论均已可解。

既有原生链中取消直接指定索引位置的 law，改用选中 Bool 与期望 Bool 相等来驱动位置；期望 true→false 后求解出的索引、几何宽度 3/8→1/16 m 同步改变，源变量投影、免求解恢复及分类伪造拒绝保持。本项接线核验结束。

2.3 有界逐成员关系模板

源 relationTemplates 以稳定模板 ID 声明 {structure,path,member,captures,expressions,laws}。structure/path 选已有有限数组，member 是当前标量叶的局部绑定；captures 将局部名字显式绑定到源 expression 或 structureExpression；expressions/laws 使用同一现有 AST。三类局部名字必须互异，表达式 var/input 不能隐式读取外部状态，应捕获指向该状态的源表达式。局部表达式可前向引用，由同一依赖图检查循环。模板定义本身不是第二个设计图，不声明新未知量或另一个求解目标。

语义与证明。 设数组叶引用为 a₀,…,aₙ₋₁，模板关系体为 L(item,captures)。其语义是有限合取 ∧ⱼ L(aⱼ,captures)。展开时为每个实例的局部表达式/law 分配互不捕获的私有名字，member 替换为原叶引用，captures 替换为原源引用，其余操作不变。对局部表达式 DAG 按拓扑序归纳，替换前后各节点在相同外部赋值下值与定义域相同；law 两侧及 when 因而相同，再由有限合取得整个展开与源模板等价。共同未知量未复制，实例没有新增自由度。空数组产生空合取，无新增约束；局部名称与显式捕获仍检查，类型义务由实际实例化后的共享类型检查器核对。

身份与预算。 源持久保存模板，不写回逐成员展开物。生成节点保留模板 expression/law 的源 Pointer 和数组成员 Pointer；联合失败诊断可同时返回两者。数组顺序与模板内容已包含在源身份内，改变它们必须重编译、重建实现；私有生成 ID 不充当零件或拓扑工程身份。令表达式数为 e、law 数为 l、成员数为 n，展开规模为 n(e+l)，分配前在现有 compileNodes 中检查声明与实例成本，不搜索成员组合。

原生链已核对两个模板成员共享源变量、模板 Bool 等式驱动选择与几何更新、源模板保留、免求解重开及重哈希分类伪造拒绝，该接线核验结束。当前实现覆盖固定形状标量数组的关系模板；这不是任意递归模块、数量未知的实例生成或构造步骤模板。构造程序和装配实例仍走现有正式能力，不能以此子域宣称全部工业组合完成。

3. 强制类型与作用域规则

对象	编译期规则
标量文本	沿用 canonical decimal 校验；新关系中的有限十进制按精确有理意义解析，再单独记录向后端浮点的转换。不会把当前几何运算追认成精确有理计算
类型与单位	查锁定目录，推导 SI 七维量纲及 Bool/Int/Real；角度、绝对温度与温差另有语义种类。类型签名不由调用者任填幂向量来绕过
加减与比较	量纲和语义相容；绝对温度相减得温差；绝对温度不能直接相加或当普通乘数。摄氏输入先做显式仿射换算
乘除与根号	量纲相加/相减，根号要求本规约支持的整数结果量纲；分母非零、根号参数非负是保留的定义域条件
三角与指数	sin/cos 只接 Angle，求值前转 rad；exp/log 只接无量纲 Real，log 参数正。deg→rad 含 π，不冒充有理系数转换
布尔与选择	and/or/not 只接 Bool；cmp 返回 Bool；select 两分支同型，按当前有效分支检查定义域。未知连续比较形成非光滑分支，不直接送平滑 NLP
表达式图	ExprId 图无环且全引用可解析；变量在等式中互相约束合法。派生定义展开后的依赖必须无环，否则应声明 unknown 加 law，而不是递归求值
域与初值	fixed、unknown 的域界及 initial 仅依赖已知输入；derived 可依赖未知量。初值不收紧域；finite 域非空、去重、同型；Count≥0，整数域不放松成连续后直接交付
目标	目标为一个标量；不同量纲目标须由用户明确归一化/权重组成该标量。本版不暗设多目标优先级。gap 非负且与目标同量纲
单一驱动者	同一持久对象量只有一个源定义者。多个关系节点若共享开放量，先按真实引用合并求解块；不能复制变量后分别求解

QuantityType 是上述规则导出的类型表，随编译结果记录；不是第二份可编辑单位权威。输入仅能引用上游确定值，或经联合块处理的共同未知量。由本块输出构造的几何再回流本块作“已知输入”是执行环；须有显式受支持的耦合算法，否则诊断 unsupported-coupling。

4. SolveIR：冻结输入之后的规范求解视图

以下结构使用无量纲缩放变量 z，原变量恢复为 x=offset+scale*z。数值例子的所有有理数均为既约形式，分母正，零只写 0/1；无穷界用 null，禁止字符串 Infinity。纯 Bool 与有限选择先保持类型，只有合法结构编码才能转整数列。

type Rat = { n: string; d: string };
type QuantityType = {
  scalar: "real" | "integer" | "boolean";
  dimensions: [number, number, number, number, number, number, number];
  semantic: "plain" | "angle" | "absolute-temperature" | "temperature-difference";
  canonicalUnit: string;
};
type TypedExpressions = {
  expressions: Record<ExprId, Expr>;
  types: Record<ExprId, QuantityType>;
};
type Origin = { node: Id; pointer: string; assertion?: Id };
type Affine = { constant: Rat; terms: { column: number; coefficient: Rat }[] };
type LinearRow = { id: Id; lhs: Affine; lower: Rat | null; upper: Rat | null;
  origins: Origin[] };
type NonlinearRow = { id: Id; expression: ExprId;
  lower: ExprId | null; upper: ExprId | null; origins: Origin[] };
type Column = { variable: Id; kind: "real" | "integer";
  lower: Rat | null; upper: Rat | null; offset: Rat; scale: Rat };
type Quadratic = { affine: Affine;
  hessianUpper: { row: number; column: number; value: Rat }[] };
type Problem =
  | { kind: "lp" | "milp"; rows: LinearRow[]; objective: Affine }
  | { kind: "convex-qp"; rows: LinearRow[]; objective: Quadratic;
      convexityRule: string }
  | { kind: "nlp"; rows: NonlinearRow[]; objective: ExprId };
type Reduction = { id: Id; rule: string; origins: Origin[];
  premises: ExprId[]; recover: Record<Id, ExprId> };
type ModelRelation =
  | { kind: "equivalent"; derivationRefs: Id[] }
  | { kind: "inner" | "outer"; derivationRefs: Id[] }
  | { kind: "proposal-only" };
type SolveBlock = {
  id: Id; columns: Column[]; problem: Problem;
  fixedChoices: Record<Id, ScalarAtom>;
  reductions: Reduction[]; modelRelation: ModelRelation;
  rowScales: Record<Id, Rat>; checkAssertions: Id[];
};
type SolveIR = {
  sourceModelHash: string; inputClosureHash: string; catalogHash: string;
  compilerHash: string; numericProfileHash: string;
  typedExpressionResource: string;
  blocks: SolveBlock[];
  definitionOrigins: Record<Id, Origin[]>;
  recipeSources: { node: Id; pointer: string }[];
};

typedExpressionResource 指向 TypedExpressions 内容的散列：保留源 Expr，并加入带来源的派生 Expr；NLP 残差、恢复映射和缩放均引用这里，不能引用已删除的中间对象。dimensions 是按 m、kg、s、A、K、mol、cd 排列的整数指数，Boolean 必须全零且 semantic=plain；canonicalUnit 由登记表确定。合并节点时，局部变量/表达式 ID 通过完整 (源 node ID, 局部 ID) 无碰撞编码为编译 ID，不能按同名变量误合并。pointer 是源文档 RFC 6901 JSON Pointer，带 modelHash 才构成来源；变换新增行保留全部参与来源，不能只留最后一个约束。

在此传输层中 Rational 的工程量已转为规范单位；列与行尺度的原量纲由类型表保留。NLP 有非有理界时，其 row 通过 Expr 表达；无法在本有理列界格式精确表达的变量界改为有来源的 NLP row，不能静默舍入成更窄的设计域。整数列不使用破坏格点的任意缩放：scale=1、offset 为整数，并将原有限域完整编码。

仿射 terms 按 column 升序、合并同列、删除精确零；行/列按稳定 ID 排序，顺序映射封存。二次目标约定 0.5*zᵀH*z+cᵀz+c0，H 对称且上三角只存一次；convexityRule 必须引用已核验的 PSD 构造/判据，不能因为浮点特征值“看起来非负”便宣称凸。QP 只接连续列；MILP 目标必须仿射。

Column 和两种 row 的界均为闭界。实数严格不等式若交此 IR，必须降为闭外松弛并保留原严格谓词作最终检查，整体关系不得标 equivalent/inner；不能正确建立包含关系时拒绝降低。整数严格界可按已证明的格点 ceil/floor 规则等价转换。既严格又非光滑的条件，不能靠浮点 epsilon 冒充精确编码。

ModelRelation 描述在恢复映射下本块模型与对应源接受域的包含关系；它是由锁定规则生成的核验结果，不接受 AI 自报 outer。没有合法推导只能 proposal-only。跨块合成还要验证共享输入绑定和全部源要求，不能把局部包含关系直接升格为整个产品的证明。证书使用保留的有理模型与全部域，不直接信任送入求解器时舍入过的矩阵。圆外约束界的方向依§5.3，Farkas 核验依§6。

静态 Problem 不含 time/der/pre；Modelica 分析规约在共享标量语法上定义时间语义，不能把整个动态系统误交静态 NLP。已固定输入的几何谓词进入最终检查，未绑定可微语义的几何黑盒不得包装为 CasADi 函数假装可微。

5. 必须固定的编译流程

1. **绑定。**锁定模块/类型/要求、源模型、输入闭包、数值配置、预算及 continuation 输入。prefer-current 只对当前有效见证表示偏好；其身份进入输入闭包，不把旧解强行设为硬约束。
2. **类型与定义域。**按 §3 校验，展开已知 fixed/derived 值，共享同表达式。仅在根值已知且函数有定义时直接求值；x/x 不能在未保留 x≠0 的情况下改成 1。
3. **联合未知量。**按变量—关系—目标的关联图分块；共享未知量、跨块目标及保持要求必须合并。块之间只通过真正固定的值连接。
4. **仿射提取。**lit/已知输入给 (0,c)，未知 x_j 给 (e_j,0)；加减逐项计算；乘法仅一侧依赖未知、另一侧为已知有理系数时保持仿射；除法仅除数为已知非零有理数时保持仿射。其余标记非仿射，绝不靠在初值求导当作精确仿射。
5. **有限变换。**应用有前提、来源和恢复图的局部等价代入/参数化；保留全部域、目标与检查。非线性坐标图仅在证明覆盖的分支有效。一般 presolve/排序/分解交上游；不默认生成稠密零空间。
6. **分类与编码。**LP/MILP/连续凸 QP→同一 HiGHS；光滑固定离散分支→CasADi/IPOPT。有限非线性结构按声明预算展开分支，未知连续守卫若不能正确分区则 unsupported。big-M 必须由有限域推出；严格不等式不伪装成 ≤b-1e-6，只能使用已声明间隔，或作为候选检查保留未知边界。
7. **恢复与实际交付。**从 backend 候选恢复全部变量、离散选择和构造输入，冻结候选 Realization 内容并计算 hash，再按原始类型、域、要求和数值交付规则验收。检查结果绑定该 hash；数值候选与实际构造都通过后才允许持久提交，Realization 本体不反向包含检查结果 hash；源 AST 不回写求解结果。

有限分支全部被覆盖且每支具有合法外模型不可行证据，才可合并为全域不可行；漏分支、预算用尽、局部 NLP 失败均不能这样合并。feasible-incumbent 允许验收合格但尚未最优的解；certified-gap 要有同一接受域的合法上下界且间隙达标。IPOPT 局部最优标签不能完成后一承诺。高阶比较、布尔结构、混合非线性超出接受域时精确诊断，不为了交付擅自固定变量。

HiGHS 支持的 LP/MIP/连续凸 QP 分类依据官方说明；NLP 的显式 f/g/x、变量界和约束界映射依据CasADi 接口。AST、来源保留与分层契约是本项目设计，不将它们归称上游自动提供。

6. 完整的小型 AST 与确定的降低结果

下例是 inputs.definition.const.value 的完整值，输入端口 span 绑定现有 {const:{type:"Length",value:"0.04",unit:"m"}}。它定义一半跨度，交付 typed 数值，故不需要虚构几何构造或 assertion。输入端口、输出 halfSpan:Length 及模块 hash 仍由外壳提供；这不是能直接提交给当前产品的完整 ModuleNode。

{
  "expressions": {
    "e.span": { "op": "input", "name": "span" },
    "e.zero": { "op": "lit", "atom": { "type": "Length", "value": "0", "unit": "m" } },
    "e.two": { "op": "lit", "atom": { "type": "Real", "value": "2" } },
    "e.x": { "op": "var", "id": "x" },
    "e.twox": { "op": "mul", "left": "e.two", "right": "e.x" }
  },
  "variables": {
    "x": { "type": "Length", "unit": "m", "role": "unknown", "domain": {
      "kind": "interval",
      "lower": { "value": "e.zero", "inclusive": true },
      "upper": { "value": "e.span", "inclusive": true }
    } }
  },
  "laws": { "law.half": { "left": "e.twox", "right": "e.span" } },
  "requirements": [],
  "goal": { "kind": "feasible" },
  "continuation": "fresh",
  "constructs": {},
  "outputs": { "halfSpan": { "expression": "e.x" } },
  "scope": { "writable": [], "preservedAssertions": [] },
  "budget": { "compileNodes": 1000, "branchCases": 1, "solveMilliseconds": 500 }
}

令 x 的 offset=0 m、scale=1 m，降低得到 0≤z≤1/25、2z=1/25，目标为零。仿射行是 terms=[{column:0,coefficient:{n:"2",d:"1"}}]、constant=0/1、lower=upper=1/25；来源包含 law.half 和 span 输入。等价代入得到 x=1/50 m，本例可以直接求值，不必启动 HiGHS。预算是示例显式输入，不是全产品性能承诺。

即使本例解析解已知，向 binary64 / OCCT 的交付仍单独核验。写入两个源量 span=0.04 和 x=0.02 再删除等式，会丢失“始终一半”的设计；正确持久化是保留上述 AST，并把已选值放入 Realization。

7. 失败、身份与实现检查点

阶段	必须返回的内容
解析/绑定	非法字段、缺失引用、未知模块/单位、重复驱动者；精确源 pointer，不尝试求解
编译	unsupported-domain / unsupported-coupling / compile-budget；指出具体算子、变量或关系，不伪装成无解
求解	后端终止原因、候选是否存在、已覆盖分支；候选验收、全域证据、最优性结论分别记录
验收	原 assertion、原单位残差/区间、证据等级、pass/fail/unknown；不只返回矩阵行号
提交/恢复	依架构绑定规则封存所选结构、数值表示、恢复结果和构造；恢复不重新执行设计搜索

修改源 AST/要求改变 modelHash；改变输入闭包、编译器、后端配置和容差策略使相关求解缓存失效。规范 JSON 使用现有 NFC/JCS 哈希设施，map 顺序不决定身份；数组中具有语义的次序保留。branch 生成次序稳定不等于浮点求解跨机器逐位确定，选解结果仍必须封存。

构造地址与实现内容身份分开。当前降低器以 NFC/JCS 哈希 ["aira.relation-construction-address/1", sourceNodeId, constructName, operationRef, operationContractHash] 生成派生节点地址；不使用整个 boundNodeHash 或拓扑遍历序号。于是同一具名步骤的尺寸改变、未知量选解改变和其他独立步骤插入不使该地址变化；换名或换操作契约改变地址。完整输入、解和构造仍进入 blockHash、execution modelHash 与 Realization 根，不因地址相同复用旧几何或旧检查。跨文档沿既有 document/revision/context 绑定隔离，合并图仍检查源节点和其他构造的地址冲突。

该规则只建立构造节点的地址，不证明面/边、工艺角色或替换算法等价。每次真实几何求值后仍按现有 SemanticRef 的 lineage、拓扑、基数和演化策略解析；被删除、分裂或更名的构造不得靠相似几何补回旧身份。源关系公开端口到构造地址的输出映射保存在 Realization。

当前已接入既有 exact-lineage 扩展：源关系节点保存以该关系公开 solid/shape 输出为 scope 的面定义，下游抽壳/倒角/圆角引用源定义。执行投影通过已核验的输出别名定位实际构造，保留 lineageOrigins、基数及演化策略，生成目标 scope 的面定义及新的选择器身份；源面 ID、定义 hash 和选择器 scope 必须一致。只有实际原生选择解析与几何要求检查通过才提交。源节点不写入派生节点或求解变量；投影后的定义属于 execution 身份，历史重放仍验证保存的完整 Realization。

这里复用 exact-lineage 的精确来源集合与 incident-semantic-refs 边选择，不允许按位置猜测重绑定。直接指向某构造的引用与指向关系公开输出的引用有不同的作用域：改名会改变构造地址，但若关系公开输出仍有恰一面满足原来的完整来源集合，公开引用可继续成立。丢失来源或出现歧义则拒绝候选。此机制不证明任意算法替换等价，不包含其他命名引用、工艺角色或产品分析目标的自动改写；未处理的关系 scope 仍返回对应不足。

预算为正安全整数，受已公开能力上限和宿主资源上限共同约束；不能因为源文档填写巨大数字就获得无限展开。预算、数值结果大小和构造数量在执行前检查，循环中保留取消点；超限诊断必须区分未尝试分支和已排除分支。

实施时逐条核对：同一 AST 的类型/域、降低模型、恢复映射和来源完整；固定输入可直接计算；改为 unknown 后可正确分类；每条变换有等价或包含关系依据；预算/取消/不支持不产生成功提交。文档中的例子是语法规约示例，不能代替编译器与实际产品接线的完成证据。

2.4 记录成员的关系模板（2026-09-21）

同一 relationTemplates.member 现在接受局部名称到成员相对路径的映射，例如 {mass:["mass"], load:["loads",0]}；字符串仍表示绑定当前标量叶，等价于该名称映射到空路径。路径中的字段与位置使用已有结构语义，必须落在标量叶。编译器先按数组声明的 element 类型检查全部路径，包括空数组，再对实际成员绑定原表达式；不生成新的变量或另建记录求解器。成员绑定、显式 captures、局部 expressions 名称互异，源语义仍为同一模板的有限合取。

设第 j 个记录为 rⱼ，绑定路径为 p₁…pₖ，模板体为 L。精确定义为 ∧ⱼ L(πₚ₁(rⱼ),…,πₚₖ(rⱼ),captures)。路径投影由字段/固定位置的结构递归唯一确定；编译只将局部名替换成该叶原有表达式，再进行原有无捕获展开。由路径长度归纳得到每个投影对应同一叶，由表达式 DAG 归纳得到值与定义域不变，最后由有限合取得源约束与展开约束相同。重复引用同一叶保持共享未知量，不能为每个成员复制变量；也不能把两个字段恰好数值相同当作身份相同。

令 k 为绑定数、h 为路径总长度，e/l 为模板表达式/约束数、n 为数组长度。先检查声明成本与 n(e+l+k+h) 的工作预算，再展开；路径遍历与生成按这些有限量计费，不枚举变量取值或成员组合。预算耗尽拒绝编译，不表示数学不可行。源记录、映射和模板进入原模型哈希，派生节点保留原模板及成员路径；求解、精确候选检查、封存与重开均复用同一展开链。该规则支持固定记录/嵌套定长数组的标量字段关系，不隐含数量未知的构造实例或递归模块生成。

实际原生链已核对记录 Bool 字段与嵌套定长数组字段共同实例化关系，两个成员保留共享未知量；公开关系创建/编辑驱动几何宽度从 3/8 m 变为 1/16 m。源模板保留、私有辅助量不暴露为可编辑源变量，禁止 Worker 后重开保持封存实现；重新哈希的辅助量分类篡改仍拒绝。空数组的越界绑定在编辑中拒绝且 head 不变。契约/工具构建、Web 类型、Core WASM 构建及改动 ESLint/格式检查通过；此能力的接线核验结束。

2.5 记录集合的选择与折叠（2026-09-21）

index 与 fold 的 elementPath 可指定每个元素内的固定字段/数组位置路径，省略表示当前标量元素。例如同一 parts 数组可用 index/elementPath:[“width”] 读取被选部件的宽度，用同一 index 变量及 elementPath:[“flags”,0] 读取该部件的布尔字段；fold/elementPath:[“mass”] 表达按原顺序累加质量。AI 不需要先复制记录为平行标量数组，源仍只有一份成员数据。路径必须在声明元素类型和实际成员中落在标量叶，空 fold 也检查元素类型路径；空 index 仍拒绝。

设 A=[r₀,…,rₙ₋₁]，πₚ 是已有固定路径投影，语义直接定义为 index(A,i,p)=πₚ(rᵢ)，fold(A,p,op,z)=fold(op,z,[πₚ(r₀),…,πₚ(rₙ₋₁)])。编译先读取各投影对应的原叶表达式，再复用已证明的有限索引编码或严格左折叠。由固定投影的结构归纳与原索引/折叠等价定理组合得到变换保持值、定义域与共享变量。多个字段若引用同一源索引 i，各自私有选择量均受 k=i 约束，因此必定选中同一记录；不能对每个字段另选有利的成员。不同源索引仍表示作者明确声明的独立选择。

数值字段继续由当前精确仿射包络推导辅助值域，不以记录中其他字段的界替代；Bool 字段继续使用有限守卫 DAG。非仿射/无有限界的限制不因记录投影而消失，未知不能伪装成可解。折叠不交换操作次序，不用实数结合律重排浮点执行。路径长度 h 的额外成本为 (n+1)h，与原节点生成成本合并检查；仅对已经声明的有限成员作展开，不枚举未知量取值。源 elementPath 与结构均纳入原模型身份，恢复从同一源重建后核对原封存块。

实际原生链已确认同一记录的 Length 与嵌套 Bool 字段受同一 choice 约束，Bool 关系驱动真实几何宽度 3/8→1/16 m；记录宽度 fold 返回精确 7/16 m。原生编辑的越界 elementPath 返回 RELATION_STRUCTURE_PATH_INVALID 且 head 不变；源结构保留，辅助量不暴露为源变量，禁止 Worker 的历史重开保持同一实现，重哈希分类篡改拒绝。契约/工具构建、Web 类型、Core WASM、改动 lint/格式通过。此字段投影能力接线核验结束，不外推为数量未知的记录或构造生成。

2.6 固定成员的构造模板（2026-09-21）

现有 relationTemplates 可附带 constructs，使用同一 RelationConstruct 与锁定 Operation Module。模板表达式、when 及构造配方的 expression/select.condition 引用局部 member/captures/expressions；配方 output 引用该模板的局部步骤，显式 input 引用当前关系节点的外部绑定。局部名称先核对，实例化后继续由原依赖图检查构造环、模块类型/输入/输出及守卫可用性。模板没有另一个执行器，也不能递归实例化关系节点。

普通 RecipeValue 增加 {instance:{template,index,step,port}}，静态指定模板数组的一个成员构造输出。展开为该成员步骤的普通 output，之后与原 expression/input/output/list/select 配方共用求值；既有 select 可从多个合法实例输出中按关系条件选择，list 可组合多个输出。index 是固定源位置，不是求解器未知量；缺模板、缺步骤或越界拒绝，输出端口和 guard 由原链接器检查。源输出实例不是新的公共可编辑几何权威。

保持性。 对每个固定成员 j，以原字段叶和显式 captures 构造无捕获替换 σⱼ，对局部构造步骤作一一重命名 ρⱼ。每个输入配方的 expression 由 σⱼ 替换，output.step 由 ρⱼ 替换，列表顺序、select 条件/两分支、模块身份与 when 保留。表达式与配方的结构归纳保证输入值及定义域相同；在既有构造 DAG 的拓扑序上归纳，各步调用同一模块、相同输入与 guard，故交付遵循相同模块契约。循环仍被拒绝，浮点/几何失败仍由原检查处理；没有从源展开推出全域几何成功，也没有对两个不同几何算法声明替换等价。

地址与编辑。 生成步骤保留模板构造 Pointer 与数组成员 Pointer；lowering 以这两个来源、原关系节点和模块契约生成构造地址，不能用全局私有分配顺序决定地址。增加无关表达式不应改变既有成员构造地址。数组插入/重排会改变位置含义，不保证原成员工程身份；需要稳定身份的设计必须保留位置或明确编辑引用，实际 face/edge lineage 仍按原契约核验，地址相同不证明拓扑相同。封存保存活动实例构造、全部潜在步骤来源与选定输出；恢复重新展开并核对整块，不重新挑选模板或成员。

公开来源与激活。 展开是从源构造与成员到私有步骤的重命名；若公共结果只保留私有步骤编号，客户端不能直接逆向定位源。因此 lowering 对每个已展开步骤封存 constructionSources：源构造 Pointer、可选成员 Pointer、可选 guard 引用及 active。令 K 为展开步骤集合、A 为活动子集，要求来源映射的定义域为 K、nodeIds 的定义域为 A，且 active(k) 等于 guard 的封存布尔值（无 guard 为真）。TS/Core 检查活动映射与守卫一致性；完整性及来源真实性由恢复时从原源重新展开、降低并比较整个块保证，单独内容哈希不提供该保证。原生读取投影同一映射，未启用成员有来源但没有实体编号；不执行第二次求解，也不由源位置宣称稳定工程身份。新增存储/遍历为 O(|K|)，不枚举变量组合，受既有块大小及编译预算约束。

工作界。 n 个成员、每体 e 个表达式、l 条关系、c 个步骤及 r 个配方节点，生成规模 O(n(e+l+c+r))，另计路径绑定和最终实例引用替换。声明扫描、实例分配和配方重写均消耗同一 compileNodes 上限；生成前核对主要实例规模，实际遍历再次计费防止嵌套配方突破预算。有限源展开没有遍历未知数值组合。当前固定成员构造不表示未知数量实例、任意递归模板或动态拓扑身份推断。

实际原生接线已确认两条记录各实例化 sketch.rectangle 与 exact.linearExtrude，共四个构造步骤；关系 Bool 条件选择对应实例作为主实体，编辑后选中宽度由 3/8 m 变为 1/16 m。增加一个在私有分配序列中更早的无关结构表达式后，四个构造地址保持；源模板 constructs 保留。越界 instance 引用拒绝且 head 不变；禁止 Worker 的历史重开保持原实现，重新哈希篡改仍被重建拒绝。契约/工具构建、Web 类型、Core WASM 与改动 lint/格式通过。该固定构造模板的接线验收结束，不追加同类样本。

2.7 有界数量选择与守卫的结构等价（2026-09-21）

本节的 Bool 谓词及端口实现不等同于开放 Bool 变量；后者的实现义务见 §2.8。

不需要再造数量专用语法。给定 N 个潜在成员的有限源数组，每个成员显式携带位置 j，一个共享有限 Int/Count 未知量 n 表示启用前 n 个成员；模板表达式 active=(j<n)，相关 constructs.when 引用 active，成员 law 若只对启用成员成立也应显式使用该 when。源声明 n 的合法有限域与目标，关系编译成同一求解问题，不逐个 n 生成几何试解。潜在成员的源变量/结构叶仍存在，其域与未加 guard 的关系仍有效；这不是删掉非活动成员的一切约束。未知结构数量的本项接受域是有固定潜在成员上界的条件实例，不含无上界或递归对象生成。

跨节点布尔边界的原始缺口（2026-09-21，已由下述有限守卫接线替代）。 单节点能使用 Bool 守卫，不推出联合编译已支持 Bool 端口。原实现仅由 knownRelationOutput 传播源已确定的布尔常量，未确定的 Bool 没有进入符号绑定、联合行与恢复见证。下述实现替代此前的 RELATION_JOINT_BOOLEAN_BOUNDARY_UNSUPPORTED 统一拒绝；不支持的谓词仍按实际编译边界拒绝。

其正确降低必须保留 b⇔P(x)，即两个方向的蕴含；仅加入 b⇒P(x) 允许 P 为真而 b 为假，会扩大源可行集。对有限域变量的比较可由其既有域成员选择变量求和得到真值，再用共享 Boolean DAG 组合 not/and/or，不能展开全部变量赋值的笛卡尔积。消费者私有 Bool 列与该真值必须等价，来源、私有量剔除、完整候选重验和恢复重建须一起贯通。源已知布尔值直接代入，不启动优化器。连续严格比较的边界不能用任意 epsilon 冒充等价；只有源域能提供已证明的分离界或后端能表达对应严格谓词时才降低，否则 unknown。需要扩展的是现有联合编译与见证类型，不引入独立布尔求解器或第二份源模型。

有限守卫边界的实现推导。 上段记录接线前缺口。现消费者私有视图以 Int 列 z∈{0,1} 替换未知 Bool 输入，每个 Bool 读取变为 z=1；列表与条件配方仍由既有代入遍历覆盖。生产者 P 是既有 compileFiniteRelationGuards 能表达的有限域比较及 not/and/or DAG，联合编译给其依赖与变量统一改名，并禁止 XOR(z=1,P)。于是任一联合可行解满足 z=1⇔P；反向将源真值映成唯一 0/1 可得到等价辅助赋值，消去 z 恢复原可行集。每条边仅增加常数个 DAG 节点，不生成赋值笛卡尔积。相同节点内的布尔等式与跨节点边界复用同一 XOR 构造。

选定候选后，生产者布尔输出以 kind:boolean 封存在同一 exactOutputs，消费者按原 Bool 类型代入并记录布尔 inputSpecializations；私有 z 从已提交 variables 中剔除。恢复从生产者已存真值暂时恢复 0/1，再检查整个联合问题和重建源输出、代入与块身份，不能仅相信保存的 true/false。未能编成现有有限守卫的谓词，以及带布尔边界的未支持非线性联合问题，仍明确拒绝；没有任意 epsilon、另一个求解器或源模型。当前 Schema 在原生成链内扩充布尔输出与代入值，Core 内嵌 Schema 同步重建，不保留旧新双版本。

谓词组合的结构归纳。 当前 Bool 类型允许 cmp.eq，不等用 not(eq(a,b)) 表达。若 a、b 已分别编译为等价守卫，则 eq(a,b) 编译为 not(XOR(a,b))：异或只在两侧真值不同时成立，取反恰好得到源等式。以常量及有限数值比较为基例，not/and/or/eq 为归纳步骤，可覆盖这些规则构成的有限无环布尔表达式，而不枚举变量赋值。实现复用 emitBooleanMismatch，保留共享子表达式；依赖收集必须递归进入布尔比较的两侧，不能把它们当作数值叶终止。每个未知布尔等式增加四个辅助守卫，根为 not；辅助守卫计入编译预算并避开源表达式名称。不能编译任一子谓词时保持未支持状态，不将其当作 false。此结论不覆盖独立 Bool 未知量的域编码、连续严格比较或未知条件的任意输出配方。

有限跨节点边界已通过原生链验证：消费者 true/false 要求更新上游有限选择，私有 0/1 列不进入源变量，布尔代入与输出封存，禁止 Worker 后重开保持实现，伪造真值被联合候选检查拒绝。谓词组合扩展已完成类型、lint 与构建，并沿同一原生流程将消费关系改为 eq(eq(flag,wanted),true)=true，核对嵌套比较的依赖与守卫顺序、更新上游选择、封存恢复及篡改拒绝。Core 的 known::binary 已处理 Bool eq，verify::evaluate_guards 按依赖序检查 not/and/or，故不另建核验路径。此运行只证明该组合规则的实际接线，不代替上述结构归纳，不计作 AI 自主成功率；本项验证结束。

Bool 条件输出的等价降低。 对有限可编译谓词 c、a、b，select(c,a,b) 等价于 (c∧a)∨(¬c∧b)。未知条件生成三个辅助守卫和一个根，保持 DAG，不分支试解；已知条件只编译选中子式，不要求未选中子式可编译。依赖收集同步按已知条件裁剪，未知条件才收集两侧。Bool 输出配方若叶仅为 expression/input，则在已经通过源类型检查的私有节点中按后序转换为同一 select 表达式，再经原 link 检查；持久源定义不变。含 output/instance 等构造叶的配方保持原样，不能把未来几何执行结果伪装成已知代数谓词。遍历及新增表达式受原 compileNodes 预算约束，表达式数量一次计数后递增，不在每个节点重复扫描全表。生成名称避开全部源表达式；既有联合见证、候选重验和恢复消费此私有视图，无第二份设计权威。同一原生流程改用条件 Bool 输出后，true/false 联动、嵌套等式、私有列剔除、免 Worker 重开与篡改拒绝均通过；不据此宣称任意数值分段输出或构造结果可联合求解。

消费实例必须证明其 guard。原传播器只按 expression ID 识别事实，模板生成的 j<n 与消费端单独声明的 n>j 因 ID 不同被拒绝。当前在已类型化表达式 DAG 的依赖序上建立结构等价类：叶保留完整类型/单位/字面量及输入/变量身份，父节点键使用操作与子类编号；只将 gt/ge 交换操作数转为 lt/le，并对 eq 的两个操作数规范排序。既有 and/or/not 事实传播同时作用于同类表达式，不增加 SAT、数值采样或任意代数化简。

证明与成本。 叶键相同蕴含同一环境下值与定义域相同；父节点具有相同操作和相同子值/定义域，按 DAG 归纳成立。比较交换满足 a>b⇔b<a、a≥b⇔b≤a 和等式对称性，不重排算术、折叠单位换算或消去未定义表达式。等价类没有使用候选数值或近似相等。故将一个守卫事实传播到同类节点保持可靠性，原不完备传播规则仍只在能证明时接受。键引用子类编号，不展开共享子树；存储按 DAG 和原文字面量规模增长，事实队列每个节点至多加入一次。

原生链已用同一 count 未知量驱动两个/一个成员的实际构造（每成员一个草图与一个实体）；仅启用成员进入 Realization，保留成员的地址不变，免 Worker 重开保持原选解。模板使用 j<count，消费端使用 count>j，按结构等价接通。把消费端条件故意放宽，不能证明目标存在时仍返回 RELATION_CONSTRUCT_AVAILABILITY_UNPROVEN，head 不变。现有 fallback 构造与潜在模板成员分别计数，未将辅助构造冒称启用成员。此接线验收结束；尚不支持的非有限守卫、非仿射边界或无界结构仍明确诊断，不能将这一次成功外推到任意 MINLP。

2.8 开放 Bool 变量：源真值与求解坐标的双射（2026-09-21）

有名定义的组合规则。 对已类型检查且无定义环的 Bool 派生变量 b:=E，编译 var(b) 必须沿 value 引用编译 E，再以同一守卫含义表示该读取；它不产生新的源未知量或独立选解。依赖收集同步遍历 value，不能在变量名处提前终止。结合已知真值、有限 Bool 未知量及已支持的有限数值比较为基例，not/and/or/eq/select 与有名定义为归纳步骤，可组合成此语法范围内的有限无环 Bool DAG。共享表达式按已有 memo 和预算处理，循环仍拒绝；定义包含不支持的叶时保留未支持，不能假定为常量。该规则已接入 relation-guards 与 relation-compiler；同一原生流程通过派生 Bool 读取源选择后，联合修改、公共真值、免 Worker 重开和篡改拒绝保持，无新增表达式语法或求解器。这是定义引用的语义保持，不证明任意连续谓词可判定。

状态：有限 Bool 未知量已贯通共享线性/离散求解、源候选、封存与公开读取。 Core 按源类型保存 Number 或 Boolean；Bool 只接受严格的 {kind:boolean,value:true/false} 对象，数值细化及候选键集合检查保持。assembleRelationProblem 将源 Bool 有限域及初值映成 Int 坐标，源 AST 不变；源 Bool 读取编译为该坐标等于 1。RelationScalarWitness 继续只表示数值坐标，新增生成类型 RelationSourceWitness 在封存 variables 与公共结果 Schema 中引用。Core 源求值仍仅声明 candidate-expression-evaluation，域与关系由既有精确代数检查承担。Bool 域成员必须是源已知真值；不从浮点容差猜真假，不增加求解器。

令源有限域 B⊆{false,true}，定义编码 e(false)=0、e(true)=1，解码 d(0)=false、d(1)=true；d 对其他数未定义。则 d∘e 为 B 上恒等，e∘d 为 e(B) 上恒等。对多个 Bool 变量逐分量应用此双射，不生成其笛卡尔积。每个变量只增加一个整数坐标，域为原 B 的像；保留单元素域，不能一律扩张成 {0,1}。空域或未能求值的域按现有准入/unknown 处理，重复成员不改变集合语义；初值只编码为初值，不能成为约束或默认选解。

源谓词中的读取 b 解释为 z_b=1，其余组合按 §2.7 结构归纳。源非布尔量原样保留。于是恢复映射 R 对数值量恒等、对布尔坐标应用 d，满足 R(S(C(D)))=S(D)，前提是每条源域、关系、目标与保持要求均已保留。源目标若通过 select 引用 Bool，仍须拥有合法的数值目标编译；本双射不能证明未经支持的分段数值表达式或 MINLP 可求解。求解器返回 0.999999 不能四舍五入为 true：必须先按既有精确候选检查确认整数、域与关系；非 0/1 拒绝该候选，不宣称源问题无解。

一条候选链、两种明确类型。 数值求解坐标继续使用现有 rational/binary64 见证，不把 Bool 交给有理数解码器。源候选增加明确 Boolean 真值分支，按源变量类型检查，禁止把 JSON 数字或字符串隐式转成 Bool。共享编译结果保存由源定义确定的变量编码映射；后端提案经精确检查后解码为源候选，Core 以 Bool 代入原表达式重新核验。映射是可重建的编译结果，不是另一份可编辑的权威模型。实现不得将所有 RelationScalarWitness 使用点无差别放宽为任意联合类型，数值后端继续保持数值输入契约。

源码职责按现有纵向链落实：

• relation-problem.ts、relation-guards.ts：从已类型化 Bool 域构造整数坐标和读取守卫，不能要求 AI 提交数值代理；域、初值、预算与源位置同一映射。
• relation-solve.ts 保持数值提案与精确数值检查；共享候选调用处及 relation-joint-execution.ts 按同一映射编解码。联合拆分先依据节点与源变量身份，不从遍历顺序推断类型。
• relation-known.ts 与 Core known.rs：源候选按变量类型绑定数值或真值；键集合仍必须完整相等，类型错误不走 JS truthiness。源求值先恢复真值，再执行原 Bool 表达式。
• 封存 schema、relation-lowering.ts 和 relation-realization.ts：variables 中的源 Bool 保存真值，sourceVariables、公开读取及结构叶保持源类型；求解代理不能冒充源开放量。继续沿当前生成链同步 Core schema，不维护旧新双版本。
• 恢复按源声明重建映射，将保存真值编码回坐标核对联合约束，再重新求值并比较整个实现块。源域或变量类型改变后不能复用旧映射或旧见证；无需启动求解器。

完成判据是上述编码、源候选、原子提交、公开真值与免搜索恢复共同贯通。结构归纳承担组合覆盖论证；实际操作只核对这条链与错误类型/非法坐标的拒绝，不按变量数、产品名称或布尔赋值扩展试验。当前有限 Bool 变量已经接通这些边界；不据此放开数值分段目标、未经支持的派生谓词或非线性布尔耦合。

源代入已通过重建 WASM 直接调用：Bool 真值保持，not/select 按原源表达式求值；数值见证、字符串真假、额外字段及缺失变量拒绝。此检查绑定当前模块哈希，不绕过 node contract；返回 scope 仍为 candidate-expression-evaluation。Rust fmt/Clippy、WASM 构建、Web 类型及改动 lint 通过，后端编码与封存接线的验证见下段。

完整接线沿既有原生流程核对：源 Bool choice 参与联合关系，消费者 true/false 要求改变其源真值；条件输出与嵌套等式保持，私有消费者坐标不泄漏。model.read 按 revisionId/select 读取 variables.choice 的 kind:boolean，禁止 Worker 后重开保持同一 Realization，伪造输出真值被拒绝。公共查询使用公开别名，首次脚本误用内部节点 ID，按实际投影修正后通过，未修改产品别名契约。数值候选哈希与源候选哈希分别绑定各自表示：共享入口显式计算 solverCandidateHash 对照代数检查，Core 的 candidateHash 绑定解码后的源真值，lowering 校验后封存；恢复重编码再检查，不要求二者哈希相等。契约/工具构建、Core WASM、Web 类型/生产构建与相关 lint 通过，本项验证结束。原生 build-relation 的同源 Schema 描述已公开 Bool 声明与真值读取方式，AI 无需了解 0/1 编码。

原生构造的发现闭包（2026-09-21）

关系构造源必须带 operationRef、operationContractHash 和正确端口绑定。Schema 能规定这些字段的形状，却不能告诉调用者当前锁定目录中的哈希值及每种操作的端口；哈希也不能从自然语言需求推导。因此“完整关系 Schema 已公开”不足以满足无源码先验的发现要求。每个不可由需求推导、又被执行要求的值，必须由同一公开接口提供，或由宿主从权威目录注入。

当前复用已有目录解析、契约投影和完整 Schema bundle：aira_library_reference 的 scope: operations 搜索当前打包的锁定目录，返回目录身份和最多 32 个摘要；按精确 operationRef/capabilityId、detail: full 返回唯一契约及全部 Schema 依赖。构造的 operationContractHash 取 moduleHash，不让模型猜测。未指定 scope 的现有库与计划查询保持原职责。操作搜索不分页；需缩窄查询，结果数不宣称目录总数。目录内容仍不证明候选可执行、权限满足或操作适用于关系构造。

底层原生接口与 SDK 复用移入 contracts 的同一投影实现，原 Web 目录实现删除；没有复制操作描述或另建工具执行器。SDK 查询与实际 MCP tools/list、tools/call 已核对矩形构造哈希、端口和资源闭包，关系计划查询仍能返回完整源定义 Schema。这是发现路径的接线证据，不是外部 AI 自主设计成功率；真实模型建模及需求修改的限定结果见下一节。

P6 真实模型闭环的首轮反证（2026-09-21）

用户授权现有模型、总费用不超过人民币 20 元。使用现有 DeepSeek gateway 与产品 bounded-step/SDK 执行链，从空模型给出自然语言任务：厚 6 mm、高 40 mm、宽为 [60,120] mm 待求量，宽高乘积保持 3200 mm²；保存关系后另给高度改为 50 mm 的需求。没有向模型提供源码、关系定义或人工修复提示。任务判据是实际持久关系、实体及修改后的交付，不能由模型声明 done 推出。

基线 6 次 API 请求后没有创建节点。关键反例是：① 模型实际收到的 decision Schema 仍是手写副本，resources 被声明为 boolean，与 SDK 的对象类型冲突；新发现字段 scope 未进入这份副本。② finishReason=length、空文本且无工具调用被转换为 done，产生虚假完成。③ SDK 输入校验错误从读取路径抛出，绕过正常诊断与修正循环。它们是可复现的产品接口缺口，不能归因于模型不会建模。

修复从同源性推导：read/lookup 字段直接机械投影 SDK Schema，删除手写选择器副本；没有完整回答的截断/空响应进入非法决策诊断，只有正常 stop 的非空文本才可作为原有文本结束方式；执行前的输入错误返回可修正诊断，取消与非输入运行错误继续保持原失败语义。零费用核对确认资源类型和操作 scope 对齐 SDK、非法读取返回诊断，服务器检查确认空/截断不再为 done。随后已用相同需求真实运行，结果如下；这些零费用检查本身不作为任务成功。

预算核查也发现原循环仅声明 token/费用上限，未在步骤中消费。现补充调用前及用量累计后的 token 检查、真实 gateway 用量完整性检查；这属于已用量上限，不能冒充下次调用的费用预留。本轮另在真实 provider fetch 前限制模型、输出 token 和总实际请求次数，重试/失败亦计数。按 DeepSeek 官方价格 的高峰输入 2 元/百万、输出 8 元/百万，保守取最大输入 1,048,576 token、每请求输出 8192 token，单请求上界 2.162688 元。基线全部用量按无缓存高峰价的上界为 0.43749 元；在剩余额度内最多再放行 9 次，总上界 19.901682 元。运行产物留在被忽略目录，不提交密钥或模型推理文本，不将已有 USD 估算字段当作本轮人民币账单。

修复后的实际结果与边界

同需求修复运行使用 9 次调用，保存一个 design.relationSystem：width 为 [60,120] mm 未知量，height 绑定可编辑参数，面积律 width×height=3200 mm²，厚度 6 mm。模型通过操作发现取得哈希与端口，自行纠正枚举字面量绑定错误；一次输出截断已进入诊断并继续，没有误判完成。模型自主提交高度 40→32→40 的检查，实际候选测量宽度 80→100→80，面积和体积保持。源变量的封存见证 2/25 是 SI 米（80 mm），不是数值 80；模型摘要对此有不严谨表述，以源和交付证据为准。

该阶段达到预先保守预留的 9 次调用额度，后续请求在真实 fetch 前被拒绝，没有新增计费。核对全部实际用量后，累计上界 1.750166 元；同一 20 元授权剩余最多放行 8 次（最坏累计 19.05167 元）。前一临时浏览器已关闭，因此从记录原样回放模型两份成功计划恢复几何，再向模型只给原定高度 50 mm 与 STEP 需求；没有人工修改设计或提供解法。后续用了 4 次调用，模型仅编辑 p:height，width 自动解为 8/125 m=64 mm。公开求值为包围盒 [-32,-25,0]..[32,25,6] mm、6 面、体积 19200 mm³，单一有效实体要求通过；最终源定义、面积律和宽度域保持。Session 销毁后从同一 IndexedDB 重开，Realization 哈希与完整公开求值保持。此重开是后续会话的持久化检查，不冒充先前关闭浏览器数据的直接恢复。

原模型计划含 export-step，执行状态 completed。零费用原样回放取得交付字节，STEP 为 AP214CD、mm、15463 字节；SHA-256 为 c9151be3c2632f94d54e3532a235a5a5b8c4f93d05a39eb5e09475e9a733a446，与真实模型收到的收据一致，源 B-Rep 哈希也与最终求值一致。当前环境未运行独立 OCP 读回，不能声称第三方几何验收完成。交付文件是几何 STEP，不包含可编辑关系；关系留在原生文档与封存实现中。

费用按实际返回 input/output token、全量无缓存高峰价保守计算：基线 154173/16143 为 0.437490 元；修复 547226/27278 为 1.312676 元；指定修改 127005/5757 为 0.300066 元；总计 19 次调用、2.050232 元。这是价格上界核算，不是服务商账单；没有缺失用量的计费调用。计费网关已停止，未花完预算不构成继续调用授权。

结论限于一个预先指定任务：外部模型已经通过公开产品工具自主发现、构造持久关系、按诊断修复并完成需求修改；数学求解承担宽度重算。修复前后同输入的结果从未建模变为完成交付，但单次随机模型轨迹不构成统计因果估计，没有独立留出或一般成功率结论。常规模型知识仍存在，所谓无先验仅指不提供 Aira 源码、专用技能和人工建模方案。没有引入新求解器或平行 Agent 循环，也没有放宽浮点或几何判定来得到通过。最后核查还纠正已有界面索引的 resources:true 示例为 resources:{}；这是 SDK 契约同步，不是针对该题的提示补丁。

P6 计划组合与恢复的公开语义（2026-09-21）

模型索引曾同时声称整个 plan 是原子事务以及每一步独立提交；SDK 与实际执行采用后者。这不是措辞细节：若已提交 S₁ 而 S₂ 失败，当前状态是 S₁(D)，不是 D；让 AI 按整体回滚理解会重复创建已存在对象。现纠正索引两个整单原子性声明，明确失败或取消不撤销早前提交，依据 diagnostic、changes 和当前状态只提交剩余工作。没有改变源模型、事务或历史语义；需要同一不变量下同时修改的多项关系仍由已有 edit-relations 的单一候选/提交承担，不能用顺序 plan 冒充联合原子修改。

沿真实原生 SDK，以模型上一轮成功关系方案原样重建，再提交两个参数步骤：height=50 成功后 height=60。由 width≥60 mm、height=60 mm 得面积≥3600 mm²，与面积律 3200 mm² 矛盾，因此第二步应拒绝，无需尺寸遍历。实际返回 needs-repair、stepsCommitted=1、RELATION_INFEASIBLE，诊断带原面积律与 width 域来源及 exact-algebraic-infeasibility 检查通过的证据；最终包围盒 [-32,-25,0]..[32,25,6]，Session 重开公开求值完全一致。该零费用操作核对失败路径与持久状态，不计作 AI 自主恢复成功，也未在本次重跑取消路径。改动 lint、diff 检查通过；此前构建/类型结果仍适用于未变更的执行代码。

P6 引用集合随计划前缀变化（2026-09-21）

生成时的模型快照只有引用集合 R(D)，而第 k 步的合法引用来自 R(Sₖ₋₁…S₁(D))。当前缀创建对象、节点或参数时，后者不必是前者的子集。因此把 bodyId/nodeId/parameterId 限成当前摘要枚举，会拒绝合法的先创建再使用；body 摘要也不包含所有无 Body 的关系/分析节点，不能充当 nodeId 全集。即使摘要未截断，此约束仍然错误。

现删除 decision-schema 的摘要别名枚举及 gateway 为此传入的快照参数；决策层保留引用字符串形状，既有完整计划 Schema、逐步 resolveExactAliases、目标类型检查、授权和事务验证仍为执行权威。没有自动接受不存在的目标，也不增加一套未来对象索引。真实 SDK 执行已有关系底板后，在同一个计划创建 auxiliary_plate，再以 b:auxiliary_plate 设置 6061-T6 材料；返回 completed/stepsCommitted=2，公共 Body 材料绑定正确，Session 重开求值一致。此为零费用执行接线检查，不计作额外模型成功率；Web 类型与相关 lint 通过。

P2 条件数值端口的联合仿射编译（2026-09-21）

此前 outputValue 只能在候选确定条件后解释数值 select；若下游关系需要用该输出约束上游，编译在选解之前即拒绝。这不是缺少求解器，而是缺少条件边界等式。

令输出 y=select(c,a,b)。当 c 是既有有限守卫可编译的 Bool、a/b 是有定义的有理或仿射量时，它与两条关系 c⇒y=a、¬c⇒y=b 等价：任意源真值恰好激活一支，故既不遗漏合法输出，也不允许额外值。嵌套配方以沿途条件合取定义叶守卫；递归分割覆盖原条件域。实现遍历源配方语法，不枚举变量真值或求解候选；条件路径复制也消费 compileNodes 预算。配方 select 与直接引用的 select 表达式通过同一只读分支视图处理，分支再次直接引用 select 时递归应用；没有改写源 AST。包在加法、乘法等任意算术运算内部的 select 与未经支持的非仿射叶不被本规则分配展开。

联合编译复用消费者已有的私有边界坐标和源变量，不新增一套持久变量。各叶通过同一类型/规范单位检查，用同一 alpha-renaming 合并进联合线性问题；守卫由既有有限 Bool DAG 编译，条件等式经既有 Core 精确候选核验。源、目标和要求不改变，非线性或无法编译的守卫继续明确拒绝此路径。

条件行所需边界不能使用任意大 M。对全部可能叶的仿射值，由现有 encloseRelationAffineJson 在完整联合源变量域上求精确包围 hull；只有该边界坐标确为编译器创建的无界 interval 时，才赋予该推导域。它是所有合法分支值的外包围，因此不会删除原解；真实分支选择仍由守卫等式限制，不把 hull 内任意值当成合法输出。缺少有限界、无法建立包围或预算耗尽，不签发源不可行结论；参数域与请求哈希重新核对，不按某个 incumbent 猜界。现阶段相互依赖且不能从现有源域得到有限包围的条件边界仍未支持。

已知条件只访问选中子树；只有实际被另一关系读取的标量端口才为联合编译提前收集条件，其余施工输出继续在候选确定后按需解释。候选选定后 outputWitness 用原配方重新求值，选定精确输出、源 Bool 真值及条件代入进入既有 Realization；重开重新构造联合守卫/包围及完整块并核对身份，不启动求解器。

实际 SDK 关系实体链：数值端口在 40/50 mm 间选择，下游要求 50 mm 得到 false 分支及精确 1/20 m；修改下游要求为 40 mm 得到 true 分支及 1/25 m。要求 45 mm 被拒绝且 head 不变，禁止 Worker 后重开保持实现根。最初验证脚本误把必须生成 Body 的 build-relation 用于纯标量节点，现改为真实关系实体附带数值输出，未修改产品 Schema 来迁就脚本。Web 生产构建、类型及改动 lint 通过；本结果不等于一般分段数值表达式、MINLP 或任意非凸问题的全局求解。

同输入改写为输出直接引用 select 表达式后，真实 SDK 仍完成 50→40 mm 反向选支，45 mm 拒绝且 head 不变，禁止 Worker 重开保持实现根；Web 类型与改动 lint 通过。这验证两种源表示在该输入上的执行与恢复一致，不构成所有嵌套表达式的覆盖证明。

P2 布尔端口环的求解语义与执行顺序（2026-09-21）

直接标量关系端口声明联立等式，不是“先执行生产者再执行消费者”。这一结论与标量取值是实数还是 Bool 无关：a=¬b、b=¬a 的方程组有解；将端口环直接解释为施工 DAG 环会在既有 MILP/精确核验之前错误拒绝。未知 Bool 和布尔连接的有限编码已经存在，本项复用该后端，不引入新的 SAT 求解器或迭代赋值机制。

Rust validate_module_nodes 和共同 WorkbenchFeatureGraph 现对关系节点之间的直接 Bool 端口采用与数值端口相同的施工边豁免。先校验全部引用，完整语义依赖仍保留；只从施工排序图移除这类联立边。不豁免实体、列表、一般程序节点或其他非标量依赖，也不推导所有允许准入的方程都有解。准入之后仍须联合编译、独立候选检查、封存与共享提交。

真实 SDK 建立两个有实体输出的关系节点并闭合互补 Bool 环，固定 b=false 得 a=true；将 b 要求改为 true 得 a=false。将一个互补律改为相等律后矛盾，修改拒绝且 head 不变。额外实体端口形成的施工环由 Core 返回 DEPENDENCY_CYCLE，stepsCommitted=0。禁止 Worker 后重开保持实现根。WASM 构建、Web 类型、Rust fmt/clippy 和改动 lint 通过；未创建 test/spec 或平行执行器，此结果不声称任意混合整数非线性环均能求解。

P2 条件边界的组合包围与选支后精确恢复（2026-09-21）

条件输出串联普通仿射端口时，后者的私有边界坐标初始无界；只向包围器提供条件叶会丢失 y=f(x) 的已知连接。现从条件边界出发，沿仿射叶中非零系数引用收集必要的边界连接，每个边界处理一次，遍历消费现有编译预算。普通连接提供单成员 hull，条件连接提供所有叶的 hull，统一交给既有 Core 拓扑顺序和精确区间运算。未被条件边界需要的普通关系环不加入 hull 图；需要的包围依赖成环时仍明确 unknown，不迭代猜界。

保持性来自依赖图归纳：普通边界满足 y=f(x)，故其值属于 f 对输入包围的外包围；条件边界恰取某一叶，故属于各叶外包围的 hull。按无环依赖顺序传播得到所有合法解的外包围，原联合等式和守卫仍限制真实值，不把 hull 当作输出定义。只收紧编译器生成的无界边界坐标，不覆盖源变量域。

实际接线还发现：分支已经选定，binary64 的 40/50 mm 近似却因条件等式被恢复器跳过，留下精确残差 3/3602879701896396800，导致独立候选检查拒绝。现恢复器复用同一守卫解释器读取完整候选，先用等式固定每个比较守卫所读取的值，再将激活的条件等式与无条件等式共同做稀疏有理消元和回代。固定比较输入使整个 Bool DAG 的真值保持，因此条件行的使用不会反过来改变其适用前提。无候选时仍不猜测分支；固定后的矛盾只表示该候选无法按此规则恢复，不是全域不可行证明。域、整数性、全部守卫、等式与要求继续由独立原问题检查器核验。

验证使用四个真实关系实体：40/50 mm 条件源→普通仿射转接→选择原值或加 10 mm→下游高度要求。要求 60 mm 反向选择源 50 mm；改为 40 mm 选择源 40 mm；45 mm 拒绝且 head 不变，禁止 Worker 后重开保持实现根。初始验证误保留了中间实体的面积乘积律，产生额外双未知乘积，已按此项仿射接受域修正验证输入，未扩大产品接受域来绕过它。此链验证组合包围和精确恢复，不证明一般条件环、MINLP 或任意算术内部 select 均可求解。

最终构件上的同输入链验证通过；另核对候选 x=0、守卫 x=0 激活条件律 x=1 时，恢复返回 unknown / RELATION_EQUALITIES_INCONSISTENT，不通过修改 x 来使守卫失效。WASM 构建、Web 类型、Rust fmt/clippy、改动 lint 与 diff 检查通过。

P6 关系与控制量的原子源编辑（2026-09-21）

合法设计集合通常不对分步编辑封闭。若旧状态满足 R₀(x,u₀)，目标状态满足 R₁(x,u₁)，不能要求 R₀(x,u₁) 或 R₁(x,u₀) 也有解。因此关系、控制量及要求需要在一个候选中替换，不能让 AI 临时删除约束来穿过无解的中间状态。

现有 edit-relations 增加可选 parameterEdits，复用 set-parameters 的寻址与类型/单位校验，并与完整关系定义、显式 requirement edits 合成一个 patch。current 始终读取起始修订中的目标有效参数值，配置参数编辑只修改指定已有配置的覆盖，不自动切换配置。配置 ID 没有伴随参数编辑时拒绝。所有参数操作仍经现有 Core mutability、范围、配置及源引用检查，最终候选进入共同求值和封存链；未显式修改的独立要求继续约束交付。

真实公开 SDK 操作以固定宽 80 的板验证：旧面积 3200、高 40，目标面积 4000、高 50。单改参数或单改关系均失败且不移动 head；同时修改两者与独立边界要求成功，只提交一个步骤。下一候选面积 4800、高 60 与保留边界冲突时拒绝，源文档完全不变。成功状态保存重开保持实现根；contracts/SDK 构建、Web 类型与相关 lint 通过。该验证针对原子编辑接线，不把步骤数当作 AI 自主成功率。

原生错误的共享诊断投影（2026-09-21）

机器错误码不能通过任意消息文本的首个冒号推导。wasm-bindgen 返回的 JSON 字符串、工作线程包装的 Error.message 与 AiraCoreError 均应进入既有 Core 解码器；只有载荷具有 code 或 diagnostics 时才采用结构化内容，普通文本保留显式 fallback。operationErrorData 继续仅输出既有字段，不暴露错误栈或任意实例属性。关系校验器的 pointer 在无专有 details 时保存为 details.jsonPointer，指针保持原校验器作用域，不伪造全局路径或恢复建议。

实际 Core 的错误单位交付在原始抛出值和 Error 包装下均保留 RELATION_BINARY64_DELIVERY_FAILED；同次公开 SDK 关系/分析操作的错误热容单位返回 RELATION_UNIT_INVALID 与 /expressions/C1/atom，head 不变。通过案例的连续修改及恢复保持。此结果证明诊断信息传输，不宣称外部模型已经能自主修复所有错误。