On the Realizability of Prime Conjectures in Heyting Arithmetic

TL;DR

This work identifies a fundamental barrier to the constructive realizability of prime-related conjectures in Heyting Arithmetic: no total Σ1 extractor can uniformly convert a Π1 Prime predicate into explicit Σ1 witnesses without violating normalization. The authors develop three complementary lenses—geometric packing interpretations, a proof-theoretic nonuniformity argument, and recursion-theoretic connections to fixed-point/Skolem phenomena in PA—to explain why uniform witness extraction is blocked. They show how bounded geometric schemata fail to capture large-factor composites, relate primality to diagonal constructions (diagonal primes) and Busy Beaver-like hardness, and connect these insights to Euler products via fixed-point decompositions. Collectively, the results delineate how constructivist realizability diverges from classical arithmetical truth, yielding a precise boundary between HA and PA and offering interpretive links to information theory and forcing analogies. The findings imply that primes encode global knowledge with higher informational cost, and that resolving uniform primality questions constructively lies beyond the reach of HA, with implications for the understanding of arithmetic truth in constructive systems.

Abstract

We show that no total functional can uniformly transform $Π_1$ primality into explicit $Σ_1$ witnesses without violating normalization in $\mathsf{HA}$. The argument proceeds through three complementary translations: a geometric interpretation in which compositeness and primality correspond to local and global packing configurations; a proof-theoretic analysis demonstrating the impossibility of uniform $Σ_1$ extraction; and a recursion-theoretic formulation linking these constraints to the absence of total Skolem functions in $\mathsf{PA}$. The formal analysis in constructive logic is followed by heuristic remarks interpreting the results in informational terms.

Figures (6)

• Figure 1: Predicting the decomposition of cuboids would effectively provide an oracle. Can the semantics of primality (gold) be syntactically separated from the "combinatorial entropy" of decompositions (right)? This question frames the present investigation.
• Figure 2: A $2\times2$ rectangular packing realizing $\mathsf{Comp}(4)$. The configuration makes the multiplicative structure of $4$ explicit (blue) within the grid semantics of $\mathcal{G}$.
• Figure 3: The number $6$ and $8$ admit consistent rectangular decompositions, while $5$ and $7$ yield none. This illustrates the asymmetry of verification: composites produce explicit local witnesses (blue), whereas primality is detected only through the global ($\Pi_1$) absence of such configurations.
• Figure 4: Primality as a logical Farey sequence problem, connecting to franel24, on $xy=n$. Factor pairs within the finite bound $a,b\le D$ (solid points) are detected by the bounded verifier, while those beyond the window remain invisible. Composites with large factors thus appear prime to any finite local schema—the Continuum Hypothesis of cantor1915 returns in a different form.
• Figure 5: Combinatorial growth in $n=9$. The sequence of structural configurations (gray) follows a fractal pattern until a composite witness appears (blue). As combinatorial complexity increases, local configurations become compressible.

Theorems & Definitions (61)

• Definition 2.1: Base Theory
• Definition 2.2: Proof Semantics
• Example 2.3
• Definition 2.5: Basic Predicates
• Remark
• Definition 2.6: Constructive Goldbach's Principle
• Lemma 3.1: Constructive Completeness
• Lemma 3.2: Geometric Reduction Principle
• Definition 3.3
• Definition 3.4: Geometric Semantics