{"id":"bfba3b5c-1d41-4836-95f2-a746827881c1","arxiv_id":"2511.07774","paper_version":3,"verdict":"REJECT","confidence":"HIGH","novelty_score":3.0,"correctness_risk":"high","formal_verification":"none","parameter_count":2,"one_line_summary":"Claims a realizability barrier prevents Heyting Arithmetic from uniformly extracting prime witnesses, making Goldbach-type theorems constructively unrealizable; the barrier fails because primality is decidable by bounded search.","lead":"This paper argues that primality cannot be constructively converted into explicit witnesses, and claims this blocks any constructive proof of Goldbach-type conjectures in Heyting Arithmetic. The argument collapses because primality is decidable by bounded search — the paper's own abstract and final section say so.","discovery_kind":"unclear","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Barrier rests on misclassifying bounded primality as a genuinely unbounded Π1 predicate; the paper's own abstract and §8 contradict this, so the central realizability barrier never touches primes.","rationale":"The reader's weakest_assumption is exactly this: primality's classification as a nontrivial Π1 predicate. I agree. The misclassification is not cosmetic; it is cited in the Remark after Def 2.7 and used in every theorem that claims HA cannot uniformize prime witnesses. A correct proof that bounded formulas are decidable in HA is standard (e.g., Troelstra–van Dalen), and the paper's own §8 concedes the point. Therefore the barrier result, even if true for genuinely undecidable Π1 predicates, has no instance at primes. The verdict should remain REJECT; no new objection beyond the reader's is needed, but the concern is real and load-bearing.","tokens_in":17509,"tokens_out":10194,"duration_ms":111088,"concrete_test":"Formalize the formula PrimeΠ from Def 2.7 in a proof assistant (e.g., Coq, Lean, or Agda) and prove ∀n, PrimeΠ(n)∨¬PrimeΠ(n) using induction on the bound n. Then define the bounded-search function f(n)=μp≤n (PrimeΠ(p) ∧ PrimeΠ(n−p)) and observe that it is primitive recursive. If the decidability proof succeeds, the paper's premise 'PrimeΠ is constructively undecidable' is refuted, and the uniform realizability barrier cannot apply to GC*Π.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that no total term of system T can realize Π1(n) ⇒ ∃yΣ1(n,y), and hence that GC*Π, even if true in N, has no total Σ1 constructor in HA. The load-bearing premise is that PrimeΠ, as defined in Def 2.7/2.10, is a genuinely unbounded Π1 predicate requiring universal reflection and not decidable in HA. This premise is false: the definition is n>1 ∧ ∀a,b≤n(a·b=n ⇒ a=1∨b=1), with only bounded quantifiers. In HA every bounded formula is decidable by induction on the bound, so HA proves PrimeΠ(n)∨¬PrimeΠ(n) for each n. The paper itself says the opposite in its abstract ('both searches are bounded, both predicates are decidable') and in §8 (8.110) ('Such predicates are Δ0 because all quantifiers range over explicit finite domains'), contradicting the Remark after Def 2.7. All barrier results (Theses 2.5/2.6, Prop 4.7, Thm 6.5, §7.1) reach primes only through this classification. Without it there is no generic normalization obstruction: if GC*Π holds in N, the function f(n)=least p≤n with p and n−p prime is primitive recursive (bounded search plus decidable primality test), so a total Σ1 extractor exists; the real issue is merely whether HA proves GC*Π, not a universal realizability barrier.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper claims to establish a proof-theoretic barrier: no total functional in Heyting Arithmetic (HA) can uniformly transform Π₁ primality predicates into explicit Σ₁ witnesses, so that the constructive Goldbach principle, even if true in ℕ, has no uniform realizer in HA. The argument is built on a classification of primality as a genuinely unbounded Π₁ predicate (Definition 2.7, Remark after Definition 2.7, Thesis 2.5/2.6) and on several non-uniformization and diagonalization principles. The paper also includes geometric, forcing, and analytic interpretations of this claimed barrier.","tokens_in":1780,"tokens_out":1769,"duration_ms":39133,"significance":"If the central claim were correct, it would describe a fundamental logical obstruction to constructive proofs of prime conjectures, with consequences for proof theory and the philosophy of mathematics. However, the paper's own definition of primality is a bounded (Δ₀) formula, and the paper itself acknowledges this in the abstract and in Section 8 (8.110). Since HA proves decidability of every bounded formula, the central classification premise is false, and the claimed realizability barrier does not apply to primality as defined. Consequently, the paper's main result does not stand. The paper does contain useful reminders about boundedness of standardized primality tests, but these points are already standard and do not support the claimed barrier.","major_comments":[{"comment":"The load-bearing premise is that PrimeΠ(n) = n>1 ∧ ∀a,b≤n [a·b=n ⇒ a=1∨b=1] is a genuinely unbounded Π₁ predicate that is 'not constructively decidable' (Remark after Def. 2.7). This is false: all quantifiers in the displayed formula are bounded, so the formula is Δ₀. In HA every bounded formula is decidable by induction on the bound; hence HA proves PrimeΠ(n) ∨ ¬PrimeΠ(n) for each n. The paper itself contradicts this in the abstract ('both searches are bounded, both predicates are decidable') and in §8, (8.110), where primality is correctly described as Δ₀. Since Theses 2.5/2.6, Proposition 4.7, Theorem 6.5, and §7.1 all reach the primes only through this misclassification, the central claim collapses.","section":"Def. 2.7 and Remark; abstract; §8 (8.110)"},{"comment":"Prop. 4.5 asserts a non-uniform extraction theorem 'by [Friedman, 1975; Beeson, 1985]' to the effect that no total primitive recursive F can satisfy HA⊢∀n(∃y R(n,y) ⇒ R(n,F(n))) for Σ₁ R with Π₁ parameters. This is not a theorem of the cited works in the form used. More importantly, for a decidable (Δ₀) relation R, such an F does exist by bounded search. Thus the proposition is either misstated or vacuous. The same problem infects Theorem 4.10 and Corollary 6.4, which transfer the alleged constructive barrier to PA.","section":"Thesis 2.5/2.6; Prop. 4.5"},{"comment":"Lemma 4.6 attempts a diagonal argument against a Σ₁ predicate Dec(e,n,m) 'deciding' PrimeΠ(m). The step 'by the diagonal lemma there exists n_e such that PrimeΠ(n_e) ↔ ¬Dec(e,n_e,n_e)' conflates a formula with its Gödel number and presumes that primality is an undecidable semantic property. Since PrimeΠ is Δ₀ and decidable in HA, no such contradiction arises. The Rice-style analogy is also unsound: Rice's theorem concerns semantics of partial computable functions, not decidable arithmetical predicates. The same issue appears in §8, (8.111), where a non-uniformization theorem is invoked to assert the existence of primes beyond any machine's 'operational horizon'.","section":"Lemma 4.6; §8, (8.111)"},{"comment":"Theorem 5.9 claims that forcing over models of HA yields generic extensions M[G1] and M[G2] with M[G1]⊨GC*Π and M[G2]⊨¬GC*Π. This is not a legitimate use of forcing: forcing is a technique for set theory, not for Heyting Arithmetic, and the paper provides no formal definition of the forcing relation for HA or proof that the generic extensions preserve HA. Moreover, the later 'derivation' of the Euler product from Bekić's lemma (Logic 5.11, Theorem 5.18) is not a derivation within HA: it uses analytic convergence, classical manipulations, and an unproved fixed-point schema (Thesis 5.13). These sections are speculative and do not provide a rigorous alternative proof of the paper's central thesis.","section":"Thm. 5.9; §5.4–5.5"}],"minor_comments":[{"comment":"The notation is inconsistent: PrimeΠ is sometimes described as Π₁, sometimes as Π⁰₁, and sometimes as Δ₀ (e.g., Def. 2.7 vs. Def. 4.2 vs. §8, 8.110). This inconsistency is not merely cosmetic; it drives the central confusion.","section":"Throughout"},{"comment":"The Remark after Def. 2.7 invokes Markov's Principle and claims ¬¬Comp(n)→Comp(n) is not derivable in HA. For a bounded predicate Comp(n), HA does prove Comp(n) ∨ ¬Comp(n), independently of Markov's Principle. The remark should be corrected or removed.","section":"Def. 2.7, Remark"},{"comment":"The geometric translation is informal: 'Rect(a,b;n)' is asserted to be Δ₀ and locally decidable, but the intended relationship between the geometric configuration Γ(n) and the arithmetic equality A(PQRS)=n is never formally specified. Figures 2–6 are illustrative and do not constitute a proof.","section":"§3, Def. 3.4/3.5"},{"comment":"The claim that a Cantor-style diagonal argument on rational aspect ratios yields an 'irrational slope' corresponding to a prime is mathematically incoherent: the enumeration is countable and there is no uncountable space of 'potential divisive configurations' in arithmetic.","section":"§5.3, Heuristic 5.7"},{"comment":"The entropy–packing and 'cost of knowledge' heuristics introduce constants Φ and k without any derivation from the stated formalism. Equations (7.102)–(7.109) are heuristic analogies, not theorems, and should be clearly labeled as such if the paper is revised.","section":"§7.4–7.6"}],"recommendation":"reject","confidential_remarks":"The paper has a serious internal contradiction between its abstract and the Remark after Def. 2.7, and the main theorem is built on a classification of a bounded Δ₀ predicate as an unbounded Π₁ predicate. This is not a matter of presentation or of a small gap that could be patched; it undermines the central claim. The paper also cites standard works for non-uniformization theorems in a form that does not appear to exist. The speculative sections (forcing over HA, Euler product from fixed points, information-theoretic interpretations) do not meet the standards of a research article in mathematical logic. I see no path to a publishable version without a fundamental reconceptualization."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague — quick take on 2511.07774. The paper is not ready for the literature. Its central claim — that no HA-definable functional can uniformly turn Π1 primality evidence into Σ1 witnesses, hence that GC*Π is constructively obstructed — rests on a classification mistake. PrimeΠ as defined in Def 2.7 is bounded: ∀a,b≤n. That is Δ0, hence decidable in HA. The paper itself says so in the abstract ('both predicates are decidable') and in §8 (8.110), while the Remark after Def 2.7 says the opposite. That internal contradiction is fatal for the barrier: every barrier result in the paper walks through that classification.\n\nTo be fair, the geometric packing intuition is a nice way to picture divisors, and some observations are correct: trial division is bounded search, the Euler product follows from unique factorization, and Section 7 is honestly labeled heuristic. The author has read the relevant literature and is engaged with real material.\n\nBut the theorems in §§3–6 are asserted as results, and they don't hold up. Thesis 2.5/2.6 are postulates, not derived. Prop 4.5 cites [Friedman 1975; Beeson 1985] for a non-uniformization theorem those works do not contain. Gödel–Gentzen negative translation alone refutes Logic 6.3: every Π2 formula provable in PA is provable in HA, so if PA proves GC*Π then HA proves it. Thm 4.9's minimality argument is broken — adding the missing prime p to C gives a strict superset, contradicting minimality, but the proof treats that as a contradiction of the assumption that C had even coverage. Thm 5.9's forcing cannot change Σ1 facts about numerals in models of HA. The Φ-adic equilibrium in §5.4 is manufactured from a hand-posited recurrence.\n\nMy recommendation: desk reject. The valid content is standard textbook material, and the wrapping does not turn it into a genuine result. Not worth referee time, though a short note pointing out the Def 2.7/abstract contradiction might save the author from embarrassment.","headline":"A load-bearing misclassification of bounded primality as unbounded Π1 makes the paper's central realizability barrier false, and the paper contradicts its own abstract.","tokens_in":18459,"tokens_out":2227,"would_cite":false,"duration_ms":25070,"reading_group":"no","serious_thinker":"no","would_accept_peer_review":false},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03F50","03F55","11A41","11P32"],"pacs":[],"model":"deepseek-v4-flash","headline":"No total constructive functional can uniformly turn primality into explicit prime-sum witnesses in Heyting arithmetic.","keywords":["Heyting arithmetic","realizability","Goldbach conjecture","primality","Π1 predicates","BHK semantics","constructive proof theory","non-uniformization"],"falsifier":"Formalize trial division in HA: for a given numeral n, a primitive-recursive program checks every a from 2 to ⌊√n⌋ and decides whether a divides n; this is a finite, terminating computation over a bounded range. Since bounded quantification over numerals is provably decidable by induction in HA, the procedure decides the paper's own formula PrimeΠ(n) constructively, contradicting the claim that primality is a constructively undecidable Π1 predicate and thus removing the premise on which the barrier theorems rest.","tokens_in":17103,"feed_emoji":"🔢","tokens_out":7956,"duration_ms":81006,"temperature":0.7,"pith_summary":"The paper argues that the constructive status of prime conjectures is determined by realizability, not by the distribution of primes. Working in Heyting arithmetic under the BHK interpretation, it claims that no total functional can uniformly convert a Π1 primality judgment into explicit Σ1 witnesses, because such a conversion would violate strong normalization. Applied to a constructive Goldbach principle — every even number is a sum of two primes, with primality expressed by the bounded universal formula PrimeΠ — the conclusion is that even if the principle holds in the standard natural numbers, HA cannot supply a uniform constructor for the prime summands. If this is right, the difficulty of Goldbach's conjecture is a logical boundary of constructive definability, and HA, PA, and true arithmetic separate into three distinct layers.","feed_headline":"Primality blocks uniform Goldbach witnesses in constructive arithmetic","feed_subtitle":"Even if every even number is a sum of two primes, the paper argues no constructive proof can uniformly extract those primes.","key_machinery":"The load-bearing object is the bounded primality predicate PrimeΠ(n) ≡ n>1 ∧ ∀a,b≤n[a·b=n ⇒ a=1∨b=1], treated as a Π1 condition, together with the BHK reading of implication as a total functional. The argument's work is done by the thesis that any uniform realizer of Π1 ⇒ ∃yΣ1 would be a global Skolem function, and that such a function would contradict normalization in HA. The paper also builds a geometric packing semantics — composites are finite rectangles, primes are the universal absence of such rectangles — to make the local/global asymmetry vivid and to connect the logical barrier to bounded divisor schemata that can always miss composites with large factors.","core_discovery":"In the paper's own terms, the discovery is a realizability barrier: a proof in HA of statements of the form ∀x(φ(x)⇒∃yψ(x,y)) must yield a total, closed realizer t such that for every x, ψ(x,t(x)) holds. For primality, φ(n)=PrimeΠ(n) is classified as Π1 and compositeness as ∃ with Σ1 witness; the paper asserts there is no total primitive-recursive functional, and no closed term in any strongly normalizing typed λ-calculus adequate for HA, that uniformly transforms PrimeΠ evidence into such witnesses. Consequently the constructive Goldbach principle GC*Π has no total Σ1 constructor in HA, so even a classical proof of Goldbach would not give a constructive proof. The paper translates this into","pith_inferences":["Editorial inference: The paper's own final section concedes that every modern system implements primality as a bounded, decidable Δ0₀ predicate; if that is the right formalization, the claimed barrier would have to be restated for an unbounded universal predicate and would no longer concern the primality used in ordinary arithmetic.","Editorial inference: The same uniformization argument, if sound, would generalize to any Π1-premised existential statement about primes, such as twin-prime or prime-k-tuple conjectures, predicting they too are constructively unprovable in HA for realizability reasons rather than arithmetical ones.","Editorial inference: The bounded-search criterion in the paper suggests a constructive repair: replace an unbounded prime conjecture by a bounded version that assumes an explicit search bound B(n) for witnesses; such bounded approximations should fall into the constructively provable case, giving finite Goldbach certificates for each n."],"forward_implications":["A classical proof of the strong Goldbach conjecture would not yield a constructive proof; the constructive Goldbach principle GC*Π would remain unprovable in HA even if arithmetically true.","Any prime conjecture whose conclusion requires witnesses for a truly Π1 premise and has no primitive-recursive bound on the witnesses is predicted to be constructively unprovable, regardless of its truth in N.","PA proves that no total recursive index uniformly realizes the Σ1 witnesses for GC*Π; any alleged uniform extractor would create constant-length proofs for infinitely many instances, colliding with proof-length speedup.","Goldbach's constructive form sits in the gap between HA and true arithmetic: true in N (if the classical conjecture is true) but not HA-provable."],"fun_headline_variants":["No total realizer maps primality to Goldbach witnesses","Uniform Goldbach extraction impossible in constructive arithmetic","Classical Goldbach won't yield a constructive uniform proof","Heyting Arithmetic lacks uniform witnesses for Goldbach","Even true Goldbach can't be uniformly realized constructively"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The load-bearing premise is that the paper's own primality formula — no factorization with factors up to n — is a genuinely undecidable universal claim; because the search is bounded, intuitionistic arithmetic can decide it by finite checking, and the barrier results stand or fall with that classification.","fun_headline_variants_meta":{"raw":{"variants":["No total realizer maps primality to Goldbach witnesses","Uniform Goldbach extraction impossible in constructive arithmetic","Classical Goldbach won't yield a constructive uniform proof","Heyting Arithmetic lacks uniform witnesses for Goldbach","Even true Goldbach can't be uniformly realized constructively"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001068,"raw_usage":{"total_tokens":4265,"prompt_tokens":652,"completion_tokens":3613,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":396,"completion_tokens_details":{"reasoning_tokens":3551}},"tokens_in":396,"tokens_out":3613,"duration_ms":26680,"temperature":1.0,"reasoning_tokens":3551,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T23:02:55.552566+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Formalize trial division in HA: for a given numeral n, a primitive-recursive program checks every a from 2 to ⌊√n⌋ and decides whether a divides n; this is a finite, terminating computation over a bounded range. Since bounded quantification over numerals is provably decidable by induction in HA, the procedure decides the paper's own formula PrimeΠ(n) constructively, contradicting the claim that primality is a constructively undecidable Π1 predicate and thus removing the premise on which the barrier theorems rest.","supporting_citations":[],"review_version":1}