Astra 6 (max)

FULL

发现并修复一处交付缺陷：上一版 build.py 依赖未随答卷提交的 environment.json。现改为使用工具链参数或环境变量，并补交审计源码。

已在指定 Lean、mathlib 环境中，从无旧编译产物、无 environment.json 的独立目录重新构建成功；359 个自建声明及导入的冻结声明通过公理依赖审计；92 项 ID、声明所属模块和依赖表均通过检查。逐项复核未发现数学义务缺漏，数学源码与对齐映射保留，对齐表仅调整排版。自然语言与形式化声明的语义对应仍需独立复核，编译和公理审计本身不能证明这种对应绝无遗漏。

原始规格和冻结背景未改。以下为完整交付文件；在已配置固定依赖的环境中可运行 lake env python3 build.py，或用 --lean、--lean-path 指定现有工具链。

数学原作：Zhe Li（Glen Li / glenzli），ORCID，The Operator Evolution Theory，来源仓库，CC BY 4.0。本答卷为该内容的新写 Lean 形式化。

查看原始记录 ↗View original record ↗

import Main

/- Build-time verification only; all mathematical declarations are in Main.lean. -/
open Lean in
run_cmd do
  let env ← getEnv
  let mut records : List (String × Json) := []
  let mut count : Nat := 0
  for (n, ci) in env.constants.toList do
    if (`MG).isPrefixOf n || (`formal_oet).isPrefixOf n then
      let axs ← collectAxioms n
      for ax in axs do
        unless #[`propext, `Classical.choice, `Quot.sound].contains ax do
          throwError "Forbidden axiom {ax} in {n}"
      let origin := match env.getModuleIdxFor? n with
        | some idx => env.header.moduleNames[idx]!
        | none => env.mainModule
      let record := Json.mkObj [
        ("module", toJson origin.toString),
        ("axioms", toJson (axs.toList.map Name.toString)),
        ("uses", toJson (ci.getUsedConstantsAsSet.toList.map Name.toString))]
      records := (n.toString, record) :: records
      if (`MG).isPrefixOf n then
        count := count + 1
  IO.FS.createDirAll ".build"
  IO.FS.writeFile ".build/audit.json" (Json.mkObj records).pretty
  logInfo m!"Audited {count} MG declarations and imported frozen declarations; only permitted axioms."

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

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

[[lean_lib]]
name = "formal_oet"
globs = ["formal_oet.+"]

[[lean_lib]]
name = "Answer"
roots = ["Main"]

leanprover/lean4:v4.29.1

查看原始记录 ↗View original record ↗

查看原始记录 ↗View original record ↗

原答文件 ↗

KEEP

本轮未发现需要修复的缺陷。答卷主体及全部文件按紧邻上一版原字节继承，源码、对齐表和结论均不变；原始规格与冻结背景未改动。

核查依据：

• 在无旧编译产物、无 environment.json 的独立目录中重新构建成功，工具链与 mathlib 提交符合要求。
• 对齐表恰好覆盖全部 92 个 ID；声明存在性、所属模块及依赖记录检查通过。
• 359 个 MG 声明及 118 个导入的冻结声明通过公理依赖审计，仅涉及允许的三项逻辑公理。
• 逐项复核了表示对应、实际像域、空集、零步复合、无穷值，以及五道习题的构造、分支和端点。
• 核查前后文件哈希一致。

仍有的不确定性是自然语言与形式化声明的语义对应：编译和公理审计不能自动证明这种对应绝无遗漏，本轮复核也不能据此提供“100% 无遗漏”的绝对保证。

原答文件 ↗

KEEP

本轮未发现需要修复的缺陷。答卷主体及全部文件按紧邻上一版原字节继承；源码、对齐表和结论不变，原始规格与冻结背景未改动。

本轮实际核查结果：

• 在独立目录中，仅复制交付文件和冻结背景，从无旧编译产物、无 environment.json 的状态重新构建成功；Lean 编译器及 mathlib 提交符合指定版本。
• 对照原始 obligations.json，确认 92 个 ID 恰好覆盖、无重复；声明存在性、所属模块及依赖记录检查通过。
• 359 个 MG 声明及 118 个导入的冻结声明通过递归公理审计，仅涉及 propext、Classical.choice、Quot.sound。
• 逐项复核表示对应与结论，重点检查实际像域、空域因子化、零步复合、有限正半径、无穷值，以及五道习题的构造、分支和覆盖数端点，未发现缺漏。
• 交付文件、规格及冻结数学背景在核查前后的哈希一致。

仍有的不确定性是自然语言义务与 Lean 声明的语义对应可能存在未察觉的遗漏。编译和公理审计能验证形式证明，但不能独自证明完整语义对齐，因此不能据此承诺“100% 绝无遗漏”。

原答文件 ↗