{"id":"db3878bd-1f50-4ad4-96bf-0c66a015bc8a","arxiv_id":"2412.16759","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Using six-functor sheaf theory, the Bauer-Furuta invariant is defined as the proper pushforward f_* f^!(1), with f^!(1) computed as the Thom spectrum of the family index.","lead":"This paper builds the Bauer-Furuta invariant, a stable homotopy invariant of 4-manifolds, in a coordinate-free way using sheaves of spectra instead of finite-dimensional approximations. The approach gives a canonical map for single manifolds and for families, and sketches how to add Lie group equivariance.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Linearization hypothesis is proven only under an unadvertised compact-difference condition; without it the straight-line homotopy can leave the Fredholm operators, so Summary 1.1(4) overreaches.","rationale":"The reader's weakest assumption correctly targets the linearization step. My stress-test sharpens that concern: the issue is not only local constancy along [0,1] but the prior requirement that the straight-line homotopy φ has Fredholm differentials. This requirement is guaranteed by the compact-difference condition, which the proof states but the summary and corollary statements omit. Since the Seiberg–Witten map satisfies the condition, the non-equivariant construction for the intended application is defensible, so the reader's CONDITIONAL verdict remains appropriate. The equivariant incompleteness is also a genuine limitation, but the paper explicitly warns it is an outline, making it less of a hidden defect. The most load-bearing concern for the paper's advertised generality is the linearization overreach, and the concrete test above demonstrates why the extra condition is indispensable.","tokens_in":27914,"tokens_out":42938,"duration_ms":363723,"concrete_test":"On ℓ^2, take A=I and B=I-2P, where P is an orthogonal projection with infinite rank and infinite corank. Both A and B are Fredholm (in fact invertible), but A-B=2P is non-compact. The straight-line path T_t=(1-t)A+tB = I-2tP is not Fredholm at t=1/2, since its kernel is im P, which is infinite-dimensional. This confirms the Fredholm region is not convex and shows that the compact-difference condition in Construction 2.1.11 is not merely technical. To settle the concern directly, attempt to re-derive the isomorphism f^!(1)≃(df)^!(1) for a C^1 Fredholm map whose differentials at two points are A and B but whose difference is non-compact; if no alternative argument is supplied, the statements of Summary 1.1(4) and Corollary 2.1.12 must be revised to include the compact-difference hypothesis.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's headline Summary 1.1(4) and Corollary 2.1.12 state the linearization hypothesis for every C^1-differentiable map with Fredholm differentials: f^!(1) ≃ (df)^!(1) ≃ Th(ind(df)). However, the proof in Construction 2.1.11 requires an additional hypothesis, introduced only as 'assume further for simplicity that any differentials at two distinct points differ only by a compact linear operator.' Without this condition, the straight-line homotopy φ(t,x,v)=(t,(1-t)f(v)+t(d_x f)v) need not have Fredholm vertical differentials: the path (1-t)d_v f + t d_x f between two Fredholm operators can leave the open subset of Fredholm operators, because that subset is not convex. Thus the linearization argument, and hence the identification of the Bauer–Furuta domain with Th(ind(df)), is established only under the compact-difference condition. The condition does hold for the Seiberg–Witten map (f=l+c with c compact), so the intended application survives, but the prominently stated general linearization hypothesis is not proven. This is a scope gap rather than an internal contradiction, and it should be explicitly reflected in the abstract and summary statements.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a new, canonical construction of the Bauer–Furuta invariant using the six-functor formalism for sheaves of spectra on topological spaces. The invariant is defined as the counit map r_* f^!(1) -> q_*(1) associated to a proper C^1 Fredholm map f between Banach bundles over a base S, avoiding finite-dimensional approximations. The non-equivariant section proves that such Fredholm maps are locally proper, identifies f^!(1) with the Thom spectrum sheaf of the Atiyah–Singer families index under a linearization hypothesis, develops purity results, and gives a comparison with the classical finite-dimensional approximation of Bauer and Furuta. Section 3 outlines a genuine equivariant analogue based on an axiomatically assumed site of G-smooth maps and defines a candidate genuine equivariant Bauer–Furuta map. Appendices contain the six-functor formalism for locally proper maps and the relevant Banach manifold facts.","tokens_in":28190,"tokens_out":12297,"duration_ms":111561,"significance":"If the main construction is correct, this is a valuable conceptual advance: it gives a coordinate-free, pullback-stable definition of the Bauer–Furuta invariant and a clean explanation of the appearance of the index Thom spectrum. The paper has real strengths: the local factorization of Fredholm maps (Lemma 2.1.6) and local properness (Corollary 2.1.7) are proved directly; the identification with the Atiyah–Singer index is explained in Remark 2.1.9; and a comparison to finite-dimensional approximations is attempted in Theorem 2.3.1. The approach contains no fitted parameters and does not assume the target theorem. At the same time, the general linearization hypothesis of Summary 1.1(4) is only proved under a compact-difference condition, and the genuine equivariant part of Section 3 is conditional on an unconstructed site. The intended Seiberg–Witten application is likely unaffected, but the advertised generality is not yet justified.","major_comments":[{"comment":"The linearization hypothesis is proved only under an additional compact-difference condition that is introduced without emphasis. Immediately before defining the deformation phi(t,x,v) = (t, (1-t)f(v)+t(d_x f)v), the text says 'assume further for simplicity that any differentials at two distinct points differ only by a compact linear operator.' This hypothesis is essential: the vertical differential of phi is (1-t)d_v f + t d_x f, and the locus of Fredholm operators is open but not convex, so without the compact-difference assumption this path can leave the Fredholm locus. Consequently Summary 1.1(4) and Corollary 2.1.12, which state the identification f^!(1) ≃ (df)^!(1) ≃ Th(ind(df)) for every C^1 map with Fredholm differentials, are not proven as stated. The paper should either prove local constancy of phi^!(1) without the compact-difference assumption or explicitly restrict the statements to maps whose differentials differ by compact operators. The Seiberg–Witten application, where f = l + c with c compact, survives, but the general formulation overreaches.","section":"Construction 2.1.11 / Summary 1.1(4) / Corollary 2.1.12"},{"comment":"The genuine equivariant six-functor formalism is not actually constructed. Definition 3.2.1 merely 'fixes' a collection of G-smooth maps satisfying axioms (1)–(6), and the text states that the 'precise definition will not be needed in the following arguments.' No concrete site is built, and no proof is given that any nonempty collection satisfying all six axioms exists. As a result, SH^G_top(X) in Definition 3.2.6 and the genuine equivariant Bauer–Furuta map in Construction 3.2.7 are defined relative to an unverified axiom. The introduction's warning that this part is only an outline is appropriate, but the body should not present Construction 3.2.7 as a definition without either a concrete construction of the site or an explicit statement that the result is conditional. As written, Section 3 does not establish the existence of the genuine equivariant Bauer–Furuta invariant.","section":"Section 3.2, Definition 3.2.1 and Construction 3.2.7"}],"minor_comments":[{"comment":"The notation p is overloaded within the construction: it denotes both the projection L ×_S L -> L and the projection L ×_S Y -> L. Please use distinct letters or explicitly qualify each occurrence.","section":"Section 2.1, Construction 2.1.11"},{"comment":"The proof is quite compressed. In particular, the conclusion 'by pullback-stability ... BF_{g'_{N''}} ≃ BF_{g_{N'}}' is stated without a diagram verifying the relevant cartesian square, and the 'purity triangles' later in the proof are not drawn. Adding these diagrams would make the zig-zag argument auditable.","section":"Theorem 2.3.1, proof"},{"comment":"There is a typo in the proof: 'The fist claim' should read 'The first claim'.","section":"Corollary 2.1.12, proof"},{"comment":"The induction notation ind^G_K(S) and ind^G_H(S) is not defined. A one-sentence explanation or a reference to the proper equivariant homotopy theory convention would help the reader.","section":"Definition 3.2.1(5)"}],"recommendation":"major_revision","confidential_remarks":"The non-equivariant contribution is potentially solid and valuable, and the linearization gap is fixable by restating the results with the compact-difference hypothesis. Section 3, however, is closer to a research announcement than a developed theory; if the paper is accepted, the editor may want the authors to present Section 3 explicitly as a conditional outline or to move it to a 'prospectus' section. The abstract's phrase 'family version' should also be qualified to the topological-base setting, since the stacky gauge-equivariant families are deferred to future work."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"I read it. The genuine contribution is the non-equivariant part: defining the Bauer–Furuta map as the counit r_* f^!(1) → q_* (1) on sheaves of spectra, bypassing finite-dimensional approximations. That is a real reformulation, not cosmetic. The author works out the local factorization for C^1 Fredholm maps, proves local properness, builds the six-functor formalism for separated locally proper maps between non-compact spaces, and then shows in Theorem 2.3.1 that the construction agrees with the classical BF map in the Seiberg–Witten setting. That comparison is the load-bearing evidence. The appendix is substantial; extending shriek functors from locally compact spaces to locally proper Banach-bundle maps is a useful service in itself.\n\nThe soft spot is exactly where the stress-test note lands. Summary 1.1(4) and the abstract state the linearization hypothesis for every C^1 Fredholm map: f^!(1) ≃ (df)^!(1) ≃ Th(ind(df)). But Construction 2.1.11 needs the extra assumption that differentials at distinct points differ by a compact operator. That is not a technicality: the straight-line homotopy φ(t,v) = (1−t)f(v) + t(d_x f)v has Fredholm differentials only when the path stays in the Fredholm locus, and that locus is open but not convex. Without the compact-difference condition the path can leave it. So the full-strength linearization claim is unproved. The intended application survives, since the Seiberg–Witten map is f = l + c with c compact, and Corollary 2.1.12 is careful enough because it points back to Construction 2.1.11. But the summary and abstract overreach. That is a scope gap, not an internal contradiction, and it is fixable by restating the hypothesis in the bold claims.\n\nThe equivariant section is honestly labeled as an outline. There is no concrete G-smooth site, and the author says so. The abstract's word “accommodates” is doing more work than the proof supports, but this is a stated limitation, not a hidden one. I would not count it against the paper's integrity, just against its completeness.\n\nThe citation pattern is normal and the mathematical style is careful. No fitting, no circularity. This paper deserves a serious referee. I would send it out and ask the author to (1) put the compact-difference condition into the abstract and Summary 1.1(4), and (2) clearly separate the speculative equivariant part from the proven non-equivariant claims.","headline":"The non-equivariant six-functor construction of Bauer–Furuta is real and mostly solid, but the advertised linearization theorem is proven only under an extra compact-difference condition that the summary omits.","tokens_in":28710,"tokens_out":3525,"would_cite":true,"duration_ms":31353,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["55P42","19K56","58B15"],"pacs":[],"model":"deepseek-v4-flash","headline":"Bauer–Furuta invariants, including their family version, can be defined canonically as a counit of a proper pushforward on sheaves of spectra, with no finite-dimensional approximation.","keywords":["Bauer–Furuta invariant","sheaves of spectra","six-functor formalism","Fredholm maps","Thom spectrum sheaf","Atiyah–Singer families index","Borel–Moore homology","equivariant stable homotopy theory"],"falsifier":"Take a C$^1$ Fredholm map $f\\colon H'\\to H$ of the form $l+c$ with $l$ Fredholm and $c$ compact, and compute $f^!(1)$ and $\\operatorname{Th}(\\operatorname{ind}(df))$ over a base that is a circle; a single loop where the two Thom-spectrum sheaves disagree would falsify Corollary 2.1.12. A more direct check is to test whether the vertical differential of $\\varphi(t,x,v)=(t,(1-t)f(v)+t(d_x f)v)$ is Fredholm for every $t$, since a non-Fredholm point would break the constancy argument of Lemma B.5.6.","tokens_in":27672,"feed_emoji":"📐","tokens_out":10172,"duration_ms":82530,"temperature":0.7,"pith_summary":"The paper proposes a new, coordinate-free definition of the Bauer–Furuta invariant of a closed spin-c 4-manifold, together with its family version, using the six-functor formalism for sheaves of spectra on topological spaces. The invariant is the counit map $r_* f^!(1) \\to q_*(1)$ associated to a C$^1$ Fredholm map $f\\colon L\\to Y$ over a base $S$, where $f^!(1)$ is the dualizing sheaf computed by shriek functors. The key technical observation is that C$^1$-differentiable Fredholm maps between Banach manifolds are locally proper, which makes the shriek functors available even though the spaces are not locally compact. The paper then identifies $f^!(1)$ with the Thom spectrum sheaf $\\operatorname{Th}(\\operatorname{ind}(df))$ of the Atiyah–Singer families index, and proves that this construction agrees with the classical finite-dimensional approximation. If correct, the classical invariant and its family version are reproduced by one canonical formula, with functoriality and independence from choices built in.","feed_headline":"Bauer–Furuta invariant rebuilt, no finite-dimensional approximations","feed_subtitle":"C1 Fredholm maps are locally proper, so the invariant is a canonical pushforward of index Thom spectra.","key_machinery":"The central object is the six-functor formalism for sheaves of spectra on topological spaces, extended from locally compact Hausdorff spaces to separated locally proper maps. The mechanism that carries the argument is the shriek functor $f^!$ for a locally proper Fredholm map, together with the factorization of a C$^1$ Fredholm map locally as a zero-section followed by a cohomologically smooth map (Lemma 2.1.6). The load-bearing identity is $f^!(1)\\simeq \\operatorname{Th}(\\operatorname{ind}(df))$, proved via the straight-line homotopy $\\varphi$ and the constancy lemma (Lemma B.5.6) for locally constant sheaves along Banach bundles. The Thom spectrum sheaf $\\operatorname{Th}(V)=q_*q^!(1)$ is the coordinate-free replacement for the sphere $S^{\\operatorname{ind}(df)}$.","core_discovery":"On the paper's own terms, the Bauer–Furuta map is not an invariant built from large finite-dimensional subspaces but the counit of a proper pushforward: for $f\\colon L\\to Y$ proper over $S$, set $\\mathrm{BF}_f = q_*(\\mathrm{counit}) \\colon r_* f^!(1) \\to q_*(1)$ in sheaves of spectra. The central statement is the linearization hypothesis: for a C$^1$ Fredholm map whose differentials differ by compact operators, $f^!(1)\\simeq (df)^!(1)\\simeq \\operatorname{Th}(\\operatorname{ind}(df))$, where $\\operatorname{Th}(\\operatorname{ind}(df))$ is the Thom spectrum sheaf of the families index; this is obtained by deforming $f$ to $df$ through $\\varphi(t,x,v)=(t,(1-t)f(v)+t(d_x f)v)$. The same six-functor framework yields a comparison theorem identifying the new map with the classical finite-dimensional approximation, and a family version over arbitrary bases. For group actions, the paper outlines a genuine equivariant formalism based on a G-smooth site and defines the equivariant Bauer–Furuta map by the same counit formula in a category $\\mathrm{SH}^G_{\\mathrm{top}}$.","pith_inferences":["The paper leaves implicit that the counit definition makes the Bauer–Furuta invariant a plausible building block for a fully extended topological field theory in four dimensions; the six-functor language is local and base-change stable, which is what such a structure would need.","The linearization principle suggests a general recipe for other nonlinear Fredholm problems: whenever a map is C$^1$ with differentials differing by compact operators, the shriek of the unit should be the index Thom sheaf; this could be tested on Floer-type or other gauge-theoretic equations beyond Seiberg–Witten.","The removal of excision from the construction, noted in Remark 1.2, opens a plausible route to a motivic lift of the invariant, because proper pushforward is available in motivic settings where arbitrary open excision is not; the paper only raises this as a hope.","The equivariant formalism's viability hinges on finding a genuine G-smooth site; a natural test is whether the smallest class satisfying Definition 3.2.1 provably yields proper basechange and correctly computes the Pin(2)-equivariant Seiberg–Witten map."],"forward_implications":["The family Bauer–Furuta invariant is defined by the same counit formula over arbitrary bases, including noncompact and non-CW bases, where finite-dimensional approximations were impractical.","The invariant is pullback-stable, and over contractible bases it is independent of perturbations, because the purity construction (2.2.3) reduces it to the proper pushforward along the moduli projection.","Choosing a section of $L\\to S$ recovers the classical sphere map $S^{\\operatorname{ind}(d_x f)}\\to S$ inside locally constant sheaves, showing that the appearance of the index sphere is a coordinate artifact.","Theorem 2.3.1 shows the new map is homotopic to the finite-dimensional approximation of the classical construction, so the classical invariant is a special case.","The genuine equivariant version is defined by the same counit formula once a concrete G-smooth site satisfying Definition 3.2.1 is supplied."],"supporting_citations":[{"why":"supplies the six-functor formalism argument used in Theorem B.4.1 to extend shriek functors to separated locally proper maps.","marker":"[Man22]"},{"why":"provides shriek functors for separated locally proper maps, the base theory the paper adapts to Fredholm maps between Banach spaces.","marker":"[SS16]"},{"why":"gives the six-functor formalism for locally compact Hausdorff spaces underlying the Poincaré duality and purity computations.","marker":"[Vol23]"},{"why":"introduces the Seiberg–Witten proper map and the lemma on bounded preimages used to get properness.","marker":"[Fur01]"},{"why":"defines the classical finite-dimensional approximation of the Bauer–Furuta invariant that Theorem 2.3.1 compares against.","marker":"[BF04]"},{"why":"defines sheaves of spectra and supplies the foundational six-operation facts used throughout.","marker":"[Lur09]"},{"why":"supplies A1-homotopy invariance and the monodromy equivalence used in Corollary B.5.7 and Theorem B.5.8.","marker":"[Lur17]"},{"why":"supplies the proper morphism theory of ∞-topoi used in the proper basechange theorem.","marker":"[MW24]"}],"fun_headline_variants":["Bauer–Furuta invariant via six-functors, no finite-dim steps","C1 Fredholm maps make Bauer–Furuta fully canonical","Six-functor formalism yields family and equivariant Bauer–Furuta","Bauer–Furuta via shriek functors, no finite-dim approximation","Bauer–Furuta as counit of proper pushforward"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The argument depends on the straight-line deformation from a map to its derivative staying in the class of Fredholm maps, so that the associated shriek sheaf is locally constant along the deformation; if local constancy fails over infinite-dimensional Banach bundles, the central identification with the index Thom spectrum collapses, and the equivariant part additionally presupposes a concrete G-smooth site satisfying Definition 3.2.1.","fun_headline_variants_meta":{"raw":{"variants":["Bauer–Furuta invariant via six-functors, no finite-dim steps","C1 Fredholm maps make Bauer–Furuta fully canonical","Six-functor formalism yields family and equivariant Bauer–Furuta","Bauer–Furuta via shriek functors, no finite-dim approximation","Bauer–Furuta as counit of proper pushforward"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001432,"raw_usage":{"total_tokens":5786,"prompt_tokens":970,"completion_tokens":4816,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":586,"completion_tokens_details":{"reasoning_tokens":4716}},"tokens_in":586,"tokens_out":4816,"duration_ms":31499,"temperature":1.0,"reasoning_tokens":4716,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T10:15:18.147047+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a C$^1$ Fredholm map $f\\colon H'\\to H$ of the form $l+c$ with $l$ Fredholm and $c$ compact, and compute $f^!(1)$ and $\\operatorname{Th}(\\operatorname{ind}(df))$ over a base that is a circle; a single loop where the two Thom-spectrum sheaves disagree would falsify Corollary 2.1.12. A more direct check is to test whether the vertical differential of $\\varphi(t,x,v)=(t,(1-t)f(v)+t(d_x f)v)$ is Fredholm for every $t$, since a non-Fredholm point would break the constancy argument of Lemma B.5.6.","supporting_citations":[],"review_version":1}