# 固定命题证明：W-M01 验收示例 v1.0.0

命题：对任意实数x、y，2xy≤x²+y²。固定形式签名、Lean 4.19.0与Mathlib commit见input.json。这里选择已固定的可重放版本，不声称它是最新版本。提交仅proof body，以by开始；运行器注入不可变的声明、所需import和#print axioms。允许的基础公理仅propext、Classical.choice、Quot.sound；不允许sorry/admit、额外假设、修改声明、增加公理、native_decide、代码执行型元编程。

参考用(x-y)²≥0，替代用(y-x)²≥0。空文件、占位证明、类型不符、改命题和额外公理均应被拒。核验同时检查实际内核编译与传递公理清单；形式命题与中文题意仍需接收者核对。返回未找到证明不能改写为命题不成立。

复跑：准备指定revision的Mathlib及缓存，以python3 scripts/check-work-unit-examples.py --lean-project PATH --lean-bin PATH/bin运行。未配置内核时必须记environment_blocked，不允许把字符串检查写成数学证明通过。整个包为验收器校准，没有新模型试次、没有一般数学成功率。

本代表校准采用明确受限的证明语法：by、have、show/from、exact、calc、nlinarith、sq_nonneg、rfl、le_refl、le_of_eq、pow_two、ring_nf，变量x/y及h编号局部引理；拒绝其它标识符、注释、字符串和额外命令。超出语法返回unsupported_submission，表示需要改用更完整且隔离的证明运行器，不表示数学命题或证明错误。随后仍实际编译并检查传递公理。追加lemma或initialize也必须在执行前拒绝。