{"id":"4026879f-5820-4fa0-9cd8-26eaf89bea45","arxiv_id":"2411.13300","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Projective delineability lets polynomial roots pass through infinity, and the paper proves conditions under which it can replace classical delineability in CAD, potentially shrinking the projection set.","lead":"This paper introduces a new mathematical notion called projective delineability, a weaker version of the classical condition used in cylindrical algebraic decomposition (CAD), where polynomial roots are allowed to go to infinity. It proves local and global theorems showing when this weaker property is enough, which could let CAD algorithms skip some projection polynomials and compute more efficiently.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 2's proof omits the empty-fiber case: Z_RP1(P,S) may have p^{-1}(U)=∅, which Definition 12 disallows, so the covering-space step needs an explicit case split.","rationale":"The paper's central mathematical contribution is sound in outline: projective delineability is well-defined, Theorem 1 gives local projective delineability under discriminant hypotheses, and Proposition 4 shows the simple-connectivity assumption in Theorem 2 is necessary. The weakest point is indeed the proof of Theorem 2, where the covering-space step fails if Z_RP1(P,S) is empty on an open set, because Definition 12 explicitly requires non-empty local trivializations. The reader's verdict already identifies this and correctly treats it as a minor gap rather than a fatal flaw. I agree with that assessment: the empty case makes the conclusion vacuous, and the nonempty case should follow from order-invariance of the discriminant, so the fix is likely a case split plus a short lemma on local constancy of the number of projective roots. No reason appears to change the reader's CONDITIONAL verdict; the paper should be accepted pending this proof repair. I do not see a deeper issue with the local theorem, the algebraic transformation argument, or the claimed computational motivation, although the practical single-cell-construction claim still lacks a benchmarked algorithmic development.","tokens_in":13229,"tokens_out":29640,"duration_ms":342857,"concrete_test":"Re-prove Theorem 2 with a case split: if Z_RP1(P,S) = ∅, set k = 0 and stop. Otherwise, prove that the number of projective root functions supplied locally by Theorem 1 is locally constant on S, using the order-invariant discriminant to rule out creation/annihilation of roots and continuity to rule out changes at infinity; this implies p^{-1}(x) ≠ ∅ for every x, making p a covering. If local constancy cannot be established, try to construct a connected analytic S and a polynomial P satisfying the theorem's hypotheses with a nonempty fiber over one open subset of S and an empty fiber over another; such an example would refute Theorem 2.","verdict_should_be":"UNCHANGED","load_bearing_attack":"In the proof of Theorem 2, the authors assert that Theorem 1 implies p : Z_RP1(P,S) → S is a covering space in the sense of Definition 12. Definition 12 requires p^{-1}(U) to split as a disjoint union of a non-empty family of open sheets each homeomorphic to U. If E_s(P) has no projective roots over some connected neighbourhood N_s (for instance P = x_n^2 + 1 over any S), then p^{-1}(N_s) = ∅, so the covering condition fails and the covering-space theorem [7, Cor. 13.8] cannot be invoked. The conclusion of Theorem 2 is then vacuous in that case, but the proof as written is incomplete: it must either split off the empty-fiber case or prove that a nonempty fiber at one point forces p^{-1}(x) ≠ ∅ for every x in connected S. This is a genuine proof gap, though not a disproof of the theorem.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces projective delineability, a relaxation of McCallum delineability in which root functions are allowed to take values in the real projective line, so that roots may pass through infinity. It proves a local projective delineability theorem (Theorem 1), a global version under the additional assumption that the base submanifold is simply connected (Theorem 2), an explicit counterexample on the circle showing that this assumption is necessary (Proposition 4), and an extension of McCallum's equational-constraint theorem to the projective setting (Theorem 3). The stated motivation is to justify omitting leading coefficients in single-cell CAD construction when projective delineability is sufficient.","tokens_in":13404,"tokens_out":31963,"duration_ms":350726,"significance":"The notion is natural and well motivated, and the paper gives a clean mechanism — the GL(2,R) reparametrization of the last variable — for locally moving roots away from infinity. The global theorem identifies a genuine monodromy obstruction, and Proposition 4 supplies a convincing explicit quartic with a computable discriminant. The potential algorithmic payoff for SMT-oriented CAD is clear, and the paper is self-contained: definitions are precise, the supporting lemmas are stated with proofs, and the connection to McCallum's results is explicit. One step in the proof of Theorem 2 needs repair, but the central claims appear defensible.","major_comments":[{"comment":"The assertion that Theorem 1 makes p : Z_RP1(P,S) → S a covering space in the sense of Definition 12 is not justified, because Definition 12 requires p^{-1}(U) to be split into a non-empty family of sheets. Under the hypotheses of Theorem 2 it can happen that p^{-1}(U)=∅ for every U: e.g. P=x_n^2+1 over any simply connected S, where Disc_{2,x_n}(P)=-4 is order-invariant and P is never nullified, but Z_RP1(P,S)=∅. Hence [7, Cor. 13.8] cannot be invoked without an explicit case split. The proof should first dispose of the empty total space, then show that when one fibre is non-empty the set {s∈S | p^{-1}(s)≠∅} is both open and closed using the local conclusion of Theorem 1, and only then apply the covering-space argument. As written, the proof does not cover the empty-fibre case.","section":"§VI, proof of Theorem 2"}],"minor_comments":[{"comment":"The statement 'Elementary computations show that it has order 2 on S' is misleading: the displayed discriminant restricts to the nonzero constant 2^14 on S, so its order of vanishing at points of S is 0, not 2. If 'order 2' refers to the multiplicity of S as a component of the zero set of Disc, this should be stated explicitly.","section":"§IV, Proposition 4"},{"comment":"There is a typo in 'mutliplicity', and the reindexing argument would be easier to follow if the closedness of the sets C_i and the use of the finite pasting lemma were spelled out before the new functions θ'_j are defined.","section":"§IV, Proposition 3 proof"},{"comment":"The paper should state explicitly whether k=0 is allowed in Definition 11. This matters for the empty-fibre case in Theorem 2, since a projective delineability statement with zero root functions is exactly the case that the covering-space argument must handle separately.","section":"§II, Definition 11 and §VI, Definition 12"}],"recommendation":"major_revision","confidential_remarks":"For the editor: I see no concern about novelty or attribution. The main issue is a fixable but genuine gap in the proof of Theorem 2, namely the missing empty-fibre case split. The authors should also be asked to clarify the order statement in Proposition 4. Once these points are addressed, the paper would be suitable for publication."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nYou should know two things about this paper. First, projective delineability is a genuinely new way to relax a core definition in CAD theory: allow root functions to take values in RP1, and you can drop leading coefficients from the projection set in single-cell construction. That is a real theoretical step. Second, the global theorem (Theorem 2) has a proof gap, but it is small and fixable; the theorem itself appears true.\n\nWhat is actually new: the definition itself, the local result (Theorem 1), the global result (Theorem 2) with the counterexample (Proposition 4) showing simple connectivity is needed, and a projective analogue of McCallum's product theorem (Theorem 3). The proofs use standard tools—McCallum's delineability theorem, resultant/discriminant transformation under GL(2,R), covering space triviality—and the computations in Proposition 4 check out. The paper earns credit for giving the counterexample that shows why the global assumption is needed.\n\nThe soft spots, in proportion. The proof of Theorem 2 asserts that Z_RP1(P,S) is a covering space in the sense of their Definition 12, which requires non-empty local trivializations. But if the polynomial has no projective roots over a connected neighborhood (e.g., P = x_n^2 + 1 over any S), the fiber is empty and the covering-space theorem cannot be invoked. The conclusion is vacuously true in that case, so the theorem is not false; the proof just needs an explicit case split, or an argument that a nonempty fiber at one point forces nonempty fibers everywhere. This is exactly the kind of thing a referee should catch, and it is a minor repair.\n\nThe paper's practical claim—that this allows omitting leading coefficients—is supported theoretically but not benchmarked. That is fine for a theory paper; the authors are clear that this is a foundation, not an experimental study. The relationship between projective and classical delineability is also more nuanced than \"strictly weaker\" (Proposition 3), and the paper handles that honestly.\n\nI think the paper is a solid contribution to CAD theory. The definition is new, the theorems are mostly correct, and the counterexamples are instructive. A serious referee should engage with it. I would accept it for review, conditional on fixing the Theorem 2 gap. I would cite it if I worked in CAD/SMT cell construction.","headline":"Projective delineability is a real new idea in CAD theory; the main theorem has a fixable gap, and the paper deserves a serious referee.","tokens_in":13950,"tokens_out":3258,"would_cite":true,"duration_ms":34758,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["14P10","68W30"],"pacs":[],"model":"deepseek-v4-flash","headline":"Projective delineability relaxes CAD's delineability so root functions may take values in $\\mathbb{RP}^1$, and the paper proves this relaxation is locally guaranteed and global on simply connected cells, enabling CAD single-cell…","keywords":["cylindrical algebraic decomposition","projective delineability","real projective line","root functions","leading coefficients","single cell construction","covering spaces"],"falsifier":"A reader can falsify the global theorem by taking $S$ to be the unit circle, $P = (1-x_1)x_3^4 + 4x_2 x_3^3 + (2+6x_1)x_3^2 - 4x_2 x_3 + (1-x_1)$, and computing that the discriminant is $2^{14}(x_1^2+x_2^2-1)^2(x_1^2+x_2^2)$, which is order-invariant on $S$, while the projective zero set is connected yet would have to split into two closed graphs if projective delineability held.","tokens_in":13048,"feed_emoji":"📐","tokens_out":7355,"duration_ms":68287,"temperature":0.7,"pith_summary":"This paper introduces projective delineability, a version of the classical delineability condition at the heart of cylindrical algebraic decomposition (CAD) in which the real root functions of a polynomial are allowed to take values in the projective line $\\mathbb{RP}^1$ rather than only in $\\mathbb{R}$. The central claim is that when a polynomial never vanishes on a connected analytic submanifold and its discriminant is nonzero and order-invariant there, projective delineability holds locally; if the submanifold is simply connected, it holds globally. The point of the relaxation is computational: projective delineability can be certified without controlling leading coefficients, so algorithms that build a single CAD cell around a sample point can omit leading coefficients from the projection whenever projective delineability is enough. A counterexample on the circle shows that the global theorem genuinely needs simple connectivity.","feed_headline":"Projective delineability lets CAD omit leading coefficients","feed_subtitle":"Root functions may reach the point at infinity, so fewer projection polynomials are needed to build a single cell.","key_machinery":"The machinery is the projective compactification of the cylinder: instead of following real roots $S \\to \\mathbb{R}$, one follows projective root functions $\\theta_l : S \\to \\mathbb{RP}^1$ defined as graphs inside $S \\times \\mathbb{RP}^1$. The key algebraic tools are the binary-form homogenization $H_{d_n}$ with respect to a fixed degree, the projective roots-and-multiplicities factorization of binary forms, and for an invertible matrix $A$ the polynomial $A^{*d_n}P$ obtained by acting on the last variable; choosing $A$ so that the transformed polynomial has no root at infinity moves the singularities away, after which the classical delineability theorem for polynomials with nonvanishing leading coefficient applies. The global step is the observation that the zero set forms a covering space of $S$, and the covering is trivial when $S$ is simply connected; the circle counterexample isolates the failure of triviality as exactly the obstruction.","core_discovery":"The paper establishes that the classical delineability theorem for CAD generalizes when zeros are viewed in $\\mathbb{RP}^1$. Writing $H_{d_n}(P)$ for the homogenization with respect to the degree $d_n$ of $P$ in the last variable, define projective roots as zeros of $H_{d_n}(P)$ in $\\mathbb{RP}^1$, so a root may be the point at infinity exactly where the leading coefficient vanishes. Theorem 1 proves that under $P \\neq 0$ on a connected analytic submanifold $S$ and order-invariance of a nonzero discriminant $\\operatorname{Disc}^{d_n}_{x_n}(P)$ on $S$, each point has a neighbourhood on which $P$ is projectively delineable and $H_{d_n}(P)$ is order-invariant on each projective section. Theorem 2 upgrades this to all of $S$ when $S$ is simply connected, by observing that the projective zero set is a covering space of $S$ and every covering of a simply connected space is trivial. Proposition 4 shows the circle $x_1^2+x_2^2=1$ satisfies all local hypotheses while projective delineability fails globally, so the simple-connectivity assumption cannot be dropped.","pith_inferences":["The covering-space proof makes a further claim plausible: on a cell with a hole, the obstruction to global projective delineability is exactly the monodromy of the projective roots around the cell's loops. An algorithm that tracks how roots permute as they go around the loop, rather than demanding simple connectivity, could recover a global description in the non-simply-connected case. This is an ","The same projective compactification could be applied to other CAD-based data structures, such as cylindrical algebraic coverings and non-uniform CADs, wherever an artificial cell split is created only because a root is passing through infinity. A testable extension would be to see whether replacing real root functions by projective ones reduces the number of cells in those algorithms too.","Because projective delineability is certified using discriminants and resultants only, it may combine with existing work that prunes resultants to produce a projection that is strictly smaller than the reduced projection in the single-cell construction. Whether the pruning remains complete for entire CADs, not just single cells, is a natural next question."],"forward_implications":["In the single-cell CAD construction, leading coefficients of polynomials can be omitted from the projection when projective delineability of the polynomial is sufficient, because projective delineability is certified using only discriminants and resultants.","For simply connected cells, the local projective delineability certificates patch into global projective root functions defined on the whole cell, with order-invariance of the homogenized polynomial on each projective section.","On cells that are connected but not simply connected, CAD routines must either work with the local neighbourhoods provided by Theorem 1 or explicitly track the monodromy of projective roots around loops.","When a polynomial never develops a root at infinity, projective delineability coincides with classical delineability; the new notion only matters where leading coefficients vanish, which is exactly the case where classical projection over-constrains the cell.","The resultant theorem extends to projective delineability: along a projective section of $P$, a projectively delineable $Q$ either vanishes completely or never vanishes, provided their resultant is nonzero and order-invariant on $S$."],"supporting_citations":[{"why":"Defines cylindrical algebraic decomposition and the original delineability notion that this paper relaxes.","marker":"[5]"},{"why":"Supplies the classical delineability theorem and analytic delineability framework on analytic submanifolds.","marker":"[10]"},{"why":"Provides the improved projection operation and the delineability theorem that the local proof applies after transforming the polynomial.","marker":"[11]"},{"why":"Gives the improved projection whose leading coefficients are exactly what projective delineability lets algorithms omit.","marker":"[3]"},{"why":"Provides the result on order-invariance of resultants for products of delineable polynomials that Theorem 3 extends to the projective setting.","marker":"[12]"},{"why":"Describes the single-cell CAD construction whose projection set projective delineability is designed to reduce.","marker":"[13]"},{"why":"Supplies the theorem that every covering of a simply connected space is trivial, used in the proof of the global result.","marker":"[7]"},{"why":"Provides the standard resultant and discriminant transformation laws under linear change of variables used in Lemma 1 and Proposition 1.","marker":"[8]"}],"fun_headline_variants":["Projective roots at infinity for CAD","Covering space proves projective delineability","Delineability works even at infinity","CAD generalized to projective roots","Simple connectivity key for projective CAD"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The global conclusion rests on the assumption that the cell has no holes in the sense that every loop can be shrunk to a point; on a cell with a hole, such as a circle, the same local hypotheses can hold while no global projective delineation exists.","fun_headline_variants_meta":{"raw":{"variants":["Projective roots at infinity for CAD","Covering space proves projective delineability","Delineability works even at infinity","CAD generalized to projective roots","Simple connectivity key for projective CAD"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000148,"raw_usage":{"total_tokens":1124,"prompt_tokens":813,"completion_tokens":311,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":429,"completion_tokens_details":{"reasoning_tokens":253}},"tokens_in":429,"tokens_out":311,"duration_ms":3963,"temperature":1.0,"reasoning_tokens":253,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T16:36:55.371148+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A reader can falsify the global theorem by taking $S$ to be the unit circle, $P = (1-x_1)x_3^4 + 4x_2 x_3^3 + (2+6x_1)x_3^2 - 4x_2 x_3 + (1-x_1)$, and computing that the discriminant is $2^{14}(x_1^2+x_2^2-1)^2(x_1^2+x_2^2)$, which is order-invariant on $S$, while the projective zero set is connected yet would have to split into two closed graphs if projective delineability held.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines cylindrical algebraic decomposition and the original delineability notion that this paper relaxes."},{"cited_title":"McCallum","cited_arxiv_id":null,"evidence_quote":"Supplies the classical delineability theorem and analytic delineability framework on analytic submanifolds."},{"cited_title":"McCallum","cited_arxiv_id":null,"evidence_quote":"Provides the improved projection operation and the delineability theorem that the local proof applies after transforming the polynomial."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Gives the improved projection whose leading coefficients are exactly what projective delineability lets algorithms omit."},{"cited_title":"McCallum","cited_arxiv_id":null,"evidence_quote":"Provides the result on order-invariance of resultants for products of delineable polynomials that Theorem 3 extends to the projective setting."},{"cited_title":"Nalbach, E","cited_arxiv_id":null,"evidence_quote":"Describes the single-cell CAD construction whose projection set projective delineability is designed to reduce."},{"cited_title":"Fulton.Algebraic Topology: A First Course","cited_arxiv_id":null,"evidence_quote":"Supplies the theorem that every covering of a simply connected space is trivial, used in the proof of the global result."},{"cited_title":"Gelfand, M","cited_arxiv_id":null,"evidence_quote":"Provides the standard resultant and discriminant transformation laws under linear change of variables used in Lemma 1 and Proposition 1."}],"review_version":1}