Papers

Safety and comfort in human-robot physical in-teractions are essential aspects in the development of social technologies, where natural gestures, such as handshakes, represent a challenge due to their direct physical contact. The implementation of series elastic actuators (SEA) to absorb impacts is proposed as a design strategy that favors safer interactions. This paper presents an experimental study aimed at evaluating how the incorporation of SEAs in robotic arms influences perceived safety and the interaction experience dur-ing handshaking. The design allows a direct comparison of the effect of rigidity versus the incorporation of elastic elements, in order to identify the advantages of SEAs in improving the physical safety and social acceptance of robotic systems in everyday contexts. The experiment was carried out with 10 volunteers (6 men and 4 women), who performed two interactions with each robotic arm: one with rigid joints and the other with flexible joints using SEA. During testing, objective data on end-effector trajectories were collected, as well as subjective information through a perception survey focused on safety, naturalness, and confidence during the handshake. The survey results show increased perceptions of safety and comfort with the SEA-equipped arm, supporting its potential to facilitate safer and more socially accepted human-robot interactions.

Small clinical tabular datasets require interpretable machine learning because deep learning is often impractical and ensemble models can be difficult to inspect. A key pitfall is that statistical significance does not necessarily imply predictive utility. Using data from the Panama Aging Research Initiative–Health Disparities (PARI-HD) cohort (n=165), we implemented a leakage-safe threshold-likelihood Bernoulli/Categorical Naive Bayes (BNB/CNB) classifier. Within every training fold, each continuous predictor was reduced to a supervised chi-square-derived state, while income entered the model through a categorical likelihood. All data-dependent steps were performed within repeated stratified 10-fold cross-validation with 30 repeats. The demographic baseline achieved a ROC-AUC of 0.630 +/- 0.017. I-309 (CCL1) was the dominant incremental feature, increasing AUC by 0.110, with paired DeLong tests yielding p<0.05 in 100% of repeats. In the pre-specified primary analysis, I-309 produced a fixed-partition DeLong p=0.0018, with robustness assessed across 200 random partitions, where the median p-value was 0.0011. Within the exploratory family of 18 candidate markers, I-309 achieved a Benjamini-Hochberg-adjusted q=0.032 on the frozen partition and satisfied q<0.05 in 85% of random partitions, whereas no other marker demonstrated reliable incremental predictive value. Because the fitted model is an inspectable table of thresholds and class-conditional probabilities, these results identify I-309/CCL1 as an interpretable candidate feature for tabular prediction of cognitive impairment, pending external validation.

We investigate static-to-dynamic electromagnetic field conversion in a temporally switched Lorentz medium initially subjected to an electrostatic field. An abrupt change of the oscillator strength drives the material away from its initial equilibrium, while the polarization retains memory of the pre-switch state and acts as the source of the resulting transient. We formulate the resulting initial-value problem in the Laplace domain and derive an analytical representation of the generated field in terms of the poles of the finite Lorentz slab. Material dispersion gives rise to a richer modal structure than in the nondispersive case, including families of slab-mode poles that accumulate toward the singularities associated with the Lorentz polarization dynamics. We further show that material memory governs the earliest stage of the transient, producing a smooth field onset and setting the velocity of the earliest propagating disturbance through the high-frequency permittivity. Because the temporal switch generates broadband spectral content, the transient samples positive-, near-zero-, and negative-permittivity regions of the post-switch material response, leading to qualitatively different spatial field distributions. These results reveal how material dispersion and memory fundamentally shape the generation and evolution of radiation produced from an initially static electromagnetic state.

The Pachter-Sturmfels phylogenetic rank of a graph G is the minimal number of metric trees needed to embed G isometrically. Here, all edges of G are of length one and the product of metric trees is endowed with the supremum norm. We develop both a greedy and an exact algorithm for computing phylogenetic ranks. Using our algorithms, we construct a database of phylogenetic ranks which includes all graphs on 6 and 7 vertices. In particular, we exhibit examples disproving that the phylogenetic rank is hereditary, bounded by $\lceil \frac{n}{2} \rceil$, and a generalised 4-point conjecture by Pachter and Sturmfels. In addition, we show that the phylogenetic rank is subadditive under 1-sums and certain 2-vertex-sums, and that it is trivially upper bounded by n-1, where n denotes the number of vertices. We also provide a complete classification of graphs with phylogenetic rank 1 and construct several infinite families with phylogenetic rank $\lceil \frac{n}{2} \rceil$.

We formulate and analyze a system of non-linear ordinary differential equations that describe key metabolic and immunological interactions between butyrate produced by fiber-fermenting gut microbiota, colorectal cancer cells and host cell populations. The model is studied both independently and in conjunction with a pre-existing carbohydrate fermentation model. The parameter space is explored through sensitivity analyses. Simulation experiments are conducted to illustrate the emergence of varying dynamical behaviour driven by butyrate availability. Our model predicts that butyrate production is driven by fiber consumption and further supported by probiotics in the case of microbial dysbiosis. It also suggests that butyrate may help in suppressing tumour growth. We also show that by adding noise with sufficiently high intensity, cancer elimination occurs almost surely in infinite time and that this threshold level of noise intensity decreases with increasing butyrate concentrations.

In clinical settings, predicting binary outcomes is often complicated by right-censoring, which prevents us from distinguishing individuals in whom the event never occurs (i.e., negative, or non-susceptible) from those where it occurs after the censoring time (i.e., positive, or susceptible). To discriminate between these subpopulations, we can use mixture cure models (MCMs), which model both the outcome probability over an infinite horizon and its time-to-event (TTE) distribution when observed. However, the TTE approach requires event timestamps, which can be unreliable, costly to obtain, or biased due to disparities in clinical care. Alternatively, the task can be formulated as positive-unlabeled (PU) learning, in which individuals without an observed event are grouped as "unlabeled" rather than negative, recognizing that this group includes positives whose event occurred after censoring. Here we analyze the relationship between these frameworks and provide evidence-based recommendations for choosing between them. We begin by showing that both families optimize a shared likelihood but differ in how they constrain the probability of event occurrence prior to censoring among susceptible patients, which in PU learning is known as the labeling propensity; and that an MCM may be viewed as a PU model whose labeling propensity is parameterized as a TTE distribution, which makes the model identifiable. In systematic simulations and two real-world clinical cohorts, we examine whether and when including the TTE component benefits binary classification. We show that MCMs are preferred in only one specific regime: under selective censoring where the exact features governing censoring cannot be identified. Otherwise, PU learning achieves equivalent performance while avoiding challenges and potential biases associated with the TTE approach.

Aims. Filamentary structures in molecular clouds are widely recognized as fundamental components of star formation. Observations report a length-mass relation of the form $L \propto M^\alpha$ with $\alpha \simeq 0.5$. We characterize this relation in simulated molecular clouds and investigate the influence of hierarchical fragmentation and spatial resolution. Methods. We apply a two-step filament identification method to high-resolution 3D hydrodynamical and magnetohydrodynamical simulations from the SILCC-Zoom project, combining the Rolling Hough Transform with dendrogram-based segmentation for hierarchical decomposition. We analyze the resulting structures across multiple spatial resolutions. Results. The identified structures span column densities of $\sim 10^{21}$–$\sim 10^{23}\,\mathrm{cm}^{-2}$. Across multiple resolutions and, separately, the full hierarchical decomposition at the highest resolution, the ensemble exhibits a sub-linear $L-M$ relation close to $L \propto M^{0.5}$. When individual structures are traced across resolutions, the slopes remain sub-linear ($\alpha \simeq 0.45$–$0.70$), consistent with the geometric prediction $L \propto M^{0.5}$ of a fragmentation-driven random walk. In contrast, decomposing individual structures at the highest resolution yields a wide range of slopes ($\alpha \simeq 0.2$–$3$), peaking at $\alpha<1$. A simple toy model shows that this diversity arises from differences in the internal column-density distribution and segmentation geometry. Conclusions. Taken together, these results indicate that the average sub-linear length-mass relation with $\alpha \simeq 0.5$ is a robust property of the hierarchical structure and fragmentation occurring in molecular clouds.

We use metric functionals to construct a topology on metric spaces that induces $d$-weak convergence. We show that this topology is invariant under surjective isometries and characterize its convergence in terms of weak metrics. We prove that the topology is $T_1$ on every metric space. For normed linear spaces, we further show that it is Hausdorff and coarser than the classical weak topology. Finally, we construct a sequence in $C[0,1]$ that is unbounded in the sup-norm yet converges $d$-weakly, thereby correcting an assertion in an earlier work.

Ensuring intrinsic safety in physical human robot interaction (pHRI) is a critical requirement for social and service robots. While Series Elastic Actuators (SEAs) offer hardware based compliance, traditional metallic designs often require complex, multi part assemblies. This paper presents the design, finite element analysis (FEA), and experimental validation of a low stiffness, torsional spring for SEAs, manufactured via 3D printed thermoplastic polyurethane (TPU). The compliant element exhibits a highly linear torque deformation response (Ks = 0.066 Nm/degree), matching numerical predictions with under 3% deviation, a variance attributed to FDM structural anisotropy. To accommodate external interactions using standard position limited servomotors, a hybrid position controller with torque threshold switching was implemented. Experimental evaluations demonstrate the system ability to accurately track non stationary trajectories and safely yield to external disturbances. Furthermore, the inherent material damping of the TPU acts as a passive low pass filter, preventing high frequency oscillations during control mode transitions. The proposed architecture offers a cost effective, reliable, and easily manufacturable solution for safe pHRI.

Prior work has shown that internal harmfulness representations in large language models vary across risk categories, while sharing a common general harm representation component. This raises a question about the role of the category-specific component beyond general harm representation in LLM safety. To answer this question, we isolate the category-specific component by removing shared general harmfulness representation from each categorical harmfulness representation, yielding a category residual that is orthogonal to general harmfulness at every layer. Using activation steering with category residuals across 11 risk categories in 3 instruction-tuned LLMs, we find that whether category residuals encode harmfulness varies across categories, and that this category-wise pattern is similar across models. Whether category residuals induce refusal also varies across categories, but this category-wise pattern is more model-dependent. We also find that category residuals increase LLMs' downstream internal alignment with shared general harmfulness representation. Together, these findings demonstrate that more fine-grained category residuals should also be considered beyond shared general harmfulness representation to fully understand LLM safety. More broadly, our findings show that even a direction orthogonal to a concept at one layer can contribute to the concept's downstream amplification.

The complex interaction history between the Large and Small Magellanic Clouds (L/SMC) has left significant imprints on their structural and chemical evolution. In this work, we use a sample of 70 star clusters located in the southern outer disk of the LMC ($R > 5^{\circ}$) to trace the magnitude of these tidal perturbations. Using deep $g,i$ photometry from the SMASH DR2 survey and the Automated Stellar Cluster Analysis (ASTeCA) code, we provide a homogeneous determination of cluster ages, metallicities, and heliocentric distances. Our results show a population with ages ranging from 1.02 to 3.34 Gyr and metallicities between -0.70 and -0.07 dex. We find that clusters at greater heliocentric distances are predominantly located toward the western regions, facing the SMC. Analysis of the vertical distribution reveals an oscillatory variation in the mean height ($\langle Z \rangle$) relative to the LMC mid-plane and an increase in intrinsic vertical dispersion ($W$) toward the West. These geometric features are consistent with a corrugated disk structure induced by recent tidal encounters with the SMC. Chemically, the clusters follow the age-metallicity relationship typical of the LMC and are well-represented by a bursting-type formation model. The lack of chemically distinct clusters suggests that while the interaction was sufficient to dynamically deform and corrugate the outer disk, it did not lead to significant cluster capture from the SMC. We conclude that the southern outer disk remains structurally and chemically part of the LMC, despite being heavily perturbed by tidal forces.

Health misinformation disproportionately harms women, yet interventions rarely address the community norms that sustain false beliefs. We test whether culturally adaptive AI-generated video in which the presenter looks like someone from her community reduces misinformation belief among low-literacy women in suburban India. In a field experiment (N=434), participants watched an AI-generated video featuring either an adaptive or neutral presenter. The culturally adaptive presenter reduced misinformation belief by 30%, nearly twice the reduction produced by the neutral presenter compared to the non-intervention control condition. Post-experiment interviews suggest women recalled the neutral condition as a generic video but recognized the adaptive presenter. Gains persisted for three weeks. The adaptive advantage was largest for beliefs reinforced by community, such as blaming women for infertility, and negligible for medical knowledge gaps, such as understanding vaccines. These findings demonstrate the potential of culturally adaptive AI interventions to counter socially embedded health misinformation.

The query and key projections $\WQ,\WK$ in attention are almost always trained by Euclidean optimizers with no geometric constraint. We constrain them to the Stiefel manifold and optimize with a Riemannian Adam carrying one scalar second moment per frame—the form of \citet{becigneul2019}, here extended to the compact, non-Hadamard $\St(d,r)$ with a tangent projector, step-norm cap, and polar retraction. Four propositions prove steepest descent in the embedded metric, gradient-scale independence, well-conditioning, and exact $\mathrm{O}(d)$-equivariance. A fifth records that weight decay has identically zero Riemannian gradient on $\St(d,r)$ ($W{=}WI_r$ lies in the normal space), so decay cannot act on the constrained frames. On a CIFAR-10 patch benchmark at $n{=}10\mathrm{k}$ this rule gains $\mathbf{+6.79}$\,pp over AdamW across 12 paired starts ($t{=}38.33$, $12/12$); earlier fixed-step Riemannian SGD gains $+1.97$\,pp, of which $+1.69$\,pp comes from frozen orthonormal initialization alone. The corrected Adam's lead grows with data: $+1.9$\,pp at $n{=}1\mathrm{k}$ to $+6.7$\,pp at $n{=}50\mathrm{k}$. A 12-seed ablation credits all gain to the scale-free step ($+4.63$\,pp, $12/12$), nothing to the projector or equivariance; a targeted $\varepsilon$-sweep causally confirms the mechanism ($-2.6$\,pp at $\varepsilon{=}0.1$, $p{<}0.001$). Two five-seed grokking studies confirm the constrained arm does not grok better than the baseline ($p{=}0.019$, A2 wins): the weight-decay exemption has no grokking consequence. A single-seed pilot exploiting this localization achieves the first stable grokking under slingshot conditions—Stiefel + targeted circuit regularization keeps routing-frame isometry error $10^6\times$ lower than the unconstrained ablation through every collapse.

We study high-order safety-critical control of quadrotor teams under bounded inputs and pairwise collision-avoidance constraints. Squared-distance barriers may lose thrust effectiveness when the relative displacement is orthogonal to the available thrust directions, while nonsingular constraints may still be jointly infeasible under shared bounds. We characterize both phenomena through pairwise effectiveness and aggregate feasibility measures. A torque-aware dynamic extension exposes attitude torques in a fourth-order barrier and prevents the extended-input row from vanishing under positive thrust. Gaussian processes directly learn the fourth-order HOCBF residual, providing robust margins without differentiating unknown perturbations. Under residual-bound and persistent-feasibility assumptions, the resulting QP guarantees collision avoidance and recovers the nominal input whenever it satisfies the robust safety and actuator constraints.

Rotationally excited HCN and CN lines, due to their high critical densities, are often used as tracers of gas densities. ALMA, with its high spectral and spatial resolution, provides unique access to the spatial morphology and kinematics of HCN and CN emission to study the substructures of the molecular cloud edges. We present new sub-arcsecond imaging of HCN 4-3 and CN 3-2 lines to probe the density structure in the Orion Bar. We study their spatial distribution and compare them to other existing tracers inside the PDR. We complemented these data with multiple J lines observed with the IRAM 30m and Herschel telescopes to study HCN and CN excitation near the dissociation front (DF). We find that HCN and CN emission are more spatially extended toward the more UV-shielded cloud than C2H and H2. However, they both peak very close to the DF, in disagreement with previous lower-angular-resolution observations. This morphology can be explained by the enhanced UV-driven chemistry. In dense and irradiated environments, HCN is efficiently formed via H2+CN. Hence, its emission can also probe warmer gas near the DF. CN emission is observed in the atomic PDR, not accounted by stationary gas-phase chemistry due to the very low H2 abundances. We interpret this as photoprocessing of CN-bearing PAHs. We derive high densities near the DF when comparing observations with RADEX and Meudon PDR Code models. Finally, we do not find evidence of small-scale high-density clumps and argue that the observed density gradient could explain the variation of excitation between the different tracers. We resolve two velocity components in HCN emission: 10.5 km/s (velocity of the Bar) and 11.5 km/s. The very structured emission of HCN observed in this redshifted emission component is more compatible with the signature of the propagation of a UV-induced shock compressing the gas than clumps.

The increasing complexity of modern power systems, driven by high renewable penetration, load variability, and operational uncertainty, demands fast and reliable solutions to the AC optimal power flow problem (AC-OPF). Traditional optimization methods, though accurate, often struggle with scalability and high computational burdens, making them impractical for real-time use in large networks. This paper introduces PowerModels-ACOPF-AI, a two-stage Bayesian Neural Network (BNN) surrogate designed to predict generator set points, bus voltages, and phase angles with uncertainty. The framework integrates a performance-sensitive on-the-fly learning mechanism that identifies regions of degraded prediction accuracy and dynamically retrains with additional AC-OPF solutions generated by PowerModels.jl. This self-adaptive loop ensures robust performance, enabling the model to maintain accuracy under novel or highly variable operating conditions. Validation on benchmark test systems of different sizes, namely the 30-bus, 200-bus, and 500-bus networks, demonstrates strong generalization capability, efficient handling of stochastic renewable injections, and the ability to provide rapid, uncertainty-aware predictions. Beyond predictive accuracy, the proposed approach offers practical value as both a real-time advisory tool for system operators and a fast initializer for conventional solvers, thus supporting resilient and efficient grid operation in future power systems.

Falls in older adults are often preceded by changes in mobility, balance, and postural transitions. This paper presents a wireless smart insole platform and machine-learning workflow for recognizing sitting, standing, walking, and unstable walking from plantar-pressure and inertial signals. Each insole integrates 16 active pressure-sensing locations and a six-dimensional IMU stream consisting of tri-axial acceleration and angular velocity. Data were collected from 15 healthy adults at 80~Hz and segmented into overlapping windows. Window length and candidate model families were first screened with stratified 10-fold cross-validation; the primary performance estimate was then obtained with participant-independent 5-fold Stratified Group cross-validation, ensuring that all windows from a participant remained in a single fold. Under this protocol, Histogram-Based Gradient Boosting (HGB) achieved macro-F1 scores of 0.954 and 0.959 for the left and right feet, respectively, and 0.980 with bilateral sensing. A compact 1D-CNN evaluated with the same participant-independent folds did not significantly outperform HGB ($p=0.0625$). The results show that low-profile footwear sensing can infer activity state from pressure and IMU measurements for participants unseen during training, establishing a basis for activity monitoring and fall prevention in elderly care.

Three-dimensional object detection for autonomous driving is dominated by detectors trained on large corpora of human-annotated 3D boxes. Such a detector learns a fixed category list, and everything outside it is invisible. This paper asks whether the task can be solved training-free and open-vocabulary. A promptable segmentation model (SAM3), queried with class names as text prompts, supplies instance masks in the vehicle's six surround-view cameras, and the masks are turned into metric 3D boxes using the geometry of the scene. The core is a controlled three-stage comparison on nuScenes in which 2D detection is held fixed and only the source of 3D geometry changes. Geometry predicted from images alone reaches 0.183 mean average precision (mAP) under the official protocol; fitting boxes from raw LiDAR points inside the same masks with training-free rules reaches 0.298 mAP / 0.348 nuScenes detection score (NDS) at zero labeling cost; borrowing supervised box geometry at inference time lifts the same detections to 0.413 mAP / 0.555 NDS, which locates the pipeline's largest deficit in measurement precision rather than 2D detection, while class confusion and confidence calibration survive that substitution. Reversing the direction, a three-state camera-witness rule built from the same masks improves a supervised LiDAR-only detector from 0.596 to 0.630 mAP, roughly half the gain of fully supervised camera fusion, with no training. A coverage analysis shows that SAM3 finds 84% of in-range objects with a correctly named mask; the classes that fail in the official metric are misnamed or geometrically unforgiving, not unseen.

We propose a framework for restricted inference on random dot product graphs whose latent positions lie on an unknown low-dimensional support manifold. For general decision problems, we propose semisupervised decision rules that use auxiliary data to learn the support manifold. Specifically, our rules use the Isomap manifold learning procedure to construct a low-dimensional Euclidean representation of the observed graph, in which space an isometrically invariant function maps configurations of points to actions. We study the behavior of the proposed rules as the quantity of auxiliary data sampled from the unknown support manifold increases. We show that, as the auxiliary sample size increases, the risk of the semisupervised rule converges to the risk of an oracle rule that relies on the maximal amount of low-dimensional Euclidean structure that can be extracted from the support manifold. Examples, applications, and simulation studies are deferred to a sequel.

We introduce a new method to guide flow matching models. Our approach, which we call probe guidance, uses the frozen internal states of an existing diffusion model to construct a guidance signal. This works using a similar principle as autoguidance, but eliminates the need for an additional forward pass at inference time and provides a reliable path to ensure that the weak and strong model share similar dynamics. We apply and benchmark this method on continuous diffusion language models, where probe guidance sets a new state-of-the-art performance on unconditional generation. When applied to a 1.7B diffusion language model, probe guidance consistently improves on multiple choice question answering benchmarks. Using our probes, we study the traditional autoguidance setting where the strong model is a weak checkpoint, and find that the weak model must come from a low-entropy region of training. These findings both provide a practical way to improve diffusion language models and shed light on the actual mechanism behind autoguidance, which is currently poorly understood.

We investigate pressure-dependent melting of ordered B2-NiAl using neural-network molecular dynamics with a Deep Potential interatomic model. Melting temperatures are determined from two-phase solid-liquid coexistence simulations over a broad pressure range, yielding the melting curve $T_m(P)$. Relative to available experimental and previous molecular-dynamics results, the present calculations predict a stronger increase of the melting temperature with pressure at elevated compression. To assess the thermodynamic consistency of the calculated melting line, we evaluate the enthalpy and volume changes upon melting and compare the Clapeyron slope with the derivative of the fitted $T_m(P)$ curve. The two estimates are in good agreement over most of the investigated pressure range, supporting the internal consistency of the coexistence results. To probe the character of melting, we perform a layer-resolved composition analysis of the coexistence configurations and find that the coexisting liquid remains essentially equiatomic at all studied pressures, with deviations of the aluminum fraction from the stoichiometric value not exceeding $5\times10^{-3}$. This provides direct atomistic evidence that melting of B2-NiAl remains congruent within the present model. Together, these results establish a thermodynamically consistent pressure-dependent melting description of B2-NiAl and clarify the character of its melting under compression.

Automated action quality assessment (AQA) in Olympic sports remains a challenging task due to the complexity of human motion and the subjectivity inherent in expert judging. This work evaluates the capability of open-source Vision-Language Models (VLMs) to perform zero-shot action quality assessment on Olympic diving videos using the AQA-7 benchmark dataset. In this regard, a regression-based framework is pro-posed to leverage both the semantic reasoning and phase-level sub-scores generated by the VLMs, combining TF-IDF vectorization, dimensionality reduction, and ensemble learning to predict final competition scores. Experimental results show that standalone VLMs achieve moderate Spearman correlations below 0.32, while the proposed ensemble regression framework substantially improves performance in the reported evaluation, reaching a Spearman correlation of 0.67 with a four-model configuration. Textual reasoning features con-sistently outperformed raw numerical sub-scores, highlighting the richness of VLM-generated explanations for action quality analysis. These findings suggest that VLMs hold strong potential as assistive tools for explainable and semi-automated sports performance evaluation. The code is publicly available on GitHub https://github.com/hvelesaca/olympic diving judge vlm

Proofs of UNSAT are a standard primitive in formal verification and software assurance. In many real-world settings, the proof itself encodes proprietary or security-sensitive information, making public disclosure undesirable. Zero-knowledge certification of UNSAT addresses this tension: it enables a prover to convince a verifier that no satisfying assignment exists, without revealing anything about the underlying proof beyond its validity. Luo et al. recently introduced ZkUnsat, a protocol that achieves this goal by proving the validity of a weakened resolution proof in zero knowledge. ZkUnsat demonstrates the feasibility of zero-knowledge certification; however, its scalability to larger, real-world instances is constrained by substantial prover memory overhead, limiting its real-world applicability. Motivated by advances in UNSAT proof formats such as LRAT, which enable efficient plain-text verification, we present a preprocessing technique that improves the efficiency of ZkUnsat without introducing additional leakage. Our approach normalizes the proof so that each derived clause is justified by a resolution chain of fixed public length k. This eliminates chain-length leakage and reduces prover memory usage. With k = 16, our method certifies roughly 62% more instances than baseline ZkUnsat on the SAT 2002 competition benchmarks. Furthermore, for an equivalent number of certified instances, the memory footprint drops to under 25% of that required by the baseline.

We present FloatLib, a verified arbitrary-precision floating-point arithmetic library in Lean 4 that combines broad format coverage, machine-checked correctness, and efficient certified execution. To our knowledge, FloatLib is the first Lean library to unify IEEE binary and decimal arithmetic, arbitrary-width posits, P3109, and user-defined formats and rounding rules behind interchangeable certified software backends. Every certified backend is proved equal to a complete encoded specification, preserving signed zeros and exceptional values, while numerical theorems connect execution to real rounding, error bounds, and exactness. FloatLib combines exhaustive certified tables for small formats with verified word and limb kernels based on guard-and-sticky invariants and independently checked quotient candidates. Its posit development additionally proves standard rounding thresholds and exact quire accumulation within capacity for arbitrary widths. Across matched workloads, FloatLib achieves speedups of up to 1.46x over FLoPS and 116x over Universal, while remaining slower in some regimes such as binary arithmetic against MPFR. Independent conformance testing includes more than 102 million TestFloat evaluations with zero differences under the tested relation. We release the library, proofs, benchmarks, evaluation data, and guide as open source.

Assuming Jensen's diamond principle, we construct a separable crowded compact zero-dimensional space $K$ of weight $\aleph_1$ and cardinality $2^{\aleph_1}$ such that $C_p(K)$ has no infinite-dimensional Hausdorff separable linear quotient. In particular, $K$ is an Efimov space: it contains neither a nontrivial convergent sequence nor a copy of $\beta\mathbb N$. We also prove in ZFC that the existence of a separable quotient of this kind is equivalent to the existence of a metrisable one. On the positive side, established finite-support random-sign methods give a split quotient of $C_p(K)$ onto $(c_0)_p$ whenever $K$ is infinite compact and $w(K)<\operatorname{cov}\mathcal N$, with explicit norm-one operators. Consequently, the universal quotient assertion for compacta of weight $\aleph_1$ is independent relative to the consistency of ZFC alone. A real-valued measurable continuum gives the positive result below the continuum and reduces the remaining problem to separable compacta of weight exactly the continuum. The counterexample uses direct diamond prediction, a simultaneous successor lemma, and a compactness argument converting localised measure limits into differences of point masses.

Designing road networks for wind farms in complex terrain is a challenging task, especially under tight construction budgets. Traditional manual methods are time-consuming and may yield suboptimal results. We propose a structured three-phase optimization framework, TriPhase, to automate and minimize road construction costs from corridor selection to earthwork. Phase one formulates corridor selection as a Steiner minimum tree problem over a terrain-aware graph, incorporating slope and curvature constraints. In phase two, each road segment undergoes horizontal alignment optimization using a bilevel model, where a mixed-integer program evaluates vertical alignment costs. To ensure solver compatibility and performance, the model is reformulated explicitly for Gurobi. The final phase applies a network-wide convex optimization model to refine vertical alignment. Numerical experiments on real-world sites demonstrate up to 14% cost savings compared to industry-standard manual designs, validating the framework's effectiveness and practical relevance.

Magnetic surveys are widely used in archaeology to reveal buried features by detecting variations in the Earth's magnetic field caused by past human activities. However, as sensor height increases, magnetic anomalies produced by subsurface sources weaken and broaden, posing challenges for both ground-based and aerial (UAV) surveys. This study quantifies that altitude-dependent loss of signal and spatial definition using a fully synthetic model of a uniformly magnetized circular kiln together with upward continuation of measured fluxgate data from the Storbekken 1 iron-production site in central Norway. The synthetic experiment shows that a 2 m diameter, 1 m thick magnetized cylinder buried 0.3 m below ground retains only about 11% of its near-surface (0.2 m) peak amplitude at 2 m sensor height and about 3% at 4 m. In the hybrid experiment, composite furnace anomalies of several hundred nanoteslas collapse to tens of nanoteslas by 2 to 3 m, while distinct lobes merge into broad, low-contrast features. The results show that UAV-borne magnetometry can remain effective for site detection and delineation at elevations where detailed intra-site morphology is already strongly degraded. For small or subtle archaeological targets, sub-metre to low-metre sensor heights provide substantially greater interpretative detail. Recent field evidence on UAV-system noise further indicates that practical detectability will depend not only on source-distance attenuation but also on platform configuration and acquisition strategy. The resulting attenuation curves and morphological observations provide transferable guidance for planning archaeological and shallow-geophysical UAV magnetic surveys.

Topological phases of periodically driven systems are commonly classified through Floquet Hamiltonians, whose definition relies on a repeated driving cycle. However, this framework breaks down for systems whose realized evolution is aperiodic or nonlinear, even when robust topological phenomena appear to persist. Here, we introduce an evolution-history spectral localizer framework that classifies Chern topology directly from a system's finite-time unitary evolution operator. The method produces a time-resolved local Chern marker and an associated local gap, allowing topology and its protection to be tracked during the actual dynamics of a driven system. We demonstrate this approach in quasiperiodically driven and nonlinear photonic models, where it identifies transient topological protection, its subsequent loss, and the recovery of topology after nonlinear excitations disperse. The developed framework provides a route for analyzing driven photonic systems whose topological behavior depends on finite-time dynamics rather than an idealized Floquet cycle.

Robotic additive manufacturing (AM) extends material-extrusion printing beyond gantry kinematics but makes process planning robot-dependent. A slicer-generated plan that appears favorable in part coordinates can become infeasible or robotically unfavorable on a manipulator because slicer-process decisions and part orientation determine the generated path, while part orientation and workspace placement affect its kinematic realization. Existing AM tools, large language model (LLM)-based decision-support methods, and digital-shadow systems do not provide integrated pre-execution evaluation of these coupled decisions. This paper presents agentic robotic additive manufacturing (A-RAM), an agent-specialist-tool framework that converts user intent and a part file into traceable, execution-ready plans. The LLM interprets manufacturing objectives and constraints, identifies prescribed and searchable planning variables, and encodes this reasoning in a schema-constrained request; a deterministic Planning Agent instantiates the corresponding search workflow, while domain tools compute quantitative evidence for slicing, placement, inverse kinematics, trajectory timing, Joint-6 jerk, and extrusion. The framework is evaluated on a six-axis robotic-arm AM cell through three case studies covering expert-specified planning, goal-only planning, objective-dependent infill screening, and geometry-dependent orientation-placement selection. Across the evaluated candidate sets, selected plans achieve up to 53.5% lower maximum Joint-6 jerk and 48.3% lower mean absolute Joint-6 jerk than the least favorable valid candidates, while objective-specific infill screening yields motion-plan completion times up to 40.1% shorter and extrusion paths up to 12.7% shorter than the corresponding least favorable screened patterns.

According to the classical Skitovich–Darmois theorem, the Gaussian distribution on the real line is characterized by the independence of two linear forms of a finite number of independent random variables $\xi_j$. This theorem has been extended in various directions. In particular, S.G. Ghurye and I. Olkin established an analogous result for the case where $\xi_j$ are $n$-dimensional independent random vectors and the coefficients of the linear forms are invertible $n\times n$ matrices. Subsequently, A.A. Zinger and later I.A. Ibragimov investigated linear forms of an infinite sequence of $n$-dimensional independent random vectors. In the present paper, we investigate, for the first time, linear forms of a sequence of independent random variables taking values in a second-countable locally compact Abelian group $X$ under either of the following conditions: $X$ contains no nontrivial compact subgroups, or $X$ contains no subgroups topologically isomorphic to the circle group and has a finite topological automorphism group. Furthermore, we investigate the case where the independent random variables take values in an $\mathbf{a}$-adic solenoid $\Sigma_{\mathbf{a}}$. In all these settings, the coefficients of the linear forms are topological automorphisms of the corresponding group.