test(formal): add checked Lean core and pruning lemmas

[nichinichisou0609]

状态与范围

本 PR 尚未完成原请求的「第一档全量 Lean 证明」，保持 Draft。 当前已完成两轮可实际编译、经过传递公理审计的数学证明；第二轮闭合了首个具体 Power 数学实例。全场景、每条生产剪枝的数学连接仍有缺口，这些仍属于第一档，不能归入 Rust refinement 后宣称完成。

对照 Rust 基线：5c6dff7387e57384b9b2c989ab4f535cdd74f098（PR #43 合并后的 main）。当前提交：c2a680e8e5ef554719094390ff1590e96c0e2262；上一轮：769f704deeb291ad1c124bc2dcd3c24afb9cf434。不修改 Rust 搜索、评分、服务器、WASM 或 Cargo 依赖，不合并 main。

第二轮的实质进展

新增 5 个模块、41 条显式定理、784 行模块源码；累计 17 个模块、172 条显式 theorem、2,708 行 Allium/*.lean 源码。数量不是覆盖率。

Allium.ConcretePower.power_search_exact 完成以下具体数学实例：

公开的五槽合法性规范
→ 全部 49 个 composition regimes
→ 实际解码后八槽 power 查表（允许非单调）
→ per-character / per-card top-five 上界
→ honor 后应用可选 power cap
→ 重叠场景共享阈值搜索
→ canonical Top-K = Enumeration.exhaustiveKeys 的 Top-K

主定理不接受抽象 SearchTree.Sound、score ≤ upper 或场景覆盖作为外部前提；这些条件由具体定义和引理在内部构造。初始种子必须合法，空种子自动满足。K=0、同分、公共卡组去重及养成/摆位变体保留由同一 canonical 框架处理。

边界： ConcretePower 显式枚举已接纳的合法叶子，证明场景级剪枝的数学实现；不是已验证全部生产 DFS 优化，不是专用 solver/power.rs fast path 的整体验证，也没有性能结论。全部受理域/特殊角色约束与其他评分目标仍在 S05 中。

另外完成：

• PowerModel：八槽索引、六单位计数等于五人与公共单位交集的关系、全队同属性条件、任意表的上下界、selected/free 组合，以及先加 honor 后应用 cap 的最大化/最小化严格剪枝。下界显式保留非空单位集合前提。
• Composition：49 场景覆盖、语义归属 Matches 与宽松池过滤 Admits 的区别、真实查表 key 的包含及其场景上界。
• ScenarioSearch：上界只需覆盖本场景负责的叶子，其余访问叶子仍须全局合法；证明重叠场景共享 tracker 的全局精确性。不错误要求外部阈值下每个场景还保留自身的局部 Top-K。
• ScenarioPower：专用 Power 的多单位 singleton envelope 上界、空/单单位精确性、真实公共单位的接纳性；三个普通 decide 内核检查反例保护非单调、接纳性和空单位边界。这些反例不被冒充为已确认可触发的 Rust bug。

第一轮已有的数学核心

Canonical 五字段顺序、公共身份与养成/摆位代表分离、精确结果数量、逐次收集和分组合并；分支限界与超时传播；五槽合法枚举；不同角色 Top-r 松弛；整数阈值/打包/取整；人数与异单位/参考技能；二次包络、联合 power/skill 上界；DP 可达性与分量压缩；支援排除单调性与截止替换代数。

泛型 Allium.search_exact 仍要求 SearchTree.Sound score；complete_exact 还要求 deadlineHit = false。Arithmetic.grid_floor_of_error 仍有严格误差前提，不能替代全部 binary64 N1–N7 逐表达式误差证明。

实际验证

本地 Windows，固定 Lean 4.24.0、Mathlib f897ebcf72cd16f89ab4577d0c826cd14afaafc7、Python 3.14.7：

cd formal/lean
python verify.py --self-test

实际 exit code 0：31 个对照源码哈希、17 个模块全导入、整库构建（3105 jobs）通过。公理审计通过 591 个声明、332 个包含自动生成项的定理，只允许 propext、Classical.choice、Quot.sound。显式定理数是 172，不与生成项混淆。

四项公理负向测试（sorry、外部自定义公理、未使用本地公理、native_decide）与两项覆盖负向测试（删掉剪枝机制、把第一档数学义务移出范围）全部通过。检查器、允许列表、源文件哈希与 CI 判定逻辑没有放宽；git diff --check 通过。未把历史 Rust 测试算成本轮新执行结果。

python verify.py --require-complete

已实际运行：构建与审计通过后，exit code 1 明确列出 40 项未完成义务，拒绝第一档全量完成声明。

当前提交的远端检查已核实： Linux Lean proofs / check-proofs 成功，包括整库构建及传递公理/负向测试；commitlint 成功。常规 ci 请以其当前结果为准，不用上一轮绿灯代替。

覆盖与剩余工作

coverage.json 保留原文档全部 41 个剪枝机制及顺序，另列核心和边界义务。当前 6 proved / 27 partial / 13 open / 1 out_of_scope；stage_one_complete 为 false。

第二轮 P18、P38、S05 从 open 推进到 partial，P36 增补具体证明及边界。没有把整项提前标为 proved；40 个未闭合条目数量没有减少，因为本轮完成的是大条目中的子义务，不能据此换算完成百分比。

仍需完成：专用 Power 的 unit-mask 交集工作表完整性、best_completion 扫描与 least/cap 下同分剪枝；numeric 受理域、摘要与固定槽对应；普通/WL/Final 完整 RegimePlan 特征及评分连接；完整支配与 Top-K 逆恢复；bonus-tier/first-N/key/slack/refill/certificate；log-linear/区间/atanh 余项；全部评分目标的 binary64 误差预算；所有实际场景与启用剪枝的数学实例化。

详细记录：README、ROUND2、VALIDATION。

普通 CI 绿灯只表示声明范围内的证明与审计通过，不表示全量第一档完成，更不表示 Rust 二进制已验证。

[nichinichisou0609]

远端验证更新（提交 769f704deeb291ad1c124bc2dcd3c24afb9cf434）：

Lean proofs / run 36542932632 已在 Linux 上完成，结论为 success。该工作流包含整库构建、源码对照与全部模块检查、传递公理审计、四个公理负向测试及两个覆盖负向测试。提交格式检查也已通过。

这与 Windows 本地验证一致。PR 仍保持 Draft：coverage.json 的 stage_one_complete 仍为 false，第一档全量证明的 40 项部分完成/未证明义务没有被 CI 绿灯消除。