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 128 GiB locked for it: once with Lean’s original pipeline and once with LOT’s infrastructure, all five optimizations on. Both runs accepted every level.LOT 证这道题时，有一条 12 层的中间定理链同时收口：每一层都由下一层推出。我们把这条链检查了两遍，每一遍单独运行，独占锁定 8 个完整 CPU 核（16 个逻辑 CPU）和 128 GiB 内存：一遍用 Lean 原始流程，一遍用 LOT 基础设施（5 项优化全开）。两遍都接受了每一层。
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 five 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 optimization, which acts across a whole tree, has 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 基础设施（5 项优化全开）：最新流程检查同一条链的总用时，先做一次复用下一层编译产物的探测编译，再用并行内核重放把整条链一次查完。在这次单独回放里，账本虽然开着但从空开始；排队这一项是在整棵树的层面起作用的，这里没有可以重叠的东西。两个时间都不含根检查、排队等待和调度器的停顿。这条链不一定是这棵树里最长的：它是一次“收口”，即最底层定理证完后，上面各层依次变得可检查；挑选时兼顾规模和多样性。
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 run reached the 12-hour cap; its lane shows the progress made by then, and the rest is estimated: level 1 ran to the end (42035 s, measured); level 2 was stopped at the 12 h cut after 1193 s, in its solution_build stage (1106 s in it, Lake at 9964/10072); its remainder, 10410 s, is the rest of that stage (1451 s, at least 0) plus the later stages (8960 s): level 1's measured run (42035 s)'s stages times 0.274 (the build had compiled 860 of the 1988 Submission modules in the import closure in 1106 s (whole build ~2556 s, linear)); levels 3-12 not started (the 12 h of timeline were used up): each estimated as level 1's time (42035 s, measured) times the square root of the import-closure ratio (L3 1999, L4 2001, L5 2002, L6 2003, L7 2006, L8 2007, L9 2011, L10 2015, L11 2027, L12 2473 vs 1987 Submission modules; time ~ sqrt(closure): on the seven finished examples' original runs, median error 7% per level, -39%..+30%). The 12 h are displayed timeline: the levels' measured durations inside their containers, one after another原始流程跑满 12 小时被截止；这一条画的是截止时的实际进度，剩余部分为估计：level 1 ran to the end (42035 s, measured); level 2 was stopped at the 12 h cut after 1193 s, in its solution_build stage (1106 s in it, Lake at 9964/10072); its remainder, 10410 s, is the rest of that stage (1451 s, at least 0) plus the later stages (8960 s): level 1's measured run (42035 s)'s stages times 0.274 (the build had compiled 860 of the 1988 Submission modules in the import closure in 1106 s (whole build ~2556 s, linear)); levels 3-12 not started (the 12 h of timeline were used up): each estimated as level 1's time (42035 s, measured) times the square root of the import-closure ratio (L3 1999, L4 2001, L5 2002, L6 2003, L7 2006, L8 2007, L9 2011, L10 2015, L11 2027, L12 2473 vs 1987 Submission modules; time ~ sqrt(closure): on the seven finished examples' original runs, median error 7% per level, -39%..+30%). The 12 h are displayed timeline: the levels' measured durations inside their containers, one after another
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
The root is the problem’s own theorem. Since LOT 4.5 a new tree checks it like the other nodes, with LOT’s optimizations: the fast root check makes the same comparison as the official check, but reuses the build of the root commit and runs with the ledger and the parallel kernel replay. The official check from scratch then runs once more after the proof as the final check of record, outside the tree’s time. Both are shown here, under the same premise as above (everything below the root already proved and pre-checked).根就是题目本身的定理。从 LOT 4.5 起，新树像检查其他节点一样、打开 LOT 的优化检查根：快速根检查做的比对与官方检查相同，只是复用根提交的编译产物，并使用账本和并行内核重放。证完之后，再用官方流程从头做一次终检，作为最终结论，不计入树的用时。下面两种都列出，前提与上文相同（根下面的一切都已证明并做过预检查）。
The official root check ran alone for 12 hours on the isolated cores and was stopped there; the coloured part of its bar is what it did by then, the empty part the estimated remainder: run for 12 h and stopped, in its lean stage (18229 s in it); the remainder, 9485 s, is the rest of that stage (9485 s, at least 0) plus the later stages (0 s): level 1's original run (measured to its end), its stages times 0.929 (its nanoda stage took 2475 s against the reference's 2663 s).官方根检查在独占核上单独跑了 12 小时后截止；色条有颜色的部分是截止时实际完成的，空白部分是估计的剩余：run for 12 h and stopped, in its lean stage (18229 s in it); the remainder, 9485 s, is the rest of that stage (9485 s, at least 0) plus the later stages (0 s): level 1's original run (measured to its end), its stages times 0.929 (its nanoda stage took 2475 s against the reference's 2663 s)。
≈ 86.84× 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.约快 86.84 倍。每条色条对应各自那次运行（颜色同上方图例）。不计入 LOT 用时、在此单独列出的有：根的探测编译（177 秒），在检查最后几层时就已提前完成；以及从这条链自己的检查里学到的 141,538 个常量的账本。
| Configuration配置 | Wall clock (min)用时（分钟） | CPU-hours used实际 CPU 小时 |
|---|---|---|
| Lean's original pipelineLean 原始流程 (12 h measured, rest estimated)（实测 12 小时，其余估计） | ≈ 8013.9 | 27.879 (12 h) |
| LOT’s infrastructure (all five optimizations)LOT 基础设施（5 项优化全开） | 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 128 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，含超线程）和 128 GiB 内存，运行期间独占锁定，其他进程用不了这些 CPU；断网，所有工具和库只读挂载；Lean leanprover/lean4:v4.35.0-rc3。原始流程是未经改动的官方检查器[3,4]，每层运行一次；两条泳道都不计排队等待和层与层之间调度器的停顿。测于 2026-10-24。