arXiv subjects

Teng Zhang

Publications and source records attributed to Teng Zhang.

At least 37 records · Page 2Linked to original sources

arXiv2026

Theoretical Guarantees for the Subspace-Constrained Tyler's Estimator

This work analyzes the subspace-constrained Tyler's estimator (STE), a method designed to recover a low-dimensional subspace from a dataset that may be heavily corrupted by outliers. The STE has previously been shown to be competitive for fundamental computer vision problems. We assume a weak inlier-outlier model and allow the inlier fraction to fall below the threshold at which robust subspace recovery becomes computationally hard. We show that, in this setting, if the initialization of STE satisfies a certain condition, then STE, which is computationally efficient, can effectively recover the underlying subspace. To demonstrate the usefulness of this result, we use a common setting in the theoretical computer science community, whose special case is when the inliers are sampled from a Gaussian distribution and there are no restrictions on the outliers. We show that in this setting, with high probability, STE initialized by a polynomial algorithm exactly recovers the underlying subspace with linear convergence. Furthermore, we establish approximate recovery guarantees for STE in the presence of noisy inliers. Finally, under the asymptotic generalized haystack model, we demonstrate that STE initialized with Tyler's M-estimator (TME) recovers the subspace even when the inlier fraction is too small for TME to succeed on its own.

math.ST↗

arXiv2026

Formal Verification of Imperative First-Class Functions in Move

The Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language. Recently, Move on Aptos was extended with higher-order functions: imperative functions as first-class values that can be passed around, stored in data structs, and kept in persistent storage, enabling dynamic dispatch. This paper describes the representation of function values in the Move specification language and their implementation in MVP. We introduce behavioral predicates which characterize Move functions (aborts and pre/post conditions) by single-state or two-state predicates. We also introduce state labels for naming intermediate memory states in which expressions are evaluated and which allow to compose behavioral predicates to describe sequences of state transitions. On SMT level, function values are encoded by discriminating over the possible function values reaching a call site: when the concrete function is known, its effect is accounted for directly; when it is unknown (for example, a function parameter, or a closure loaded from storage), its behavioral predicates describe the effect. Our approach goes beyond, for example, Dafny, by supporting imperative first-class functions which can modify state via Rust-style references and global variables, and leads to more efficient SMT encodings than separation logic because of the static separation of memory enabled by Move. We further extend MVP's specification inference tool to work with function values: given arbitrary higher-order Move code, weakest-precondition analysis semi-automatically derives behavioral-predicate-based specifications, reducing the annotation burden and providing a validation pipeline for the new specification constructs.

cs.PL↗

arXiv2026

Defense-in-Depth Runtime Safety in Move

Move is a smart-contract language used to execute transactions on the Aptos blockchain. Move programs execute in a sandboxed VM as typed bytecode. The VM statically verifies foundational safety properties like type safety and reference safety at code loading time. In principle, this design gives strong guarantees for Move. However, the static verification logic is complex and continually evolving with the language; like any software, it is not immune to bugs. In a live blockchain setting, a missed rule violation can translate directly into loss of assets, forged authority, or unrecoverable corruption of on-chain state. For this reason, Aptos relies on defense-in-depth runtime safety checks that independently verify the critical invariants during execution, providing protection against latent verifier bugs and malicious bytecode. This paper motivates and describes the runtime safety checks for Move on Aptos.

cs.PL↗

arXiv2026

KILVO: Kinematic-Inertial-LiDAR-Visual Odometry with Robust Multimodal Adaptation for Humanoid Robots

This article presents a kinematic-inertial-LiDAR-visual odometry for humanoid robots, called KILVO. Tailored to the platform features, requirements, and real-world complexity, it fully utilizes the sensors commonly equipped on humanoid robots, including joint encoders, IMU, LiDAR, and camera, within an asynchronous-sequential hybrid error-state iterated Kalman filter (ESIKF). Specifically, inertial data are used for prediction, leg kinematics are processed asynchronously at a high rate and provide proprioceptive constraints, while exteroception is updated sequentially, first by registering LiDAR points for geometric priors and then by updating the visual component via photometric errors. Moreover, the framework is elaborately designed with multimodal adaptation for resilience to sensor failures. A compact contact estimation module is also developed, sharing information with state estimation without additional sensors. Extensive experiments on public datasets and in the real world across multiple humanoid robots, gait patterns, and scenarios demonstrate that KILVO achieves highly competitive accuracy, efficiency, and output rates, with strong robustness against sensor degradation and failures, making it more suitable for humanoid robots than state-of-the-art fusion methods. Our code and datasets are released on GitHub.

cs.RO↗

arXiv2026

The $A$-optimal design problem and the $S$-matrix conjecture

The $S$-matrix conjecture was formulated by Sloane and Harwit in 1976, motivated by an $A$-optimal design problem arising in spectroscopy. It states that if $A$ is a nonsingular real $n\times n$ matrix whose entries lie in $[0,1]$, then $$\left\|A^{-1}\right\|_F\ge\frac{2n}{n+1}.$$ Moreover, equality holds if and only if $A$ is an $S$-matrix. In this paper, we prove the conjecture by combining a variational trace inequality in odd dimensions with a sharp range-constrained estimate for the Moore--Penrose inverse of a centered matrix in even dimensions.

math.FA↗

arXiv2026

Sendov's conjecture holds for every degree $n\ge 10^{200000}$

Sendov's conjecture, first formulated in 1958, asserts that if a complex polynomial $f$ of degree $n \geq 2$ has all its zeros in the closed unit disk ${z \in \mathbb{C} : |z| \leq 1}$, then, for every zero $λ_0$ of $f$, there exists a critical point $ζ$ of $f$ such that $|ζ-λ_0| \leq 1$. The conjecture was previously known to hold for polynomials of degree $n \leq 8$, as well as in several special higher-degree cases. In 2022, using compactness methods, balayage, and the argument principle, Tao~\cite{Tao22} proved that there exists an absolute constant $n_0$ such that Sendov's conjecture holds for all $n \geq n_0$. However, Tao's argument does not provide an explicit admissible value of $n_0$. In the present paper, we make Tao's result effective and prove that one may take $$ n_0 = 10^{200000}. $$

math.CV↗

arXiv2026

Sharp tangent inequalities in noncommutative $L_p$-spaces

Let $\mathcal{M}$ be a von Neumann algebra equipped with a faithful normal semifinite weight, and let $L_p(\mathcal{M})$ denote the associated Haagerup noncommutative $L_p$-space. For $1<p<\infty$, let $q=p/(p-1)$. For $z\in L_q(\mathcal{M})$ and $y\in L_p(\mathcal{M})$, denote by $\langle z,y\rangle=\operatorname{Re}\operatorname{Tr}(z^*y)$ the canonical real duality pairing between $L_q(\mathcal{M})$ and $L_p(\mathcal{M})$. Define the normalized duality map by $J_p(x)=\|x\|_p^{\,2-p}u|x|^{p-1}$ for $x=u|x|\neq0$, and set $J_p(0)=0$. We establish the sharp tangent inequality $$\|x+y\|_p^2\ge\|x\|_p^2+2\langle J_p(x),y\rangle+(p-1)\|y\|_p^2,\qquad x,y\in L_p(\mathcal{M}),\quad 1<p\le2.$$ The reverse inequality holds for $2\le p<\infty$, and the constant $p-1$ is optimal. Our inequality extends Xu's tangent inequality \cite{Xu89} from classical $L_p$-spaces to general noncommutative $L_p$-spaces and provides the sharp tangent formulation of the Ricard--Xu convexity inequality \cite{RX16}. When specialized to Schatten $p$-classes, it also yields the corresponding tangent formulation of the Ball--Carlen--Lieb convexity inequality \cite{BCL94}. Under a suitable positivity assumption, we further establish a sharp complement to Xu's tangent inequality for Schatten $p$-classes in the range $0<p<1$.

math.OA↗

arXiv2026

On the embedding rigidity problem for uniformly locally finite coarse spaces

In this paper, we construct countable uniformly locally finite metric spaces $X$ and $Y$ such that $C_u^*(X)$ is isomorphic to a hereditary $C^*$-subalgebra of $C_u^*(Y)$, while $X$ does not coarsely embed into$Y$. This gives a negative answer to the embedding rigidity problem for uniformly locally finite coarse spaces. On the positive side, we prove that, if every sparse subspace of $Y$ yields only compact ghost projections, then any isomorphism of $C_u^*(X)$ onto a hereditary $C^*$-subalgebra of $C_u^*(Y)$ induces an injective coarse embedding $X\to Y$. This strengthens a main result in \cite{BFV20} by upgrading coarse embeddability to injective coarse embeddability under the same hypothesis.

math.OA↗

arXiv2026

Isomorphism rigidity of uniform Roe algebras over arbitrary uniformly locally finite coarse spaces

Let $(X,\mathcal E)$ and $(Y,\mathcal F)$ be uniformly locally finite coarse spaces. We prove that every $C^*$-algebra isomorphism $C_u^*(X,\mathcal E)\cong C_u^*(Y,\mathcal F)$ forces $(X,\mathcal E)$ and $(Y,\mathcal F)$ to be bijectively coarsely equivalent. This completely resolves the isomorphism rigidity problem for uniform Roe algebras over arbitrary uniformly locally finite coarse spaces.

math.OA↗

arXiv2026

A Case-Bundle Operating Model for Coding Agents in OpenFOAM-Based CFD

General-purpose coding agents can set up computational fluid dynamics (CFD) cases, execute solvers, and manage remote jobs. Reviewable and reusable work additionally depends on persistent engineering context and evidence. We present a case-bundle operating model with two modes. Build supports agent-assisted case development under engineering review. Replay applies a reviewed case to new variants. We used this model in an OpenFOAM-7 interFoam study for screening injector designs. GPT-5.5 in Codex helped develop a case bundle containing the simulation configuration, geometry-processing and meshing procedures, remote-execution scripts, post-processing code, and review records. The bundle was replayed to execute and post-process 140 Stereolithography (STL) geometry variants on a remote high-performance computing system. A separate replay exercise used the Pi coding agent as the runtime with four different LLM backends. All four runs succeeded and produced verified results. Tool use and token consumption varied across runs. The results show how reviewed case bundles can support bounded, reusable automation with distinct roles for routine execution and engineering judgment.

cs.SE↗

arXiv2026

On interrelations among different versions of a Heron type mean and commutativity in $C^*$-Algebras

The extension of the concept of a mean of positive real numbers to noncommutative settings, e.g., for Hilbert space operators, is a widely studied question. For example, in quantum information science, it is an important issue to find such extensions that fit the "best" to the studied physical problems. In fact, typically, there are many different ways of extension which, for commuting variables, all give the same value. In this paper, we are concerned with the converse: to what extent the coincidence of two extensions determines commutativity. Concretely, in our present work, we consider three different versions of the most common Heron type mean on the positive definite cone of a $C^*$-algebra: the Kubo-Ando type Heron mean, the naive or conventional version of the Heron mean, and the Wasserstein mean. We study equality relations among those objects and verify that they are closely connected to certain commutativity properties. They characterize either the commutativity of particular pairs of elements of a positive definite cone, or the centrality of positive definite elements, or the commutativity of the underlying algebra.

math.FA↗

arXiv2026

Bonded-particle model for magneto-elastic rods

We develop a bonded-particle model for magneto-elastic rods that unifies large deformations, contact, and long-range magnetic interactions within a single discrete-element framework. The rod is discretized into orientable particles connected by co-rotational bonds that capture stretching, shearing, twisting, and bending through a symmetric decomposition of relative displacement and rotation. Magnetic coupling is introduced at the particle level: each particle carries a dipole moment that rotates with it, enabling both external-field actuation and long-range dipole--dipole interactions without modifying the structural formulation. We implement the model in LAMMPS to take advantage of its parallel efficiency, long-range electrostatic solvers, and multiphysics capabilities. We validate the model on three problems spanning writhing instabilities, non-uniform magnetic actuation, and dipole-induced mechanical hysteresis. To demonstrate multiphysics capability, we couple the model with a lattice Boltzmann fluid solver via the immersed boundary method and simulate filaments in oscillatory channel flow and fluid pumping by magnetically actuated cilia arrays. Across all examples, the model shows good agreement with experimental, analytical, and numerical reference results.

cond-mat.soft↗

arXiv2026

Impurity-Preserved Density Matrix Embedding Theory for Local Electronic Excitations

Density matrix embedding theory (DMET), which is usually based on a Schmidt decomposition of Slater determinants by partitioning the full system into impurity and environment in terms of local orthogonal orbitals (LOs), has demonstrated considerable promise in electronic structure studies because it enables the extraction of local properties using a high-level solver within an embedded impurity subsystem with greatly reduced degrees of freedom, thereby achieving a balance between accuracy and computational cost. However, its application to excited states of strongly correlated systems, such as lanthanide complexes, remains challenging because the errors relative to all-electron results can still be significant. Motivated by the success of the previously developed atomic orbitals (AOs) based DMET framework (Ai, Li, and Jiang, Phys. Rev. Lett. 2025, 135, 026502.), termed AO-DMET, which attains improved accuracy by constructing the embedded subspace based on a non-orthogonal decomposition of the Slater determinant in terms of AOs, we propose a new LO-based partitioning scheme that fully preserves the impurity space spanned by corresponding AOs and can achieve accuracy closely matching that of AO-DMET while retaining the orthogonal partition and its associated computational efficiency. The performance of the proposed method is demonstrated through excitation energy calculations for several representative lanthanide complexes. These results establish an efficient and accurate partitioning scheme for describing excited states in strongly correlated systems within the DMET framework.

physics.chem-ph↗

arXiv2026

EnchantDance: Unveiling the Potential of Music-Driven Dance Movement

The task of music-driven dance generation involves creating coherent dance movements that correspond to the given music. While existing methods can produce physically plausible dances, they often struggle to generalize to out-of-set data. The challenge arises from three aspects: 1) the high diversity of dance movements and significant differences in the distribution of music modalities, which make it difficult to generate music-aligned dance movements. 2) the lack of a large-scale music-dance dataset, which hinders the generation of generalized dance movements from music. 3) The protracted nature of dance movements poses a challenge to the maintenance of a consistent dance style. In this work, we introduce the EnchantDance framework, a state-of-the-art method for dance generation. Due to the redundancy of the original dance sequence along the time axis, EnchantDance first constructs a strong dance latent space and then trains a dance diffusion model on the dance latent space. To address the data gap, we construct a large-scale music-dance dataset, ChoreoSpectrum3D Dataset, which includes four dance genres and has a total duration of 70.32 hours, making it the largest reported music-dance dataset to date. To enhance consistency between music genre and dance style, we pre-train a music genre prediction network using transfer learning and incorporate music genre as extra conditional information in the training of the dance diffusion model. Extensive experiments demonstrate that our proposed framework achieves state-of-the-art performance on dance quality, diversity, and consistency.

cs.SD↗

arXiv2026

DC response of an interferometer topology with an L-shaped cavity: a tabletop study

A new interferometer topology for kilohertz gravitational-wave detection was recently proposed in [Zhang et al. Phys. Rev. X 13, 021019 (2023)]. The design is based on an L-shaped optical cavity pumped through a Sagnac-like vortex. We report a tabletop experiment that characterizes the interferometer's optical response near DC. When the laser frequency is locked to the resonance of the L-shaped cavity, we observe that the cavity input coupler becomes effectively transparent, yielding a simple Michelson-like response. Moreover, the Sagnac vortex separates into upper and lower paths, which behave as two independent pumping paths driving the cavity. These observations are in agreement with theoretical predictions. Our results provide an intuitive physical picture of this interferometer topology and offer insight into its lock acquisition strategy.

physics.ins-det↗

arXiv2026

The Sharp Phase Transition of Tyler's M-Estimator for Robust Subspace Recovery

Robust Subspace Recovery (RSR) aims to identify an underlying d-dimensional subspace from a dataset heavily corrupted by outliers. Complexity-theoretic results establish a threshold for the problem's computational hardness based on the dimension-scaled signal-to-noise ratio (DS-SNR): the problem is SSE-hard when the DS-SNR is strictly less than 1, and solvable via practical algorithms when it is greater than 1 under general position assumptions. However, the exact behavior of practical algorithms at the critical boundary DS-SNR = 1 has remained unknown. This work resolves the behavior of Tyler's M-estimator (TME) at this critical boundary, consequently establishing a sharp phase transition. Specifically, we prove that TME converges exactly to the true subspace for DS-SNR \geq 1 under a new stability condition, which is less restrictive than the general position assumptions used in prior literature. Our analysis utilizes a decomposition of the TME iterates within a majorization-minimization framework.

cs.IT↗

arXiv2026

The separable case of Kadison's problem on orthonormal bases of unitaries for type $\mathrm{II}_1$ factors

In 1967, Kadison asked ``does every type $\mathrm{II}_1$ factor have an orthonormal (with respect to the trace) basis consisting of unitaries?'' Using a noncommutative Lyapunov theorem of Akemann and Weaver, we prove that if $M$ is a separable diffuse finite von Neumann algebra with a normal faithful trace $τ$, then $L^2(M,τ)$ admits an orthonormal basis consisting of self-adjoint unitaries in $M$. Consequently, we affirm the separable case of the Kadison problem.

math.OA↗

arXiv2026

Combining Mechanical and Agentic Specification Inference for Move

In this paper, we describe early work on a specification inference tool for the Move Prover that combines a weakest-precondition (WP) analysis over Move bytecode with an agentic coding CLI such as Claude Code. Specification inference reduces the boilerplate of writing specifications in Move: in order to verify a high-level property such as a global state invariant, pre- and post-conditions for the supporting functions typically have to be written by hand, which is tedious. In our setting, a Model Context Protocol (MCP) service exposes the WP analysis and the prover itself to the coding agent. The WP analysis provides a sound, mechanical baseline for inference; the AI is used precisely where WP is weakest -- for loop invariants and high-level idiomatic specifications such as monotonicity, conservation, and structural invariants. The Move Prover serves as the oracle that decides whether the generated specs are valid, and the agent is equipped to generate proof hints and to refine the inferred specification until verification succeeds. The tool has been applied to a corpus of canonical Move code, including code that uses higher-order functions, dynamic dispatch, global state, references, and various forms of loops.

cs.PL↗