{"id":"d66fd90e-8788-4e84-bd2b-3af87c7abf58","arxiv_id":"2505.08427","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":4,"one_line_summary":"A subdivision algorithm with verified bounds yields guaranteed lower bounds on the reach of zero sets of smooth functions, with applications to homology, distances, eigenvalues, and deformations.","lead":"This paper presents a subdivision algorithm that computes certified lower bounds on the reach of a manifold defined as the zero set of smooth functions, using verified numerical bounds. It extends reach computations beyond polynomials and opens up applications in homology computation, distance comparison, eigenvalue estimates, and deformation stability.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Reach lower-bound proof is sound, but the planar homology application's Proposition 6.5 retraction claim has a gap: the push map does not keep the homotopy inside \\tilde S.","rationale":"The core reach result is solid: Proposition 3.1's termination argument and the derivation of Corollary 4.8 from Propositions 4.1 and 4.3 and Theorem 2.10 are correct, and the practical difficulty of supplying tight bounds B2 and B3 noted by the reader is a usability limitation rather than a correctness flaw. The central theorem is conditional on those bounds, and the constants check out. However, Section 6's advertised planar homology algorithm has a genuine proof gap in Proposition 6.5: the push map does not ensure that the homotopy stays inside \\tilde S, so the claimed deformation retraction from \\tilde S to M is not established. Since this application is highlighted in the abstract and used for Corollary 6.10, the paper should either provide a correct retraction argument or soften the claim. The right verdict is CONDITIONAL: accept the reach contribution, but require the homology application to be fixed or appropriately qualified.","tokens_in":51110,"tokens_out":41326,"duration_ms":415915,"concrete_test":"Run a concrete grid example: take M a circle, grid spacing δ=τ/3 aligned so that \\tilde S contains a vertex-adjacent pair F=[0,1]^2, F'=[1,2]^2 with p=(0.1,0.9) and \\pi(p)=(1.1,1.9). Compute H(1/2,p) and apply push; check whether the result lies in \\tilde S. If it lies outside \\tilde S, Proposition 6.5's retraction is invalid. Alternatively, check analytically whether push∘H_t maps \\tilde S to itself for all t; the proof currently provides no such containment.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"In Proposition 6.5 the authors claim that M is a deformation retract of \\tilde S, the union of all grid boxes meeting M. The proof defines the nearest-point homotopy H(t,p)=(1-t)p+t\\pi(p) and then composes with the map 'push' that sends every point in a box outside \\tilde S to the boundary of that box along a ray from the box's center. They assert that push∘H 'defines a deformation retract from \\tilde S to M.' This does not follow: for a point p in a box F and its nearest point \\pi(p) in a box F' that meets F only at a vertex, the straight segment H(t,p) can leave F∪F'. Example: for F=[0,1]^2, F'=[1,2]^2, p=(0.1,0.9), \\pi(p)=(1.1,1.9), at t=1/2 the point is (0.6,1.4), in neither box. The proof has not shown this point lies in \\tilde S; if it lies in an outside box, push may map it to a boundary face shared with another outside box, so the image of the homotopy is not contained in \\tilde S. Thus the claimed deformation retraction, and hence Corollary 6.10 for the homology of planar curves, is not established. This concern does not affect Propositions 3.1 or 4.3/Corollary 4.8.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces a deterministic, verified-numerics method to compute rigorous lower bounds for the reach of a smooth submanifold presented as the zero set of one or more smooth functions. The main algorithmic contribution is a recursive subdivision of a bounding box into boxes that are certified either to contain no zero set ('CaseOneBoxes') or to carry a lower bound on |∇f|_1 ('CaseTwoBoxes'); Proposition 3.1 proves termination and the gradient bound. Combining this with a curvature estimate (Proposition 4.1) and a bottleneck estimate (Proposition 4.3) yields the central reach bound Corollary 4.8: for M=V(f)⊂K with |Hess f|_2≤g1 on K and |∇f|_1≥g2 on M, one has τ≥g2/(2√N g1). The paper then derives applications: a comparison inequality between intrinsic and extrinsic distances (Section 5), a homology-computation method for planar curves based on selected grid boxes (Section 6), eigenvalue bounds for the Laplacian (Section 7), and stability bounds for deformations of algebraic varieties (Section 8). Appendix A generalizes the reach bound to higher codimension, and Appendix B gives a proof of the quantitative tubular neighborhood theorem.","tokens_in":51404,"tokens_out":9047,"duration_ms":98444,"significance":"The core reach-bound result is genuinely useful and largely self-contained. It is the first deterministic certified reach bound that works for zero sets of arbitrary smooth functions, not only polynomials, and the constants in Corollary 4.8 are explicit enough for direct use. The proof strategy is clean: the reach lower bound is obtained from rigorous gradient and Hessian bounds produced by the algorithm, not by fitting to the reach itself, and the termination argument in Proposition 3.1 is sound up to minor details. The multi-function generalization in Appendix A is also substantive. If the homology application in Section 6 were fully established, it would be a notable contribution to computing Betti numbers of planar curves from a cubical complex. As written, however, the proof of the key deformation-retraction claim has a gap that currently blocks that application. The eigenvalue application is honestly acknowledged by the authors as too weak for numerical use, which is a limitation rather than an error.","major_comments":[{"comment":"The proof of Proposition 6.5 does not establish that push∘H is a deformation retraction from \\tilde S to M. The homotopy H(t,p)=(1-t)p+tπ(p) is a straight segment, and the fact that p and π(p) lie in adjacent boxes does not imply that the whole segment lies in \\tilde S: for F=[0,1]^2 and F'=[1,2]^2, with p=(0.1,0.9) and π(p)=(1.1,1.9), the midpoint (0.6,1.4) lies in neither box. The segment can therefore pass through boxes outside \\tilde S, and the map push sends points in an outside box to the boundary of that box, which need not be contained in \\tilde S at all; it can even be a boundary shared with another outside box. Moreover, push is undefined at the midpoints of boxes outside \\tilde S, and H(t,p) may pass through such a midpoint. Hence the composition push∘H is not shown to be defined with image in \\tilde S, and the claimed deformation retraction is not proved. Since Corollary 6.10 relies on Proposition 6.5, the homology claim for planar curves is not established by the present argument. This gap is local to Section 6 and does not affect the reach bounds in Sections 3–5 or Appendix A.","section":"Section 6, Proposition 6.5"}],"minor_comments":[{"comment":"The statement reads 'Let M be a semi-Riemannian submanifold of M'; the second M should presumably be the ambient manifold, for example ℝ^N or \\bar M.","section":"Theorem 7.7 statement"},{"comment":"In the infinite-descent argument, the algorithm's conditions are stated at midpoints, but the proof applies the resulting bounds to arbitrary points D_i∈F_i. The intended argument can be completed by first using the gradient/Hessian bounds to transfer the midpoint bounds to all points of the box; as written, the displayed inequalities skip this step.","section":"Proposition 3.1, termination proof"},{"comment":"The authors correctly state that the eigenvalue lower bound is far smaller than the smallest positive floating-point number. This is an honest limitation, but the abstract and introduction present eigenvalue estimation as one of the applications; a sentence there noting that this application is currently only theoretical would better calibrate reader expectations.","section":"Section 7, Example 7.15"},{"comment":"The paper uses closed boxes whose union is the whole square, so 'the homology of the selected boxes' needs a precise convention for the resulting cubical complex on shared boundaries. This is standard and probably harmless, but stating the convention would improve the presentation.","section":"Section 6, Definition 6.1 and Corollary 6.10"}],"recommendation":"major_revision","confidential_remarks":"The central reach-bound contribution is sound and, in my assessment, publishable after the Section 6 issue is addressed. The stress-test concern about Proposition 6.5 lands: the composition push∘H is not shown to have image in \\tilde S, and the example with two corner-adjacent boxes is a genuine obstruction to the proof as written. This is a load-bearing gap for the homology application but not for the main reach theorem. I would be happy to accept once Proposition 6.5 is repaired or the homology claim is removed or weakened accordingly."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The reach lower bound is a solid, genuinely useful addition to the certified-geometry toolkit. The planar homology application, however, has a proof gap in Proposition 6.5 that I think is real; the authors will need to fix it before that part is publishable.\n\nWhat's actually new: the subdivision algorithm with verified gradient bounds is the first such method that handles non-polynomial zero sets. Proposition 3.1 is clean and the termination argument is sound. Corollary 4.8, giving τ ≥ g2/(2√N g1), is a neat consequence and the constants check out. The distance comparison d_M≤2d_E for |x-y|<τ/2 is a small but nice improvement, and the multiple-function generalization in the appendix is thoughtfully done. I also appreciate that the authors state clearly when their estimates are too weak to be numerically useful; the eigenvalue section is honest about being theoretical.\n\nWhere it gets soft. The stress-test note is on target. In Proposition 6.5 the proof only establishes that p and its nearest point π(p) lie in adjacent boxes (touching at least at a vertex). It then claims the straight homotopy between them, composed with 'push', stays inside S̃. That does not follow. The segment can pass through boxes that are not in S̃. Example: F=[0,1]², F'=[1,2]², p=(0.1,0.9), π(p)=(1.1,1.9); at t=1/2 the point is (0.6,1.4), in neither box. There is no argument that this point lies in S̃, and 'push' could map it to a boundary outside S̃. So the deformation retraction—and hence Corollary 6.10—is not established. This does not affect the main reach theorem, but it does mean the headline homology application needs more work.\n\nMinor: no code is shipped, which makes the numerical claims harder to reproduce. The eigenvalue section is self-admittedly useless numerically; that's okay as theory, but it's not an application anyone will use.\n\nWho this is for: computational geometers and TDA practitioners who want certified reach bounds for implicit manifolds. The core result deserves a serious referee. My recommendation: send it to review, but flag the homology gap; the authors should either fix the retraction proof or drop the homology claim.","headline":"The certified reach lower bound is a solid new tool, but the planar homology application has a real gap in Proposition 6.5 that the authors need to fix.","tokens_in":51941,"tokens_out":4463,"would_cite":true,"duration_ms":41913,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["65G40","53A07","55N31"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper proves that a box-subdivision algorithm converts verified gradient and Hessian bounds into a certified lower bound for the reach of a smooth zero set, and applies it to distances, homology, eigenvalues, and smooth deformations.","keywords":["reach","lower bound","zero set","verified numerics","subdivision algorithm","bottleneck","homology computation","intrinsic distance"],"falsifier":"Take a smooth function with a known exact reach, such as a sinusoidal perturbation of the unit circle whose curvature maxima determine the true reach, and run Algorithm 1 with interval-arithmetic bounds; if the reported lower bound ever exceeds the true reach, or if the loop fails to terminate on a non-singular example, the paper's guarantee is refuted.","tokens_in":50891,"feed_emoji":"📐","tokens_out":10422,"duration_ms":94629,"temperature":0.7,"pith_summary":"This paper develops a rigorous, terminating algorithm for computing a guaranteed lower bound on the reach of a smooth submanifold presented as the zero set of smooth functions, with no requirement that the functions be polynomials. The reach controls how large a tubular neighbourhood remains single-sheeted, and lower bounds on it are what let geometric and topological conclusions be certified from finite computation. The central inequality states that for $M=V(f)\\subset K$ with $|\\nabla f|_1\\ge g_2$ on $M$ and $|\\operatorname{Hess} f|_2\\le g_1$ on $K$, the reach satisfies $\\tau\\ge g_2/(2\\sqrt{N}g_1)$. The same pipeline gives a lower bound on the gradient norm, a comparison bound between intrinsic and extrinsic distance, a homology computation for planar curves, a Laplacian eigenvalue estimate, and explicit bounds for deforming varieties without changing their diffeomorphism type.","feed_headline":"Certified reach bounds for any smooth zero set","feed_subtitle":"A subdivision algorithm turns gradient and Hessian estimates into provable geometric guarantees, beyond polynomials.","key_machinery":"The load-bearing device is the subdivision-classification loop of Algorithm 1. Starting from the bounding box $[-B_1,B_1]^N$, it halves a box and applies two mean-value-theorem tests based on verified bounds $|\\nabla f|_2\\le B_2$ and $|\\operatorname{Hess} f|_2\\le B_3$: if the midpoint value of $f$ is too large for $f$ to vanish inside the box, the box is discarded; if the midpoint gradient is large enough to force $|\\nabla f|_1>0$ throughout the box, the box is kept and contributes to the gradient bound. Non-singularity of $V(f)$ rules out an infinite nested sequence of unresolved boxes, so the loop terminates. The reach bound then combines the level-set curvature formula $|II(u,v)|=|\\operatorname{Hess} f(u,v)|/|\\nabla f|$ and the bottleneck estimate $\\lambda\\ge|\\nabla f|/|\\operatorname{Hess} f|$ through the reach decomposition $\\tau=\\min\\{\\text{bottleneck radius},\\text{curvature radius}\\}$.","core_discovery":"The discovery is that a reach lower bound for $V(f)$ can be assembled from two affordable pieces: a lower bound on $|\\nabla f|_1$ along the variety and an upper bound on $|\\operatorname{Hess} f|_2$ over the containing convex set. The first piece is produced by a subdivision algorithm that keeps halving boxes until each box either provably contains no point of $V(f)$ or provably has $|\\nabla f|_1$ above a positive threshold; non-singularity forces termination (Proposition 3.1). The second piece bounds the second fundamental form by $|\\operatorname{Hess} f(u,v)|/|\\nabla f|$, and a Rolle-theorem argument along a bottleneck chord bounds the smallest bottleneck from below by $|\\nabla f|/|\\operatorname{Hess} f|$ (Propositions 4.1 and 4.3). Feeding these into the standard decomposition of reach as the minimum of the bottleneck radius and the curvature radius yields $\\tau\\ge g_2/(2\\sqrt{N}g_1)$, and an analogous determinant-based argument handles varieties defined by several functions.","pith_inferences":["The classification of each box depends only on local midpoint values and global bounds, so the loop is embarrassingly parallel; a GPU implementation could push the method onto examples that currently take too long, including the Calabi-Yau-relevant cases the paper mentions.","The eigenvalue application's weakness is traceable to the diameter estimate: replacing the ball-covering count by a tighter certified intrinsic diameter would likely turn the theoretical Laplacian bound into a usable one, independently of improving the reach bound.","The same midpoint-test pattern could certify other gradient-controlled quantities, such as local feature size or separation between sheets, for smooth implicit sets in non-Euclidean ambient spaces whenever corresponding bounds on first and second derivatives are available.","Because the final bound is proportional to $1/|\\operatorname{Hess} f|$, using local per-box Hessian bounds rather than one global bound is not a minor optimization; it is the difference between a vacuous reach certificate and a useful one for functions with large curvature."],"forward_implications":["Certified reach lower bounds become available for zero sets of transcendental and other non-polynomial smooth functions, where the existing deterministic algorithms may fail or run too long.","For any two points of $M$ whose extrinsic distance is less than $\\tau/2$, the intrinsic distance is at most twice the extrinsic distance (Corollary 5.9).","The homology of a planar curve $V(f)$ is exactly the homology of the cubical complex formed by boxes whose vertices bracket $f$, provided the box side is at most $\\tau/2.37$ (Corollary 6.10).","A reach lower bound yields a lower bound on the first non-zero Laplacian eigenvalue through the Li and Yau estimate, though the diameter estimate used in the paper makes the resulting numbers far too small for practical computation (Example 7.15).","For a smooth variety $V(f)$, a perturbation $f+\\varepsilon g$ stays smooth for all $\\varepsilon\\in[0,1)$ whenever $|g|$ and $|\\nabla g|$ obey the explicit threshold produced by the box classification (Proposition 8.1)."],"supporting_citations":[{"why":"Defines the reach and supplies the curvature-measure theorem used in the quantitative tubular-neighbourhood proof.","marker":"Federer 1959"},{"why":"Provides the decomposition of the reach into the radius of the smallest bottleneck and the minimal radius of curvature, and the angle-to-reach bound used in the homology argument.","marker":"Aamari et al. 2019"},{"why":"Gives the intrinsic-versus-extrinsic distance estimate that Section 5 strengthens to the explicit constant-2 comparison.","marker":"Niyogi et al. 2008"},{"why":"Supplies the eigenvalue lower-bound theorem applied after bounding Ricci curvature and diameter in terms of the reach.","marker":"Li and Yau 1980"},{"why":"Characterises focal points on normal lines, used to prove the quantitative tubular-neighbourhood theorem.","marker":"Milnor 1963"}],"fun_headline_variants":["Guaranteed reach bounds for smooth zero sets","Provable reach bounds beyond polynomial zero sets","Subdivision algorithm certifies reach of submanifolds","Reach lower bound from subdivision and Hessian","Any smooth zero set gets certified reach"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the user can supply verified global bounds $B_2$ and $B_3$ on $|\\nabla f|$ and $|\\operatorname{Hess} f|$ over the entire bounding box, and since the reach bound contains $1/B_3$, a loose Hessian bound can shrink the certified output to a size far below the true reach.","fun_headline_variants_meta":{"raw":{"variants":["Guaranteed reach bounds for smooth zero sets","Provable reach bounds beyond polynomial zero sets","Subdivision algorithm certifies reach of submanifolds","Reach lower bound from subdivision and Hessian","Any smooth zero set gets certified reach"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001179,"raw_usage":{"total_tokens":4879,"prompt_tokens":958,"completion_tokens":3921,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":574,"completion_tokens_details":{"reasoning_tokens":3851}},"tokens_in":574,"tokens_out":3921,"duration_ms":27438,"temperature":1.0,"reasoning_tokens":3851,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T21:55:42.382608+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a smooth function with a known exact reach, such as a sinusoidal perturbation of the unit circle whose curvature maxima determine the true reach, and run Algorithm 1 with interval-arithmetic bounds; if the reported lower bound ever exceeds the true reach, or if the loop fails to terminate on a non-singular example, the paper's guarantee is refuted.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines the reach and supplies the curvature-measure theorem used in the quantitative tubular-neighbourhood proof."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the decomposition of the reach into the radius of the smallest bottleneck and the minimal radius of curvature, and the angle-to-reach bound used in the homology argument."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Gives the intrinsic-versus-extrinsic distance estimate that Section 5 strengthens to the explicit constant-2 comparison."}],"review_version":1}