Formal in Silico · mini-CALPHAD

模型

体系	二元 A–B，温度与压力固定；成分 x = x_B ∈ [0, 1]。每个相给出每摩尔原子的 Gibbs 能 G(x)，与 pycalphad 的 `GM` 相同。
代换溶体	一个混合亚点阵，其余亚点阵只有空位：理想混合 RT(x log x + (1 − x) log(1 − x)) 加 Redlich–Kister 过剩项 x(1 − x) Σ L_k(1 − 2x)^k。
磁性	可选的 Inden–Hillert–Jarl 项 RT log(1 + β(x)) g(T_c(x)/T)：T_c 与 β 是 `TC`、`BMAGN` 参数的 Redlich–Kister 和，为负时除以反铁磁因子。g 的两支在 T = T_c 处的值与斜率都相等——Lean 对任意结构因子 p 证明了这个恒等式。
化合物	化学计量化合物：只在一个精确成分（例如 2/3）存在。
参数	T 的分段 SGTE 表达式。驱动选出区间、展开函数引用；每一项是 c·Tⁿ 或 c·Tⁿ log T，c 是 TDB 中十进制串的精确乘积。
尚不支持	有序–无序模型中的有序相（无序相与 pycalphad 一样照常计算）、间隙溶体、多个混合亚点阵、多于两个组元。这些相被跳过并在报告中列出；结论只对参与计算的相成立。

证书认证的是证书里写的精确模型。把 TDB 文件翻译成这个模型由不受信任的驱动完成（假设 A-CAL-01）；基准把每个相的 G(x) 与 pycalphad 逐点对照，相对差不超过 5×10⁻¹²（pycalphad 在 T_c 上加 10⁻⁹ 防止奇点，证书用精确的连续形式）。

认证了什么

平衡的 Gibbs 能 G*(x₀) 是所有可行配置总 Gibbs 能的下确界：任意有限个相、成分与摩尔分数，只要总成分正确。几何上它是所有相曲线的下凸包在 x₀ 处的值。

平衡是一个可行配置加一条公切线 ℓ(y) = μ_A(1 − y) + μ_By：它在所有相的下方，并且经过该配置；μ_A、μ_B 是化学势。Lean 证明了平衡使总 Gibbs 能最小（CAL-C02），并且平衡一定存在（CAL-C03）。

Gibbs 能最小化程序可能停在局部极小、漏掉一个相或漏掉混溶隙。检查器的结论针对每一个可行配置与每一个平衡，所以这类错误只会让检查失败或区间变宽，不会得出错误的结论。

输出行	Lean 定理保证的内容
G_OK lo hi	G*(x₀) ∈ [lo, hi]：每个可行配置的总 Gibbs 能 ≥ lo，证书自己的配置 ≤ hi。
MU_OK A\|B lo hi	任意平衡的化学势都在这些区间内。
WINDOW 相 a b	任意平衡中该相的每个成分都落在它的某个窗口里。
ABSENT 相	该相不出现在任何平衡中。
DF_OK 相 lo hi	该相的驱动力 max_x (ℓ(x) − G(x))（pycalphad 的 `DF`，亚稳相为负，稳定相为 0），ℓ 是任意平衡的切线。它是对所有成分的全局最大值。
EXISTS	平衡存在，所以上面的结论不是空话。
TANGENT、EPS、KAPPA、FRAC	诊断信息：用的是谁的切线（单相区由检查器自己计算）、它在各相下方多远、窗口用到的切线误差界，以及证书自己的配置。

实例：Al–Zn 的混溶隙

Al–Zn，600 K，x(Zn) = 0.3，数据库是 pycalphad 自带的 Mey（1993）。这个温度下面心立方溶体分成两相：平衡是含锌约 22% 与 49% 的两个 fcc 相。检查器证明 LIQUID 与 HCP_A3 不出现在任何平衡中，把任意平衡中 fcc 的成分限制在两个宽度不超过 3×10⁻⁷ 的窗口里，把 G* 与两个化学势确定到输出的最后一位（10⁻⁹ J/mol），并以同样的精度给出每个相的驱动力。运行加检查约一秒。

build/mini-calphad --tdb alzn_mey.tdb --comps AL,ZN --T 600 --x 0.3 --certify run.cert --verify

…
Lean  G_OK -22985.126672267 -22985.126672266
Lean  TANGENT cert
Lean  EPS -0.000000000002425
Lean  FRAC FCC_A1 0.220126286673 0.705704921583
Lean  FRAC FCC_A1 0.491533181263 0.294295078416
Lean  MU_OK A -20590.725231961 -20590.725231960
Lean  MU_OK B -28572.063366314 -28572.063366313
Lean  KAPPA 0.000000000022
Lean  ABSENT LIQUID
Lean  WINDOW FCC_A1 0.220126163802 0.220126409545
Lean  WINDOW FCC_A1 0.491533032729 0.491533329798
Lean  ABSENT HCP_A3
Lean  DF_OK LIQUID -896.512026734 -896.512026733
Lean  DF_OK FCC_A1 -0.000000001 0.000000001
Lean  DF_OK HCP_A3 -379.321840947 -379.321840946
Lean  EXISTS

Al–Zn，600 K：fcc 相与认证的切线

FCC_A1 的 Gibbs 能减去公切线 ℓ，单位 J/mol。曲线两次接触 ℓ（混溶隙），圆点标出两个 Lean 窗口，各宽不超过 3×10⁻⁷。LIQUID 与 HCP_A3 离 ℓ 最近处分别高出 896.5 与 379.3 J/mol（即它们认证的驱动力），远在图的范围之外。曲线用 pycalphad 计算，仅作示意；切线与窗口来自 Lean 的报告。

显示数值

磁性：Cr–Fe 的混溶隙

Cr–Fe 的体心立方溶体在铁一侧是铁磁性的（T_c = 1043 K，β = 2.22），在铬一侧是反铁磁性的：那里的 TC、BMAGN 为负，要除以反铁磁因子。正是磁性能使 bcc 相在约 860 K 以下分成富 Cr 与富 Fe 两个溶体。600 K、x(Fe) = 0.5 时，检查器约两秒把两个成分认证到宽 10⁻⁷ 的窗口里。

磁性项不是多项式，也没有方便的二阶导数，所以检查器在每个区间上不用导数，而用割线斜率给出界：log(1 + β)、反铁磁约定、幂 tⁿ 与 t⁻ⁿ、Inden–Hillert–Jarl 函数的两支，在区间内任意两点之间的斜率都有有理数界，都在 Lean 中证明（CAL-C04）。这样得到的下界只差一个与区间宽度平方同阶的量，足以让分支定界收敛。

build/mini-calphad --tdb crfe_bcc_magnetic.tdb --comps CR,FE --phases BCC_A2 --T 600 --x 0.5 --certify run.cert --verify

…  相： BCC_A2（磁性）
Lean  G_OK -19793.346508744 -19793.346508743
Lean  MU_OK A -19642.803579468 -19642.803579467
Lean  MU_OK B -19943.889438020 -19943.889438019
Lean  WINDOW BCC_A2 0.432097736118 0.432097836657
Lean  WINDOW BCC_A2 0.903631494701 0.903631563012
Lean  DF_OK BCC_A2 -0.000000001 0.000000001
Lean  EXISTS

Cr–Fe：磁性混溶隙的认证边界

平衡中两个 bcc 溶体的成分 x(Fe)，400 K 到 850 K，步长 25 K。每个点是一个 Lean 窗口的中点（窗口宽不超过 2×10⁻⁶），每个温度一份证书（连同单相区共 57 份）。两条边界在约 860 K 处相遇，混溶隙闭合。pycalphad 的 binplot 画出同样的曲线。

显示数值

相图

--map T1:T2:dT 在温度网格的每个温度上求等温截面：驱动沿下凸包把 [0, 1] 分成单相区与公切线，用 Newton 法细化每条公切线，并在每个区域的中点写一份点平衡证书。两相区证书的两个窗口就是该温度下认证的相界，其余相在那里被证明不出现。

基准：Pb–Sn 300–600 K（43 个区域）、Al–Zn 400–900 K（35 个，含 fcc 混溶隙）、Cu–Mg 600–1300 K（31 个）、Cr–Fe 400–900 K（31 个）、Al–Fe 700–1700 K（63 个区域、34 条公切线，含纯铁附近的 γ 环）。203 份证书全部通过，相界窗口宽不超过 2×10⁻⁶，pycalphad 的 equilibrium 在每个证书点给出相同的相与成分。认证的相界点落在 pycalphad binplot 的曲线上；Al–Fe 在 1300–1430 K 之间 binplot 漏画了 Al₂Fe 区，而 pycalphad 自己的 equilibrium 与我们的证书都有这个区。

认证的是列出的每个区域在中点处的平衡。区域划分是否完整（会不会漏掉比驱动网格间距 5×10⁻⁴ 更窄的两相区）、网格温度之间的情况都不在证书内；基准在成分网格上把区域划分与 pycalphad 逐点对照。

检查器如何工作

全程是精确的有理数运算。驱动只提供候选切线、候选配置、探测点，以及每个相的最低点附近的一个成分。

1
参数区间与切线
log T 用与 mini-DFT 共用的有理级数界包住；每个代换溶体写成有理多项式加理想混合项（与磁性项），舍入误差有一致的界。单相区里检查器用自己在 x₀ 处算的有理切线代替驱动的双精度切线——可靠性对任意切线成立，所以这不需要新的证明，只让结果更紧。
2
对每个相分支定界
在每个区间上，G − ℓ 的下界来自多项式的精确 Taylor 系数、已证明的混合项二次下界（CAL-C01）、磁性项的割线斜率界（CAL-C04）与二次函数的精确最小值。每个相得到自己的下界 e_i，它们的最小值 e ≤ 0 是所有相的下界。
3
G* 的区间
每个可行配置的总 Gibbs 能 ≥ ℓ(x₀) + e（CAL-C02）；证书的配置（摩尔分数按杠杆定律精确算出）给出上端。
4
化学势
任意平衡的切线在 x₀ 处经过 G* 的区间，并在两侧的探测点处位于各相下方；这确定了它的斜率，也就确定了 μ_A、μ_B——两相区约 10⁻⁹ J/mol，单相区 10⁻⁸ 到 10⁻⁷ J/mol。
5
驱动力
任意平衡的切线在 [0, 1] 上与证书的切线相差不超过 κ，所以 min (G_i − ℓ*) ≥ e_i − κ；驱动给出的最低点附近的成分给出另一端。
6
成分窗口
出现在平衡中的相满足 G − ℓ ≤ κ。第二遍分支定界排除下界大于 κ 的区间，剩下的就是窗口。

二分规则只影响速度与精度。可靠性只依赖证明检查的两件事：被排除的区间下界大于阈值，所有区间覆盖 [0, 1]。

可信账本中的命题

T4 端到端 · 1 T3 机器证明 · 4

命题	内容	等级
CAL-C01	理想混合项 S(x) 在任意区间上的二次下界	T3
CAL-C02	平衡使总 Gibbs 能最小；出现的每个相都接触切线；G − ℓ 的下界给出每个可行配置的下界	T3
CAL-C03	0 < x₀ < 1 且至少有一个代换溶体时平衡存在，包括磁性相（它们的 Gibbs 能连续）	T3
CAL-C04	Inden–Hillert–Jarl 磁性项的区间界（割线斜率）：任意区间上带二阶误差的多项式下界，有理点处的上界	T3
CAL-B01	检查器可靠：G* 的区间，以及任意平衡的化学势、成分窗口、不出现的相与驱动力；平衡存在	T4

目标 G3——对照 pycalphad 的带证书 CALPHAD

参照：pycalphad 0.11.1，同一数据库、同一组相。完成标准与 G1、G2 相同，而且证书必须针对数据库模型真正的全局平衡。顺序：先做完二元（C0–C1），分支定界在一个成分变量上进行；再做多元与亚点阵模型（C2），分支定界在单纯形的乘积上进行；最后是派生计算（C3）。

完成：实现、一致、有证书未开始

二元点平衡

8 / 8

二元扩展：相图、磁性、不变反应

4 / 8

多元与亚点阵模型

0 / 4

Scheil、拟合与其他模型

0 / 3

C0 · 二元点平衡——全部完成

功能	pycalphad	状态	认证的内容
TDB 读取：函数、分段、引用、参数	`Database`	完成	不在可信链内（A-CAL-01）；每个相的 G(x) 与 pycalphad 的 `calculate` 逐点一致
代换溶体：理想混合 + Redlich–Kister	`Model`（GM）	完成	混合项二次下界 CAL-C01；检查器 CAL-B01
化学计量化合物	`Model`	完成	成分是精确分数，例如 2/3
点平衡：平衡相、成分、摩尔分数	`equilibrium`（Phase、X、NP）	完成	对任意平衡的 `WINDOW` 与 `ABSENT`；证书的摩尔分数由杠杆定律精确给出
平衡 Gibbs 能	`equilibrium`（GM）	完成	`G_OK`：对每个可行配置成立的全局下界
化学势	`equilibrium`（MU）	完成	`MU_OK`，对任意平衡成立
混溶隙（同一相的两个成分）	`equilibrium`	完成	每个成分各有一个窗口
平衡的存在性	—	完成	CAL-C03：`EXISTS`，所以“对任意平衡”从不是空话

C1 · 二元扩展——8 项完成 4 项

功能	pycalphad	状态	认证的内容
T–x 网格上的二元相图	`binplot`、`map`	完成	每个温度的每个区域一份证书；相界由公切线证书的窗口给出。区域划分的完整性不在证书内（见缺口）
磁性贡献（Inden–Hillert–Jarl）	`Model`（TC、BMAGN）	完成	CAL-C04（割线斜率界）与磁性相的 CAL-C03；Cr–Fe、Al–Fe 进入基准
驱动力	`DormantPhase(…).driving_force`	完成	`DF_OK`，对任意平衡成立；是对所有成分的全局最大值，pycalphad 求的是局部值
单相区的化学势收紧	`equilibrium`（MU）	完成	检查器自己的有理切线：宽度从约 10⁻⁴ 降到 10⁻⁸–10⁻⁷ J/mol
等温截面的完整性	—	未开始
不变反应（共晶、包晶）温度	`map`	未开始
热力学性质 H、S、C_p	`calculate`	未开始
间隙溶体	`Model`	未开始

计划：C2–C3（7 项，均未开始）

C2 · 多元与亚点阵模型

三元及多元溶体（Muggianu 外推、三元参数）
多个亚点阵（化合物能量形式）
有序–无序
以化学势或活度为条件

C3 · 更多计算

Scheil 凝固
参数拟合（ESPEI）：拟合本身不受信任，结论只依赖最终的数据库
离子液体与准化学模型

交叉校验与佐证

每个相在 x = k/20 处的 G(x) 对照 pycalphad 的 calculate相对差 ≤ 5×10⁻¹²
Al–Zn、Pb–Sn、Cu–Mg、Cr–Fe、Al–Fe 的 29 个平衡对照 pycalphad 的 equilibrium：成分 / Gibbs 能< 10⁻⁶ / < 10⁻⁵ J/mol
pycalphad 的 GM、MU 与平衡相成分落在 Lean 的区间与窗口内
141 个驱动力：pycalphad DormantPhase 的值落在 Lean 区间内；6 处 pycalphad 停在局部解，用它自己的 calculate 在我们的取值点处求值，落在区间内全部一致
相图：五个体系 203 份证书；每个证书点 pycalphad 的平衡相与成分全部通过，窗口 ≤ 2×10⁻⁶
篡改的证书失败，或仍然正确的结论
每个平衡的检查时间；整个基准0.1 – 2.4 秒；218 秒
驱动在 AddressSanitizer 与 UBSan 下运行点平衡与相图无报告
报告校验：报告中每一行 Lean 都是检查器自己的输出；检查器拒绝、崩溃或不存在时驱动以错误退出通过
收紧输入解析后，在 AddressSanitizer 与 UBSan 下对驱动做模糊测试（约 34 000 个变异输入）无内存错误、未定义行为与崩溃

Al–Fe 在 1000 K、x = 0.9 时，pycalphad 多相 equilibrium 的 GM 比它自己的 calculate 与单相平衡在同一点高 6×10⁻⁶ J/mol，恰好落在 Lean 区间之外。证书是对的；基准对 pycalphad GM 的容差因此取 10⁻⁵ J/mol。

尚未解决的缺口

从 TDB 文件到认证的模型选温度区间、展开函数引用、判断相的类型由驱动完成，不在可信链内（A-CAL-01）。基准把结果与 pycalphad 对照。模糊测试曾发现一些输入让驱动写出另一个模型的证书、检查器照样接受：3*T**1.5 被读成 3T + 0.5，系数在定长缓冲区里被截断，精确位置比运算溢出导致相被丢掉，0.25*2 这样的命令行数值在驱动和检查器里含义不同。10 月 1 日起驱动拒绝一切无法精确翻译的输入；此前被静默读错的三个 pycalphad 测试数据库现在与 pycalphad 读法一致，另有四个无法精确翻译的数据库改为报错。检查器仍然既不重算也不回显模型。
相图的完整性列出的每个区域在中点处有证书；区域划分是否完整、中点之间与网格温度之间的情况都没有证书。计划：用相邻证书的切线把中间任意成分处的平衡切线夹住。
有序–无序、间隙溶体、亚点阵与多元模型Lean 中尚未定义。驱动跳过这些相并列出；结论只对参与计算的相成立。TC 或 BMAGN 依赖 log T 的磁性相也被跳过。
驱动本身网格搜索与 Newton 迭代不受信任（T0），报告中如此标注；所有结果都经过检查器。

mini-CALPHAD

模型