openai/math, paper family 304. OpenAI, The Hilbert-Smith conjecture in every finite dimension, OpenAI math release (paper family 304). Statement formalised from Theorem 1.1 of the paper.openai/math 第 304 族。OpenAI, The Hilbert-Smith conjecture in every finite dimension, OpenAI math release (paper family 304). Statement formalised from Theorem 1.1 of the paper. github.com/openai/math
When LOT proved this problem, a 12-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 证这道题时，有一条 12 层的中间定理链同时收口：每一层都由下一层推出。我们把这条链检查了两遍，每一遍单独运行，独占锁定 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 17043 s from scratch on the same 8 cores, 5500 modules. The ledger is not assumed: the LOT run starts with an empty one.前提。两遍检查从相同的情况开始：链上每个定理都已经证明完毕。LOT 那一遍还默认 LOT 此前已经做完的工作：链下面的一切都做过预检查，紧挨着链的那一层库已经编译好、可以直接复用。这部分工作发生在 agent 还在证明的时候，不计入下面 LOT 的用时；单独测量，这次从头编译在同样的 8 个核上用时 17043 秒，5500 个模块。账本不算在前提里：LOT 那一遍从空账本开始。
What the two times are. Lean original is the wall-clock time to check the 12 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 上把这 12 层依次检查完的总用时，每层都用未改动的官方检查器从头检查。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.每条色条从头到尾对应各自那次运行，按实测各阶段用时画出，所以两条最终一样长；右侧分钟数和共用的时钟显示各自的真实用时。白色刻线分隔各层。 The original lane is an estimate, drawn hatched: not run (estimate-only, user decision): each of the 12 levels holds the heavy proofs, so each original check = a from-scratch build of ~5,500 modules (10,920 s: the tree's own root compile on 16 cores) + export (~180 s, estimated) + nanoda (2,760 s: 46 min measured on this node) + the serial Lean replay (28,070 s: the o206/o207 node's serial replay measured in the check-v12 tests); 12 levels one after another. Resources differ from the isolated runs: the build figure was measured on 16 cores while every isolated run here has 8, and the nanoda and serial-Lean figures come from a production check worker, not isolated cores. The estimate assumes the 16-core build, which makes the original look faster than an 8-core isolated run would be, so the estimated speed-up is a lower bound; nothing was rescaled原始流程那一条是估计值，用斜线画出：not run (estimate-only, user decision): each of the 12 levels holds the heavy proofs, so each original check = a from-scratch build of ~5,500 modules (10,920 s: the tree's own root compile on 16 cores) + export (~180 s, estimated) + nanoda (2,760 s: 46 min measured on this node) + the serial Lean replay (28,070 s: the o206/o207 node's serial replay measured in the check-v12 tests); 12 levels one after another. Resources differ from the isolated runs: the build figure was measured on 16 cores while every isolated run here has 8, and the nanoda and serial-Lean figures come from a production check worker, not isolated cores. The estimate assumes the 16-core build, which makes the original look faster than an 8-core isolated run would be, so the estimated speed-up is a lower bound; nothing was rescaled
A level lights up when a run has checked it: red for the original pipeline, teal for the optimized one.某次运行检查完一层，该层就会亮起：红色是原始流程，青色是优化后的流程。
hs304_sphere_character_classes_from_finite_cutoffAssuming the actual finite-test cutoff theorem and the original compact-derived-coproduct hypothesis, construct the original compatible primitive sphere comparison, its normalized rational coordinate and exact 2^d cyclic relations, and one simultaneous integral character-class family with all four original laws modulo torsion. Proper projection/acyclicity is imported from accepted o199.
(∀ (X : TopCat.{0}) [T2Space X] [∀ Z : TopCat.{0}, HasDerivedCategory.{1} (TopCat.Sheaf (ModuleCat.{0} ℝ) Z)] [∀ (Z : TopCat.{0}) (f : Quiver.Hom Z X), (TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) f).Additive] (M : ∀ (r : ℕ) (S : Set (Fin r → ℝ)), C(S,X) → Prop), (∀ (r : ℕ) (T : Set (Fin r → ℝ)), T ∈ BooleanSubalgebra.closure {s | ∃ P : MvPolynomial (Fin r) ℝ, s = {x | 0 < MvPolynomial.eval x P}} → ∀ (S : Set (Fin r → ℝ)) (f : C(S,X)) (h : T ⊆ S), M r S f → M r T (f.comp ⟨Set.inclusion h, continuous_inclusion h⟩)) → (fun (G : TopologicalSpace.Opens X → CategoryTheory.ObjectProperty (DerivedCategory.Plus (TopCat.Sheaf (ModuleCat.{0} ℝ) X))) => ∀ (O : TopologicalSpace.Opens X) (K : Set X), IsClosed K → K ⊆ O → ∀ (n : ℕ) (A : DerivedCategory.Plus (TopCat.Sheaf (ModuleCat.{0} ℝ) X)), (((G ⊤).shiftClosure ℤ).binaryProductsClosure.extensionProductIter n) A → ∃ B, (G O).triangEnvelope B ∧ ∃ s : Quiver.Hom B A, ∃ N : TopologicalSpace.Opens X, K ⊆ N ∧ ∀ x ∈ N, ∀ i : ℤ, CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor (ModuleCat.{0} ℝ) x).map ((TopCat.Sheaf.forget (ModuleCat.{0} ℝ) X).map ((DerivedCategory.Plus.homologyFunctor _ i).map s)))) (fun O A => ∃ (r : ℕ) (S : Set (Fin r → ℝ)) (f : C(S,X)), S ∈ BooleanSubalgebra.closure {s | ∃ P : MvPolynomial (Fin r) ℝ, s = {x | 0 < MvPolynomial.eval x P}} ∧ IsCompact S ∧ M r S f ∧ (∀ x, f x ∈ O) ∧ Nonempty (A ≅ (TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).rightDerivedFunctorPlus.obj ((DerivedCategory.Plus.singleFunctor _ 0).obj ((CategoryTheory.constantSheaf (Opens.grothendieckTopology (TopCat.of S)) (ModuleCat.{0} ℝ)).obj (ModuleCat.of.{0} ℝ ℝ))))))→(∀ (X Y:TopCat.{0}) [CompactSpace X] [T2Space X] [T2Space Y] [HasDerivedCategory.{1} (TopCat.Sheaf (ModuleCat.{0} ℝ) X)] [HasDerivedCategory.{1} (TopCat.Sheaf (ModuleCat.{0} ℝ) Y)] (f:C(X,Y)) [(TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).Additive],CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℕ) (TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).rightDerivedFunctorPlus)→∀ (p d:ℕ) [Fact p.Prime] (W:Set (EuclideanSpace ℝ (Fin d))),IsOpen W→IsConnected W→3≤d→Odd d→∀ [AddAction (PadicInt p) (OnePoint W)] [ContinuousVAdd (PadicInt p) (OnePoint W)] [TopologicalSpace.MetrizableSpace (OnePoint W)],(∀ g:PadicInt p,g +ᵥ (OnePoint.infty:OnePoint W)=OnePoint.infty)→(∀ g:PadicInt p,∃ r:W ≃ₜ W,∀ x:W,g +ᵥ (x:OnePoint W)=(r (r x):OnePoint W))→∀ (S Y:Type) [TopologicalSpace S] [TopologicalSpace Y] (eY:Quotient (AddAction.orbitRel (PadicInt p) (OnePoint W)) ≃ₜ Y) (q:C(OnePoint W,Y)),(∀ x,q x=eY (Quotient.mk'' x))→∀ (e:OnePoint (EuclideanSpace ℝ (Fin d)) ≃ₜ S) (c:C(OnePoint (EuclideanSpace ℝ (Fin d)),OnePoint W)),c OnePoint.infty=OnePoint.infty→(∀ x:W,c ((x:EuclideanSpace ℝ (Fin d)):OnePoint _)=(x:OnePoint W))→(∀ x:EuclideanSpace ℝ (Fin d),x ∉ W→c (x:OnePoint _)=OnePoint.infty)→∀ deg:C(S,S)→ℤ,(∀ D,((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).map (TopCat.ofHom D)=deg D • CategoryTheory.CategoryStruct.id _)→∃ (F E:AddCommGrpCat.{0}) (cmp:F→+E) (ρ:E→+ℚ) (u v:F) (z:∀ k:ℕ,C(Y,S)→Fin (p^k)→E),(∀ (x:F) (m n:ℤ),m • x=n • u→∃ t:ℤ,m*t=n)∧ρ (cmp u)=1∧(∃ b:ℤ,b • v=(2^d:ℕ) • u)∧(∀ x:E,∃ b:ℤ,b • cmp v=(2^d:ℕ) • x)∧(∀ k t,∃ n:ℕ,0<n∧n • (∑ i,z k t i)=n • ((4*deg (((t.comp q).comp c).comp ⟨e.symm,e.symm.continuous⟩)) • cmp u))∧(∀ k D t i,∃ n:ℕ,0<n∧n • z k (D.comp t) i=n • (deg D • z k t i))∧(∀ k t₀ t₁,t₀.Homotopic t₁→∀ i,∃ n:ℕ,0<n∧n • z k t₀ i=n • z k t₁ i)∧∀ k,0 < k→∀ (U:Set (OnePoint W)) (β:OnePoint W→ZMod (p ^ k)),IsOpen U→U.Nonempty→OnePoint.infty ∉ U→(∀ g:PadicInt p,∀ x ∈ U,g +ᵥ x ∈ U)→IsLocallyConstant (U.restrict β)→(∀ g:PadicInt p,∀ x ∈ U,β (g +ᵥ x)=β x + PadicInt.toZModPow k g)→∀ h:C(Y,S),(∃ b,∀ y ∉ q '' U,h y=b)→∀ i j,∃ n:ℕ,0<n∧n • z k h i=n • z k h jhs304_sphere_character_classes_from_proper_projectionFrom the actual proper projection/acyclicity theorem and original compact-derived-coproduct hypothesis, construct one semialgebraic/continuous sphere group comparison with primitive orientation u, normalized rational coordinate rho, propagated generator v whose cyclic image contains 2^d times every continuous class, the corresponding semialgebraic relation, and one simultaneous integral character-class family satisfying all four original identities modulo torsion. Accepted generic finite cohomology, convex splitting and open adjoints are available directly in lib.
(∀ (X Y : TopCat.{0}) [CompactSpace X] [T2Space X] [T2Space Y] (f : Quiver.Hom X Y) [(TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) f).Additive] [MX : CategoryTheory.MonoidalCategory (TopCat.Sheaf (ModuleCat.{0} ℝ) X)] [MY : CategoryTheory.MonoidalCategory (TopCat.Sheaf (ModuleCat.{0} ℝ) Y)], MX = CategoryTheory.Sheaf.monoidalCategory (Opens.grothendieckTopology X) (ModuleCat.{0} ℝ) → MY = CategoryTheory.Sheaf.monoidalCategory (Opens.grothendieckTopology Y) (ModuleCat.{0} ℝ) → ∀ [_m : (TopCat.Sheaf.pullback (ModuleCat.{0} ℝ) f).Monoidal], (∀ (A : TopCat.Sheaf (ModuleCat.{0} ℝ) Y) (B : TopCat.Sheaf (ModuleCat.{0} ℝ) X), CategoryTheory.IsIso ((TopCat.Sheaf.pullbackPushforwardAdjunction (ModuleCat.{0} ℝ) f).homEquiv _ _ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ (TopCat.Sheaf.pullback (ModuleCat.{0} ℝ) f) ((TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) f).obj B) A) (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((TopCat.Sheaf.pullbackPushforwardAdjunction (ModuleCat.{0} ℝ) f).counit.app B) ((TopCat.Sheaf.pullback (ModuleCat.{0} ℝ) f).obj A))))) ∧ ∀ (I : TopCat.Sheaf (ModuleCat.{0} ℝ) X), CategoryTheory.Injective I → ∀ (A : TopCat.Sheaf (ModuleCat.{0} ℝ) Y) (q : ℕ), 0 < q → CategoryTheory.Limits.IsZero (((TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) f).rightDerived q).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj I ((TopCat.Sheaf.pullback (ModuleCat.{0} ℝ) f).obj A))))→(∀ (X Y:TopCat.{0}) [CompactSpace X] [T2Space X] [T2Space Y] [HasDerivedCategory.{1} (TopCat.Sheaf (ModuleCat.{0} ℝ) X)] [HasDerivedCategory.{1} (TopCat.Sheaf (ModuleCat.{0} ℝ) Y)] (f:C(X,Y)) [(TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).Additive],CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℕ) (TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).rightDerivedFunctorPlus)→∀ (p d:ℕ) [Fact p.Prime] (W:Set (EuclideanSpace ℝ (Fin d))),IsOpen W→IsConnected W→3≤d→Odd d→∀ [AddAction (PadicInt p) (OnePoint W)] [ContinuousVAdd (PadicInt p) (OnePoint W)] [TopologicalSpace.MetrizableSpace (OnePoint W)],(∀ g:PadicInt p,g +ᵥ (OnePoint.infty:OnePoint W)=OnePoint.infty)→(∀ g:PadicInt p,∃ r:W ≃ₜ W,∀ x:W,g +ᵥ (x:OnePoint W)=(r (r x):OnePoint W))→∀ (S Y:Type) [TopologicalSpace S] [TopologicalSpace Y] (eY:Quotient (AddAction.orbitRel (PadicInt p) (OnePoint W)) ≃ₜ Y) (q:C(OnePoint W,Y)),(∀ x,q x=eY (Quotient.mk'' x))→∀ (e:OnePoint (EuclideanSpace ℝ (Fin d)) ≃ₜ S) (c:C(OnePoint (EuclideanSpace ℝ (Fin d)),OnePoint W)),c OnePoint.infty=OnePoint.infty→(∀ x:W,c ((x:EuclideanSpace ℝ (Fin d)):OnePoint _)=(x:OnePoint W))→(∀ x:EuclideanSpace ℝ (Fin d),x ∉ W→c (x:OnePoint _)=OnePoint.infty)→∀ deg:C(S,S)→ℤ,(∀ D,((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).map (TopCat.ofHom D)=deg D • CategoryTheory.CategoryStruct.id _)→∃ (F E:AddCommGrpCat.{0}) (cmp:F→+E) (ρ:E→+ℚ) (u v:F) (z:∀ k:ℕ,C(Y,S)→Fin (p^k)→E),(∀ (x:F) (m n:ℤ),m • x=n • u→∃ t:ℤ,m*t=n)∧ρ (cmp u)=1∧(∃ b:ℤ,b • v=(2^d:ℕ) • u)∧(∀ x:E,∃ b:ℤ,b • cmp v=(2^d:ℕ) • x)∧(∀ k t,∃ n:ℕ,0<n∧n • (∑ i,z k t i)=n • ((4*deg (((t.comp q).comp c).comp ⟨e.symm,e.symm.continuous⟩)) • cmp u))∧(∀ k D t i,∃ n:ℕ,0<n∧n • z k (D.comp t) i=n • (deg D • z k t i))∧(∀ k t₀ t₁,t₀.Homotopic t₁→∀ i,∃ n:ℕ,0<n∧n • z k t₀ i=n • z k t₁ i)∧∀ k,0 < k→∀ (U:Set (OnePoint W)) (β:OnePoint W→ZMod (p ^ k)),IsOpen U→U.Nonempty→OnePoint.infty ∉ U→(∀ g:PadicInt p,∀ x ∈ U,g +ᵥ x ∈ U)→IsLocallyConstant (U.restrict β)→(∀ g:PadicInt p,∀ x ∈ U,β (g +ᵥ x)=β x + PadicInt.toZModPow k g)→∀ h:C(Y,S),(∃ b,∀ y ∉ q '' U,h y=b)→∀ i j,∃ n:ℕ,0<n∧n • z k h i=n • z k h jhs304_characters_from_generic_cohomologyGeneric bounded finite locally constant cohomology of compact semialgebraic coordinate projections and the stated convex local splitting imply the original normalized integer character system, assuming open-extension adjoints and compact-image derived coproduct preservation. The full ball premise follows from accepted o162 and o138.
(∀ (n r:ℕ) (K:Set ((Fin n→ℝ)×(Fin r→ℝ))),K ∈ BooleanSubalgebra.closure {s | ∃ P:MvPolynomial (Sum (Fin n) (Fin r)) ℝ,s={x | 0 < MvPolynomial.eval (Sum.elim x.1 x.2) P}}→IsCompact K→∀ (f:C(K,Fin r→ℝ)),(∀ x,f x=x.val.2)→∀ [(TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).Additive],∃ V:Set (Fin r→ℝ),IsOpen V∧Dense V∧∀ y ∈ V,∃ U:TopologicalSpace.Opens (Fin r→ℝ),y ∈ U∧∃ N:ℕ,∀ q:ℕ,∃ A:(ModuleCat.{0} ℝ),Module.Finite ℝ A∧(N < q→CategoryTheory.Limits.IsZero A)∧Nonempty ((TopCat.Sheaf.pullback (ModuleCat.{0} ℝ) (TopCat.ofHom (⟨Subtype.val,continuous_subtype_val⟩:C(U,Fin r→ℝ)))).obj (((TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).rightDerived q).obj ((CategoryTheory.constantSheaf (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj (ModuleCat.of.{0} ℝ ℝ)))≅(CategoryTheory.constantSheaf (Opens.grothendieckTopology U) (ModuleCat.{0} ℝ)).obj A))→(∀ (n:ℕ) (B:Set (EuclideanSpace ℝ (Fin n))),Convex ℝ B→∀ [HasDerivedCategory.{1} (CategoryTheory.Sheaf (Opens.grothendieckTopology B) (ModuleCat.{0} ℝ))] (A:DerivedCategory.Plus (CategoryTheory.Sheaf (Opens.grothendieckTopology B) (ModuleCat.{0} ℝ))) (l u:ℤ),(∀ i:ℤ,i < l ∨ u < i→CategoryTheory.Limits.IsZero ((DerivedCategory.Plus.homologyFunctor _ i).obj A))→(∀ i:ℤ,∃ V:(ModuleCat.{0} ℝ),Module.Finite ℝ V∧Nonempty ((DerivedCategory.Plus.homologyFunctor _ i).obj A≅(CategoryTheory.constantSheaf (Opens.grothendieckTopology B) (ModuleCat.{0} ℝ)).obj V))→∃ (N:ℕ) (j:Fin N→ℤ) (V:Fin N→(ModuleCat.{0} ℝ)),(∀ i,Module.Finite ℝ (V i))∧(∀ i,l≤j i∧j i≤u)∧Nonempty (A≅CategoryTheory.Limits.biproduct (fun i=> (DerivedCategory.Plus.singleFunctor _ (j i)).obj ((CategoryTheory.constantSheaf (Opens.grothendieckTopology B) (ModuleCat.{0} ℝ)).obj (V i)))))→(∀ (X:TopCat.{0}) (U:TopologicalSpace.Opens X),CategoryTheory.Functor.IsRightAdjoint (TopCat.Sheaf.pullback (ModuleCat.{0} ℝ) (TopCat.ofHom (⟨Subtype.val,continuous_subtype_val⟩:C(U,X)))))→(∀ (X Y:TopCat.{0}) [CompactSpace X] [T2Space X] [T2Space Y] [HasDerivedCategory.{1} (TopCat.Sheaf (ModuleCat.{0} ℝ) X)] [HasDerivedCategory.{1} (TopCat.Sheaf (ModuleCat.{0} ℝ) Y)] (f:C(X,Y)) [(TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).Additive],CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℕ) (TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).rightDerivedFunctorPlus)→∀ (p d:ℕ) [Fact p.Prime] (W:Set (EuclideanSpace ℝ (Fin d))),IsOpen W→IsConnected W→3≤d→Odd d→∀ [AddAction (PadicInt p) (OnePoint W)] [ContinuousVAdd (PadicInt p) (OnePoint W)] [TopologicalSpace.MetrizableSpace (OnePoint W)],(∀ g:PadicInt p,g +ᵥ (OnePoint.infty:OnePoint W)=OnePoint.infty)→(∀ g:PadicInt p,∃ r:W ≃ₜ W,∀ x:W,g +ᵥ (x:OnePoint W)=(r (r x):OnePoint W))→∀ (S Y:Type) [TopologicalSpace S] [TopologicalSpace Y] (eY:Quotient (AddAction.orbitRel (PadicInt p) (OnePoint W)) ≃ₜ Y) (q:C(OnePoint W,Y)),(∀ x,q x=eY (Quotient.mk'' x))→∀ (e:OnePoint (EuclideanSpace ℝ (Fin d)) ≃ₜ S) (c:C(OnePoint (EuclideanSpace ℝ (Fin d)),OnePoint W)),c OnePoint.infty=OnePoint.infty→(∀ x:W,c ((x:EuclideanSpace ℝ (Fin d)):OnePoint _)=(x:OnePoint W))→(∀ x:EuclideanSpace ℝ (Fin d),x ∉ W→c (x:OnePoint _)=OnePoint.infty)→∀ deg:C(S,S)→ℤ,(∀ D,((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).map (TopCat.ofHom D)=deg D • CategoryTheory.CategoryStruct.id _)→∃ (a:ℕ) (ζ:∀ k:ℕ,C(Y,S)→Fin (p ^ k)→ℤ),a≤d∧(∀ k t,(∑ i,ζ k t i)=(2:ℤ) ^ (a + 2) * deg (((t.comp q).comp c).comp ⟨e.symm,e.symm.continuous⟩))∧(∀ k D t i,ζ k (D.comp t) i=deg D * ζ k t i)∧(∀ k t₀ t₁,t₀.Homotopic t₁→∀ i,ζ k t₀ i=ζ k t₁ i)∧∀ k,0 < k→∀ (U:Set (OnePoint W)) (β:OnePoint W→ZMod (p ^ k)),IsOpen U→U.Nonempty→OnePoint.infty ∉ U→(∀ g:PadicInt p,∀ x ∈ U,g +ᵥ x ∈ U)→IsLocallyConstant (U.restrict β)→(∀ g:PadicInt p,∀ x ∈ U,β (g +ᵥ x)=β x + PadicInt.toZModPow k g)→∀ h:C(Y,S),(∃ b,∀ y ∉ q '' U,h y=b)→∀ i j,ζ k h i=ζ k h jhs304_characters_from_generic_projectionAssuming generic compact semialgebraic projection triviality with finite-polyhedral fibers, and all three original o163 premises including the full closed-ball dualizing calculation, construct the normalized simultaneous integer character system.
(∀ (n r:ℕ) (K:Set ((Fin n → ℝ) × (Fin r → ℝ))), K ∈ BooleanSubalgebra.closure {s | ∃ P:MvPolynomial (Sum (Fin n) (Fin r)) ℝ, s = {x | 0 < MvPolynomial.eval (Sum.elim x.1 x.2) P}} → IsCompact K → ∃ V:Set (Fin r → ℝ), IsOpen V ∧ Dense V ∧ ∀ y ∈ V, ∃ U:Set (Fin r → ℝ), IsOpen U ∧ y ∈ U ∧ ∃ (m:ℕ) (L:Geometry.SimplicialComplex ℝ (EuclideanSpace ℝ (Fin m))), L.faces.Finite ∧ ∃ h:({z:K // z.val.2 ∈ U}) ≃ₜ (U × L.space), ∀ z, (h z).1.val = z.val.val.2) → (∀ (X:TopCat.{0}) (U:TopologicalSpace.Opens X),CategoryTheory.Functor.IsRightAdjoint (TopCat.Sheaf.pullback (ModuleCat.{0} ℝ) (TopCat.ofHom (⟨Subtype.val,continuous_subtype_val⟩:C(U,X))))) → (∀ (n:ℕ) (K:Set (EuclideanSpace ℝ (Fin n))),IsCompact K → ∀ [HasDerivedCategory.{1} (CategoryTheory.Sheaf (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ))] [HasDerivedCategory.{1} (ModuleCat.{0} ℝ)] [((CategoryTheory.sheafSections (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).Additive],∃ R,Nonempty (CategoryTheory.Adjunction ((CategoryTheory.sheafSections (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).rightDerivedFunctorPlus R) ∧ ∀ (U:TopologicalSpace.Opens K),K = Metric.closedBall 0 1 → (∀ x:K,x ∈ U ↔ ‖(x:EuclideanSpace ℝ (Fin n))‖ < 1) → ∀ J,Nonempty (CategoryTheory.Adjunction J (TopCat.Sheaf.pullback (ModuleCat.{0} ℝ) (TopCat.ofHom (⟨Subtype.val,continuous_subtype_val⟩:C(U,K))))) → Nonempty (R.obj ((DerivedCategory.Plus.singleFunctor _ 0).obj (ModuleCat.of.{0} ℝ ℝ)) ≅ (CategoryTheory.shiftFunctor _ (n:ℤ)).obj ((DerivedCategory.Plus.singleFunctor _ 0).obj (J.obj ((CategoryTheory.constantSheaf (Opens.grothendieckTopology U) _).obj (ModuleCat.of.{0} ℝ ℝ)))))) → (∀ (X Y:TopCat.{0}) [CompactSpace X] [T2Space X] [T2Space Y] [HasDerivedCategory.{1} (TopCat.Sheaf (ModuleCat.{0} ℝ) X)] [HasDerivedCategory.{1} (TopCat.Sheaf (ModuleCat.{0} ℝ) Y)] (f:C(X,Y)) [(TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).Additive],CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℕ) (TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).rightDerivedFunctorPlus) → ∀ (p d:ℕ) [Fact p.Prime] (W:Set (EuclideanSpace ℝ (Fin d))),IsOpen W → IsConnected W → 3 ≤ d → Odd d → ∀ [AddAction (PadicInt p) (OnePoint W)] [ContinuousVAdd (PadicInt p) (OnePoint W)] [TopologicalSpace.MetrizableSpace (OnePoint W)],(∀ g:PadicInt p,g +ᵥ (OnePoint.infty:OnePoint W) = OnePoint.infty) → (∀ g:PadicInt p,∃ r:W ≃ₜ W,∀ x:W,g +ᵥ (x:OnePoint W) = (r (r x):OnePoint W)) → ∀ (S Y:Type) [TopologicalSpace S] [TopologicalSpace Y] (eY:Quotient (AddAction.orbitRel (PadicInt p) (OnePoint W)) ≃ₜ Y) (q:C(OnePoint W,Y)),(∀ x,q x = eY (Quotient.mk'' x)) → ∀ (e:OnePoint (EuclideanSpace ℝ (Fin d)) ≃ₜ S) (c:C(OnePoint (EuclideanSpace ℝ (Fin d)),OnePoint W)),c OnePoint.infty = OnePoint.infty → (∀ x:W,c ((x:EuclideanSpace ℝ (Fin d)):OnePoint _) = (x:OnePoint W)) → (∀ x:EuclideanSpace ℝ (Fin d),x ∉ W → c (x:OnePoint _) = OnePoint.infty) → ∀ deg:C(S,S) → ℤ,(∀ D,((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).map (TopCat.ofHom D) = deg D • CategoryTheory.CategoryStruct.id _) → ∃ (a:ℕ) (ζ:∀ k:ℕ,C(Y,S) → Fin (p ^ k) → ℤ),a ≤ d ∧ (∀ k t,(∑ i,ζ k t i) = (2:ℤ) ^ (a + 2) * deg (((t.comp q).comp c).comp ⟨e.symm,e.symm.continuous⟩)) ∧ (∀ k D t i,ζ k (D.comp t) i = deg D * ζ k t i) ∧ (∀ k t₀ t₁,t₀.Homotopic t₁ → ∀ i,ζ k t₀ i = ζ k t₁ i) ∧ ∀ k,0 < k → ∀ (U:Set (OnePoint W)) (β:OnePoint W → ZMod (p ^ k)),IsOpen U → U.Nonempty → OnePoint.infty ∉ U → (∀ g:PadicInt p,∀ x ∈ U,g +ᵥ x ∈ U) → IsLocallyConstant (U.restrict β) → (∀ g:PadicInt p,∀ x ∈ U,β (g +ᵥ x) = β x + PadicInt.toZModPow k g) → ∀ h:C(Y,S),(∃ b,∀ y ∉ q '' U,h y = b) → ∀ i j,ζ k h i = ζ k h jhs304_characters_from_ball_dualityGiven actual open-extension adjoints, compact derived-section adjoints with their closed-ball dualizing calculation, and compact-source total-derived coproduct preservation, construct the normalized simultaneous integer character system. Accepted proper base change, convex acyclicity and the sphere-tower algebra may be imported directly.
(∀ (X:TopCat.{0}) (U:TopologicalSpace.Opens X),CategoryTheory.Functor.IsRightAdjoint (TopCat.Sheaf.pullback (ModuleCat.{0} ℝ) (TopCat.ofHom (⟨Subtype.val,continuous_subtype_val⟩:C(U,X))))) → (∀ (n:ℕ) (K:Set (EuclideanSpace ℝ (Fin n))),IsCompact K → ∀ [HasDerivedCategory.{1} (CategoryTheory.Sheaf (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ))] [HasDerivedCategory.{1} (ModuleCat.{0} ℝ)] [((CategoryTheory.sheafSections (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).Additive],∃ R:CategoryTheory.Functor (DerivedCategory.Plus (ModuleCat.{0} ℝ)) (DerivedCategory.Plus (CategoryTheory.Sheaf (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ))),Nonempty (CategoryTheory.Adjunction ((CategoryTheory.sheafSections (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).rightDerivedFunctorPlus R) ∧ ∀ (U:TopologicalSpace.Opens K),K = Metric.closedBall 0 1 → (∀ x:K,x ∈ U ↔ ‖(x:EuclideanSpace ℝ (Fin n))‖ < 1) → ∀ (J:CategoryTheory.Functor (TopCat.Sheaf (ModuleCat.{0} ℝ) (TopCat.of U)) (CategoryTheory.Sheaf (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ))),Nonempty (CategoryTheory.Adjunction J (TopCat.Sheaf.pullback (ModuleCat.{0} ℝ) (TopCat.ofHom (⟨Subtype.val,continuous_subtype_val⟩:C(U,K))))) → Nonempty (R.obj ((DerivedCategory.Plus.singleFunctor (ModuleCat.{0} ℝ) 0).obj (ModuleCat.of.{0} ℝ ℝ)) ≅ (CategoryTheory.shiftFunctor (DerivedCategory.Plus (CategoryTheory.Sheaf (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ))) (n:ℤ)).obj ((DerivedCategory.Plus.singleFunctor (CategoryTheory.Sheaf (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)) 0).obj (J.obj ((CategoryTheory.constantSheaf (Opens.grothendieckTopology U) (ModuleCat.{0} ℝ)).obj (ModuleCat.of.{0} ℝ ℝ)))))) → (∀ (X Y:TopCat.{0}) [CompactSpace X] [T2Space X] [T2Space Y] [HasDerivedCategory.{1} (TopCat.Sheaf (ModuleCat.{0} ℝ) X)] [HasDerivedCategory.{1} (TopCat.Sheaf (ModuleCat.{0} ℝ) Y)] (f:C(X,Y)) [(TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).Additive],CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℕ) (TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).rightDerivedFunctorPlus) → ∀ (p d:ℕ) [Fact p.Prime] (W:Set (EuclideanSpace ℝ (Fin d))),IsOpen W → IsConnected W → 3 ≤ d → Odd d → ∀ [AddAction (PadicInt p) (OnePoint W)] [ContinuousVAdd (PadicInt p) (OnePoint W)] [TopologicalSpace.MetrizableSpace (OnePoint W)],(∀ g:PadicInt p,g +ᵥ (OnePoint.infty:OnePoint W) = OnePoint.infty) → (∀ g:PadicInt p,∃ r:W ≃ₜ W,∀ x:W,g +ᵥ (x:OnePoint W) = (r (r x):OnePoint W)) → ∀ (S Y:Type) [TopologicalSpace S] [TopologicalSpace Y] (eY:Quotient (AddAction.orbitRel (PadicInt p) (OnePoint W)) ≃ₜ Y) (q:C(OnePoint W,Y)),(∀ x,q x = eY (Quotient.mk'' x)) → ∀ (e:OnePoint (EuclideanSpace ℝ (Fin d)) ≃ₜ S) (c:C(OnePoint (EuclideanSpace ℝ (Fin d)),OnePoint W)),c OnePoint.infty = OnePoint.infty → (∀ x:W,c ((x:EuclideanSpace ℝ (Fin d)):OnePoint _) = (x:OnePoint W)) → (∀ x:EuclideanSpace ℝ (Fin d),x ∉ W → c (x:OnePoint _) = OnePoint.infty) → ∀ deg:C(S,S) → ℤ,(∀ D,((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).map (TopCat.ofHom D) = deg D • CategoryTheory.CategoryStruct.id (((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).obj (TopCat.of S))) → ∃ (a:ℕ) (ζ:∀ k:ℕ,C(Y,S) → Fin (p ^ k) → ℤ),a ≤ d ∧ (∀ k (t:C(Y,S)),(∑ i,ζ k t i) = (2:ℤ) ^ (a + 2) * deg (((t.comp q).comp c).comp ⟨e.symm,e.symm.continuous⟩)) ∧ (∀ k (D:C(S,S)) (t:C(Y,S)) (i:Fin (p ^ k)),ζ k (D.comp t) i = deg D * ζ k t i) ∧ (∀ k (t₀ t₁:C(Y,S)),t₀.Homotopic t₁ → ∀ i,ζ k t₀ i = ζ k t₁ i) ∧ ∀ k,0 < k → ∀ (U:Set (OnePoint W)) (β:OnePoint W → ZMod (p ^ k)),IsOpen U → U.Nonempty → OnePoint.infty ∉ U → (∀ g:PadicInt p,∀ x ∈ U,g +ᵥ x ∈ U) → IsLocallyConstant (U.restrict β) → (∀ g:PadicInt p,∀ x ∈ U,β (g +ᵥ x) = β x + PadicInt.toZModPow k g) → ∀ h:C(Y,S),(∃ b,∀ y ∉ q '' U,h y = b) → ∀ i j,ζ k h i = ζ k h jhs304_characters_from_derived_adjointsAssuming compact-source proper base change, convex constant-sheaf acyclicity, compact derived-section adjoints, and total-derived countable coproduct preservation for compact-source proper images, construct the normalized simultaneous integer character system. The dimension and compact cohomology-sum theorems are already accepted as o072 and o073.
(∀ (X Y : TopCat.{0}) [CompactSpace X] [T2Space X] [T2Space Y] (f : C(X,Y)) [(TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).Additive] (y : Y) [((CategoryTheory.sheafSections (Opens.grothendieckTopology {x : X // f x = y}) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).Additive],∀ q : ℕ,Nonempty (((TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).rightDerived q).comp ((TopCat.Sheaf.forget (ModuleCat.{0} ℝ) Y).comp (TopCat.Presheaf.stalkFunctor (ModuleCat.{0} ℝ) y)) ≅ (TopCat.Sheaf.pullback (ModuleCat.{0} ℝ) (TopCat.ofHom (⟨Subtype.val,continuous_subtype_val⟩ : C({x : X // f x = y},X)))).comp (((CategoryTheory.sheafSections (Opens.grothendieckTopology {x : X // f x = y}) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).rightDerived q))) → (∀ (n : ℕ) (K : Set (EuclideanSpace ℝ (Fin n))),Convex ℝ K → ∀ [((CategoryTheory.sheafSections (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).Additive] (M : ModuleCat.{0} ℝ) (q : ℕ),0 < q → CategoryTheory.Limits.IsZero ((((CategoryTheory.sheafSections (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).rightDerived q).obj ((CategoryTheory.constantSheaf (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj M))) → (∀ (n : ℕ) (K : Set (EuclideanSpace ℝ (Fin n))),IsCompact K → ∀ [HasDerivedCategory.{1} (CategoryTheory.Sheaf (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ))] [HasDerivedCategory.{1} (ModuleCat.{0} ℝ)] [((CategoryTheory.sheafSections (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).Additive],CategoryTheory.Functor.IsLeftAdjoint ((CategoryTheory.sheafSections (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).rightDerivedFunctorPlus) → (∀ (X Y : TopCat.{0}) [CompactSpace X] [T2Space X] [T2Space Y] [HasDerivedCategory.{1} (TopCat.Sheaf (ModuleCat.{0} ℝ) X)] [HasDerivedCategory.{1} (TopCat.Sheaf (ModuleCat.{0} ℝ) Y)] (f : C(X,Y)) [(TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).Additive],CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℕ) (TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).rightDerivedFunctorPlus) → ∀ (p d : ℕ) [Fact p.Prime] (W : Set (EuclideanSpace ℝ (Fin d))),IsOpen W → IsConnected W → 3 ≤ d → Odd d → ∀ [AddAction (PadicInt p) (OnePoint W)] [ContinuousVAdd (PadicInt p) (OnePoint W)] [TopologicalSpace.MetrizableSpace (OnePoint W)],(∀ g : PadicInt p,g +ᵥ (OnePoint.infty : OnePoint W) = OnePoint.infty) → (∀ g : PadicInt p,∃ r : W ≃ₜ W,∀ x : W,g +ᵥ (x : OnePoint W) = (r (r x) : OnePoint W)) → ∀ (S Y : Type) [TopologicalSpace S] [TopologicalSpace Y] (eY : Quotient (AddAction.orbitRel (PadicInt p) (OnePoint W)) ≃ₜ Y) (q : C(OnePoint W,Y)),(∀ x,q x = eY (Quotient.mk'' x)) → ∀ (e : OnePoint (EuclideanSpace ℝ (Fin d)) ≃ₜ S) (c : C(OnePoint (EuclideanSpace ℝ (Fin d)),OnePoint W)),c OnePoint.infty = OnePoint.infty → (∀ x : W,c ((x : EuclideanSpace ℝ (Fin d)) : OnePoint _) = (x : OnePoint W)) → (∀ x : EuclideanSpace ℝ (Fin d),x ∉ W → c (x : OnePoint _) = OnePoint.infty) → ∀ deg : C(S,S) → ℤ, (∀ D, ((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).map (TopCat.ofHom D) = deg D • CategoryTheory.CategoryStruct.id (((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).obj (TopCat.of S))) → ∃ (a : ℕ) (ζ : ∀ k : ℕ, C(Y, S) → Fin (p ^ k) → ℤ), a ≤ d ∧ (∀ k (t : C(Y, S)), (∑ i, ζ k t i) = (2 : ℤ) ^ (a + 2) * deg (((t.comp q).comp c).comp ⟨e.symm, e.symm.continuous⟩)) ∧ (∀ k (D : C(S, S)) (t : C(Y, S)) (i : Fin (p ^ k)), ζ k (D.comp t) i = deg D * ζ k t i) ∧ (∀ k (t₀ t₁ : C(Y, S)), t₀.Homotopic t₁ → ∀ i, ζ k t₀ i = ζ k t₁ i) ∧ ∀ k, 0 < k → ∀ (U : Set (OnePoint W)) (β : OnePoint W → ZMod (p ^ k)), IsOpen U → U.Nonempty → OnePoint.infty ∉ U → (∀ g : PadicInt p, ∀ x ∈ U, g +ᵥ x ∈ U) → IsLocallyConstant (U.restrict β) → (∀ g : PadicInt p, ∀ x ∈ U, β (g +ᵥ x) = β x + PadicInt.toZModPow k g) → ∀ h : C(Y, S), (∃ b, ∀ y ∉ q '' U, h y = b) → ∀ i j, ζ k h i = ζ k h jhs304_characters_from_local_sheaf_theoremsAssuming the two original universal cohomology foundations, compact-source proper base change and constant-sheaf acyclicity on convex subspaces, construct the simultaneous normalized integer character system for the original compactified p-adic action.
(∀ (n : ℕ) (K : Set (EuclideanSpace ℝ (Fin n))), IsCompact K → ∀ [CategoryTheory.Functor.Additive ((CategoryTheory.sheafSections (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤))] (q : ℕ), n < q → ∀ F : TopCat.Sheaf (ModuleCat.{0} ℝ) (TopCat.of.{0} K), CategoryTheory.Limits.IsZero ((((CategoryTheory.sheafSections (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).rightDerived q).obj F)) → (∀ (X : TopCat.{0}) [CompactSpace X] [T2Space X] [CategoryTheory.Functor.Additive ((CategoryTheory.sheafSections (Opens.grothendieckTopology X) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤))], ∀ q : ℕ, CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℕ) (((CategoryTheory.sheafSections (Opens.grothendieckTopology X) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).rightDerived q)) → (∀ (X Y : TopCat.{0}) [CompactSpace X] [T2Space X] [T2Space Y] (f : C(X, Y)) [CategoryTheory.Functor.Additive (TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f))] (y : Y) [CategoryTheory.Functor.Additive ((CategoryTheory.sheafSections (Opens.grothendieckTopology {x : X // f x = y}) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤))], ∀ q : ℕ, Nonempty (((TopCat.Sheaf.pushforward (ModuleCat.{0} ℝ) (TopCat.ofHom f)).rightDerived q).comp ((TopCat.Sheaf.forget (ModuleCat.{0} ℝ) Y).comp (TopCat.Presheaf.stalkFunctor (ModuleCat.{0} ℝ) y)) ≅ (TopCat.Sheaf.pullback (ModuleCat.{0} ℝ) (TopCat.ofHom (⟨Subtype.val, continuous_subtype_val⟩ : C({x : X // f x = y}, X)))).comp (((CategoryTheory.sheafSections (Opens.grothendieckTopology {x : X // f x = y}) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).rightDerived q))) → (∀ (n : ℕ) (K : Set (EuclideanSpace ℝ (Fin n))), Convex ℝ K → ∀ [CategoryTheory.Functor.Additive ((CategoryTheory.sheafSections (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤))] (M : ModuleCat.{0} ℝ) (q : ℕ), 0 < q → CategoryTheory.Limits.IsZero ((((CategoryTheory.sheafSections (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj (Opposite.op ⊤)).rightDerived q).obj ((CategoryTheory.constantSheaf (Opens.grothendieckTopology K) (ModuleCat.{0} ℝ)).obj M))) → ∀ (p d : ℕ) [Fact p.Prime] (W : Set (EuclideanSpace ℝ (Fin d))), IsOpen W → IsConnected W → 3 ≤ d → Odd d → ∀ [AddAction (PadicInt p) (OnePoint W)] [ContinuousVAdd (PadicInt p) (OnePoint W)] [TopologicalSpace.MetrizableSpace (OnePoint W)], (∀ g : PadicInt p, g +ᵥ (OnePoint.infty : OnePoint W) = OnePoint.infty) → (∀ g : PadicInt p, ∃ r : W ≃ₜ W, ∀ x : W, g +ᵥ (x : OnePoint W) = (r (r x) : OnePoint W)) → ∀ (S Y : Type) [TopologicalSpace S] [TopologicalSpace Y] (eY : Quotient (AddAction.orbitRel (PadicInt p) (OnePoint W)) ≃ₜ Y) (q : C(OnePoint W, Y)), (∀ x, q x = eY (Quotient.mk'' x)) → ∀ (e : OnePoint (EuclideanSpace ℝ (Fin d)) ≃ₜ S) (c : C(OnePoint (EuclideanSpace ℝ (Fin d)), OnePoint W)), c OnePoint.infty = OnePoint.infty → (∀ x : W, c ((x : EuclideanSpace ℝ (Fin d)) : OnePoint _) = (x : OnePoint W)) → (∀ x : EuclideanSpace ℝ (Fin d), x ∉ W → c (x : OnePoint _) = OnePoint.infty) → ∀ deg : C(S, S) → ℤ, (∀ D, ((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).map (TopCat.ofHom D) = deg D • CategoryTheory.CategoryStruct.id (((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).obj (TopCat.of S))) → ∃ (a : ℕ) (ζ : ∀ k : ℕ, C(Y, S) → Fin (p ^ k) → ℤ), a ≤ d ∧ (∀ k (t : C(Y, S)), (∑ i, ζ k t i) = (2 : ℤ) ^ (a + 2) * deg (((t.comp q).comp c).comp ⟨e.symm, e.symm.continuous⟩)) ∧ (∀ k (D : C(S, S)) (t : C(Y, S)) (i : Fin (p ^ k)), ζ k (D.comp t) i = deg D * ζ k t i) ∧ (∀ k (t₀ t₁ : C(Y, S)), t₀.Homotopic t₁ → ∀ i, ζ k t₀ i = ζ k t₁ i) ∧ ∀ k, 0 < k → ∀ (U : Set (OnePoint W)) (β : OnePoint W → ZMod (p ^ k)), IsOpen U → U.Nonempty → OnePoint.infty ∉ U → (∀ g : PadicInt p, ∀ x ∈ U, g +ᵥ x ∈ U) → IsLocallyConstant (U.restrict β) → (∀ g : PadicInt p, ∀ x ∈ U, β (g +ᵥ x) = β x + PadicInt.toZModPow k g) → ∀ h : C(Y, S), (∃ b, ∀ y ∉ q '' U, h y = b) → ∀ i j, ζ k h i = ζ k h jhs304_scalar_characters_from_sheaf_foundationsAssuming the two universal sheaf-cohomology foundations, construct one integer character system for all tests and p-power partitions, with normalization 2^a for a<=d, degree covariance, homotopy invariance and concentrated equality.
(∀ (n : ℕ) (K : Set (EuclideanSpace ℝ (Fin n))), IsCompact K → ∀ [CategoryTheory.Functor.Additive (CategoryTheory.Functor.comp (TopCat.Sheaf.forget (ModuleCat.{0} ℝ) (TopCat.of.{0} K)) ((CategoryTheory.evaluation (Opposite (TopologicalSpace.Opens (TopCat.of.{0} K))) (ModuleCat.{0} ℝ)).obj (Opposite.op (⊤ : TopologicalSpace.Opens (TopCat.of.{0} K)))))], ∀ (q : ℕ), n < q → ∀ F : TopCat.Sheaf (ModuleCat.{0} ℝ) (TopCat.of.{0} K), CategoryTheory.Limits.IsZero ((CategoryTheory.Functor.rightDerived (CategoryTheory.Functor.comp (TopCat.Sheaf.forget (ModuleCat.{0} ℝ) (TopCat.of.{0} K)) ((CategoryTheory.evaluation (Opposite (TopologicalSpace.Opens (TopCat.of.{0} K))) (ModuleCat.{0} ℝ)).obj (Opposite.op (⊤ : TopologicalSpace.Opens (TopCat.of.{0} K))))) q).obj F)) → (∀ (X : TopCat.{0}) [CompactSpace X] [T2Space X] [CategoryTheory.Functor.Additive (CategoryTheory.Functor.comp (TopCat.Sheaf.forget (ModuleCat.{0} ℝ) X) ((CategoryTheory.evaluation (Opposite (TopologicalSpace.Opens X)) (ModuleCat.{0} ℝ)).obj (Opposite.op (⊤ : TopologicalSpace.Opens X))))], ∀ q : ℕ, CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℕ) (CategoryTheory.Functor.rightDerived (CategoryTheory.Functor.comp (TopCat.Sheaf.forget (ModuleCat.{0} ℝ) X) ((CategoryTheory.evaluation (Opposite (TopologicalSpace.Opens X)) (ModuleCat.{0} ℝ)).obj (Opposite.op (⊤ : TopologicalSpace.Opens X)))) q)) → ∀ (p d : ℕ) [Fact p.Prime] (W : Set (EuclideanSpace ℝ (Fin d))), IsOpen W → IsConnected W → 3 ≤ d → Odd d → ∀ [AddAction (PadicInt p) (OnePoint W)] [ContinuousVAdd (PadicInt p) (OnePoint W)] [TopologicalSpace.MetrizableSpace (OnePoint W)], (∀ g : PadicInt p, g +ᵥ (OnePoint.infty : OnePoint W) = OnePoint.infty) → (∀ g : PadicInt p, ∃ r : W ≃ₜ W, ∀ x : W, g +ᵥ (x : OnePoint W) = (r (r x) : OnePoint W)) → ∀ (S Y : Type) [TopologicalSpace S] [TopologicalSpace Y] (eY : Quotient (AddAction.orbitRel (PadicInt p) (OnePoint W)) ≃ₜ Y) (q : C(OnePoint W, Y)), (∀ x, q x = eY (Quotient.mk'' x)) → ∀ (e : OnePoint (EuclideanSpace ℝ (Fin d)) ≃ₜ S) (c : C(OnePoint (EuclideanSpace ℝ (Fin d)), OnePoint W)), c OnePoint.infty = OnePoint.infty → (∀ x : W, c ((x : EuclideanSpace ℝ (Fin d)) : OnePoint _) = (x : OnePoint W)) → (∀ x : EuclideanSpace ℝ (Fin d), x ∉ W → c (x : OnePoint _) = OnePoint.infty) → ∀ deg : C(S, S) → ℤ, (∀ D, ((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).map (TopCat.ofHom D) = deg D • CategoryTheory.CategoryStruct.id (((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).obj (TopCat.of S))) → ∃ (a : ℕ) (ζ : ∀ k : ℕ, C(Y, S) → Fin (p ^ k) → ℤ), a ≤ d ∧ (∀ (k : ℕ) (t : C(Y, S)), (∑ i, ζ k t i) = (2 : ℤ) ^ (a + 2) * deg (((t.comp q).comp c).comp ⟨e.symm, e.symm.continuous⟩)) ∧ (∀ (k : ℕ) (D : C(S, S)) (t : C(Y, S)) (i : Fin (p ^ k)), ζ k (D.comp t) i = deg D * ζ k t i) ∧ (∀ (k : ℕ) (t₀ t₁ : C(Y, S)), t₀.Homotopic t₁ → ∀ i, ζ k t₀ i = ζ k t₁ i) ∧ ∀ (k : ℕ), 0 < k → ∀ (U : Set (OnePoint W)) (β : OnePoint W → ZMod (p ^ k)), IsOpen U → U.Nonempty → OnePoint.infty ∉ U → (∀ g : PadicInt p, ∀ x ∈ U, g +ᵥ x ∈ U) → IsLocallyConstant (U.restrict β) → (∀ g : PadicInt p, ∀ x ∈ U, β (g +ᵥ x) = β x + PadicInt.toZModPow k g) → ∀ h : C(Y, S), (∃ b, ∀ y ∉ q '' U, h y = b) → ∀ i j, ζ k h i = ζ k h jhs304_integral_character_modelAn orientation-preserving compactified local p-adic action and collapse admit compatible reduced semialgebraic and continuous integral sphere-group towers, finite-relation signatures, and integral character classes for every test and finite p-power partition. Their sum is four times the pushed orientation class; they satisfy covariance, homotopy invariance and equality for a concentrated finite-sheet test. Sphere pushforward has the prescribed degree on the orientation class modulo torsion.
∀ (p d : ℕ) [Fact p.Prime] (W : Set (EuclideanSpace ℝ (Fin d))), IsOpen W → IsConnected W → 3 ≤ d → Odd d → ∀ [AddAction (PadicInt p) (OnePoint W)] [ContinuousVAdd (PadicInt p) (OnePoint W)] [TopologicalSpace.MetrizableSpace (OnePoint W)], (∀ g : PadicInt p, g +ᵥ (OnePoint.infty : OnePoint W) = OnePoint.infty) → (∀ g : PadicInt p, ∃ r : W ≃ₜ W, ∀ x : W, g +ᵥ (x : OnePoint W) = (r (r x) : OnePoint W)) → ∀ (S Y : Type) [TopologicalSpace S] [TopologicalSpace Y] (eY : Quotient (AddAction.orbitRel (PadicInt p) (OnePoint W)) ≃ₜ Y) (q : C(OnePoint W, Y)), (∀ x, q x = eY (Quotient.mk'' x)) → ∀ (e : OnePoint (EuclideanSpace ℝ (Fin d)) ≃ₜ S) (c : C(OnePoint (EuclideanSpace ℝ (Fin d)), OnePoint W)), c OnePoint.infty = OnePoint.infty → (∀ x : W, c ((x : EuclideanSpace ℝ (Fin d)) : OnePoint _) = (x : OnePoint W)) → (∀ x : EuclideanSpace ℝ (Fin d), x ∉ W → c (x : OnePoint _) = OnePoint.infty) → ∀ deg : C(S, S) → ℤ, (∀ D, ((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).map (TopCat.ofHom D) = deg D • CategoryTheory.CategoryStruct.id (((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).obj (TopCat.of S))) → ∃ (F E : ℕ → AddCommGrpCat.{0}) (cmp : ∀ j, F j →+ E j) (sF : ∀ j, F j →+ F (j + 1)) (sE : ∀ j, E j →+ E (j + 1)) (u : F d) (push : C(S, S) → (E d →+ E d)) (z : ∀ k : ℕ, C(Y, S) → Fin (p ^ k) → E d), (Nonempty (F 0 ≃+ ℤ) ∧ Function.Bijective (cmp 0) ∧ (∀ j, (sE j).comp (cmp j) = (cmp (j + 1)).comp (sF j)) ∧ ∀ j, (∀ x, sF j x = 0 → (2 : ℕ) • x = 0) ∧ (∀ y, ∃ x, sF j x = (2 : ℕ) • y) ∧ (∀ x, sE j x = 0 → (2 : ℕ) • x = 0) ∧ (∀ y, ∃ x, sE j x = (2 : ℕ) • y)) ∧ (∀ (x : F d) (m n : ℤ), m • x = n • u → ∃ t : ℤ, m * t = n) ∧ (∀ D, ∃ N : ℕ, 0 < N ∧ N • push D (cmp d u) = N • (deg D • cmp d u)) ∧ (∀ (k : ℕ) (t : C(Y, S)), (∑ i, z k t i) = (4 : ℕ) • push (((t.comp q).comp c).comp ⟨e.symm, e.symm.continuous⟩) (cmp d u)) ∧ (∀ (k : ℕ) (D : C(S, S)) (t : C(Y, S)) (i : Fin (p ^ k)), push D (z k t i) = z k (D.comp t) i) ∧ (∀ (k : ℕ) (t₀ t₁ : C(Y, S)), t₀.Homotopic t₁ → ∀ i, z k t₀ i = z k t₁ i) ∧ ∀ (k : ℕ), 0 < k → ∀ (U : Set (OnePoint W)) (β : OnePoint W → ZMod (p ^ k)), IsOpen U → U.Nonempty → OnePoint.infty ∉ U → (∀ g : PadicInt p, ∀ x ∈ U, g +ᵥ x ∈ U) → IsLocallyConstant (U.restrict β) → (∀ g : PadicInt p, ∀ x ∈ U, β (g +ᵥ x) = β x + PadicInt.toZModPow k g) → ∀ h : C(Y, S), (∃ b, ∀ y ∉ q '' U, h y = b) → ∀ i j, z k h i = z k h jhs304_character_latticeFor an odd-dimensional oriented local test, the sheaf/Witt theory supplies a fixed positive denominator L and a nonzero integer delta before k. Any one equivariant p^k-sheet region and a nonzero-degree postcomposition concentrated there give p^k equal rational parts with sum 4 delta and each L times a part integral.
∀ (p d : ℕ) [Fact p.Prime] (W : Set (EuclideanSpace ℝ (Fin d))), IsOpen W → IsConnected W → 3 ≤ d → Odd d → ∀ [AddAction (PadicInt p) (OnePoint W)] [ContinuousVAdd (PadicInt p) (OnePoint W)] [TopologicalSpace.MetrizableSpace (OnePoint W)], (∀ a : PadicInt p, a +ᵥ (OnePoint.infty : OnePoint W) = OnePoint.infty) → (∀ a : PadicInt p, ∃ h : W ≃ₜ W, ∀ x : W, a +ᵥ (x : OnePoint W) = (h (h x) : OnePoint W)) → ∀ (e : OnePoint (EuclideanSpace ℝ (Fin d)) ≃ₜ ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (d + 1))) 1)) (c : C(OnePoint (EuclideanSpace ℝ (Fin d)), OnePoint W)) (a : C(Quotient (AddAction.orbitRel (PadicInt p) (OnePoint W)), ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (d + 1))) 1))), c OnePoint.infty = OnePoint.infty → (∀ x : W, c ((x : EuclideanSpace ℝ (Fin d)) : OnePoint _) = (x : OnePoint W)) → (∀ x : EuclideanSpace ℝ (Fin d), x ∉ W → c (x : OnePoint _) = OnePoint.infty) → ((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).map (TopCat.ofHom (((a.comp (⟨Quotient.mk'', continuous_quotient_mk'⟩ : C(OnePoint W, Quotient (AddAction.orbitRel (PadicInt p) (OnePoint W))))).comp c).comp ⟨e.symm, e.symm.continuous⟩)) ≠ 0 → ∃ (L : ℕ) (δ : ℤ), 0 < L ∧ δ ≠ 0 ∧ ∀ (k : ℕ), 0 < k → ∀ (U : Set (OnePoint W)) (β : OnePoint W → ZMod (p ^ k)), IsOpen U → U.Nonempty → OnePoint.infty ∉ U → (∀ g : PadicInt p, ∀ x ∈ U, g +ᵥ x ∈ U) → IsLocallyConstant (U.restrict β) → (∀ g : PadicInt p, ∀ x ∈ U, β (g +ᵥ x) = β x + PadicInt.toZModPow k g) → ∀ (D : C(↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (d + 1))) 1), ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (d + 1))) 1))) (h : C(Quotient (AddAction.orbitRel (PadicInt p) (OnePoint W)), ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (d + 1))) 1))), ((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).map (TopCat.ofHom D) ≠ 0 → (D.comp a).Homotopic h → (∃ b, ∀ y ∉ (⟨Quotient.mk'', continuous_quotient_mk'⟩ : C(OnePoint W, Quotient (AddAction.orbitRel (PadicInt p) (OnePoint W)))) '' U, h y = b) → ∃ z : Fin (p ^ k) → ℚ, (∀ i, ∃ t : ℤ, (L : ℚ) * z i = t) ∧ (∑ i, z i) = 4 * (δ : ℚ) ∧ ∀ i j, z i = z jhs304_signature_coreAssuming supported-map transport and odd-sphere orbit-null descent, finite quotient sheets exclude a faithful continuous local p-adic action on a positive-dimensional connected open Euclidean set. The proved compactification, averaging and homotopy-extension library modules supply the other topological inputs; the remaining proof is the fixed-lattice/character-class argument of Sections 2-4 and 6 and the assembly of Section 5.
(∀ (d : ℕ) (W : Set (EuclideanSpace ℝ (Fin d))), IsOpen W → IsConnected W → ∀ (Z : Type) [TopologicalSpace Z] (P : C(EuclideanSpace ℝ (Fin d), Z)) (b : Z), (∀ x : EuclideanSpace ℝ (Fin d), 1 ≤ ‖x‖ → P x = b) → ∀ (z₀ z₁ : EuclideanSpace ℝ (Fin d)) (r₀ r₁ : ℝ), 0 < r₀ → 0 < r₁ → Metric.closedBall z₀ r₀ ⊆ W → Metric.closedBall z₁ r₁ ⊆ W → ∃ H : C(↥unitInterval × OnePoint W, Z), (∀ x : W, H (0, (x : OnePoint W)) = P (r₀⁻¹ • ((x : EuclideanSpace ℝ (Fin d)) - z₀))) ∧ (∀ x : W, H (1, (x : OnePoint W)) = P (r₁⁻¹ • ((x : EuclideanSpace ℝ (Fin d)) - z₁))) ∧ (∀ t : ↥unitInterval, H (t, OnePoint.infty) = b) ∧ ∃ K : Set W, IsCompact K ∧ ∀ (t : ↥unitInterval) (x : W), x ∉ K → H (t, (x : OnePoint W)) = b) → (∀ (p d : ℕ) [Fact p.Prime] (X : Type) [TopologicalSpace X] [CompactSpace X] [TopologicalSpace.MetrizableSpace X] [AddAction (PadicInt p) X] [ContinuousVAdd (PadicInt p) X], 3 ≤ d → Odd d → ∀ (v : C(Quotient (AddAction.orbitRel (PadicInt p) X), ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (d + 1))) 1))), (v.comp ⟨Quotient.mk'', continuous_quotient_mk'⟩).Nullhomotopic → ∃ D : C(↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (d + 1))) 1), ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (d + 1))) 1)), ((AlgebraicTopology.singularHomologyFunctor.{0} (ModuleCat.{0} ℤ) d).obj (ModuleCat.of.{0} ℤ ℤ)).map (TopCat.ofHom D) ≠ 0 ∧ (D.comp v).Nullhomotopic) → (∀ (p : ℕ) [Fact p.Prime] (W : Type) [TopologicalSpace W] [T2Space W] [AddAction (PadicInt p) W] [ContinuousVAdd (PadicInt p) W] [FaithfulVAdd (PadicInt p) W] (k : ℕ), ∃ (U : Set W) (β : W → ZMod (p ^ k)), IsOpen U ∧ U.Nonempty ∧ (∀ a : PadicInt p, ∀ x ∈ U, a +ᵥ x ∈ U) ∧ IsLocallyConstant (U.restrict β) ∧ ∀ a : PadicInt p, ∀ x ∈ U, β (a +ᵥ x) = β x + PadicInt.toZModPow k a) → ∀ (n p : ℕ) [Fact p.Prime] (O : Set (EuclideanSpace ℝ (Fin n))) (T : PadicInt p → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)), 1 ≤ n → IsOpen O → IsConnected O → (∀ a, Set.MapsTo (T a) O O) → (∀ x ∈ O, T 0 x = x) → (∀ a b, ∀ x ∈ O, T (a + b) x = T a (T b x)) → ContinuousOn (fun q : PadicInt p × EuclideanSpace ℝ (Fin n) => T q.1 q.2) (Set.univ ×ˢ O) → (∀ a : PadicInt p, a ≠ 0 → ∃ x ∈ O, T a x ≠ x) → Falsehs304_local_exclusionPaper Theorem 6.8 (thm:contradiction) for the local model of R2, with the orientation step of Prop 5.1 done inside (pass to the subgroup 2ℤ_p, which acts by orientation-preserving homeomorphisms because every element is a double; index 2 only for p = 2; the restricted action stays faithful). The proof is the whole signature machinery: §2 test categories T(X) and Witt groups E_r(X) = W_r(T(X)) with homotopy invariance (Thm 2.9), §3 cutoff/germs/Witt localization/dense doubling (Thm 3.3, 3.4, 3.6), §4 the fixed sphere lattice (Thm 4.7) and degree action (Prop 4.8), §5 the local tests (Lemmas 5.2–5.7, Prop 5.8; R3 supplies 5.2/5.3/5.6/5.7), §6 character classes and the equal-parts contradiction (Props 6.4–6.7, Thm 6.8). The frozen-type constraint: Mathlib has no D^b(Sh_ℝ(X)), Rf_*, f^!, Witt groups; DEC must state sub-obligations with Mathlib vocabulary only (see NOTES.md §5). Expected to stay at 1–2 levels in 72 h.
((∀ (K X : Type) [AddCommGroup K] [TopologicalSpace K] [IsTopologicalAddGroup K] [CompactSpace K] [T2Space K] [TopologicalSpace X] [CompactSpace X] [TopologicalSpace.MetrizableSpace X] [AddAction K X] [ContinuousVAdd K X] (d : ℕ) (f : C(X, ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (d + 1))) 1))), (∀ (a : K) (x : X), dist (f (a +ᵥ x) : EuclideanSpace ℝ (Fin (d + 1))) (f x : EuclideanSpace ℝ (Fin (d + 1))) < 1 / 2) → ∃ g : C(X, ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (d + 1))) 1)), (∀ (a : K) (x : X), g (a +ᵥ x) = g x) ∧ Nonempty (ContinuousMap.HomotopyRel f g {x : X | ∀ a : K, f (a +ᵥ x) = f x})) ∧ (∀ (Y : Type) [TopologicalSpace Y] [CompactSpace Y] [TopologicalSpace.MetrizableSpace Y] (F : Set Y), IsClosed F → ∀ (d : ℕ) (f : C(Y, ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (d + 1))) 1))) (H : C(↥unitInterval × ↥F, ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (d + 1))) 1))), (∀ y : ↥F, H (0, y) = f (y : Y)) → ∃ H' : C(↥unitInterval × Y, ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (d + 1))) 1)), (∀ y : Y, H' (0, y) = f y) ∧ ∀ (t : ↥unitInterval) (y : ↥F), H' (t, (y : Y)) = H (t, y)) ∧ (∀ (p : ℕ) [Fact p.Prime] (W : Type) [TopologicalSpace W] [T2Space W] [AddAction (PadicInt p) W] [ContinuousVAdd (PadicInt p) W] [FaithfulVAdd (PadicInt p) W] (k : ℕ), ∃ (U : Set W) (β : W → ZMod (p ^ k)), IsOpen U ∧ U.Nonempty ∧ (∀ (a : PadicInt p), ∀ x ∈ U, a +ᵥ x ∈ U) ∧ IsLocallyConstant (U.restrict β) ∧ ∀ (a : PadicInt p), ∀ x ∈ U, β (a +ᵥ x) = β x + PadicInt.toZModPow k a) ∧ (∀ (K X : Type) [AddGroup K] [TopologicalSpace K] [IsTopologicalAddGroup K] [CompactSpace K] [TopologicalSpace X] [CompactSpace X] [TopologicalSpace.MetrizableSpace X] [AddAction K X] [ContinuousVAdd K X], CompactSpace (Quotient (AddAction.orbitRel K X)) ∧ TopologicalSpace.MetrizableSpace (Quotient (AddAction.orbitRel K X)))) → ∀ (n p : ℕ) [Fact p.Prime] (O : Set (EuclideanSpace ℝ (Fin n))) (T : PadicInt p → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)), 1 ≤ n → IsOpen O → IsConnected O → (∀ a, Set.MapsTo (T a) O O) → (∀ x ∈ O, T 0 x = x) → (∀ a b, ∀ x ∈ O, T (a + b) x = T a (T b x)) → ContinuousOn (fun q : PadicInt p × EuclideanSpace ℝ (Fin n) => T q.1 q.2) (Set.univ ×ˢ O) → (∀ a : PadicInt p, a ≠ 0 → ∃ x ∈ O, T a x ≠ x) → Falseimport ChallengeDeps
open scoped Manifold ContDiff
/-- Theorem 1.1 (the Hilbert–Smith conjecture): a locally compact second-countable Hausdorff
group acting faithfully and jointly continuously on a connected Hausdorff second-countable
topological `n`-manifold without boundary, `n ≥ 1`, is a Lie group. -/
theorem hilbert_smith {G M : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[LocallyCompactSpace G] [SecondCountableTopology G] [T2Space G]
(n : ℕ) (hn : 1 ≤ n) [TopologicalSpace M] [T2Space M] [SecondCountableTopology M]
[ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M]
[MulAction G M] [ContinuousSMul G M] [FaithfulSMul G M] :
∃ (k : ℕ) (_ : ChartedSpace (EuclideanSpace ℝ (Fin k)) G),
LieGroup 𝓘(ℝ, EuclideanSpace ℝ (Fin k)) ∞ G := by
sorry
LOT always checks the root, the problem’s own theorem, with the unmodified official pipeline from scratch, as Lean-Eval does. As a what-if we also checked the root once as an ordinary node with all of LOT’s optimizations, under the same premise as above: everything below it already proved and pre-checked.LOT 对根（题目本身的定理）总是用未改动的官方流程从头检查，与 Lean-Eval 一致。作为假设对比，我们还把根当作普通节点、打开 LOT 全部优化检查了一次，前提与上文相同：它下面的一切都已证明并做过预检查。
The official root check was not run on the isolated cores here; its bar is hatched and its time is an estimate: the tree's own official root check (check.sh root, from scratch, serial), 57,814 s, measured by the tree on its root worker, not on the isolated 8 cores used here; not rescaled.官方根检查没有在这里的独占核上运行；它的色条用斜线画出，时间是估计值：the tree's own official root check (check.sh root, from scratch, serial), 57,814 s, measured by the tree on its root worker, not on the isolated 8 cores used here; not rescaled。
≈ 162.26× faster. Each bar spans its own run (colours as in the legend above). Not inside the LOT time, and listed here: the root’s probe build (177 s), done ahead of time while the last levels were checked, and the ledger of 141,538 constants learned from the chain’s own checks.约快 162.26 倍。每条色条对应各自那次运行（颜色同上方图例）。不计入 LOT 用时、在此单独列出的有：根的探测编译（177 秒），在检查最后几层时就已提前完成；以及从这条链自己的检查里学到的 141,538 个常量的账本。
hilbert_smith : {G M : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] [T2Space G] (n : ℕ) (hn : 1 ≤ n) [TopologicalSpace M] [T2Space M] [SecondCountableTopology M] [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [MulAction G M] [ContinuousSMul G M] [FaithfulSMul G M] : ∃ (k : ℕ) (_ : ChartedSpace (EuclideanSpace ℝ (Fin k)) G), LieGroup (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin k))) ((⊤ : ℕ∞) : WithTop ℕ∞) G| Configuration配置 | Wall clock (min)用时（分钟） | CPU-hours used实际 CPU 小时 |
|---|---|---|
| Lean's original pipelineLean 原始流程 (estimated, not run)（估计，未实际运行） | ≈ 8386.0 | – |
| LOT’s infrastructure (all six optimizations)LOT 基础设施（6 项优化全开） | 77.9 | 17.077 |
| As it ran in the proved tree (that day’s pipeline, queueing included)证明树当时实际用时（当时的流程，含排队） | 609.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。