arXiv subjects

Yijun Yuan

Publications and source records attributed to Yijun Yuan.

At least 19 recordsLinked to original sources

arXiv2026

Formalization of Harder-Narasimhan theory

The Harder-Narasimhan theory provides a canonical filtration of a vector bundle on a projective curve whose successive quotients are semistable with strictly decreasing slopes. In this article, we present a formalization of Harder-Narasimhan theory in the proof assistant Lean 4 with Mathlib. The formalization is based on a recent approach to Harder-Narasimhan theory by Chen and Jeannin, which reinterprets the theory in order-theoretic terms and avoids the classical dependence on algebraic geometry. As an application, we formalize the uniqueness of the coprimary filtration of a nontrivial finitely generated module over a Noetherian ring, as well as the existence of a Jordan-Hölder filtration for a semistable Harder-Narasimhan game.

math.AG↗

arXiv2026

Formalization of non-Archimedean functional analysis 1: spherically complete spaces

In this article, we present a formalization of spherically complete spaces, a fundamental notion in non-Archimedean functional analysis, using the Lean theorem prover (v4.31.0), building over Mathlib. This work includes the equivalent definitions of spherically complete spaces, their basic properties, examples and non-examples such as the field $\mathbf{C}_p$ of $p$-adic complex numbers. As applications, we formalize the notion of Birkhoff-James orthogonality, the Hahn-Banach extension theorem and the spherical completion for non-Archimedean Banach spaces. URL of code: https://github.com/YijunYuan/SphericalCompleteness/tree/paper

math.NT↗

arXiv2026

SLAMFormer-$\infty$: Infinite SLAM Transformer for Unbounded Frontend and Backend Processing

We introduce the Infinite SLAM Transformer (SLAMFormer-$\infty$), the first geometric transformer capable of supporting both long-range frontend and backend processing without an explicit distance bound. Instead of relying on a first-frame-anchored formulation, SLAMFormer-$\infty$ employs memory conditions to define flexible coordinate systems and scales for input frames, enabling more expressive structural conditioning. Built upon this formulation, the frontend preserves efficient local computation, while the backend jointly optimizes long-range trajectories and scene geometry in a globally consistent manner. Experimental results demonstrate that SLAMFormer-$\infty$ achieves superior or highly competitive performance in both trajectory estimation and scene reconstruction across large-scale datasets. Notably, SLAMFormer-$\infty$ generalizes to extremely long trajectories, successfully operating on sequences exceeding $17\mathrm{km}$.

cs.CV↗

arXiv2026

SLAM-Former: Putting SLAM into One Transformer

We present SLAM-Former, a neural approach that integrates full SLAM capabilities into a single transformer. Similar to traditional SLAM systems, SLAM-Former comprises both a frontend and a back-end that operate in tandem. The frontend processes sequential monocular images in real-time for incremental mapping and tracking, while the backend performs global refinement to ensure a geometrically consistent result. This alternating execution allows the frontend and back-end to mutually promote one another, enhancing overall system performance. Comprehensive experimental results demonstrate that SLAM- Former achieves superior or highly competitive performance compared to state-of-the-art dense SLAM methods.

cs.CV↗

arXiv2026

$p$-adic Hahn series with sparse support

Let $p$ be a prime number. We introduce a sparseness condition on the supports of $p$-adic Hahn series, and prove that this condition implies transcendence over $\breve{\mathbf Q}_p$, the completed maximal unramified extension of $\mathbf{Q}_p$. As an application, we prove the order-type conjecture of $\mathbf{Q}_p$-algebraic $p$-adic Hahn series with bounded support under the condition that the support has only finitely many accumulation points. All results in this paper have been fully formalized in the Lean theorem prover (v 4.31.0), building over Mathlib.

math.NT↗

arXiv2026

Hyper-algebraic invariants of $p$-adic algebraic numbers

Let $p\geq 3$ be a prime. The hyper-algebraic elements in the $p$-adic Mal'cev-Neumann field $\mathbb{L}_p$ form an algebraically closed subfield $\mathbb{L}_p^{\operatorname{ha}}$. In this article, we clarify the relations among the fields $\mathbb{L}_p^{\operatorname{ha}}$, $\overline{\mathbb{Q}}_p$ and $\mathbb{C}_p$. We introduce two arithmetic invariants (hyper-tame index and hyper-inertia index) of hyper-algebraic elements and study the relation between these invariants and classical arithmetic invariants of $p$-adic algebraic numbers. Finally, we give a criterion for hyper-algebraic elements to be tamely ramified over $\mathbb{Q}_p$.

math.NT↗

arXiv2026

VRSafe: A Secure Virtual Keyboard to Mitigate Keystroke Inference in Virtual Reality

Password-based authentication is one of the most commonly used methods for verifying user identities, and its widespread usage continues in virtual reality (VR) applications. As a result, various forms of attacks on password-based authentication in traditional environments such as keystroke inference and shoulder surfing, are still effective in VR applications. While keystroke inference attacks on virtual keyboards have been studied extensively, few efforts have developed an effective and cost-efficient defense strategy to mitigate keystroke inferences in VR. To address this gap, this paper presents a novel QWERTY keyboard called \textit{VRSafe} that is resilient to keystroke inference attacks. The proposed keyboard carefully introduces false positive keystrokes into the information collected by attackers during the typing process, making the inference of the original password difficult. \textit{VRSafe} also incorporates a novel malicious login detector that can effectively identify unauthorized login attempts using credentials inferred from keystroke inference attacks with high detection rate and minimal time and memory cost. The proposed design is evaluated through both simulation experiments and a real-world user study, and the results show that \textit{VRSafe} can significantly reduce the accuracy of keystroke inference attacks while incurring a modest overhead from a usability standpoint.

cs.CR↗

arXiv2026

Complet4R: Geometric Complete 4D Reconstruction

We introduce Complet4R, a novel end-to-end framework for Geometric Complete 4D Reconstruction, which aims to recover temporally coherent and geometrically complete reconstruction for dynamic scenes. Our method formalizes the task of Geometric Complete 4D Reconstruction as a unified framework of reconstruction and completion, by directly accumulating full contexts onto each frame. Unlike previous approaches that rely on pairwise reconstruction or local motion estimation, Complet4R utilizes a decoder-only transformer to operate all context globally directly from sequential video input, reconstructing a complete geometry for every single timestamp, including occluded regions visible in other frames. Our method demonstrates the state-of-the-art performance on our proposed benchmark for Geometric Complete 4D Reconstruction and the 3D Point Tracking task. Code will be released to support future research.

cs.CV↗

arXiv2025

Descent of $(φ,τ)$-modules in characteristic $p$

In this article, we study the descent of $(φ,τ)$-modules over perfectoid period rings in characteristic $p$ via Berger and Rozensztajn's theory of super-Hölder vectors. This is a generalization of their work on $(φ,Γ)$-modules. As an application, we answer a question of Caruso regarding the connection between $(φ,τ)$-modules and $(φ,Γ)$-modules without involving Galois representations as intermediaries.

math.NT↗

arXiv2025

On the $p$-adic transcendence of $\sum_{k=1}^\infty p^{-1/p^k}$

Let $p$ be a prime number. In this article, we prove that the $p$-adic Hahn series $\sum_{k=1}^\infty p^{-1/p^k}$, which is the mixed-characteristic analogue of Abhyankar's solution $\sum_{k=1}^\infty t^{-1/p^k}$ to the Artin-Schreier equation $X^p-X-t^{-1}=0$ over $\mathbf{F}_p\left(\!\left(t\right)\!\right)$, is a $p$-adic complex number, but not a $p$-adic algebraic number. Based on this result, we formulate a conjecture about the possible order type of the support of an algebraic $p$-adic Hahn series and prove that it is implied by a tentative observation of Kedlaya.

math.NT↗

arXiv2025

Multivariable period rings of $p$-adic false Tate curve extension

Let $p\geq 3$ be a prime number and $K$ be a finite extension of $\mathbf{Q}_p$ with uniformizer $π_K$. In this article, we introduce two multivariable period rings $\mathbf{A}_{\mathfrak{F},K}^{\operatorname{np}}$ and $\mathbf{A}_{\mathfrak{F},K}^{\operatorname{np},\operatorname{c}}$ for the étale $(φ,Γ_{\mathfrak{F},K})$-modules of $p$-adic false Tate curve extension $K\left(π_K^{1/p^\infty},ζ_{p^\infty}\right)$. Various properties of these rings are studied and as applications, we show that $(φ,Γ_{\mathfrak{F},K})$-modules over these rings bridge $(φ,Γ)$-modules and $(φ,τ)$-modules over imperfect period rings in both classical and cohomological sense, which answers a question of Caruso. Finally, we construct the $ψ$ operator for false Tate curve extension and discuss the possibility to calculate Iwasawa cohomology for this extension via $(φ,Γ_{\mathfrak{F},K})$-modules over these rings.

math.NT↗

arXiv2025

SceneFactory: A Workflow-centric and Unified Framework for Incremental Scene Modeling

We present SceneFactory, a workflow-centric and unified framework for incremental scene modeling, that conveniently supports a wide range of applications, such as (unposed and/or uncalibrated) multi-view depth estimation, LiDAR completion, (dense) RGB-D/RGB-L/Mono/Depth-only reconstruction and SLAM. The workflow-centric design uses multiple blocks as the basis for constructing different production lines. The supported applications, i.e., productions avoid redundancy in their designs. Thus, the focus is placed on each block itself for independent expansion. To support all input combinations, our implementation consists of four building blocks that form SceneFactory: (1) tracking, (2) flexion, (3) depth estimation, and (4) scene reconstruction. The tracking block is based on Mono SLAM and is extended to support RGB-D and RGB-LiDAR (RGB-L) inputs. Flexion is used to convert the depth image (untrackable) into a trackable image. For general-purpose depth estimation, we propose an unposed \& uncalibrated multi-view depth estimation model (U$^2$-MVD) to estimate dense geometry. U$^2$-MVD exploits dense bundle adjustment to solve for poses, intrinsics, and inverse depth. A semantic-aware ScaleCov step is then introduced to complete the multi-view depth. Relying on U$^2$-MVD, SceneFactory both supports user-friendly 3D creation (with just images) and bridges the applications of Dense RGB-D and Dense Mono. For high-quality surface and color reconstruction, we propose Dual-purpose Multi-resolutional Neural Points (DM-NPs) for the first surface accessible Surface Color Field design, where we introduce Improved Point Rasterization (IPR) for point cloud based surface query. ...

cs.CV↗

arXiv2024

Uni-Fusion: Universal Continuous Mapping

We present Uni-Fusion, a universal continuous mapping framework for surfaces, surface properties (color, infrared, etc.) and more (latent features in CLIP embedding space, etc.). We propose the first universal implicit encoding model that supports encoding of both geometry and different types of properties (RGB, infrared, features, etc.) without requiring any training. Based on this, our framework divides the point cloud into regular grid voxels and generates a latent feature in each voxel to form a Latent Implicit Map (LIM) for geometries and arbitrary properties. Then, by fusing a local LIM frame-wisely into a global LIM, an incremental reconstruction is achieved. Encoded with corresponding types of data, our Latent Implicit Map is capable of generating continuous surfaces, surface property fields, surface feature fields, and all other possible options. To demonstrate the capabilities of our model, we implement three applications: (1) incremental reconstruction for surfaces and color (2) 2D-to-3D transfer of fabricated properties (3) open-vocabulary scene understanding by creating a text CLIP feature field on surfaces. We evaluate Uni-Fusion by comparing it in corresponding applications, from which Uni-Fusion shows high-flexibility in various applications while performing best or being competitive. The project page of Uni-Fusion is available at https://jarrome.github.io/Uni-Fusion/ .

cs.CV↗

arXiv2023

Uniformizer of the False Tate Curve Extension of $\mathbb{Q}_p$ (II)

In this article, we investigate the explicit formula for the uniformizers of the false-Tate curve extension of $\mathbb{Q}_p$. More precisely, we establish the formula for the fields ${\mathbb{K}}_p^{m,1}={\mathbb{Q}}_p(ζ_{p^m}, p^{1/p})$ with $m\geq 1$ and for general $n\geq 2$, we prove the existence of the recurrence polynomials ${\mathcal{R}}_p^{m,n}$ for general field extensions ${\mathbb{K}}_p^{m, n}$ of ${\mathbb{Q}}_p$, which shows the possibility to construct the uniformizers systematically.

math.NT↗

arXiv2023

NSLF-OL: Online Learning of Neural Surface Light Fields alongside Real-time Incremental 3D Reconstruction

Immersive novel view generation is an important technology in the field of graphics and has recently also received attention for operator-based human-robot interaction. However, the involved training is time-consuming, and thus the current test scope is majorly on object capturing. This limits the usage of related models in the robotics community for 3D reconstruction since robots (1) usually only capture a very small range of view directions to surfaces that cause arbitrary predictions on unseen, novel direction, (2) requires real-time algorithms, and (3) work with growing scenes, e.g., in robotic exploration. The paper proposes a novel Neural Surface Light Fields model that copes with the small range of view directions while producing a good result in unseen directions. Exploiting recent encoding techniques, the training of our model is highly efficient. In addition, we design Multiple Asynchronous Neural Agents (MANA), a universal framework to learn each small region in parallel for large-scale growing scenes. Our model learns online the Neural Surface Light Fields (NSLF) aside from real-time 3D reconstruction with a sequential data stream as the shared input. In addition to online training, our model also provides real-time rendering after completing the data stream for visualization. We implement experiments using well-known RGBD indoor datasets, showing the high flexibility to embed our model into real-time 3D reconstruction and demonstrating high-fidelity view synthesis for these scenes. The code is available on github.

cs.CV↗

arXiv2023

Truncated expansion of $ζ_{p^n}$ in the $p$-adic Mal'cev-Neumann field

Fix an odd prime $p$. In this article, we provide a $\mathrm{mod}\ p$ harmonic number identity, which appears naturally in the canonical expansion of a root $ζ_{p^n}$ of the $p^n$-th cyclotomic polynomial $Φ_{p^n}(T)$ in the $p$-adic Mal'cev-Neumann field $\mathbb{L}_p$. We establish a $\frac{2}{(p-1)p^{n-2}}$-truncated expansion of $ζ_{p^n}$ via a variant of the transfinite Newton algorithm, which gives the first $\aleph_0^2$ terms of the canonical expansion of $ζ_{p^n}$. The harmonic number identity simplifies the expression of this expansion.

math.NT↗

arXiv2022

An Algorithm for the SE(3)-Transformation on Neural Implicit Maps for Remapping Functions

Implicit representations are widely used for object reconstruction due to their efficiency and flexibility. In 2021, a novel structure named neural implicit map has been invented for incremental reconstruction. A neural implicit map alleviates the problem of inefficient memory cost of previous online 3D dense reconstruction while producing better quality. % However, the neural implicit map suffers the limitation that it does not support remapping as the frames of scans are encoded into a deep prior after generating the neural implicit map. This means, that neither this generation process is invertible, nor a deep prior is transformable. The non-remappable property makes it not possible to apply loop-closure techniques. % We present a neural implicit map based transformation algorithm to fill this gap. As our neural implicit map is transformable, our model supports remapping for this special map of latent features. % Experiments show that our remapping module is capable to well-transform neural implicit maps to new poses. Embedded into a SLAM framework, our mapping model is able to tackle the remapping of loop closures and demonstrates high-quality surface reconstruction. % Our implementation is available at github\footnote{\url{https://github.com/Jarrome/IMT_Mapping}} for the research community.

cs.CV↗

arXiv2022

Indirect Point Cloud Registration: Aligning Distance Fields using a Pseudo Third Point Ses

In recent years, implicit functions have drawn attention in the field of 3D reconstruction and have successfully been applied with Deep Learning. However, for incremental reconstruction, implicit function-based registrations have been rarely explored. Inspired by the high precision of deep learning global feature registration, we propose to combine this with distance fields. We generalize the algorithm to a non-Deep Learning setting while retaining the accuracy. Our algorithm is more accurate than conventional models while, without any training, it achieves a competitive performance and faster speed, compared to Deep Learning-based registration models. The implementation is available on github for the research community.

cs.RO↗