{"id":"a96d6aef-3d4e-42d4-a895-121076b72460","arxiv_id":"2607.05701","paper_version":2,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Definable functions in FO(Z,+,≤), FO(R,+,≤) and FO(R,Z,+,≤) are exactly the piecewise-linear or piecewise-simple functions, and mixed sets coincide with semi-polinear sets.","lead":"The paper proves that functions definable in integer, real, and mixed additive arithmetic are exactly the piecewise-linear or piecewise-simple functions, and that mixed-definable sets are the semi-polinear sets. These pure algebraic characterizations unify three classical decidable theories and correct an earlier error on mixed sets.","discovery_kind":"unification","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified","rationale":"The reader correctly identifies Ginsburg–Spanier plus the stability lemma as the sole external pillars. Both are classical and are used only as black boxes whose conclusions are applied verbatim; the paper’s own contributions (piecewise-linear and piecewise-simple normal forms, semi-polinear sets, and the monoid correction) are self-contained algebraic arguments that introduce no free parameters or unstated hypotheses. The concrete verification step above simply reconfirms the elementary linear-algebra step that is common to all three function theorems; a successful check leaves the ACCEPT verdict and high confidence untouched.","tokens_in":13716,"tokens_out":502,"duration_ms":5749,"concrete_test":"Independently re-derive the matrix M of Proposition 3.1 for the concrete stable monoid graph generated by {(2,1),(0,1)} (domain 2N, f(2k)=k) without invoking the general basis argument; if the same rational slope is recovered, the stability lemma is confirmed for the integer case that feeds Theorems 4.2 and 5.9.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claims rest on the classical Ginsburg–Spanier theorem (Theorem 4.1) and the elementary stability lemma (Proposition 3.1). Both are standard and correctly applied: for FO(Z,+,≤) the graph is semi-linear, reduced via Lemma 2.1 to a single linear set, then translated to a stable monoid graph to which Prop. 3.1 yields a rational matrix; for FO(R,+,≤) the same stability argument is combined with density of Q-points inside polyhedra (Prop. 3.3). For the mixed theory the semi-polinear characterisation (Thm. 5.4) is proved by structural induction on FO(R,Z,R≥0,G+), with the only non-trivial base case (the addition relation) handled by an explicit finite decomposition into polinear pieces; the function case (Thm. 5.9) then extracts the fractional and integer parts separately, using a short linear-algebra argument that P⊥ cannot lie in Q^n\times{0}. No hidden assumption, circularity or gap appears. The correction of Weispfenning’s monoid-versus-group error is accurate.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The paper extends the Ginsburg–Spanier theorem from sets to functions and from pure integer/real additive theories to the mixed theory FO(R,Z,+,≤). It proves that FO(Z,+,≤)- and FO(R,+,≤)-definable functions are exactly the piecewise-linear functions (Theorems 4.2 and 3.4), introduces semi-polinear sets and shows they coincide with mixed-linear sets (Theorem 5.4), and characterises FO(R,Z,+,≤)-definable functions as the piecewise-simple functions (Theorem 5.9). All arguments are purely algebraic, relying on a stability lemma (Proposition 3.1), density of rationals in polyhedra, Fourier–Motzkin elimination, and the classical Ginsburg–Spanier theorem; an error in Weispfenning’s description of mixed-linear sets of R is corrected (Remark 5.5).","tokens_in":13994,"tokens_out":673,"duration_ms":6901,"significance":"If correct, the results supply the missing algebraic row of the comparison table for the three classical additive theories and give clean, logic-free normal forms (piecewise linear / piecewise-simple) that are immediately usable in verification, synthesis and constraint solving. The proofs are short, self-contained and free of automata or quantifier-elimination machinery; the correction of the monoid-versus-group error in Weispfenning is a genuine service to the literature. The notions of semi-polinear set and piecewise-simple function are new and natural. The work therefore unifies three well-studied decidable theories under a single geometric framework and fills a surprising gap that had remained open despite decades of related automata-theoretic and logical characterisations.","major_comments":[],"minor_comments":[{"comment":"In the proof of Theorem 5.9 the extraction of the integer-part function h relies on a short linear-algebra argument that P⊥ cannot lie inside Q^n × {0}. A one-sentence remark that the same conclusion follows from the fact that the projection of a monoid graph that is a function must itself be a monoid would make the argument even more transparent.","section":null},{"comment":"Table 1 lists “semi-polinear” and “piecewise-simple” in bold as contributions of the paper; it would be helpful to add a footnote or parenthetical citation to the corresponding theorems so that a reader scanning the table can jump directly to the statements.","section":null},{"comment":"The open problem on FO(Z,+,Vp)-definable functions is interesting; a one-line pointer to the known automata or logical characterisations of Büchi arithmetic would orient the reader.","section":null},{"comment":"A few minor typographical inconsistencies appear (e.g., “polinear” vs. “polylinear” in informal prose, spacing around “FO(R,Z,+,≤)”). They do not affect readability but should be cleaned in the final version.","section":null}],"recommendation":"accept","confidential_remarks":"The manuscript is a substantially revised 2008 draft; the authors are transparent about LLM assistance for writing and verification. The technical content is solid and the novelty claim (first explicit algebraic statement of the function characterisations) appears justified. Fit for LMCS is excellent."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The punchline is simple: Finkel and Leroux give explicit geometric normal forms for the functions (not just the sets) of FO(Z,+,≤), FO(R,+,≤) and FO(R,Z,+,≤). Presburger and real-additive functions are exactly the piecewise-linear ones; mixed functions are the new “piecewise-simple” class (linear separately on fractional and integer parts, possibly with different slopes). They also introduce semi-polinear sets and prove they coincide with the mixed-definable sets, correcting Weispfenning’s monoid-versus-group slip on R.\n\nWhat is actually new is the packaging and the mixed case. Applying Ginsburg–Spanier to the graph of a Presburger function and reading off linearity was always available; nobody wrote the theorem with a direct algebraic proof. The real case is similar once you have density of rational points in polyhedra. The mixed material is the real contribution: the semi-polinear definition, the structural-induction proof that mixed sets are exactly those, the extraction of simple pieces for functions, and the explicit fix of Weispfenning. All of it is done with linear algebra, Fourier–Motzkin and Ginsburg–Spanier; no automata, no QE black boxes beyond the classical ones.\n\nThe proofs are short and look solid. The stability lemma (stable rational graph implies linear) is elementary and correctly applied; the mixed-function argument that the integer part cannot have a non-trivial kernel in the last coordinate is clean. Soft spots are minor: the paper is candid that the integer and real function results were “implicit,” the significance is inside the subfield rather than a new decision procedure, and the open problem on Büchi arithmetic is left open. None of that undercuts the claims.\n\nThis is for people who work with Presburger, real or mixed linear arithmetic in verification, synthesis or constraint solving and want geometric normal forms they can actually use. It deserves a serious referee; I would accept it for peer review and I would cite the mixed characterisations and the Weispfenning correction. Bring it to reading group if the group cares about additive theories or geometric model theory of arithmetic.","headline":"Clean algebraic normal forms for functions in three additive theories, plus a real correction of Weispfenning; short, elementary, and worth citing.","tokens_in":14574,"tokens_out":539,"would_cite":true,"duration_ms":5033,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B25","03C10","68Q60"],"pacs":[],"model":"grok-4.5","headline":"Definable functions in the three classical additive theories are exactly the piecewise-linear and piecewise-simple functions, characterized purely algebraically.","keywords":["Presburger arithmetic","semi-linear sets","piecewise linear functions","mixed real-integer arithmetic","semi-polinear sets","piecewise-simple functions","additive theories","Ginsburg–Spanier theorem"],"falsifier":"Exhibit a function whose graph is definable by a first-order formula using only addition and order over Z (or R, or R and Z) but that fails to be piecewise linear (or piecewise-simple) on any finite definable partition of its domain, or exhibit a mixed-definable set that is not a finite union of polinear sets.","tokens_in":14603,"feed_emoji":"➕","tokens_out":743,"duration_ms":6075,"temperature":0.7,"pith_summary":"This paper gives a single geometric picture of the sets and functions that can be defined using only addition and order, over the integers, over the reals, and over both at once. It starts from the classical Ginsburg–Spanier theorem (definable integer sets are the semi-linear sets) and extends it in two directions. First, the functions definable over the integers or over the reals are exactly the piecewise-linear functions on a definable partition of the domain. Second, for the mixed theory that talks about both reals and integers, the definable sets are exactly the new semi-polinear sets (a polyhedral fractional piece plus a semi-linear integer piece), and the definable functions are exactly the piecewise-simple functions that treat the integer and fractional parts of each argument with independent linear coefficients. The proofs use only linear algebra and a short stability lemma, with no automata or quantifier-elimination machinery, and they also correct an earlier incomplete description of the mixed sets. A sympathetic reader cares because the three theories now sit in one clean algebraic framework that can be used directly in verification, constraint solving, and synthesis.","feed_headline":"Additive logics define only piecewise-linear functions","feed_subtitle":"Three classical theories of addition and order get a single algebraic description of their sets and functions","key_machinery":"Semi-polinear sets (a polyhedral convex piece in the unit cube plus a finitely generated monoid of integer vectors) together with the stability lemma that any additive function whose graph lies in rational vectors is linear; these objects turn the classical Ginsburg–Spanier theorem into function and mixed-arithmetic characterisations.","core_discovery":"The paper proves that FO(Z,+,≤)-definable functions are exactly the FO(Z,+,≤)-piecewise linear functions, that FO(R,+,≤)-definable functions are exactly the FO(R,+,≤)-piecewise linear functions, that FO(R,Z,+,≤)-definable sets are exactly the semi-polinear sets, and that FO(R,Z,+,≤)-definable functions are exactly the piecewise-simple functions.","pith_inferences":[],"forward_implications":[],"fun_headline_variants":["Ginsburg-Spanier lifts to piecewise-linear functions over Z and R","FO(Z,+) and FO(R,+) define exactly the piecewise-linear functions","Mixed FO(R,Z,+) sets equal semi-polinear; functions are piecewise-simple","Algebraic proofs unify definable sets and functions across three additive FO theories","Additive theories FO(Z,+), FO(R,+) and mixed yield piecewise-linear and simple maps"],"cache_read_input_tokens":0,"weakest_assumption_plain":"The whole argument treats the classical Ginsburg–Spanier theorem (integer-definable sets are semi-linear) as a black box; any gap there would immediately break the function and mixed characterisations.","fun_headline_variants_meta":{"raw":{"variants":["Ginsburg-Spanier lifts to piecewise-linear functions over Z and R","FO(Z,+) and FO(R,+) define exactly the piecewise-linear functions","Mixed FO(R,Z,+) sets equal semi-polinear; functions are piecewise-simple","Algebraic proofs unify definable sets and functions across three additive FO theories","Additive theories FO(Z,+), FO(R,+) and mixed yield piecewise-linear and simple maps"]},"model":"grok-4.5","effort":"low","cost_usd":0.005616,"raw_usage":{"total_tokens":1548,"prompt_tokens":870,"num_sources_used":0,"completion_tokens":117,"cost_in_usd_ticks":56160000,"prompt_tokens_details":{"text_tokens":870,"audio_tokens":0,"image_tokens":0,"cached_tokens":128},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":561,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":870,"tokens_out":117,"duration_ms":6323,"temperature":1.0,"reasoning_tokens":561,"cache_read_input_tokens":128,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-11T03:28:25.341219+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Exhibit a function whose graph is definable by a first-order formula using only addition and order over Z (or R, or R and Z) but that fails to be piecewise linear (or piecewise-simple) on any finite definable partition of its domain, or exhibit a mixed-definable set that is not a finite union of polinear sets.","supporting_citations":[],"review_version":1}