arXiv subjects

Milan Rosko

Publications and source records attributed to Milan Rosko.

8 recordsLinked to original sources

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↗

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

A Constructive Fragment of Physical Propositions

We develop a proof-theoretic analysis of the Operational Standard of Matsas, Pleitez, Saa, Vanzella (2024) showing that admissible measurement in Minkowski Spacetime yields only finite observational sequences and thereby restricts the class of physically meaningful propositions to those admitting terminating extraction procedures or uniform stability conditions. These correspond exactly to the arithmetical fragment $\Sigma^0_1 \cup \Pi^0_2$, and the induced realizability structure interprets $\Delta_0$ Heyting Arithmetic on the code of observational data. A diagonal argument then establishes an operational form of incompleteness: there exist true arithmetical propositions about admissible extraction that no sound, recursively axiomatizable theory of spacetime can decide. The result is structurally analogous to classical incompleteness but arises from the evidential limits of measurement rather than from ontological assumptions.

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↗

arXiv2025

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 $\Sigma^0_0$ by exhibiting a factorization; primality is expressed in $\Pi^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↗

arXiv2025

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 $\Phi$ 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↗

arXiv2025

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

Carryless Pairing: Additive Pairing in the Fibonacci Basis

We define a pairing map $\pi_{\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↗