← 研踪 PaperTrailarXiv:2610.39746 · v1
Step Recursion: Rational Strides and Exact Inclusion Orders over the Reals
首次提交 2026-10-29 18:06
版本更新 2026-10-29 18:06
雷达观测 2026-10-30 13:28
摘要
We study finite-terminating, address-only step recursion on the nonnegative reals, from zero, unit successor and projections. For reduced positive rational strides $s=a/q$ and $t=b/v$, we prove $\mathcal{C}s\subseteq\mathcal{C}t$ if and only if $q$ divides $v$, for both the bounded and unbounded algebras $\mathcal{C}\in{\mathcal{B},\mathcal{U}}$. The bounded compiler preserves earlier global majorants on every auxiliary input. Mixed rational stride sets are classified by least common denominators and supernatural denominators. Primitive-recursive translated-coordinate grid codes characterize the unbounded algebras and yield $\mathcal{U}{1/q}\cap\mathcal{U}{1/v}=\mathcal{U}{1/\gcd(q,v)}$. For bounded intersections, we prove an exact reduction: all corresponding identities hold if and only if the single identity $\mathcal{B}{1/2}\cap\mathcal{B}_{1/3}=\mathcal{B}_1$ holds, equivalently if the Boolean parts of the integer successor and addition algebras under scalar bounded recursion coincide. A Boolean reconstruction reduces general functions to predicates; a clipped fine-grid simulation with a frozen global resource bound identifies the union of predicate precision classes with the addition level. These reductions do not decide the resulting predicate equality, so literal bounded intersections remain unresolved. We also prove that unbounded-program equality is $Π^0_1$-complete and extensional bounded-algebra membership is $Σ^0_2$-complete. The model has no free real arithmetic or Zeno limits; semantic majorant validity is distinguished from syntax transformation.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v1 · 2026-10-29 18:06 · 最新观测版本
Step Recursion: Rational Strides and Exact Inclusion Orders over the Reals
We study finite-terminating, address-only step recursion on the nonnegative reals, from zero, unit successor and projections. For reduced positive rational strides $s=a/q$ and $t=b/v$, we prove $\mathcal{C}s\subseteq\mathcal{C}t$ if and only if $q$ divides $v$, for both the bounded and unbounded algebras $\mathcal{C}\in{\mathcal{B},\mathcal{U}}$. The bounded compiler preserves earlier global majorants on every auxiliary input. Mixed rational stride sets are classified by least common denominators and supernatural denominators. Primitive-recursive translated-coordinate grid codes characterize the unbounded algebras and yield $\mathcal{U}{1/q}\cap\mathcal{U}{1/v}=\mathcal{U}{1/\gcd(q,v)}$. For bounded intersections, we prove an exact reduction: all corresponding identities hold if and only if the single identity $\mathcal{B}{1/2}\cap\mathcal{B}_{1/3}=\mathcal{B}_1$ holds, equivalently if the Boolean parts of the integer successor and addition algebras under scalar bounded recursion coincide. A Boolean reconstruction reduces general functions to predicates; a clipped fine-grid simulation with a frozen global resource bound identifies the union of predicate precision classes with the addition level. These reductions do not decide the resulting predicate equality, so literal bounded intersections remain unresolved. We also prove that unbounded-program equality is $Π^0_1$-complete and extensional bounded-algebra membership is $Σ^0_2$-complete. The model has no free real arithmetic or Zeno limits; semantic majorant validity is distinguished from syntax transformation.
查看此版本解读 →查看此版本原文 ↗