arXiv subjects

Milan Rosko

Publications and source records attributed to Milan Rosko.

8 recordsLinked to original sources

arXiv2026

Operational Evidence and Incompleteness: A Minkowski Radar Model

A uniformly computable family of stationary reflector distances makes finite radar verification of a strict bound equivalent to halting. Every fixed-precision protocol terminates. Nevertheless, every effective theory sound for the corresponding absence statements and their negations leaves infinitely many true absence statements undecided. These are $Π^0_1$ sentences. The contribution is a simple radar realization of a standard computability obstruction.

math.LO↗

arXiv2026

Remarks on Primitive Regulation

We prove, and mechanize in Rocq, an obstruction to closure-level Excluded Middle for primitive regulators $C : \mathsf{Form} \to \mathsf{Prop}$ over the closed implication-falsity fragment $A,B ::= \bot \mid A \to B$. Write $\mathsf{LEM}(C)$ for the demand that $C(A)\lor C(\lnot A)$ hold for every formula $A$. If $C$ is closed under Modus Ponens, is consistent, and admits a formula $B$ satisfying $B\simeq_C\lnot B$, where $A \simeq_C B$ abbreviates $C(A \to B) \land C(B \to A)$, then $\mathsf{LEM}(C)$ is impossible. In fact, consistency excludes both $C(B)$ and $C(\lnot B)$, so the global conclusion uses only the excluded-middle instance at $B$.

math.LO↗

arXiv2026

An Intuitionistic Glance at Primes

This paper gives a proof-theoretic account of how positive integers must be classified as $1$, prime, or composite in intuitionistic logic. Compositehood is expressed in $Σ^0_0$ by exhibiting a factorization; primality is expressed in $Π^0_0$ by exhibiting a lack of interior factorization. Because both searches are bounded, both predicates are decidable. Organizing the checks in stages yields a recursive sieve for the primes, a characterization of modular cancellation, and finite arithmetic certificates. The final sections distinguish what Heyting Arithmetic ($\mathsf{HA}$) proves internally from what depends on the standard interpretation of $\mathbb{N}$.

math.LO↗

arXiv2026

On the Golden Ratio and Stable Self-Application

This paper studies a boundary between local self-application and global self-certification. Irrational quantities are treated operationally, as procedures whose approximations are refined by effective update rules. The golden ratio $Φ$ is used as a model of stable local recurrence: the reciprocal update $R(x)=1+1/x$ has a unique positive fixed point and admits finite witnessed approximations. By contrast, global reflection asks a system to certify its own correctness uniformly. The proof-theoretic claim is therefore contrastive: primitive-recursive proof checking and local soundness preserve correctness through bounded checks and bounded witnesses, but they do not yield internal global reflection. No complexity advantage, decision procedure, or new reflection principle is claimed.

math.LO↗

arXiv2026

Carryless Pairing: Additive Pairing in the Fibonacci Basis

We define a pairing map $π_{\mathsf{CL}} : \mathbb{N}^2\to\mathbb{N}$ that encodes $x$ and $y$ into two disjoint bands of Zeckendorf indices separated by a delimiter computed from $x$. The construction is "carryless" by design: the combined support has no consecutive indices, so each produced code is already in Zeckendorf-normal form, and both evaluation and inversion proceed by additive support operations alone, without multiplication, factorization, or positional digit interleaving. The map is injective not surjective, image membership is decidable by the same support machinery used for decoding. The core correctness theorems are mechanized in Rocq.

math.LO↗

arXiv2026

Considering The Satisfiability of Cubic Diophantine Equations

Our contribution is a bounded cubic compilation theorem. For each fixed resource parameter $k$, syntactic proof checking at resource level $k$ is faithfully represented by a finite bounded-domain system of cubic polynomial equations. Every emitted equation has degree at most 3. Degree-3 terms arise only when a linear selector variable activates a quadratic verification obligation. Earlier versions of this manuscript claimed a reduction from unbounded theoremhood to satisfiability of a fixed bounded-domain cubic polynomial instance. That claim is withdrawn. The error and its source are identified precisely. The bounded construction, the degree bookkeeping, and the Zeckendorf-based carryless encoding stand independently of the withdrawn claim. The note closes by identifying the uniformization gap that separates a family of decidable bounded slices from a single many-one reduction target, and records why closing that gap would require a compression principle not supplied here.

math.LO↗

arXiv2025

Adversarial Barrier in Uniform Class Separation

We identify a strong structural obstruction to Uniform Separation in constructive arithmetic. The mechanism is independent of semantic content; it emerges whenever two distinct evaluator predicates are sustained in parallel and inference remains uniformly representable in an extension of HA. Under these conditions, any putative Uniform Class Separation principle becomes a distinguished instance of a fixed point construction. The resulting limitation is stricter in scope than classical separation barriers (Baker; Rudich; Aaronson et al.) insofar as it constrains the logical form of uniform separation within HA, rather than limiting particular relativizing, naturalizing, or algebrizing techniques.

math.LO↗

arXiv2025

The Solver's Paradox in Formal Problem Spaces

This paper investigates how global decision problems over arithmetically represented domains acquire reflective structure through class-quantification. Arithmetization forces diagonal fixed points whose verification requires reflection beyond finitary means, producing Feferman-style obstructions independent of computational technique. We use this mechanism to analyze uniform complexity statements, including $\mathsf{P}$ vs. $\mathsf{NP}$, showing that their difficulty stems from structural impredicativity rather than methodological limitations. The focus is not on deriving separations but on clarifying the logical status of such arithmetized assertions.

cs.CC↗