{"id":"5759d0a4-9cce-478c-bcc1-53d637b99386","arxiv_id":"2506.13673","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A class of structures recognizes coordinates in reduced products if and only if the formula x=x' -> y=y' is equivalent to an h-formula in the common theory of the class.","lead":"This paper shows that a class of mathematical structures has a strong coordinate-rigidity property in reduced products exactly when one simple equality formula has a special syntactic form, called an h-formula. The authors then use this test to determine which families of groups, including symmetric groups, simple groups, and free products, have the property.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Proposition 3.5 relies on a false saturation claim: under CH, not every nonprincipal ultrafilter on N yields ℵ1-saturated ultrapowers; the subsequent absoluteness transfer inherits this gap.","rationale":"The reader's verdict flagged the forcing absoluteness transfer as the weakest assumption. Close reading shows the deeper fragility is one step earlier: the CH-case in Proposition 3.5 already contains a false universal claim about arbitrary nonprincipal ultrafilters. Since Lemma 3.6 is designed to eliminate CH and cardinality bounds by forcing, it can only succeed if the CH-case is actually proved; otherwise the absoluteness transfer has nothing to transfer. This is load-bearing because Proposition 3.5 is the unique implication (2)→(4) in Theorem 3.8, and Theorem 3.8 is the paper's central equivalence (recognizing coordinates ↔ h-formula condition). The gap is concrete and testable, and it is plausibly repairable by selecting an ℵ1-good ultrafilter, so the appropriate verdict remains conditional rather than rejection.","tokens_in":48471,"tokens_out":31547,"duration_ms":303956,"concrete_test":"Inspect the proof of Proposition 3.5 and check whether replacing 'a nonprincipal ultrafilter U' by 'an ℵ1-good nonprincipal ultrafilter U' (which exists under CH) makes the saturation claim true and preserves the rest of the Beth-definability argument. Alternatively, verify the original claim by exhibiting a nonprincipal ultrafilter on N that is not ℵ1-good under CH and a structure of size ≤ continuum whose ultrapower by it is not ℵ1-saturated; if such a counterexample exists, the proof needs the ℵ1-good choice.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The proof of the main implication (2)→(4) of Theorem 3.8 is Proposition 3.5. In the CH-case, after fixing a nonprincipal ultrafilter U on N, the authors assert: 'If CH holds and all M_i as well as N have cardinality no greater than 2^{ℵ0}, then the ultrapowers ś_U(N,s1), ś_U(M,supp), and ś_U(N,s2) have cardinality 2^{ℵ0} and are ℵ1-saturated.' This is false for an arbitrary U. ℵ1-saturation of ultrapowers of structures of size ≤ continuum requires U to be ℵ1-good (or at least sufficiently regular/good); CH guarantees the existence of such ultrafilters but does not make every nonprincipal ultrafilter on N ℵ1-good. Since a specific U is never chosen afterwards, the existence of the isomorphisms σ and τ in (3.3) is not justified. The later removal of CH and cardinality restrictions via Lemma 3.6 exports this unproved claim to ZFC: Lemma 3.6 only transfers statements proved under ZFC+CH, and the proof of the CH-statement itself now has a gap. The theorem may be repairable by fixing an ℵ1-good ultrafilter under CH, but as written the argument for the central equivalence is incomplete.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper studies the notion, introduced in the authors' earlier work [10], of a class C of L-structures recognizing coordinates: every isomorphism between reduced products of structures in C is 'isomorphically coordinate respecting.' The central result, Theorem 3.8, gives for countable L and full C an equivalence between recognition of coordinates, recognition over N-indexed reduced products, uniform interpretability of the quotient Boolean algebra P(I)/I together with the quotient structures and projections, interpretability of the relative support function, and the purely syntactic condition that x=x' -> y=y' be equivalent to an h-formula in Th(C). From this the paper derives group-theoretic classifications (simple groups, symmetric groups, dihedral groups, free products, graph products, and others recognize coordinates; decomposable groups, nilpotent groups, and others do not), limiting examples showing failure of compactness, quantifier-elimination consequences, and rigidity corollaries under forcing axioms.","tokens_in":48679,"tokens_out":22342,"duration_ms":235464,"significance":"Should the main equivalence hold, this is a substantial conceptual result: it converts a semantic rigidity property of arbitrary reduced products into a first-order syntactic property of a single formula, and it explains and extends earlier rigidity results for quotients. The paper also contains useful tools: a detailed analysis of h-formulas, support-function definability, a folklore Feferman-Vaught reformulation, and an extensive catalogue of group-theoretic examples and non-examples. The limiting examples in Theorem 7.1 are particularly informative. A notable strength is that the paper gives explicit h-formulas for many of the positive group examples, making the criterion concrete. However, the proof of the main implication (2)->(4) in Theorem 3.8 contains a false saturation assertion and a terse absoluteness transfer; because this implication is load-bearing for the rest of the paper, the manuscript requires revision before the central claim can be regarded as established.","major_comments":[{"comment":"The proof of Proposition 3.5 asserts: 'If CH holds and all M_i as well as N have cardinality no greater than 2^{aleph0}, then the ultrapowers U(N,s1), U(M,supp), and U(N,s2) have cardinality 2^{aleph0} and are aleph1-saturated.' This is not true for an arbitrary nonprincipal ultrafilter U on N. Aleph1-saturation of an ultrapower requires U to be aleph1-good (or at least sufficiently good); CH guarantees the existence of such ultrafilters but does not make every nonprincipal ultrafilter on N aleph1-good. Since no particular U is chosen afterwards, the existence of the isomorphisms sigma and tau in (3.3) is not justified. Consequently the Beth-definability argument for support definability under CH is incomplete, and because Lemma 3.6 transfers only statements actually proved under ZFC+CH, this gap propagates to the ZFC conclusion and to implication (2)->(4) of Theorem 3.8. The argument is likely repairable by fixing an aleph1-good nonprincipal ultrafilter on N in the CH case and checking the cardinality conditions, but as written this load-bearing step is not proved.","section":"3.2, Proposition 3.5"},{"comment":"The removal of the cardinality restrictions is left as a sketch with a footnote. The Beth argument proves support definability only for reduced products whose factors and the auxiliary elementary extension N satisfy |M_i| <= 2^{aleph0} and |N| <= 2^{aleph0}; the statement theta_psi transferred by Lemma 3.6 has no such restriction. The text says that the Feferman-Vaught theorem makes C closed under elementary equivalence and then applies Lemma 3.6, but it does not spell out why the restricted CH statement suffices for a fixed M after the Levy collapse, nor how an arbitrary elementary extension N is replaced by one of size at most 2^{aleph0} (for instance, by passing to a small elementary substructure containing the finitely many parameters under consideration). Without this, the ZFC transfer of the main implication is not fully verifiable.","section":"3.2, end of Proposition 3.5 and Lemma 3.6"}],"minor_comments":[{"comment":"In the proof of item (b), the reference to 'Theorem 5.1 (2)' appears incorrect: the case of a nontrivial homomorphism into a center is condition (1) of Theorem 5.1, while condition (2) concerns decomposable products.","section":"5.2, proof of Theorem 5.3"},{"comment":"The proof begins 'Let Let G' with a duplicated word; this should be corrected.","section":"4.6, proof of Proposition 4.28"},{"comment":"The sentence 'This is clearly a preorder: for all x,y,z in M x<y<z' has garbled notation; the intended statement is the transitivity of the relation defined by the displayed formula.","section":"7.4, Proposition 7.6"},{"comment":"Lemma 7.10 is stated for arbitrary groups G and H, but its proof uses saturation of the reduced power of Z(H) over Fin via [9, Theorem 1], which in the introduction is applied to reduced products of countable structures; the cardinality hypotheses needed for the cited theorem should be stated.","section":"7.4, Lemma 7.10"}],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Bo,\n\nHere is my take on arXiv:2506.13673. The paper is working on a real problem and the main characterization (Theorem 3.8) is probably true, but the proof as written has a gap that is not cosmetic.\n\nWhat is new and good: the equivalence between coordinate recognition and the h-formula condition is exactly the bridge that was missing; the authors' earlier paper only expressed hope for it. The corollary that recognizing coordinates is a property of Th(C) is clean. The group examples are genuinely interesting, especially the quasisimple and free product cases, and the failure-of-compactness construction in Theorem 7.1 is a nice surprise. The paper is readable and honest about what is deferred to references.\n\nThe soft spot is Proposition 3.5, which proves implication (2)->(4) of Theorem 3.8. In the CH step the authors fix an arbitrary nonprincipal ultrafilter U on N and assert that the ultrapowers of N and M by U are ℵ1-saturated. That is false: saturation of ultrapowers requires U to be ℵ1-good (or at least sufficiently regular). CH only guarantees that some such ultrafilter exists; it does not make every nonprincipal ultrafilter ℵ1-good. Since the rest of the argument does not choose U, the isomorphisms σ and τ are not justified. The later absoluteness transfer (Lemma 3.6) exports this gap to ZFC, so the main equivalence is not fully proved as written. I think it is repairable: choose an ℵ1-good U under CH, or use saturated elementary extensions as in the uncountable-language case, but the present text needs that fix.\n\nThe group theorems depend on external results, but the citations look appropriate. I found no circularity. The non-compactness result is surprising and worth checking. The quantifier-elimination applications are a bonus.\n\nVerdict: this paper deserves a serious referee. The main theorem is important enough that one round of revision to close the gap is reasonable. I would send it to a good model theory/set theory referee, not desk reject.","headline":"Main characterization likely true but proof of Proposition 3.5 has a false saturation claim; needs a fix before the theorem is fully established.","tokens_in":49291,"tokens_out":3605,"would_cite":false,"duration_ms":33930,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03C50","03C20","03E35","03C10","03E65","03E75"],"pacs":[],"model":"deepseek-v4-flash","headline":"Reduced-product rigidity reduces to one first-order formula","keywords":["coordinate recognition","reduced products","h-formulas","relative support function","rigidity of quotient structures","trivial isomorphisms","quantifier elimination","groups"],"falsifier":"Take $\\mathcal{C}=\\{S_3,\\mathrm{SL}(2,5)\\}$. The paper proves that any class containing both groups does not recognize coordinates; if a syntactic search over h-formulas of increasing quantifier depth in $\\mathrm{Th}(\\mathcal{C})$ produced an h-formula equivalent to $x=x'\\rightarrow y=y'$, then Theorem 3.8's equivalence between coordinate recognition and the syntactic condition would be refuted. More directly, inspect the proof of Proposition 3.5 for the class of all linear orders without endpoints: the paper supplies an explicit h-formula for $x=x'\\rightarrow y=y'$, so the definability of the support function in every reduced product over $\\mathbb{N}$ is directly checkable, and any ideal on $\\mathbb{N}$ where that definability failed would falsify the main theorem.","tokens_in":48223,"feed_emoji":"🧩","tokens_out":9889,"duration_ms":94380,"temperature":0.7,"pith_summary":"This paper is about when reduced products—quotients of direct products by an ideal on the index set—are rigid enough that every isomorphism between them must preserve coordinates. The main result is that, for a broad class of structures, this rigidity is not just a set-theoretic accident: it holds exactly when the formula $x=x'\\rightarrow y=y'$ is equivalent to an h-formula in the common theory of the class. That syntactic condition is equivalent to every reduced product interpreting its own quotient Boolean algebra together with the relative support function, and it unifies previous rigidity theorems for reduced products. If the characterization is right, coordinate recognition is a first-order property of a theory, so it can be checked once and then yields forcing-axiom rigidity and quantifier-elimination corollaries for entire classes of groups and other structures.","feed_headline":"One formula decides when reduced products are rigid","feed_subtitle":"The test is whether one equality implication is an h-formula; if yes, quotient-product rigidity follows.","key_machinery":"The load-bearing object is the relative support function, which sends a pair of elements of a reduced product to the set of coordinates on which they differ modulo the ideal. The syntactic side is the class of h-formulas: the smallest class of formulas containing the atomic formulas and closed under conjunction, existential and universal quantification, and the operation $(\\exists x)\\varphi\\wedge(\\forall x)(\\varphi\\rightarrow\\psi)$. These formulas have the property that their truth in a reduced product is decided by a 'large' set of coordinates, which lets a single h-formula express the inclusion of supports. The proof that recognizing coordinates forces the support function to be definable runs through saturated ultrapowers: under the Continuum Hypothesis two elementarily equivalent saturated ultrapowers of the reduced product give an automorphism that must respect coordinates, and an absoluteness argument removes the CH and cardinality assumptions. The converse direction interprets the quotient Boolean algebra from the definable support relation and then reads off the coordinate-respecting quotient maps.","core_discovery":"The paper's central claim is Theorem 3.8: for a countable language $L$ and a full class $\\mathcal{C}$ of $L$-structures, the following are equivalent: $\\mathcal{C}$ recognizes coordinates; $\\mathcal{C}$ recognizes coordinates when the index set is restricted to $\\mathbb{N}$; every reduced product over an arbitrary ideal interprets the quotient Boolean algebra together with all quotient maps; every such reduced product interprets the Boolean algebra together with the relative support function; the formula $x=x'\\rightarrow y=y'$ is equivalent to an h-formula in $\\mathrm{Th}(\\mathcal{C})$; and the formula $x=z\\rightarrow y=z$ is equivalent to an h-formula in $\\mathrm{Th}(\\mathcal{C})$. In the authors' framing, this makes 'recognizes coordinates' a first-order syntactic property of a single formula, rather than a property that has to be checked product-by-product. For uncountable languages, the equivalence between recognizing coordinates and the semantic conditions (3)–(5) remains intact. The theorem also implies that recognizing coordinates is preserved by passing from $\\mathcal{C}$ to the class of all models of $\\mathrm{Th}(\\mathcal{C})$.","pith_inferences":["Editorial inference: because the characterization is stated at the level of $\\mathrm{Th}(\\mathcal{C})$, coordinate recognition is invariant under elementary equivalence of the underlying class; this suggests the dividing line, if one exists, should be visible in the lattice of interpretable quotients of a single saturated model of $\\mathrm{Th}(\\mathcal{C})$.","Editorial inference: the paper's $|L|$-compactness result suggests that checking recognition on subclasses of size $|L|$ is sufficient; a natural testable strengthening would be to ask whether the witnessing h-formula can always be chosen uniformly from a fundamental set of formulas for $\\mathrm{Th}(\\mathcal{C})$.","Editorial inference: the failure of compactness in Theorem 7.1 indicates that coordinate recognition does not behave like a stable first-order property under unions of theories; it may be more natural to study it as a property of theories in the interpretability lattice, where the non-recognizing union phenomenon corresponds to conflicting support definitions."],"forward_implications":["For every class that recognizes coordinates, the forcing axioms used in the paper imply that any isomorphism between reduced products over the ideal of finite sets is trivial: it is lifted by a bijection between cofinite sets and coordinatewise isomorphisms.","In particular, every automorphism of the reduced product of finite symmetric groups $S_n$ for $n\\geq 3$ over the finite-set ideal lifts to an automorphism of the ordinary product, and analogous lifting holds for reduced products of $\\mathrm{SL}(n,F)$ with $|F|\\geq 4$, free products, and graph products covered by Theorem 4.6.","Reduced products whose class recognizes coordinates admit the full quantifier-elimination language from the classical reduced-product theorem as a definable expansion once a fundamental set of h-formulas exists; explicit definable quantifier elimination is obtained for reduced powers of $S_n$ with $n\\geq 4$ and $n\\neq 6$, and for $S_3$.","The property is theory-level: a full class $\\mathcal{C}$ recognizes coordinates exactly when the class of all models of $\\mathrm{Th}(\\mathcal{C})$ does, and every model of the theory of an atomless reduced product 'thinks' it is a reduced product with a definable support structure.","Many concrete classes of groups recognize coordinates—simple groups, finite symmetric groups of degree at least 3, odd dihedral groups, $\\mathrm{SL}(n,F)$ for $n\\geq 2$ and $|F|\\geq 4$, all nontrivial free products, and graph products with connected complement—so the rigidity and quantifier-elimination corollaries apply uniformly to these classes."],"supporting_citations":[{"why":"Introduces the notion of recognizing coordinates and proves the forcing-axiom rigidity theorem that motivates the characterization; the paper extends its definition and uses it as the target equivalence.","marker":"[10]"},{"why":"Shows stable reduced products over the finite-set ideal are saturated, providing non-recognition examples and motivating the countability and size restrictions that the absoluteness step must remove.","marker":"[9]"},{"why":"Identifies definability of the support function as a key property in non-reduced products; the paper extends this analysis to arbitrary reduced products.","marker":"[33]"},{"why":"Supplies the definition and basic preservation theorem for h-formulas, the syntactic class used in the characterization.","marker":"[38]"},{"why":"Provides later development of h-formulas and the reduced-product preservation theorem that underlies the equivalence with the support function.","marker":"[40]"},{"why":"The standard reference for the quantifier-elimination theorem for reduced products, used to reformulate quantifier elimination and to compare truth in reduced products.","marker":"[5]"},{"why":"Proves that statements provable in ZFC plus the Continuum Hypothesis are provable in ZFC, the absoluteness transfer used to remove CH from the definability proof.","marker":"[43]"},{"why":"Cited for the saturation and absoluteness background that lets the proof pass from structures of size at most the continuum to arbitrary cardinalities.","marker":"[23]"},{"why":"Provides non-isomorphic ultrapowers of elementarily equivalent countable structures, explaining why the proof invokes forcing and absoluteness.","marker":"[46]"}],"fun_headline_variants":["One formula decides coordinate recognition","Syntactic test for coordinate recognition","Coordinate recognition reduces to a single h-formula","Rigidity of reduced products hinges on one formula","h-formula equivalence marks coordinate recognition"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that a statement about all reduced products over $\\mathbb{N}$ proved using the Continuum Hypothesis and saturated ultrapowers remains valid in ordinary ZFC; the paper cites this absoluteness transfer instead of writing it out, and the equivalence between coordinate recognition and the syntactic h-formula condition stands on it.","fun_headline_variants_meta":{"raw":{"variants":["One formula decides coordinate recognition","Syntactic test for coordinate recognition","Coordinate recognition reduces to a single h-formula","Rigidity of reduced products hinges on one formula","h-formula equivalence marks coordinate recognition"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000381,"raw_usage":{"total_tokens":2028,"prompt_tokens":959,"completion_tokens":1069,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":575,"completion_tokens_details":{"reasoning_tokens":1005}},"tokens_in":575,"tokens_out":1069,"duration_ms":8233,"temperature":1.0,"reasoning_tokens":1005,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T19:58:19.656291+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take $\\mathcal{C}=\\{S_3,\\mathrm{SL}(2,5)\\}$. The paper proves that any class containing both groups does not recognize coordinates; if a syntactic search over h-formulas of increasing quantifier depth in $\\mathrm{Th}(\\mathcal{C})$ produced an h-formula equivalent to $x=x'\\rightarrow y=y'$, then Theorem 3.8's equivalence between coordinate recognition and the syntactic condition would be refuted. More directly, inspect the proof of Proposition 3.5 for the class of all linear orders without endpoints: the paper supplies an explicit h-formula for $x=x'\\rightarrow y=y'$, so the definability of the support function in every reduced product over $\\mathbb{N}$ is directly checkable, and any ideal on $\\mathbb{N}$ where that definability failed would falsify the main theorem.","supporting_citations":[{"cited_title":"De Bondt, I","cited_arxiv_id":null,"evidence_quote":"Introduces the notion of recognizing coordinates and proves the forcing-axiom rigidity theorem that motivates the characterization; the paper extends its definition and uses it as the target equivalence."},{"cited_title":"Saturation of reduced products","cited_arxiv_id":"2401.12539","evidence_quote":"Shows stable reduced products over the finite-set ideal are saturated, providing non-recognition examples and motivating the countability and size restrictions that the absoluteness step must remove."},{"cited_title":"Medvedev and A","cited_arxiv_id":null,"evidence_quote":"Identifies definability of the support function as a key property in non-reduced products; the paper extends this analysis to arbitrary reduced products."},{"cited_title":"Palmgren","cited_arxiv_id":null,"evidence_quote":"Supplies the definition and basic preservation theorem for h-formulas, the syntactic class used in the characterization."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides later development of h-formulas and the reduced-product preservation theorem that underlies the equivalence with the support function."},{"cited_title":"Chang and H.J","cited_arxiv_id":null,"evidence_quote":"The standard reference for the quantifier-elimination theorem for reduced products, used to reformulate quantifier elimination and to compare truth in reduced products."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Proves that statements provable in ZFC plus the Continuum Hypothesis are provable in ZFC, the absoluteness transfer used to remove CH from the definability proof."},{"cited_title":"Halevi and I","cited_arxiv_id":null,"evidence_quote":"Cited for the saturation and absoluteness background that lets the proof pass from structures of size at most the continuum to arbitrary cardinalities."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides non-isomorphic ultrapowers of elementarily equivalent countable structures, explaining why the proof invokes forcing and absoluteness."}],"review_version":2}