{"id":"15da4ab4-c7af-445f-b762-4ba3cf531ad3","arxiv_id":"2411.18186","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"The natural morphism from the henselisation of the valuation ring to the henselisation of the discrete valued field is an isomorphism, proved constructively.","lead":"This note proves, constructively, that two standard ways of building the henselisation of a valued field, one from the valuation ring and one from the valued field, give isomorphic rings. It supplies the first proof of an isomorphism that earlier literature treated as obvious.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Surjectivity of Theorem 1 hinges on an under-justified step: from δ^m η being a v-isolated zero, the paper asserts δ^m η lies in a ring Vu ⊆ Vh, without proving that the explicit isolated zero belongs to an elementary henselisation ring or to the integrally closed V[δ].","rationale":"The reader's verdict is CONDITIONAL, and my stress-test supports that condition rather than moving to a different verdict. The reader identified Lemma 4 as the weakest assumption because it is imported from Kuhlmann-Lombardi 2000 without reproof. I agree that this is a real dependency, but I think the more precise weak point is the passage from 'δ^m η is a v-isolated zero' to 'δ^m η ∈ Vh'. Lemma 4 supplies only the existence of a polynomial Q with an isolated root; it does not by itself place that root in the henselisation Vh. The paper's one-sentence assertion 'It shows that δ^m η is in the image of a certain Vu ⊆ Vh' compresses two nontrivial facts: the explicit form of an isolated zero from Kuhlmann-Lombardi 2000 Prop. 2.2, and the identification of V[δ'] with the valuation ring of K[δ'], which rests on the integral closedness results proved in the appendices. Neither is spelled out in the main proof, and the appendices are not referenced at that point. The concern is not that the statement is false; indeed Lemma 4 admits a short direct proof via valuation comparison of conjugates, and the integral closedness of Vf can be used to identify V[δ'] with the valuation ring. But the paper as written leaves a genuine gap in the central argument. I give credit for the injectivity proof, which is careful and self-contained once the appendices are accepted, and for the appendices themselves, which contain nontrivial correct-looking proofs of the normality of Vf. The concern is therefore about completeness and verifiability of the surjectivity step, not about an internal contradiction. The recommendation remains CONDITIONAL: the authors should add the missing proof of Lemma 4 and spell out the inference from isolated zero to containment in Vh, or, failing that, supply a precise reference with the necessary statements and show how the denominator issue and the valuation-ring identification are resolved. Since the reader already asked for conditions, my pass does not change the verdict.","tokens_in":8860,"tokens_out":28285,"duration_ms":247881,"concrete_test":"Write out the omitted proof of Lemma 4: for η ∈ K[δ], let η_i be the conjugates under K-embeddings; since v(δ_i)>0 for i≥2, choose m with v(δ_i^m η_i) > v(η) for all i≥2, so α = δ^m η has strictly minimal valuation among its conjugates. Take the minimal polynomial of α over K, multiply by a common denominator c ∈ V to obtain Q ∈ V[T]; then α is a v-isolated zero of Q. Next, verify the subsequent hop: using Kuhlmann-Lombardi 2000 Prop. 2.2, write α either as an element of K or as (aδ'+b)/(cδ'+d), and prove explicitly that this element lies in Vh. In the fractional-linear case, show either that cδ'+d is a unit in Vh or that the fraction simplifies into V[δ'] by invoking Lemma 12 (Vf integrally closed) and the fact that V[δ'] is then the valuation ring of K[δ'].","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is Theorem 1, and the surjectivity half is the delicate part. The proof takes η ∈ K[μ] with v(η) ≥ 0 and uses Lemma 4 to obtain m such that α := δ^m η is a v-isolated zero of some Q ∈ V[X]. The paper then says that Lemma 4 'shows that δ^m η is in the image of a certain Vu ⊆ Vh'. This inference is not demonstrated. Lemma 4 as stated only gives the existence of Q with an isolated-slope root; it does not by itself place α in any particular subring of the henselisation. To conclude α ∈ Vh one must either (i) invoke the explicit description of isolated zeros from Kuhlmann-Lombardi 2000, Prop. 2.2 — namely α ∈ K or α = (aδ'+b)/(cδ'+d) with δ' a special zero in Vh — and then show the denominator is a unit in Vh or that the fraction is in V[δ'], or (ii) prove V[δ'] equals the valuation ring of K[δ'] using the integral closedness of Vf from Appendix 2 (Lemma 12). Neither step is written out, and both are nontrivial: the denominator cδ'+d can be a nonunit even when v(α) ≥ 0, and the identification of V[δ'] with the valuation ring requires the finite extension to have a unique valuation, a fact not explicitly stated or verified constructively. Moreover, Lemma 4 itself is cited rather than proved; a short proof by comparing valuations of conjugates is available, but the paper does not supply it. If this chain cannot be completed, the surjectivity of ϕ is not established and the isomorphism claim is unproven.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper compares two constructive henselisations of a discrete valued field (K,V): the henselisation Vh of the residually discrete local ring V, built in Alonso García–Lombardi–Perdry 2008, and the valuation ring VH of the henselised field KH, built in Kuhlmann–Lombardi 2000. Theorem 1 asserts that the canonical local morphism of V-algebras φ: Vh → VH is an isomorphism, and that the proof is valid both in Bishop-style constructive mathematics and classically. Injectivity is shown by reducing to elementary steps and using a characteristic-polynomial zero test; surjectivity is reduced to showing that every element of VH with nonnegative valuation lies in Vh, using Lemma 4 on v-isolated zeros. Three appendices give constructive proofs of integral closedness of the rings Vf, based on Tate's formula.","tokens_in":9244,"tokens_out":13447,"duration_ms":121350,"significance":"If the proof is completed, the paper would fill a real gap: the identification of the two henselisations is usually taken as obvious in the literature, and the authors provide a constructive proof rather than a classical existence argument. The appendices contain useful and apparently correct constructive tools, in particular Tate's lemma and the proof that the localised rings Vf are integrally closed. The paper does not claim machine-checked proofs, but it does give explicit constructive arguments for the integral-closedness side. The main theorem is natural and likely true; however, the surjectivity argument as written leaves a load-bearing inference unjustified, so the paper is not yet ready for publication without revision.","major_comments":[{"comment":"The sentence 'It shows that δ^mη is in the image of a certain Vu ⊆ Vh' is not a consequence of Lemma 4 as stated. Lemma 4 only gives that α := δ^mη is a v-isolated zero of some Q ∈ V[X]. To conclude α ∈ Vh one must use the explicit description of v-isolated zeros quoted from Kuhlmann–Lombardi 2000, Proposition 2.2: either α ∈ K (then v(α) ≥ 0 gives α ∈ V), or α = (aδ'+b)/(cδ'+d) with δ' a special zero. In the second case the note does not prove that the fraction belongs to the elementary henselisation ring Vu obtained by adjoining δ': it is not shown that cδ'+d is a unit in Vu, nor that the alternative route via the integral closedness of V[δ'] (Lemma 12) applies, which would require proving that V[δ'] is the valuation ring of K[δ'] (i.e., uniqueness of the valuation extension). Since this step is exactly what completes the surjectivity of φ, the proof is incomplete as written.","section":"Proof of Theorem 1, Surjectivity"},{"comment":"Lemma 4 is load-bearing for Theorem 1, but its proof is reduced to a citation: 'Result given in Kuhlmann and Lombardi 2000, proof of proposition 2.3.' The note should either reproduce the proof (the comparison of valuations of conjugates mentioned in the surrounding text is short and would fit in a note) or quote the precise statement from the cited paper and explain exactly how it yields the assertion. As it stands, the main theorem depends on an unstated proof in another paper, and this dependence is not merely cosmetic: the step from 'δ^mη is a v-isolated zero' to 'δ^mη lies in the image of some Vu' is the delicate part of the surjectivity proof and needs to be visible.","section":"Equality to 0 in the henselisation of a discrete valued field, Lemma 4"}],"minor_comments":[{"comment":"In the paragraph after the definition of the special polynomial, the sentence 'The µ′_i for i ≥ 2 are units, their valuation is zero' is easy to misread: the non-special roots of g1 are µ′_i = δ_i − 1, whose valuation is zero, whereas the special zero µ has positive valuation. Please clarify which roots are being discussed.","section":"Equality to 0 in the henselisation of a discrete valued field"},{"comment":"The phrase 'Now we know that the natural morphism θ : Vg1 → VH is injective and that Vg1 itself is integral' appears after the argument that already uses the zero-divisor-free property of Vg1. The wording is confusing; it would help to state separately, before the injectivity proof, that Vg1 has no zerodivisors by Remark 3, and then to conclude injectivity at the end.","section":"Proof of Theorem 1, Injectivity"},{"comment":"The proof in Appendix 1 relies on the result of Alonso García–Lombardi–Neuwirth 2021 that Ker(θ_f) is a minimal detachable prime ideal. Since this is another externally imported fact, it should be stated precisely in the note rather than summarised by reference.","section":"Appendix 1"},{"comment":"The paper would benefit from a sentence explicitly saying which results are proved in the note and which are imported from earlier papers, so that the reader can identify the chain of dependencies for Theorem 1 at a glance.","section":"Introduction and terminology"}],"recommendation":"major_revision","confidential_remarks":"The paper is a short note with a plausible and probably true result. The main issue is that the surjectivity half of Theorem 1 is not actually demonstrated in the text: it relies on an under-explained inference from Lemma 4 to membership in an elementary henselisation ring. This is fixable by adding the missing argument or by quoting the exact contents of Kuhlmann–Lombardi 2000 that justify the step. The number of self-citations is noticeable but not circular; the paper proves its theorem from the cited constructions. I would recommend revision rather than rejection, because the core strategy is sound and the gap is localised."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Rough take: this is a small note that fills a real gap. People assumed Vh and VH are the same; the authors give a constructive proof and thereby a classical one. The injectivity half is clean: they use the KL2000 equality-to-zero test, reduce to an elementary step, and the appendices do real work proving the elementary rings are integrally closed in three different ways. The theorem is probably true, and this is a legitimate contribution to the constructive algebra literature.\n\nThe soft spot is the surjectivity proof. Lemma 4 is quoted from KL2000, and then the text says \"It shows that δ^m η is in the image of a certain Vu ⊆ Vh.\" That does not follow from Lemma 4 as stated. Lemma 4 only guarantees a v-isolated zero of some Q; you still need the explicit description from KL2000 Prop 2.2 (α in K or α = (aδ'+b)/(cδ'+d) for a special zero δ') and then you have to show the fraction actually lies in Vh. That last step is not written out, and it is not automatic: the denominator can be a nonunit in Vh even when v(α) ≥ 0. A referee should push for this to be spelled out—either by showing the denominator is a unit in a suitable Vu, or by using the integral closedness of Vf from the appendices to identify V[δ'] with the valuation ring. As it stands, the surjectivity of φ is not fully demonstrated.\n\nSecond issue: the abstract says no proof was previously available, yet the paper cites the authors' own 2021 J. Algebra paper on the comparison of two henselisations in the non-Noetherian case. That title is directly on point. The note never explains why Theorem 1 is not already a consequence of that work. Maybe it is not, but the reader should not have to guess.\n\nMinor: Lemma 4 and the equality test are imported from KL2000 without proof. That is acceptable in a note, but the paper should at least state the precise result it is relying on and where to find it.\n\nThis paper is for people in constructive commutative algebra, especially those using the ALP2008 and KL2000 constructions. It deserves a serious referee; the request should be for revision, not rejection. If the authors tighten the surjectivity step and reconcile the novelty claim with the 2021 paper, it is publishable as a note.","headline":"A modest, useful constructive proof that two henselisations coincide, but the surjectivity step is too under-documented to trust as written.","tokens_in":9757,"tokens_out":13429,"would_cite":true,"duration_ms":118055,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["13J15","13A18","03F65"],"pacs":[],"model":"deepseek-v4-flash","headline":"Two henselisation constructions coincide: proof supplied","keywords":["henselisation","discrete valued field","residually discrete local ring","special polynomial","Newton polygon","constructive mathematics","universal property","valuation ring"],"falsifier":"Take $K=\\mathbb{Q}$ with the $p$-adic valuation and $V=\\mathbb{Z}_{(p)}$, let $\\delta$ be the special zero of $g(X)=X^2-X-p$, and for a candidate $\\eta\\in\\mathbb{Q}[\\delta]$ with $v(\\eta)\\ge 0$ compute whether some $\\delta^m\\eta$ is the zero corresponding to an isolated Newton-polygon slope of a polynomial in $V[X]$; if any $\\eta$ fails the test, Lemma 4 is false and the proof breaks, while an element of $V^H$ that stays outside every intermediate $V_u$ in the colimit would falsify Theorem 1 itself.","tokens_in":8676,"feed_emoji":"🔄","tokens_out":10168,"duration_ms":84944,"temperature":0.7,"pith_summary":"The paper proves that two different constructive constructions of a henselisation—one for a residually discrete valuation ring and one for the discrete valued field it sits inside—produce the same object: the natural local morphism $V^h \\to V^H$ is an isomorphism. This fact was routinely accepted in the classical literature without a proof, and the paper supplies a constructive proof that is therefore also valid in classical mathematics. The result matters because it unifies two universal constructions developed separately and gives an algorithmic handle on the elements of a valued field's henselisation. A sympathetic reader should see the theorem as the missing bridge between the local-ring and valued-field approaches to Hensel's lemma.","feed_headline":"Two henselisation constructions coincide: proof supplied","feed_subtitle":"The canonical map between the local-ring and valued-field henselisations is an isomorphism, with proof.","key_machinery":"The argument is carried by three linked devices. First, special polynomials of the form $g(X)=X^n-X^{n-1}+a_0\\ell(X)$ with $a_0\\in m$: every Hensel polynomial can be replaced by one of these, so each elementary step of the local-ring henselisation adds a single special zero $\\delta=1+\\mu$ and computations can be done in the algebra $K[\\delta]$. Second, Newton polygons of polynomials over $V$: an isolated slope of the polygon of $q\\in V[X]$ corresponds to a v-isolated zero in $K^H$ that is explicit as an element of $K$ or as $(a\\delta+b)/(c\\delta+d)$, and the characteristic polynomials $q(T)$ and $r(T)=T p(T)$ give a test for whether $\\alpha'=p(\\mu')$ is zero. Third, Lemma 4, imported from earlier work: every $\\eta\\in K[\\delta]$ admits an $m$ with $\\delta^m\\eta$ a v-isolated zero of a polynomial with coefficients in $V$, which is what pulls arbitrary elements of $V^H$ back into $V^h$. Supporting machinery includes Tate's trace formula, used to prove $V_{g_1}$ is integrally closed and integral.","core_discovery":"Let $(K,V)$ be a discrete valued field with henselisation $(K^H,V^H)$, and let $(V^h,m^h)$ be the henselisation of the residually discrete local ring $(V,m)$. The paper establishes that the unique local morphism of $V$-algebras $\\varphi: V^h \\to V^H$ is an isomorphism. Injectivity is proved step by step: for each elementary extension $V_{g_1}$ obtained by adding the Hensel zero of a special polynomial, an element $\\alpha=p(\\mu)$ that maps to zero in $V^H$ is shown to be zero in $V_{g_1}$, using the characteristic polynomial $q(T)$ of $p(x)$ and the fact that if $q(0)=0$, writing $q=T^m q_1$ with $q_1(0)\\neq 0$, the relation $q_1(\\alpha')\\neq 0$ forces $q_1(\\alpha)\\neq 0$ and hence $\\alpha=0$. Since $V_{g_1}$ is integral, the map is injective. Surjectivity reduces to showing that every element $\\eta\\in K[\\mu]$ with $v(\\eta)\\ge 0$ lies in $V^h$: Lemma 4 gives an exponent $m$ such that $\\delta^m\\eta$ is a v-isolated zero of a polynomial with coefficients in $V$, so $\\delta^m\\eta$ lands in some intermediate henselisation step inside $V^h$, and since $1/\\delta\\in V^h$, $\\eta\\in V^h$. Consequently the fields of fractions coincide and $V^H\\subseteq V^h$, completing the isomorphism.","pith_inferences":["The proof's reliance on Newton polygons suggests that for computable valued fields the isomorphism can be made effective: one should be able to decide membership in the henselisation by computing characteristic polynomials and isolated slopes, a concrete algorithm the paper does not spell out.","Lemma 4 is the real engine of the surjectivity proof; a self-contained treatment would need to internalise the Newton-polygon characterisation rather than citing it, and the same lemma is likely to control how far the two henselisations differ for more general valuation rings.","The same coincidence plausibly extends to higher-rank or non-discrete valuations whenever an analogue of Lemma 4 holds, so the theorem may be less about discreteness and more about the availability of isolated Newton slopes.","For classical readers, the note converts a folklore commutativity of constructions into a proved statement, which matters for any work that silently identifies the two henselisations in proofs."],"forward_implications":["The henselisation $K^H$ is the field of fractions of $V^h$, giving a direct embeddability of the valued-field henselisation inside the local-ring henselisation.","Every element of $V^H$ can be written as an element of $V^h$ divided by a power of a special zero $\\delta$, so membership in the henselisation is controlled by Newton polygon data.","The two universal properties—being the universal henselian residually discrete local ring over $V$ and being the universal henselian discrete valued field over $(K,V)$—define the same extension, so results proved for one construction transfer to the other.","Because the proof is constructive, the equality-to-zero test for elements of $V^H$ yields a decision procedure for whether an element of $K[\\delta]$ lies in $V^h$."],"supporting_citations":[{"why":"Constructs the henselisation of a discrete valued field and supplies the Newton-polygon results, including the proof of Lemma 4 imported here.","marker":"Kuhlmann and Lombardi 2000"},{"why":"Constructs the henselisation of a residually discrete local ring as a filtered colimit and proves the special-polynomial reduction used as Lemma 2.","marker":"Alonso García, Lombardi, and Perdry 2008"},{"why":"Theorem 6.3 proves that $A\\{f\\}$ is normal, used to show $V_{g_1}$ has no zerodivisor.","marker":"Coquand and Lombardi 2016"},{"why":"Provides the minimal detachable prime ideal argument behind the alternative integrality proof in Appendix 1.","marker":"Alonso García, Lombardi, and Neuwirth 2021"},{"why":"Source of Tate's lemma, the trace formula used in Lemma 5 and in the integral closedness results.","marker":"Raynaud 1970"}],"fun_headline_variants":["Two henselisations coincide: missing proof supplied","Canonical map between henselisations is an isomorphism","Constructive proof: two henselisations are isomorphic","Henselisation isomorphism: injectivity and surjectivity proven","Previously missing proof of henselisation coincidence provided"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"Lemma 4, cited rather than reproved, claims that for every element $\\eta\\in K[\\delta]$ some power $\\delta^m\\eta$ is a v-isolated zero of a polynomial with coefficients in $V$; if that characterisation fails for a discrete valued field, the surjectivity conclusion $\\eta\\in V^h$ does not follow.","fun_headline_variants_meta":{"raw":{"variants":["Two henselisations coincide: missing proof supplied","Canonical map between henselisations is an isomorphism","Constructive proof: two henselisations are isomorphic","Henselisation isomorphism: injectivity and surjectivity proven","Previously missing proof of henselisation coincidence provided"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000549,"raw_usage":{"total_tokens":2610,"prompt_tokens":921,"completion_tokens":1689,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":537,"completion_tokens_details":{"reasoning_tokens":1621}},"tokens_in":537,"tokens_out":1689,"duration_ms":12031,"temperature":1.0,"reasoning_tokens":1621,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T11:25:58.924520+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take $K=\\mathbb{Q}$ with the $p$-adic valuation and $V=\\mathbb{Z}_{(p)}$, let $\\delta$ be the special zero of $g(X)=X^2-X-p$, and for a candidate $\\eta\\in\\mathbb{Q}[\\delta]$ with $v(\\eta)\\ge 0$ compute whether some $\\delta^m\\eta$ is the zero corresponding to an isolated Newton-polygon slope of a polynomial in $V[X]$; if any $\\eta$ fails the test, Lemma 4 is false and the proof breaks, while an element of $V^H$ that stays outside every intermediate $V_u$ in the colimit would falsify Theorem 1 itself.","supporting_citations":[{"cited_title":"Construction du hens\\'elis\\'e d'un corps valu\\'e","cited_arxiv_id":null,"evidence_quote":"Constructs the henselisation of a discrete valued field and supplies the Newton-polygon results, including the proof of Lemma 4 imported here."},{"cited_title":"Elementary constructive theory of H enselian local rings","cited_arxiv_id":null,"evidence_quote":"Constructs the henselisation of a residually discrete local ring as a filtered colimit and proves the special-polynomial reduction used as Lemma 2."},{"cited_title":"Some remarks about normal rings","cited_arxiv_id":null,"evidence_quote":"Theorem 6.3 proves that $A\\{f\\}$ is normal, used to show $V_{g_1}$ has no zerodivisor."},{"cited_title":"On a theorem by de Felipe and Teissier about the comparison of two henselisations in the non-Noetherian case","cited_arxiv_id":null,"evidence_quote":"Provides the minimal detachable prime ideal argument behind the alternative integrality proof in Appendix 1."}],"review_version":1}