Lean-Eval problem direct_summand (submitted by Junyan Xu). Yves André, La conjecture du facteur direct, https://arxiv.org/abs/1609.00345; Bhargav Bhatt, On the direct summand conjecture and its derived variant, https://arxiv.org/abs/1608.08882; Linquan Ma, a short proof of the direct summand theorem via the flatness lemma, https://www.math.purdue.edu/~ma326/DSC.pdf (the References of the problem's Challenge.lean; its Lean-Eval manifest has no source line)Lean-Eval 题目 direct_summand（提交者 Junyan Xu）。Yves André, La conjecture du facteur direct, https://arxiv.org/abs/1609.00345; Bhargav Bhatt, On the direct summand conjecture and its derived variant, https://arxiv.org/abs/1608.08882; Linquan Ma, a short proof of the direct summand theorem via the flatness lemma, https://www.math.purdue.edu/~ma326/DSC.pdf (the References of the problem's Challenge.lean; its Lean-Eval manifest has no source line) github.com/leanprover/lean-eval
When LOT proved this problem, a 4-level chain of intermediate theorems closed at once: each level is proved from the one below. We checked that chain twice, each run alone in its own sandbox with 8 whole CPU cores (16 CPUs) and 64 GiB locked for it: once with Lean’s original pipeline and once with LOT’s infrastructure, all six optimizations on. Both runs accepted every level.LOT 证这道题时，有一条 4 层的中间定理链同时收口：每一层都由下一层推出。我们把这条链检查了两遍，每一遍单独运行，独占锁定 8 个完整 CPU 核（16 个逻辑 CPU）和 64 GiB 内存：一遍用 Lean 原始流程，一遍用 LOT 基础设施（6 项优化全开）。两遍都接受了每一层。
Premise. Both runs start from the same situation: every theorem of the chain is already proved. LOT’s run also assumes what LOT has already done by then: everything below the chain was pre-checked, so the build of the library just below the chain is ready to reuse. That earlier work happens while the agents are still proving and is not inside the LOT time below; measured on its own, that build takes 967 s from scratch on the same 8 cores, 719 modules. The ledger is not assumed: the LOT run starts with an empty one.前提。两遍检查从相同的情况开始：链上每个定理都已经证明完毕。LOT 那一遍还默认 LOT 此前已经做完的工作：链下面的一切都做过预检查，紧挨着链的那一层库已经编译好、可以直接复用。这部分工作发生在 agent 还在证明的时候，不计入下面 LOT 的用时；单独测量，这次从头编译在同样的 8 个核上用时 967 秒，719 个模块。账本不算在前提里：LOT 那一遍从空账本开始。
What the two times are. Lean original is the wall-clock time to check the 4 levels one after another on one worker, each from scratch with the unmodified official checker. LOT’s infrastructure (all six optimizations on) is the wall-clock time of the latest pipeline on the same chain: a probe build that reuses the artefacts of the level below, then one check of the whole chain with parallel kernel replay. In this single replay the ledger is on but starts empty, and the queueing and speculative-checking optimizations, which act across a whole tree, have nothing to overlap with. Neither time includes the root check, queue waits or the scheduler’s pauses. The chain is not necessarily the tree’s longest: it is one closing cascade, the levels that became checkable one after another when the bottom theorem was proved, chosen for size and variety.两个时间分别是什么。Lean 原始流程：在一台 worker 上把这 4 层依次检查完的总用时，每层都用未改动的官方检查器从头检查。LOT 基础设施（6 项优化全开）：最新流程检查同一条链的总用时，先做一次复用下一层编译产物的探测编译，再用并行内核重放把整条链一次查完。在这次单独回放里，账本虽然开着但从空开始；排队和推测并行检查这两项是在整棵树的层面起作用的，这里没有可以重叠的东西。两个时间都不含根检查、排队等待和调度器的停顿。这条链不一定是这棵树里最长的：它是一次“收口”，即最底层定理证完后，上面各层依次变得可检查；挑选时兼顾规模和多样性。
Each bar spans its own run from start to finish, drawn from the measured stage times, so both end at the same length; the minutes on the right and the shared clock show how long each run really took. White ticks separate the levels.每条色条从头到尾对应各自那次运行，按实测各阶段用时画出，所以两条最终一样长；右侧分钟数和共用的时钟显示各自的真实用时。白色刻线分隔各层。
A level lights up when a run has checked it: red for the original pipeline, teal for the optimized one.某次运行检查完一层，该层就会亮起：红色是原始流程，青色是优化后的流程。
ds_perfectoid_bounded_tilt_modelConstruct the integral rational locally ringed space, an injective map of its global sections into E[1/p] with integral image, local regularity and principalization, a compact rational basis, its perfect characteristic-p tilt presheaf and common quotient modulo the parameters, and uniform power bounds from ordinary Tate acyclicity on both finite rational Cech complexes. No almost Cech annihilation is concluded.
∀ (E : Type*) [CommRing E] (B : Type*) [CommRing B] [Algebra B E] (p : ℕ), p.Prime → ∀ (π : ℕ → B), π 0 = (p : B) → (∀ n : ℕ, π (n + 1) ^ p = π n) → (∀ x : E, (p : E) * x = 0 → x = 0) → IsAdicComplete (Ideal.span {(p : E)}) E → (∀ x : E, ∃ y : E, x - y ^ p ∈ Ideal.span {(p : E)}) → (∀ x : E, x ^ p ∈ Ideal.span {(p : E)} → x ∈ Ideal.span {algebraMap B E (π 1)}) → ∃ (S : AlgebraicGeometry.LocallyRingedSpace.{u_1}) (e : E →+* S.presheaf.obj (Opposite.op ⊤)) (j : S.presheaf.obj (Opposite.op ⊤) →+* Localization.Away (p : E)) (𝔅 : Set (TopologicalSpace.Opens S)) (T Q : TopCat.Presheaf CommRingCat.{u_1} S.toTopCat) (t : ℕ → T.obj (Opposite.op ⊤)) (α : CategoryTheory.NatTrans S.presheaf Q) (β : CategoryTheory.NatTrans T Q), Function.Injective j ∧ j.comp e = algebraMap E (Localization.Away (p : E)) ∧ (∀ s : S.presheaf.obj (Opposite.op ⊤), IsIntegral E (j s)) ∧ (∀ (x : S) (a : S.presheaf.stalk x), (TopCat.Presheaf.Γgerm S.presheaf x).hom (e ((p : E))) * a = 0 → a = 0) ∧ (∀ (I : Ideal E), I.FG → (∃ n : ℕ, ((p : E)) ^ n ∈ I) → ∀ x : S, Submodule.IsPrincipal (Ideal.map ((TopCat.Presheaf.Γgerm S.presheaf x).hom.comp e) I)) ∧ TopologicalSpace.Opens.IsBasis 𝔅 ∧ (∀ U ∈ 𝔅, ∀ V ∈ 𝔅, U ⊓ V ∈ 𝔅) ∧ (∀ U ∈ 𝔅, IsCompact (U : Set S)) ∧ ⊤ ∈ 𝔅 ∧ (∀ U : TopologicalSpace.Opens S, (p : T.obj (Opposite.op U)) = 0 ∧ Function.Bijective (fun a : T.obj (Opposite.op U) => a ^ p)) ∧ (∀ n : ℕ, t (n + 1) ^ p = t n) ∧ (∀ n : ℕ, (β.app (Opposite.op ⊤)).hom (t n) = (α.app (Opposite.op ⊤)).hom (e (algebraMap B E (π n)))) ∧ (∀ U ∈ 𝔅, (∀ a : S.presheaf.obj (Opposite.op U), (p : S.presheaf.obj (Opposite.op U)) * a = 0 → a = 0) ∧ (∀ a : T.obj (Opposite.op U), (T.map (CategoryTheory.homOfLE (show U ≤ ⊤ from le_top)).op).hom (t 0) * a = 0 → a = 0) ∧ Function.Surjective (α.app (Opposite.op U)).hom ∧ RingHom.ker (α.app (Opposite.op U)).hom = Ideal.span {(p : S.presheaf.obj (Opposite.op U))} ∧ Function.Surjective (β.app (Opposite.op U)).hom ∧ RingHom.ker (β.app (Opposite.op U)).hom = Ideal.span {(T.map (CategoryTheory.homOfLE (show U ≤ ⊤ from le_top)).op).hom (t 0)}) ∧ ∀ (N : ℕ) (V : Fin N → TopologicalSpace.Opens S), (∀ i, V i ∈ 𝔅) → iSup V ∈ 𝔅 → (∀ k : ℕ, 0 < k → ∃ m : ℕ, ∀ c : (HomologicalComplex.homologyFunctor (ModuleCat B) (ComplexShape.up ℕ) k).obj ((CategoryTheory.cechComplexFunctor V).obj (CategoryTheory.Functor.comp (PresheafOfModules.forgetToPresheafModuleCatObj (Opposite.op ⊤) CategoryTheory.Limits.isTerminalTop.op (PresheafOfModulesOfCommRing.unit S.presheaf)) (ModuleCat.restrictScalars (e.comp (algebraMap B E))))), ((p : B) ^ m) • c = 0) ∧ (∀ k : ℕ, 0 < k → ∃ m : ℕ, ∀ c : (HomologicalComplex.homologyFunctor (ModuleCat (T.obj (Opposite.op ⊤))) (ComplexShape.up ℕ) k).obj ((CategoryTheory.cechComplexFunctor V).obj (PresheafOfModules.forgetToPresheafModuleCatObj (Opposite.op ⊤) CategoryTheory.Limits.isTerminalTop.op (PresheafOfModulesOfCommRing.unit T))), (t 0 ^ m) • c = 0)ds_perfectoid_cech_realizationUnder the hypotheses of o105 (E integral perfectoid with the integral-saturation estimate; no derived categories), there are a locally ringed space S and e : E -> Gamma(S) such that p is regular on every stalk, every finitely generated ideal of E containing a power of p has principal image in every stalk, e is almost injective (e x = 0 implies pi_n x = 0), Gamma(S) is almost in the image of e (pi_n s = e a), and S has a basis of quasi-compact opens, closed under finite intersection and containing S, on which the Mathlib Cech complex of the structure sheaf (as B-modules) of every finite cover of a basis open by basis opens is killed by every pi_n in positive degrees.
∀ (B : Type*) [CommRing B] (E : Type u_1) [CommRing E] [Algebra B E] (p : ℕ), p.Prime → ∀ (π : ℕ → B), π 0 = (p : B) → (∀ n : ℕ, π (n + 1) ^ p = π n) → (∀ x : E, (p : E) * x = 0 → x = 0) → IsAdicComplete (Ideal.span {(p : E)}) E → (∀ x : E, ∃ y : E, x - y ^ p ∈ Ideal.span {(p : E)}) → (∀ x : E, x ^ p ∈ Ideal.span {(p : E)} → x ∈ Ideal.span {algebraMap B E (π 1)}) → (∀ (n : ℕ) (z : Localization.Away (p : E)), IsIntegral E z → ∃ a : E, algebraMap E (Localization.Away (p : E)) a = algebraMap E (Localization.Away (p : E)) (algebraMap B E (π n)) * z) → ∃ (S : AlgebraicGeometry.LocallyRingedSpace.{u_1}) (e : E →+* S.presheaf.obj (Opposite.op ⊤)), (∀ (x : S) (a : S.presheaf.stalk x), (TopCat.Presheaf.Γgerm S.presheaf x).hom (e ((p : E))) * a = 0 → a = 0) ∧ (∀ (I : Ideal E), I.FG → (∃ n : ℕ, ((p : E)) ^ n ∈ I) → ∀ x : S, Submodule.IsPrincipal (Ideal.map ((TopCat.Presheaf.Γgerm S.presheaf x).hom.comp e) I)) ∧ (∀ (n : ℕ) (x : E), e x = 0 → algebraMap B E (π n) * x = 0) ∧ (∀ (n : ℕ) (s : S.presheaf.obj (Opposite.op ⊤)), ∃ a : E, e a = e (algebraMap B E (π n)) * s) ∧ ∃ 𝔅 : Set (TopologicalSpace.Opens S), TopologicalSpace.Opens.IsBasis 𝔅 ∧ (∀ U ∈ 𝔅, ∀ V ∈ 𝔅, U ⊓ V ∈ 𝔅) ∧ (∀ U ∈ 𝔅, IsCompact (U : Set S)) ∧ ⊤ ∈ 𝔅 ∧ ∀ (N : ℕ) (V : Fin N → TopologicalSpace.Opens S), (∀ i, V i ∈ 𝔅) → iSup V ∈ 𝔅 → ∀ (k n : ℕ), 0 < k → ∀ c : (HomologicalComplex.homologyFunctor (ModuleCat B) (ComplexShape.up ℕ) k).obj ((CategoryTheory.cechComplexFunctor V).obj (CategoryTheory.Functor.comp (PresheafOfModules.forgetToPresheafModuleCatObj (Opposite.op ⊤) CategoryTheory.Limits.isTerminalTop.op (SheafOfModules.unit ((CategoryTheory.sheafCompose _ (CategoryTheory.forget₂ CommRingCat.{u_1} RingCat.{u_1})).obj S.sheaf)).val) (ModuleCat.restrictScalars (e.comp (algebraMap B E))))), π n • c = 0ds_perfectoid_ringed_realizationConstruct a locally ringed affinoid perfectoid realization with p-regular stalks, principal images of finitely generated p-open ideals, and an almost-acyclic object identified with derived global sections with the canonical unit factorization; assume the integral-closure estimate.
∀ (B : Type*) [CommRing B] (E : Type u_1) [CommRing E] [Algebra B E] (p : ℕ), p.Prime → ∀ (π : ℕ → B), π 0 = (p : B) → (∀ n : ℕ, π (n + 1) ^ p = π n) → (∀ x : E, (p : E) * x = 0 → x = 0) → IsAdicComplete (Ideal.span {(p : E)}) E → (∀ x : E, ∃ y : E, x - y ^ p ∈ Ideal.span {(p : E)}) → (∀ x : E, x ^ p ∈ Ideal.span {(p : E)} → x ∈ Ideal.span {algebraMap B E (π 1)}) → (∀ (n : ℕ) (z : Localization.Away (p : E)), IsIntegral E z → ∃ a : E, algebraMap E (Localization.Away (p : E)) a = algebraMap E (Localization.Away (p : E)) (algebraMap B E (π n)) * z) → ∀ [hDB : HasDerivedCategory (ModuleCat B)] (_hDB : hDB = HasDerivedCategory.standard (ModuleCat B)), ∃ (S : AlgebraicGeometry.LocallyRingedSpace.{u_1}) (e : E →+* S.presheaf.obj (Opposite.op ⊤)), (∀ (x : S) (a : S.presheaf.stalk x), (TopCat.Presheaf.Γgerm S.presheaf x).hom (e ((p : E))) * a = 0 → a = 0) ∧ (∀ (I : Ideal E), I.FG → (∃ n : ℕ, ((p : E)) ^ n ∈ I) → ∀ x : S, Submodule.IsPrincipal (Ideal.map ((TopCat.Presheaf.Γgerm S.presheaf x).hom.comp e) I)) ∧ (∀ [hDS : HasDerivedCategory (SheafOfModules ((CategoryTheory.sheafCompose _ (CategoryTheory.forget₂ CommRingCat.{u_1} RingCat.{u_1})).obj S.sheaf))] (_hDS : hDS = HasDerivedCategory.standard (SheafOfModules ((CategoryTheory.sheafCompose _ (CategoryTheory.forget₂ CommRingCat.{u_1} RingCat.{u_1})).obj S.sheaf))) , ∀ [CategoryTheory.Functor.Additive (CategoryTheory.Functor.comp (SheafOfModules.evaluation.{u_1} ((CategoryTheory.sheafCompose _ (CategoryTheory.forget₂ CommRingCat.{u_1} RingCat.{u_1})).obj S.sheaf) ⟨⊤⟩) (ModuleCat.restrictScalars (e.comp (algebraMap B E))))], ∃ (D : DerivedCategory (ModuleCat B)) (aD : CategoryTheory.Iso D (DerivedCategory.Plus.ι.obj ((CategoryTheory.Functor.rightDerivedFunctorPlus (CategoryTheory.Functor.comp (SheafOfModules.evaluation.{u_1} ((CategoryTheory.sheafCompose _ (CategoryTheory.forget₂ CommRingCat.{u_1} RingCat.{u_1})).obj S.sheaf) ⟨⊤⟩) (ModuleCat.restrictScalars (e.comp (algebraMap B E))))).obj ((DerivedCategory.Plus.singleFunctor (SheafOfModules ((CategoryTheory.sheafCompose _ (CategoryTheory.forget₂ CommRingCat.{u_1} RingCat.{u_1})).obj S.sheaf)) 0).obj (SheafOfModules.unit ((CategoryTheory.sheafCompose _ (CategoryTheory.forget₂ CommRingCat.{u_1} RingCat.{u_1})).obj S.sheaf)))))) (i : (DerivedCategory.singleFunctor (ModuleCat B) 0).obj (ModuleCat.of B E) ⟶ D), DerivedCategory.Plus.ι.map (CategoryTheory.CategoryStruct.comp ((DerivedCategory.Plus.singleFunctor (ModuleCat B) 0).map (@ModuleCat.ofHom B _ B (S.presheaf.obj (Opposite.op ⊤)) _ _ _ (@Algebra.toModule B (S.presheaf.obj (Opposite.op ⊤)) _ _ (RingHom.toAlgebra (e.comp (algebraMap B E)))) (@Algebra.linearMap B (S.presheaf.obj (Opposite.op ⊤)) _ _ (RingHom.toAlgebra (e.comp (algebraMap B E)))))) ((LeanEval.AlgebraicGeometry.DirectSummand.rightDerivedFunctorPlusUnit' (CategoryTheory.Functor.comp (SheafOfModules.evaluation.{u_1} ((CategoryTheory.sheafCompose _ (CategoryTheory.forget₂ CommRingCat.{u_1} RingCat.{u_1})).obj S.sheaf) ⟨⊤⟩) (ModuleCat.restrictScalars (e.comp (algebraMap B E)))) 0).app (SheafOfModules.unit ((CategoryTheory.sheafCompose _ (CategoryTheory.forget₂ CommRingCat.{u_1} RingCat.{u_1})).obj S.sheaf)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((DerivedCategory.singleFunctor (ModuleCat B) 0).map (ModuleCat.ofHom (Algebra.linearMap B E))) i) aD.hom ∧ (∀ (j : ℤ) (n : ℕ) (x : (DerivedCategory.homologyFunctor (ModuleCat B) j).obj ((DerivedCategory.singleFunctor (ModuleCat B) 0).obj (ModuleCat.of B E))), ((DerivedCategory.homologyFunctor (ModuleCat B) j).map i).hom x = 0 → π n • x = 0) ∧ (∀ (j : ℤ) (n : ℕ) (y : (DerivedCategory.homologyFunctor (ModuleCat B) j).obj D), ∃ x : (DerivedCategory.homologyFunctor (ModuleCat B) j).obj ((DerivedCategory.singleFunctor (ModuleCat B) 0).obj (ModuleCat.of B E)), ((DerivedCategory.homologyFunctor (ModuleCat B) j).map i).hom x = π n • y))ds_perfectoid_generic_section_comparisonA generic lift from an integral perfectoid algebra to a proper B-scheme gives a compatible derived comparison from its global sections to an object almost cohomologically isomorphic to E[0].
∀ (B : Type*) [CommRing B] (E : Type u_1) [CommRing E] [Algebra B E] (p : ℕ), p.Prime → ∀ (π : ℕ → B), π 0 = (p : B) → (∀ n : ℕ, π (n + 1) ^ p = π n) → (∀ x : E, (p : E) * x = 0 → x = 0) → IsAdicComplete (Ideal.span {(p : E)}) E → (∀ x : E, ∃ y : E, x - y ^ p ∈ Ideal.span {(p : E)}) → (∀ x : E, x ^ p ∈ Ideal.span {(p : E)} → x ∈ Ideal.span {algebraMap B E (π 1)}) → ∀ [hDB : HasDerivedCategory (ModuleCat B)] (_hDB : hDB = HasDerivedCategory.standard (ModuleCat B)) (Y : AlgebraicGeometry.Scheme) (f : Y ⟶ AlgebraicGeometry.Spec (CommRingCat.of B)) [AlgebraicGeometry.IsProper f] (g : AlgebraicGeometry.Spec (CommRingCat.of (Localization.Away (p : E))) ⟶ Y), CategoryTheory.CategoryStruct.comp g f = AlgebraicGeometry.Spec.map (CommRingCat.ofHom ((algebraMap E (Localization.Away (p : E))).comp (algebraMap B E))) → ∀ [hDY : HasDerivedCategory (SheafOfModules Y.ringCatSheaf)] (_hDY : hDY = HasDerivedCategory.standard (SheafOfModules Y.ringCatSheaf)) (ψ : B →+* Y.presheaf.obj (Opposite.op ⊤)), ψ = ((AlgebraicGeometry.ΓSpec.adjunction.homEquiv _ _).symm f).unop.hom → ∀ (_inj : CategoryTheory.EnoughInjectives (SheafOfModules Y.ringCatSheaf)), ∃ (D : DerivedCategory (ModuleCat B)) (v : DerivedCategory.Plus.ι.obj ((CategoryTheory.Functor.rightDerivedFunctorPlus (CategoryTheory.Functor.comp (SheafOfModules.evaluation Y.ringCatSheaf ⟨⊤⟩) (ModuleCat.restrictScalars ψ))).obj ((DerivedCategory.Plus.singleFunctor (SheafOfModules Y.ringCatSheaf) 0).obj (SheafOfModules.unit Y.ringCatSheaf))) ⟶ D) (i : (DerivedCategory.singleFunctor (ModuleCat B) 0).obj (ModuleCat.of B E) ⟶ D), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.map DerivedCategory.Plus.ι (CategoryTheory.CategoryStruct.comp ((DerivedCategory.Plus.singleFunctor _ 0).map (@ModuleCat.ofHom B _ B (Y.presheaf.obj (Opposite.op ⊤)) _ _ _ (@Algebra.toModule B (Y.presheaf.obj (Opposite.op ⊤)) _ _ (RingHom.toAlgebra ψ)) (@Algebra.linearMap B (Y.presheaf.obj (Opposite.op ⊤)) _ _ (RingHom.toAlgebra ψ)))) ((LeanEval.AlgebraicGeometry.DirectSummand.rightDerivedFunctorPlusUnit' (CategoryTheory.Functor.comp (SheafOfModules.evaluation Y.ringCatSheaf ⟨⊤⟩) (ModuleCat.restrictScalars ψ)) 0).app (SheafOfModules.unit Y.ringCatSheaf)))) v = CategoryTheory.CategoryStruct.comp ((DerivedCategory.singleFunctor (ModuleCat B) 0).map (ModuleCat.ofHom (Algebra.linearMap B E))) i ∧ (∀ (j : ℤ) (n : ℕ) (x : (DerivedCategory.homologyFunctor (ModuleCat B) j).obj ((DerivedCategory.singleFunctor (ModuleCat B) 0).obj (ModuleCat.of B E))), ((DerivedCategory.homologyFunctor (ModuleCat B) j).map i).hom x = 0 → π n • x = 0) ∧ (∀ (j : ℤ) (n : ℕ) (y : (DerivedCategory.homologyFunctor (ModuleCat B) j).obj (D)), ∃ x : (DerivedCategory.homologyFunctor (ModuleCat B) j).obj ((DerivedCategory.singleFunctor (ModuleCat B) 0).obj (ModuleCat.of B E)), ((DerivedCategory.homologyFunctor (ModuleCat B) j).map i).hom x = π n • y)import Mathlib
import ChallengeDeps
/-!
# Direct summand conjecture and its derived variant
Hochster's direct summand conjecture states that any finite extension of a regular
commutative ring splits as a module, which was first proved by André in 2016.
Bhatt gave a quicker proof that circumvents the perfectoid Abhyankar lemma (André's
prior work) using a quantitative form of Scholze’s Hebbarkeitssatz (the Riemann
extension theorem) for perfectoid spaces. The same idea also leads to a proof of a
derived variant of the direct summand conjecture put forth by de Jong, which states
that if A is a regular (Noetherian) ring and X ⟶ Spec A is proper and surjective,
then A ⟶ RΓ(X, 𝒪_X) splits in the derived category D(A).
## References
* Yves André, La conjecture du facteur direct, https://arxiv.org/abs/1609.00345
* Bhargav Bhatt, On the direct summand conjecture and its derived variant, https://arxiv.org/abs/1608.08882
* Linquan Ma, a short proof of the direct summand theorem via the flatness lemma, https://www.math.purdue.edu/~ma326/DSC.pdf
-/
open CategoryTheory AlgebraicGeometry
namespace LeanEval.AlgebraicGeometry.DirectSummand
variable (A : Type*) [CommRing A] [IsRegularRing A]
instance {C : Type*} [Category* C] {J : GrothendieckTopology C} (R : Sheaf J RingCat) (X : Cᵒᵖ) :
(SheafOfModules.evaluation R X).Additive where
map_add := rfl
theorem derived_direct_summand [HasDerivedCategory (ModuleCat A)]
(X : Scheme) (f : X ⟶ Spec (.of A)) [IsProper f] (surj : Function.Surjective f)
[HasDerivedCategory (SheafOfModules X.ringCatSheaf)] :
let φ : A →+* Γ(X, ⊤) := ((ΓSpec.adjunction.homEquiv _ _).symm f).unop.hom
let : Algebra A Γ(X, ⊤) := φ.toAlgebra
∀ _ : EnoughInjectives (SheafOfModules X.ringCatSheaf), IsSplitMono <|
(DerivedCategory.Plus.singleFunctor _ 0).map
(ModuleCat.ofHom (Algebra.linearMap A Γ(X, ⊤))) ≫
(rightDerivedFunctorPlusUnit' (SheafOfModules.evaluation X.ringCatSheaf ⟨⊤⟩ ⋙
ModuleCat.restrictScalars φ) 0).app (SheafOfModules.unit X.ringCatSheaf) := by
sorry
theorem direct_summand (B : Type*) [CommRing B] [Algebra A B]
[Module.Finite A B] [FaithfulSMul A B] :
∃ π : B →ₗ[A] A, π ∘ₗ Algebra.linearMap A B = .id := by
sorry
end LeanEval.AlgebraicGeometry.DirectSummand
LOT checks the root with the unmodified official pipeline from scratch, as Lean-Eval does; this is that check, alone on the same isolated cores. No what-if with LOT’s optimizations was run for this problem: Its root fills two theorems at once, and one of them states its claim through local definitions and an instance that the challenge file itself declares, which a single node statement cannot carry..LOT 对根总是用未改动的官方流程从头检查，与 Lean-Eval 一致；这里就是这次检查，同样在独占锁定的核上单独运行。这道题没有做打开 LOT 优化的假设对比：它的根要同时填两个定理，其中一个的命题依赖局部定义和挑战文件里自己声明的实例，单个节点命题装不下。。
| Configuration配置 | Wall clock (min)用时（分钟） | CPU-hours used实际 CPU 小时 |
|---|---|---|
| Lean's original pipelineLean 原始流程 | 77.3 | 5.391 |
| LOT’s infrastructure (all six optimizations)LOT 基础设施（6 项优化全开） | 6.0 | 0.369 |
| Optimizations of the previous release, levels side by side (2 workers)上一版优化，各层并排检查（2 个 worker） | 9.1 | 0.752 |
| As it ran in the proved tree (that day’s pipeline, queueing included)证明树当时实际用时（当时的流程，含排队） | 45.8 | – |
Conditions: each run alone on 8 whole physical cores (16 CPUs, both hyperthreads) and 64 GiB of one NUMA node of one host (AMD EPYC 7B13), locked exclusively for that run so that no other process could use those CPUs; network off, every tool and library mounted read-only; Lean leanprover/lean4:v4.35.0-rc3. The original pipeline is the unmodified official checker[3,4] run once per level; queue waits and the scheduler’s pauses between levels are not counted for either lane. Measured on 2026-10-24.条件：每次运行单独占用同一台主机（AMD EPYC 7B13）一个 NUMA 节点上的 8 个完整物理核（16 个逻辑 CPU，含超线程）和 64 GiB 内存，运行期间独占锁定，其他进程用不了这些 CPU；断网，所有工具和库只读挂载；Lean leanprover/lean4:v4.35.0-rc3。原始流程是未经改动的官方检查器[3,4]，每层运行一次；两条泳道都不计排队等待和层与层之间调度器的停顿。测于 2026-10-24。