工程有效性、误差传播与耦合验收规约

研究总览 · 2026-09-20

本文给出从“程序表达并执行模型”到“某项工程主张在指定用途下成立”的确定规则，并完整推导一个可直接核验的被动 RC 热网络族。本文是待实现规约，不表示当前产品已实现检查器、已有真实材料试验或获得工业认证。不新增求解库、独立验证执行器或治理台账。

1. 所要解决的命题

工程主张必须写成：在对象 O、工况集合 U、参数集合 P、时间域 H 和假设 A 内，受检量 q 满足现有 assertion 的接受集。飞机、机器人或管线只是对象类别，不能代替上述量和范围。温度场的最大值、某节点平均温度与某采样点温度是三个不同受检量。

同一模型可能支持多种主张，但每项分别检查：

主张层次	可以据什么通过	不能据什么升级
数字模型性质	有效模型域内的代数／分析推导和可核验证据	生成代码成功、求解器 success
数字轨迹性质	模型性质及数值／时间覆盖误差界	只有积分 tolerance 或有限样点
物理对象的有界预测	前两者＋适用域内参数、边界及模型差异的外部证据	库名、CAD 外形、一次拟合或“经验合理”

研究可以闭合推理规则及明确模型族的全部数学责任；真实材料、装配状态、载荷和测量的真实性必须作为外部输入。没有这些输入时返回条件性的模型结论和 physical unknown，不能把不存在的实证补成默认真。这是可执行的证据分界，不是把架构问题推迟到逐产品试用。

NASA-STD-7009B 官方范围将模型的开发、使用、可信度及项目定义的接受准则联系起来，并要求专业分析采用相应领域做法。ASME V&V 20 官方范围明确其验证针对指定变量和验证点，域内插值／外推不能直接由该范围保证。本文借鉴这一分界，不声称执行了标准全文或取得符合性认证。

2. 同一 AMIR 权威中的数据责任

当前 AMIR assertion 已增加 assert.analysisRange@1.0.0：inputs 为 analysisNode、output、minimum、maximum；后两者是同一分析定义中的表达式 ID，不复制上下界数值。scope 当前明确限定 parameterDomain=bound-configuration、timeDomain=analysis-conditions，即固定已绑定配置的整个声明时间域；它不冒充参数集合量化能力。evidenceLevel 明确选择 model-bounded 或 physical-bounded，severity=error、onUnknown=fail。Core 检查目标节点和表达式/输出引用；分析解析器检查输出 requirementRefs 的双向对应、静态上下界及量纲一致。上下界排序、证明范围对照及物理证据准入仍须由同一候选检查器实现，未实现时不能提交。当前目录绑定已随权威 Schema 更新，不保留旧哈希兼容路径。下面更一般的参数域、物理假设与误差输入仍是完整目标，不以该固定配置子域替代。

要求、适用域、物理假设和允许的证据等级都由当前 AMIR 声明；关系 AST保存 typed 表达式，Modelica 分析声明保存方程、工况和结果绑定。下面是这两类现有语义需要增补的字段结构草案，不是另一套可编辑分析模型。

type EngineeringClaim = {
  assertionId: Id;
  analysisNode: Id;
  quantityOutput: Id;
  scope: {
    occurrenceRefs: ProductOccurrenceReference[];
    parameterDomain: ExprId;
    operatingDomain: ExprId;
    startTime: ExprId;
    stopTime: ExprId;
  };
  requiredLevel: "model-bounded" | "physical-bounded";
  assumptions: Id[];
  evidenceInputs: Id[];
};
type ValidityAssumption = {
  predicate: ExprId;
  source:
    | { kind: "derived"; ruleRef: Id; premiseRefs: Id[] }
    | { kind: "external"; evidenceRef: Id };
};
type ErrorContribution = {
  claimRef: Id;
  kind: "input" | "representation" | "numerical"
    | "coupling" | "model-discrepancy" | "observation";
  boundExpression: ExprId;
  appliesTo: Id;
  evidenceRefs: Id[];
};

Id、ExprId、ProductOccurrenceReference 直接引用已有契约。scope 和 assumptions 指向同一源表达式及物性／工况；不得复制不同数值的“验证专用模型”。接受上下限仍由 assertion 拥有。error contribution 是有来源的推导输入／输出，其值不能由求解器为了得到 pass 自动缩小。

parameterDomain/operatingDomain 必须是对明确绑定的参数和工况变量求值的 Bool 表达式；scope 表示对域内全部允许值及所声明时间段的主张，不是只在当前候选点求值一次。绑定变量、量纲、量词和观察算子由同一分析模块声明，不能留下自由变量。能力发现须区分只检查样点与能核验整个 scope 的规则。

这些字段由同一要求与分析声明生成。AI 提出温度上限、组件连接、材料及工况，不必再填写热矩阵、Lipschitz 常数或误差传播公式；适用的已登记模型规则生成证明候选并核验。缺少真实材料或边界证据时，系统准确返回缺少哪项输入，不能让 AI 猜一个误差界。

外部 evidenceRef 解析到现有内容寻址资源，至少包含：对应对象／批次、被测量和单位、测量／辨识方法、校准及测量误差、条件范围、数据内容散列、参数推导规则、覆盖期限和失效条件。不存在内容的哈希、不匹配的批次或适用范围均不能完成引用。生产中由同一 schema 登记必要的资源载荷，不新建证据数据库。

推导规则和核验器随现有 Operation Module 锁定身份；检查在同一 candidate evaluation 运行，结果复用 RequirementCheck。Realization、输入闭包、分析定义、后端身份和工况共同绑定结论。候选/修订的身份与无环哈希依分析结果绑定，不让后端修改源假设。

3. 余量与误差传播的闭合规则

先按数值规约展开同一 assertion 的接受集。以要求 q≤b 为例，若已知数字报告值 q̂ 与目标受检量满足 |q−q̂|≤E，则：

[ m=b-q̂,\qquad m\ge E\Rightarrow pass,\qquad q̂-E>b\Rightarrow fail. ]

其他情形 unknown。严格上限 q<b 要求 m>E。误差吃掉设计余量，不能以误差为理由扩大接受范围。

**串联误差定理。**若同一受检量的阶段 q₀,…,qₖ 满足 |qᵢ−qᵢ₋₁|≤eᵢ，则 |qₖ−q₀|≤Σeᵢ，直接由三角不等式得到。各阶段必须指明比较的两端；输入误差已经通过数值包围计入时，不再以另一名称重复计算。独立性没有证明时，不用均方根合并确定性界。

**有条件的灵敏度传播。**若 q=f(x)，x 与 x̂ 之间的全部线段位于声明域 D，且 D 内 |∂f/∂xⱼ|≤Lⱼ、|xⱼ−x̂ⱼ|≤δⱼ，则：

[ |f(x)-f(x̂)|\le\sum_j L_j\delta_j. ]

证明为沿线段积分梯度。Lⱼ 的单位为输出单位／第 j 输入单位。仅在 x̂ 的局部梯度、数值有限差分或少数样本得到的最大梯度，不构成整个 D 的界。非光滑模型可用已证明的 Lipschitz 界，跨分支无该保证则分域检查或 unknown。

物理差异可直接建成输出界 E_model，也可建成方程扰动并通过 §6 传播；两者不能无依据互换。制造误差、测量误差、积分误差和材料参数不确定性分别绑定其作用位置；均不得借用 OCCT 的 fuzzy tolerance 充当物理误差。

4. 从有限采样到全时域保证

设连续受检量 q 在 [t₀,tₙ] 上具有已证明的时间 Lipschitz 常数 L，即 |q(t)−q(s)|≤L|t−s|。每个采样点有 q(tᵢ)∈[lᵢ,uᵢ]，包含首尾且最大间距为 h。任意 t 距某一相邻端点不超过 h/2，故：

[ \inf_t q(t)\ge\min_i l_i-Lh/2,\qquad \sup_t q(t)\le\max_i u_i+Lh/2. ]

这就是全时域接受区间，能直接送入同一 assertion。给定允许的额外时间覆盖误差 ε_time>0，可推导 h≤2ε_time/L；L=0 时不需要加密。不能反过来从采样曲线看起来平滑推断 L。

对非均匀网格可逐区间使用 hᵢ 和当地证明的 Lᵢ，取各区间包围的并；必须覆盖整个声明时间域。只有局部积分误差或相邻 CSV 点的差商时，证据仍然只是样点检查。

有跳变的 q 不使用跨跳变 Lipschitz 界：按已识别事件分段，分别包含左右极限；事件时刻只有区间时，整个事件时间区间要覆盖所有可能模式和输出。缺失事件、可能多次切换或未界定的跳变量使全时域结果 unknown。连续温度即使热源阶跃，其导数可以跳变，但只要导数绝对界成立，仍可使用上式。

共享触发、单一赋值者和连接方程必须遵守Modelica 连接及事件语义。事件记录完整与事件模型正确是不同的责任。

5. 耦合计算的可计算充分条件

物理连接首先检查单位、方向、局部坐标、守恒变量及边界责任；程序接口形状相同不表示物理量相容。热端口连接要求温度协调与有符号热流守恒；跨域能量转换必须显式提供本构关系，不能把两个输出直接绑定就称为耦合完成。

**收缩耦合定理。*设声明的闭域 K 在选定范数下完备，真实耦合映射 F 满足 F(K)⊆K，且对全部 x,y∈K 有 ||F(x)−F(y)||≤q||x−y||，0≤q<1。则 K 中存在唯一不动点 x。对任意候选 x̂∈K：

[ |x̂-x^*|\le\frac{|x̂-F(x̂)|}{1-q}. ]

证明：三角不等式给出误差≤残差＋q·误差；存在唯一性由 K 上的收缩迭代得到。若后端只能计算 F̃，且有 ||F̃(x̂)−F(x̂)||≤η，则用可核验的实际残差 δ≥||x̂−F̃(x̂)|| 得到 E_coupling≤(δ+η)/(1−q)。只看到两次迭代差很小而没有 q、自映射和 η，不构成该证书。

两子系统 u=A(v)、v=B(u) 的全域 Lipschitz 界分别为 a、b，且组合自映射保持，则 ab<1 是组合 F=A∘B 收缩的充分条件；范数、尺度和输入域必须对应，不能相乘不相容量纲的数字。参数变化后重新核对 q，q≥1 仅表示此证明失效，不表示耦合系统一定无解。

此规则可以检查现有后端或声明耦合算法的结果，不要求新增外层迭代器。对 OpenModelica 已联合形成的 DAE，不能伪称它使用了上述分区不动点算法。耦合求值收敛也不等于物理闭环稳定；动态稳定性必须针对时间演化另证。

6. 完全可推导的族：有限被动 RC 热网络

6.1 定义域与唯一解

任意有限 n 个热节点，每个节点有常量热容 Cᵢ>0；节点间热导 Gᵢⱼ=Gⱼᵢ≥0，无自导热；节点与边界 a 的热导 Hᵢₐ≥0。边界温度 bₐ(t) 和热功率 pᵢ(t) 在有限时间域内有界且分段连续；没有状态重置或相变。本族满足：

[ C_i\dot T_i=\sum_jG_{ij}(T_j-T_i) +\sum_aH_{ia}(b_a-T_i)+p_i. ]

令 C=diag(Cᵢ)，K 的对角元为 ΣⱼGᵢⱼ＋ΣₐHᵢₐ，非对角元为 −Gᵢⱼ，fᵢ=ΣₐHᵢₐbₐ+pᵢ，则 CṪ+KT=f。矩阵 C 可逆，右端对 T 全局线性 Lipschitz，所以每个初值存在唯一连续、分段可微轨迹；任意固定参数族均如此，不需要枚举具体产品。

对任意向量 z：

[ z^TKz=\sum_{i<j}G_{ij}(z_i-z_j)^2 +\sum_{i,a}H_{ia}z_i^2\ge0. ]

因此 K 为 PSD。每个热导连通分量至少连到一个正边界热导时 K 为正定；对常量 f，稳态 K⁻¹f 唯一。时变 f 仍有唯一初值轨迹，但不由此承诺恒定稳态；K 非正定时，即使 f 为常量也不承诺唯一稳态。零输入误差系统的储能 V=eᵀCe/2 满足 V̇=−eᵀKe≤0。求和方程后内部节点间热流抵消，仅余边界交换和热源，得到全网络能量守恒。这些结论随任意有限网络规模成立。

6.2 无需时间枚举的鲁棒不变箱

设初温 Lᵢ≤Tᵢ(0)≤Uᵢ，输入满足 bₐ⁻≤bₐ(t)≤bₐ⁺、pᵢ⁻≤pᵢ(t)≤pᵢ⁺。若每个节点满足：

[ \sum_jG_{ij}(U_j-U_i)+\sum_aH_{ia}(b_a^+-U_i)+p_i^+\le0, ] [ \sum_jG_{ij}(L_j-L_i)+\sum_aH_{ia}(b_a^–L_i)+p_i^-\ge0, ]

则 T(t) 始终在 [L,U]。证明是在每个上边界面上向量场不朝外、每个下边界面上不朝外，并利用 G,H 非负及唯一解；闭箱的不变性不依赖采样或积分器成功。

不确定 C,G,H 也可纳入：Cᵢ有严格正下界；对参数域内全部值证明上式。可用带方向的区间／有理运算保守核验每项；区间相依造成过宽则 unknown，不能暗取中点。存在于参数域中但未覆盖的相关性不能自行假设独立。

有理输入和箱界可由已选有理数设施直接核对，查一个 n 节点证书只需遍历节点和实际边；这是派生检查规则，不是新求解器。若需要寻找 L/U，可使用既有线性后端提出候选，再严格检查两组不等式。

当前实现 compilePassiveThermalInvariant 将常系数、常热源的有限时间比较包络接入同一关系表达式与 Core 精确算术。每个端口连接等价类恰有一个固定初温热容或固定温度边界；热导为已知常量，热源只能由唯一已知标量方程赋值（生成器固定 alpha=0）。多个热源在同一状态节点求和，接在理想固定边界的源由边界吸收。额外方程、事件、状态依赖热源和未消去代数节点返回 unknown。

令 L₀/U₀ 为全部初温和固定边界温度的最小/最大值，pᵢ 为各状态节点净热功率，a₋=min(0,minᵢ pᵢ/Cᵢ)、a₊=max(0,maxᵢ pᵢ/Cᵢ)。则移动箱 [L₀+a₋(t−t₀), U₀+a₊(t−t₀)] 保持轨迹：上面上的内部导热非正，固定边界通量非正，而 pᵢ≤Cᵢa₊；下面上反向成立。由于 a₋≤0≤a₊，固定边界始终留在箱内。常系数线性初值问题具有唯一轨迹，比较条件给出全时域包围。取声明终点的箱即包围整个声明时间域；无热源时斜率为零，退化为前述最大值原理。不要求稳态存在或每个节点直接连接散热边界，也不要求热网络连通。

编译器生成正热容、非负热导、初值、移动边界通量条件及有理斜率/终点界，由已有 Core 核验，实际编译受资源预算限制。浏览器产物核验将结论绑定到交付模型和结果内容，scope 为 delivered-model-temperature-invariant；它不证明积分轨迹误差、源模型与交付模型等价或物理对象有效性。一般不变箱、切换输入、不确定参数与外部证据仍须实现，普通候选工程准入尚未放行。

原生 aira_analyze_candidate 现要求显式选择 mode=model-proof|numerical。前者在同一候选权限、几何准备与输入解析后直接对精确源模型推导，scope 为 source-model-temperature-invariant，成功状态 model-proved；不需要分析服务器、数值参数转换或仿真记录。结果内容绑定源输入身份、规则与精确算术证据，候选挂载独立。后者保持数值后端与交付模型结论。两模式复用同一规则编译器；源证明不继承交付模型的数值结论，也不产生提交凭据。模型模式当前返回内容摘要、证明状态、适用热状态、精确有理温度范围（K）和时间域（s），通过的模型证明以 kind=model 封入候选的同一分析见证集合；数值项 kind=numerical 同时包含源模型和交付模型证明状态。内容读取按种类核对版本、scope 及输入根，不以内容哈希核对代替数学证明重验和工程要求准入。只有模型 pass 才安装独立模型项，数值项可保留模型 unknown 诊断；当前仍不可据此提交为工程有效修订。

6.3 可证明的时间导数界与数值残差

在已证明的不变箱内，取 Dᵢⱼ=max(|Uⱼ−Lᵢ|,|Lⱼ−Uᵢ|)、Bᵢₐ=max(|bₐ⁺−Lᵢ|,|bₐ⁻−Uᵢ|)，则：

[ |\dot T_i|\le\frac{\sum_jG_{ij}^{+}D_{ij} +\sum_aH_{ia}^{+}B_{ia}+\max(|p_i^-|,|p_i^+|)}{C_i^-}. ]

右端给出 §4 所需 L，来源是方程和已证域，不是曲线差商。只有状态域检查通过后才能引用该界；若要用此界反证状态不会出域，应明确采用上述不变箱证明，避免循环论证。

当前常参数比较包络实现使用公共全时域箱 [L,U]，对状态 i 输出更保守的 (|pᵢ| + Σ_incident G·(U−L))/Cᵢ，单位 K/s。固定边界已包含在同一箱内，故该式同时覆盖内部边与边界边；同一连接节点上的自回路通量为零，不计入。pᵢ 是先精确求和的常量净功率。Core 同时计算状态箱、斜率和变化率界，只有全部前提及数值根通过才发布这些量；fail/unknown 只返回未建立前提的诊断。变化率界随同分析内容绑定时间域和交付模型，不从 CSV 估计，也不代替 §4 中采样点包围所需的数值误差证据。

对同一固定参数和输入，令连续、分段可微数值轨迹 T̂ 的残差 R=CṪ̂+KT̂−f，在全部时间上已有 |Rᵢ|/Cᵢ≤r。由于 −C⁻¹K 为 Metzler 且各行和非正，最大范数误差满足：

[ |T(t)-\hat T(t)|_\infty\le E_0+rt. ]

这可由达到最大绝对误差的节点上的单侧导数界积分推出。若全部节点 hᵢ=ΣₐHᵢₐ>0，α=minᵢ(hᵢ/Cᵢ)>0，则更紧的界为 E₀e⁻ᵅᵗ+(r/α)(1−e⁻ᵅᵗ)，整个时间域可直接使用 max(E₀,r/α)，避免为证书新增指数计算库。

只有部分节点直接连边界时，可给无量纲正权重 w，核验 Kw>0，采用 ||e||w=maxᵢ|eᵢ|/wᵢ 与 α=minᵢ(Kw)ᵢ/(Cᵢwᵢ)。同时把残差界改为 r_w≥maxᵢ|Rᵢ|/(Cᵢwᵢ)、初始界改为该加权范数下的 E₀w，才可使用相同公式；第 i 个温度误差再乘 wᵢ 恢复。w 是证书的一部分，不接受后端自报稳定性。

CSV 只能提出 T̂。要使用残差定理，明确构造插值函数、绑定插值身份，并对每段的函数及导数包围核对 R；分段线性与有界分段输入可直接做本族的区间计算。不把后端局部 tolerance 当 r；事件处保留原始记录，并确保此无温度重置模型的核验插值连续。无法包围输入或残差时，只报告数值轨迹而无该证书。

6.4 闭式单节点和耦合特例

单节点、常量 C>0、G>0、边界 b 和功率 p 满足：

[ T(t)=T_\infty+(T_0-T_\infty)e^{-Gt/C},\qquad T_\infty=b+p/G. ]

直接求导和代回即可验证初值及方程；解始终在 T₀ 与 T∞ 之间。该解析族可用于核对转换器和后端，真实零件是否符合集中模型仍由 §7 的外部证据决定。

双节点稳态，内部热导 g≥0，各自到边界的热导 h₁,h₂>0，可写 T₁=A(T₂)、T₂=B(T₁)。其斜率 a=g/(g+h₁)、b=g/(g+h₂)，因此 ab<1；正热容不参与稳态方程，但参与动态有效性。先用 §6.2 建立自映射温度箱，再应用 §5 的残差界。这样耦合误差有可算分母，不能只以“两个求解器都收敛”完成验收。

7. 一个完整的有界工程主张

声明某部件在 0–3600 s 内的物理最高温度不超过 348 K。下表是演示所需的外部证据输入数值，不是已完成的真实测量：

项目	声明范围及输入责任
集中热容	C∈[450,550] J/K，实际部件／批次的物性与质量证据
对环境有效热导	G∈[2,2.2] W/K，包含安装与接触状态的辨识依据
环境和受控功率	b(t)∈[293,294] K，p(t)∈[0,100] W；整个时间域的工况边界
初始节点温度	T₀∈[293,295] K，包含测量误差
未建模的节点净热流	d(t)∈[−2,2] W，其证据适用于节点温度 [290,350] K
空间最高温度与节点温度差

把 d 加入功率界而非忽略，取 L=292 K、U=345 K。上边界最坏热流为 2*(294−345)+100+2=0 W，下边界最坏热流为 2*(293−292)+0−2=0 W；初温在箱内。因此节点全时域位于 [292,345] K，物理最高温度≤346 K，距离 348 K 尚有 2 K 可证明余量。

这里 G 的最坏端点由温差符号推出：上边界 b−U≤0，下边界 b−L≥0，二者最不利散热／保温均取 G 的下界。C 只要为正就不影响这项不变箱证明。无需取某个 nominal C、运行 3600 秒步进或遍历参数盒角点。

物理误差假设只在 [290,350] K 内有效，但证明得到更小的严格内箱；可按首次离开该大域的时间反证，从而避免预先假定结论。T_hot 的界是额外物理证据，不能从集中节点方程自行推导。上述证据齐全且适用域匹配，当前物理主张可通过；只有演示数字而无外部证据时，模型条件定理成立、physical 仍为 unknown。

证据若把热导下界修订为 1.8 W/K，则同规则提出的节点上界 294+102/1.8≈350.667 K 超出模型差异证据的适用温度域；该证书失效，不能扩域签发 pass。但一个充分证书失效本身不决定整个主张为 unknown。

本例还能直接否定“声明域内全部参数和工况均达标”的鲁棒主张：取允许的 C=450、G=1.8、b=294、p=100、d=0、T₀=295、T_hot=T。则 T∞=3146/9，T(3600)=3146/9−(491/9)e⁻⁷²⁄⁵。由 e⁷²⁄⁵≥1＋72/5＋(72/5)²/2>64，得到 T(3600)>348.703125 K>348 K；整条轨迹在 [295,349.556] K 内，始终符合 [290,350] K 的模型适用域。故此全称主张为 fail，有明确域内反例；某个未辨识真实个体是否超温仍可为 unknown。判定必须绑定原命题的量词，程序不能把鲁棒设计不满足误写成已测得真实部件失效。

8. 哪些外部事实可以进入证明

外部输入不是一份 PDF 就自动可信：必须明确数据与目标部件、材料批次、安装方式及工况的对应，并把仪器误差、参数辨识误差和范围推广依据纳入界。样本最大残差不是全域模型差异上界；单次稳态拟合也不能同时确定热容与瞬态误差。

有限实验若要支撑整个连续域，须另有覆盖推导。例如残差函数已知 Lipschitz 常数 Ld，验证点构成半径 h 的覆盖，点上测量／数值误差上界分别为 ei，则域内差异≤maxᵢ(|rᵢ|+ei)+Ld·h。Ld 及覆盖必须有依据；用同一组残差再猜一个 Ld 会循环。统计置信界须携带分布、置信水平与适用条件，不能转换成这里的确定性有界证书。

集中热模型需要的空间温差界可以来自适用的解析传热推导、已验证更细模型或有覆盖依据的空间观测；“Biot 数小”或材料名相同本身不提供一个具体 1 K 保证。新辐射、相变、接触退化或流动机制若不在既有残差范围内，就使相应证据失效，不依靠减小积分步长修复物理模型。

几何、制造与分析的连接也须是显式输入：实际厚度／接触面积与数字几何不一致时，由其制造测量范围进入参数域；不能把 nominal CAD 几何直接当成实物的精确值。

9. 同一验收路径的确定结论

实施时先解析原 assertion 的目标及 scope，再匹配模型族和 assumptions；按锁定规则核验域、输入证据、数值表示、时间覆盖与耦合误差，生成受检量包围，最后调用现有三态要求检查。任何阶段的 unknown 必须保留原因；onUnknown:fail 可以阻止提交，但不能改写成已证明设计不可行。

情形	系统必须返回
全部假设有匹配证据、目标包围在接受集内	对指定作用域与证据等级 pass
同样证据充分、目标包围与接受集不相交	对该候选要求 fail；不证明所有设计无解
全称作用域内存在有证据的合法反例	该全称要求 fail；不据此断言实际未辨识个体已经失效
误差包围跨接受边界	unknown，明确由哪一项误差消耗余量
缺物性、模型差异、时间覆盖或耦合界	对应缺证的 unknown，同时保留可成立的较低层结论
修改超出已证域、证据过期或绑定失效	旧结论不可复用，重新匹配当前有效输入

本规约闭合了三件事：工程主张有唯一源权威及可执行证据责任；误差与耦合通过定理变成可计算余量；一个任意有限规模的实际模型族具有完整的存在、守恒、稳定性边界和全时域判据。它不声称从纯软件推导未知材料事实，也不把这一个模型族冒充全部 CAE；新的领域模型必须在同一机制下提供自己的适用域与推导规则，已有规则的任意有限组合则按其保持条件核验。