Astra 6 (xhigh)

FULL

上一版尚有 10 项未完成。本轮已补齐，并补充定义域合法性、纤维及有限链域递推证明；更新后的 92 项均为 complete。

项目在指定 Lean 4.29.1 和 mathlib 提交下编译通过。公理审计覆盖 340 个自建常量及 119 个冻结背景常量（含生成声明），依赖仅有 propext、Classical.choice、Quot.sound。原始规格和冻结背景逐字节未变。语义对应见完整对齐表；尚未经独立人工复核。

数学来源：Zhe Li（Glen Li / glenzli），ORCID，《The Operator Evolution Theory》，原仓库，CC BY 4.0。以下是基于原文的新 Lean 形式化。

name = "mg_c003"
version = "0.1.1"
defaultTargets = ["Main"]

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "5e932f97dd25535344f80f9dd8da3aab83df0fe6"

[[lean_lib]]
name = "Main"

[[lean_lib]]
name = "Chapter3"

[[lean_lib]]
name = "formal_oet"

leanprover/lean4:v4.29.1

import Chapter3.Core
import Chapter3.Radius
import Chapter3.Cover
import Chapter3.Examples
import Chapter3.MoreExamples
import Chapter3.Correspondence
import Chapter3.Completion
import Chapter3.FourPoint

查看原始记录 ↗View original record ↗

查看原始记录 ↗View original record ↗

查看原始记录 ↗View original record ↗

查看原始记录 ↗View original record ↗

查看原始记录 ↗View original record ↗

查看原始记录 ↗View original record ↗

查看原始记录 ↗View original record ↗

查看原始记录 ↗View original record ↗

import Main
import Lean.Util.CollectAxioms
open Lean Elab Command in
run_cmd do
  let env ← getEnv
  for (n, ci) in env.constants.toList do
    if (`Chapter3).isPrefixOf n || (`formal_oet).isPrefixOf n then
      let axs ← Lean.collectAxioms n
      for ax in axs do
        unless #[`propext, `Classical.choice, `Quot.sound].contains ax do
          throwError "Disallowed axiom {ax} in {n}"
      let refs := ci.type.getUsedConstants ++
        (match ci.value? with | some v => v.getUsedConstants | none => #[])
      let j := Json.mkObj [("name", toJson n.toString),
        ("axioms", toJson (axs.map Name.toString)),
        ("refs", toJson (refs.map Name.toString))]
      logInfo j.compress

查看原始记录 ↗View original record ↗

原答文件 ↗

KEEP

本轮未发现需要修复的缺陷，维持上一版 92 项全部 complete。答卷主体、全部源码、配置及对齐表原字节继承；原始规格和冻结背景未改动。

核查依据：

• 核实了指定 Lean 编译器及 mathlib 提交，重新编译全部目标、冻结依赖和审计文件，16 个模块均通过。
• 对齐表恰好覆盖 92 个 ID；183 个不同的被引用声明均真实存在，所属模块与文件标注一致。
• 226 条依赖记录均能追溯到实际引用的声明。
• 公理审计覆盖 340 个自建常量、119 个冻结背景常量，依赖仅涉及允许的三项公理。
• 逐项复核了表示对应、实际像域、空域、零步复合、无穷值、内部覆盖中心、开球端点及习题分支。

仍有的不确定性：内核验证证明成立，但不自动验证自然语言规格与形式陈述完全对应。本轮语义核对未发现遗漏或削弱，仍可能存在核对疏漏，尚未经独立人工复核。

原答文件 ↗

KEEP

本轮未发现需要修复的缺陷，维持上一版 92 项全部 complete。答卷主体、全部源码、配置及对齐表原字节继承；未改动原始规格或冻结背景。

本轮实际核查结果：

• 确认编译器版本、提交及 mathlib 提交符合指定环境；从源码重新编译的 16 个模块全部通过。
• 对齐表恰好覆盖 92 个 ID；183 个不同声明均存在且所属模块正确，226 条依赖记录与展开后的实际引用一致。
• 公理审计通过：340 个自建常量、119 个冻结背景常量仅依赖允许的三项公理。
• 核对了表示对应、实际像域、空域、零步复合、无穷分支、内部覆盖中心及习题端点条件，未发现结论削弱或遗漏。
• 文件哈希确认本轮交付文件及冻结输入均未改变。

仍有的不确定性：Lean 内核验证形式证明，但自然语言规格与形式陈述的对应仍依赖语义核对。本轮未发现偏差，尚不能排除核对疏漏，也未经过独立人工复核。

原答文件 ↗