Milan Rosko

Milan Rosko

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.

Milan Rosko

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.

Milan Rosko

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.