We show that information on the first server influences the expected total number of games and margin in a tennis match under the standard assumption that each player's serve point win probability remains constant, and identify the exact regions, in terms of these probabilities, in which this effect is non-negligible. We confirm numerically that this effect is bounded by at most $0.4$ games at both the set and match level. This translates, for example, to roughly a $9$ percent shift in the probability that a match exceeds $19.5$ games when the players' serve point win probabilities differ by $10$ percent. We complement the analysis with an empirical comparison on professional match data, illustrating the adequacy of the constant-probability assumption for modelling the total number of games.

Classroom dynamics depend on various elements that influence teaching performance and learning activities. A key challenge is to determine the most effective seating plan, where students will seat in a specific classroom setting to achieve the best learning environment. This paper introduces the Student Seat Allocation Problem (SSAP) for strategically organizing student seating in traditional classrooms to minimize interpersonal conflicts. We propose a mathematical model and an Iterated Local Search (ILS) heuristic to solve the SSAP. Computational experiments demonstrated that ILS outperformed in more complex scenarios when compared to the results obtained by a commercial solver on the introduced mathematical model. ILS was particularly efficient in real and artificial instances that exhibited a higher number of conflicts.

We study the generalized Lam'e equation (GLE) on an elliptic curve $E$ with multiple regular singularities $\mathbf{p} = (p_i)_{i = 1}^r$ of weights $\mathbf{n} = (n_i)_{i = 1}^r$. By analyzing the locus admitting quasi-periodic solutions, we construct two fundamental algebraic curves: (i) The generalized Lam'e curve (GLC), $\mathcal{Y}_{\mathbf{n}, \mathbf{p}}$, which lies in an affine bundle over $\operatorname{Sym}^n E$ for total weight $n:=\sum n_i \in \mathbb{Z}_{\geq 0}$ and parametrizes generalized Hermite--Halphen ansatz solutions. (ii) The log-free curve, $V_{\mathbf{n}, \mathbf{p}}$, a non-complete intersection variety arising when all $n_i \in \frac{1}{2}\mathbb{N}$, which we prove is a reduced curve, confirming a conjecture of Wang. We analyze the GLC as an algebraic family over the pole configuration space. By studying the addition map$$σ\colon \operatorname{Sym}^n E \longrightarrow E,$$where we establish a generically finite, universal degree formula, we show that the geometry of boundary degenerations under pole collisions perfectly mirrors the tensor algebra of $\mathfrak{sl}_2(\mathbb{C})$-modules within the BGG category $\mathcal{O}$. This provides the local structural limits needed to establish the global flatness of the GLC. Furthermore, we develop a framework of twisted isomonodromic deformations and construct $(\mathbf{n}, \mathbf{p})$-deformed pre-modular forms parameterized by twisted monodromy data $(t,s)$. Their vanishing solves the underlying monodromy problem and factorizes along boundary strata, allowing an arbitrary configuration to be continuously deformed down to the classical Lam'e equation. Finally, using an asymptotic scaling technique, we completely solve the Treibich conjecture for $r=2$ symmetric pairs, extend it to $r \leq 4$, and propose a general formula enumerating symmetric finite-gap KdV potentials for all $r$.

Let $ζ$ be Euclidean norm of the degree sequence of a graph normalized by the graph size. We prove that when the vertices of a graph are randomly colored with $s$ colors such that the fraction of vertices in each color class is bounded away from zero, only two asymptotic regimes emerge. If $ζ=o(1)$, then the sizes of the subgraphs induced by the color classes concentrate around their expected values. If $ζ=Θ(1)$, then concentration depends on the color balance: for colorings with persisting imbalance, the total number $M$ of monochromatic edges stays bounded away from its mean with positive probability; otherwise, for vanishing imbalance, $M$ still concentrates. The same dichotomy holds for a broad class of randomly colored random graphs.

We study projection-based diagnostics for distinguishing directional asymmetry from tail-ratio departure in multivariate data. The procedure reduces the problem to one-dimensional projections and computes two quantile-based summaries: a directional skewness measure evaluated over several quantile levels, and an interquantile tail-ratio evaluated relative to a chosen benchmark. The two summaries lead to a four-regime classification: symmetric benchmark-tail, symmetric tail-departed, skewed benchmark-tail, and skewed tail-departed. The quantile formulation avoids relying on third and fourth moments, which can be unstable in heavy-tailed settings. We establish population properties under central symmetry and ellipticity, uniform finite-sample bounds over the searched directions, and consistency of the threshold classifier under separated regimes. A sparse rank-one calculation is also used to show why coordinate directions can complement random directions in high dimensions. The resulting diagnostic is meant to guide subsequent modelling choices, for example whether a symmetric, skewed, tail-departed, or combined multivariate model is appropriate.

While principal component analysis (PCA) is a fundamental tool for dimensionality reduction, its dense representations make it ill-suited for high-dimensional data. Existing methods address this by promoting sparsity through explicit $\ell_1$-penalties, but these are not obvious to tune due to the unsupervised nature of the task. In contrast, we propose Adversarial PCA (AdvPCA), which leverages robust optimization to achieve sparsity by optimizing the reconstruction objective against bounded, worst-case latent space perturbations. We show that this formulation admits a closed-form reduction, leading to a practical iterative algorithm that alternates between adversarial linear regression-style updates for the sparse encoder and orthogonal updates for the decoder. By theoretically characterizing the solution, we derive a data-adaptive parameterization that allows the algorithm to perform effectively out of the box. We validate these claims through numerical experiments on synthetic and real-world genomics data.

Modeling high-dimensional data is challenging, yet essential to understanding many complex systems. Maximum entropy models such as Ising and Potts models have been used extensively to capture pairwise interactions from correlation patterns in data, allowing to infer graphical representations of complex systems from observations (e.g., from protein sequences or neural population activity). Recently, there has been growing interest in modeling higher-order correlation patterns involving simultaneously three or more variables. While progress has been made in binary data with high-order Ising models, we extend this framework to the more general case of discrete data. We introduce q-state spin models, a complete family of maximum entropy models that generalize the vector Potts model to include long-range and arbitrary high-order interactions. In the pairwise case, our models allow for more diverse interaction types compared to the standard vector Potts model. We discuss their statistical interpretation with examples and relate them to discrete Fourier analysis. Using a loop expansion of the partition function, we show that the statistical properties of spin models are fully captured by the algebraic structure of their interactions. We define gauge transformations under which this structure, and thus the partition function, remains invariant. Models equivalent under gauge transformations can be seen as different representations of the same abstract statistical model, despite generally having interactions of different orders, extending results from the binary case. For practical application to data analysis, we focus on a subset of models known in the binary case as Minimally Complex Models, generalizing them to discrete data. We obtain a closed-form expression for the marginal likelihood of these models, enabling fast model selection. We illustrate their use with simple real-world examples.

Modeling interactions among multimodal, high-dimensional data is intrinsically challenging due to ultra-high dimensionality and complex dependence structure with high level noise. Screening methods are effective for reducing dimensionality, but most existing approaches shrink only the predictor space while retaining all outcomes. In cross-modal analyses, different outcomes often select different predictor subsets, so the union remains large and the response dimension is unchanged, limiting the practical benefit of screening. This gives rise to heavy computational burdens and poor interpretability. To address these limitations, we propose a new screening framework, Graph Independence Dual Screening (GIDS), which simultaneously reduces the dimensionality of response variables and predictors. We design computationally efficient algorithms that facilitate downstream selection procedures, improving accuracy and scalability, and establish supporting theoretical results. Extensive simulation studies demonstrate that GIDS outperforms existing methods that screen only predictors. To illustrate its utility, we applied GIDS to the Alzheimer's Disease Neuroimaging Initiative (ADNI) dataset, analyzing interactions between genome-wide 865,353 DNA methylation and 49,386 transcriptomic variables. GIDS reduced the feature space to approximately 9,000 CpGs and 2,000 transcripts, uncovering blockwise interaction structures: clusters of CpG sites and gene transcripts with strong associations. These findings not only improve computational tractability but also yield interpretable biological insights, highlighting coordinated regulatory mechanisms underlying Alzheimer's disease.

We study an infinite-horizon optimal consumption-investment problem for an investor with Epstein-Zin stochastic differential utility with stochastic investment opportunities in an incomplete market. Risk aversion and intertemporal substitution are separated, and we work in the regime $θ\in(0,1)$, where there exists a unique generalised utility process for arbitrary non-negative progressively measurable consumption streams. Our main contribution is a variational characterisation of the value function. We show that the value function is the unique minimiser of a functional whose Euler-Lagrange equation coincides with the Hamilton-Jacobi-Bellman equation. Although the functional may be non-convex, the direct method yields existence, and we prove every minimiser is strictly positive, bounded, and classical. A verification theorem identifies any minimiser with the value function and gives feedback representations for optimal consumption and investment policies. The proof combines a change of measure to the myopic probability with uniqueness results for Epstein-Zin BSDEs and a perturbation argument for optimality. Examples with stochastic volatility, Gaussian excess returns, and fat-tailed excess returns illustrate the scope of the framework and its implications for intertemporal hedging.

Recently, the mapping of the replicator equation onto Bayes' theorem has been recognised, leading to an analogy between evolutionary dynamics and Bayesian learning. However, this analogy holds only for pure selection in infinite populations and breaks down when mutations -- a central mechanism of evolution -- are introduced. Here I propose that evolution by natural selection, at least for populations of haploid replicators in static environments, is best understood not as a learning process but as a process of causal inference. Each mutation event constitutes a natural experiment in which the parent serves as the control and the mutant offspring as the treated unit. Natural selection screens the causal effect of the mutation on fitness, retaining mutations with non-negative effects. I formalise this view within the Neyman-Rubin potential-outcomes framework. I first develop the general theory using a generic fitness outcome and show how the core identification assumptions in causal inference (Stable Unit Treatment Value Assumption, Consistency, Unconfoundedness, Positivity) map onto evolutionary biology. Using the unnormalised quasispecies equation, I prove that the intergenerational change in mean fitness decomposes exactly into a selection term -- recovering Fisher's Fundamental Theorem -- plus a mutation term that corresponds to a fitness-weighted average of the cumulated effect of all mutations over all parental genotypes. I show that this decomposition extends, under suitable assumptions, to the generalised replicator-mutator equation and that the frequencies of populations of matched parents-offspring update in proportion to the average causal effect of mutations on fitness.

Computing the Lipschitz constant of the solution map of a multi-parametric quadratic program is important for the analysis of optimization-based control. This problem is governed by three factors: the parameter dimension, the number of decision variables, and the number of constraints. While empirical evidence has long suggested exponential complexity, a rigorous complexity-theoretic proof has been lacking. In this paper, we fill this gap by proving that this problem is not only NP-hard but also APX-hard. Furthermore, we reveal that: (a) the problem becomes polynomial-time solvable when the number of constraints or decision variables is fixed; and (b) both NP-hardness and APX-hardness persist even in the scalar parameter case. These results confirm that the complexity stems from the number of constraints and variables, rather than the parameter dimension. Numerical experiments further validate these theoretical findings.

Formal rigor distinguishes mathematics from other disciplines, in the sense that mathematical statements are derived from explicit axioms by logically verifiable steps. Interactive theorem provers support this by expressing definitions, theorems, and proofs in a fully formal language and verifying them mechanically. We consider the benchmark problem of formalizing all published mathematics as a machine verifiable and continuously updated corpus of mathematical knowledge. This viewpoint treats mathematics as a structured database of interdependent results and raises questions about scalability and organization of large formal libraries. As a case study, we present an ongoing formalization in categorical algebra, namely dilatations of categories, extending classical localizations and illustrating what such an implementation looks like in practice.

LLM pipelines waste substantial token budgets on low-information content: repeated context, verbose responses, and redundant boilerplate. We introduce Entropy Gate, a token compression framework applying entropy quenching $-$ a thermodynamic process that progressively freezes out low-energy tokens while preserving semantic fidelity. Each token receives a multi-factor information energy $E(t)$ combining statistical, structural, and positional components. An adaptive quenching schedule $T(τ) = T_0 / (1 + ατ)$ removes tokens whose Boltzmann survival probability $p_i = \exp(-E_i / kT)$ falls below threshold, with a fidelity gate halting compression when energy-weighted similarity drops below $θ$. We prove token selection by descending $E(t)$ maximizes expected semantic preservation, that quenching produces nested survival sets, and that achievable compression approaches the information-theoretic limit $\text{CR} \to 1 - I(P; T)/H(P)$. A Phase 1 heuristic achieves 40-60% compression across five prompt categories while maintaining $S_E > 0.80$, with energy-squared amplification $E \to E^2$ adding 10-25 percentage points. Context deduplication adds 50-70% savings on repeated blocks. Output-side quenching, motivated by findings that brevity improves accuracy, further reduces response overhead. Combined with external memory, reduction composes multiplicatively to 88-96% for agentic workloads. The framework is stateless, model-agnostic, and deploys as an OpenAI-compatible HTTP proxy.

Non-negative reduced biquaternion matrix factorization (NRBMF) uses the product of reduced biquaternion (RB) matrices to incorporate the non-negativity constraints of color image pixels into the factorization process. However, NRBMF mainly focuses on reconstruction accuracy and does not exploit the local geometric structure of image data, which may limit the discriminative ability of the learned low-dimensional features. To address this issue, we propose a graph regularized non-negative reduced biquaternion matrix factorization (GNRBMF) model for color image recognition. The proposed model incorporates a graph Laplacian regularizer into the reduced biquaternion coefficient matrix, encouraging nearby samples in the original space to have similar representations in the learned feature space. Meanwhile, GNRBMF retains the non-negativity-preserving property of NRBMF in the reduced biquaternion domain. To solve the optimization problem, a component-wise alternating projected gradient algorithm is derived, and its convergence properties are analyzed. Experimental results demonstrate that the proposed GNRBMF model achieves competitive or superior recognition performance in some tested settings.

Channel charting enables location-based services (LBSs) without requiring explicit position information by using pseudo-locations from the channel chart. While this property implies inherent privacy advantages, it does not provide formal privacy guarantees. In this work, we address location privacy in channel charting referred to as chart location indistinguishability (CLI), which extends geo-indistinguishability (GI) to channel charting representations. In order to achieve CLI, a standard planar Laplace mechanism is investigated and a geometry-aware Mahalanobis norm planar Laplace (MNPL) mechanism is devised. The proposed MNPL mechanism perturbs the channel chart by injecting noise aligned with the local structure of the chart. In the CLI framework with MNPL, privacy is defined in latent channel chart manifolds using locally adaptive covariance derived from chart neighborhoods, while preserving manifold topology under privacy constraints. In addition, differential privacy is considered as a privacy baseline. The proposed approach is evaluated across multiple channel charting schemes. The performance is assessed using utility metrics such as quality loss (QL) and range query error (RQE), as well as geometry-aware metrics including trustworthiness (TW) and continuity (CT). Numerical results demonstrate that the proposed privacy mechanism provides strong privacy guarantees while preserving the channel chart for LBSs tasks.

Hyperparameter optimization (HPO) for Random Forest faces a specific difficulty in tuning the number of trees: the predictive score typically improves monotonically with ensemble size, so standard methods such as Tree-structured Parzen Estimator (TPE) and Hyperband require a predefined search range and often drive the estimate toward its right boundary. Early-stopping strategies avoid fixing such a range, but can be sensitive to score noise and prone to premature stopping. To address this, we propose an integrated triplet-based plateau-search algorithm that removes the number of trees from the direct TPE search space and still exploits information accumulated across HPO trials. The method adaptively tracks a near-minimal sufficient ensemble size by monitoring relative changes in the out-of-bag (OOB) score across a triplet of forest sizes and shifting this triplet accordingly. This yields an automated and user-interpretable procedure based on a tolerance parameter. We also provide a theoretical analysis: we relate the proposed relative OOB-score criterion to the gap between the current and limiting scores, and derive an asymptotic variance estimate for the corresponding OOB-based absolute relative difference. Experiments show that the selected number of trees can differ substantially from the common heuristic: for most classical benchmark datasets it is smaller, whereas for some high-dimensional bioinformatics datasets, such as Arcene and Dorothea, it is larger. The source code and reproducible experiments are available at https://github.com/lange-am/rf_plateau_hpo.

Quantum computing presents a promising method to overcome the efficiency and memory constraints in large-scale mechanical problems, with numerous successful applications demonstrated in fluid mechanics. However, solid mechanics problems usually require irregular grids for spatial discretization, due to the Lagrange formulations and complex boundaries, which makes the quantum simulation of the system matrix, e.g., the mass or stiffness matrix which is often referred to as the Hamiltonian in quantum computing, difficult to be effectively conducted. This study proposes a voxel-based quantum computing method (VBQC) for the quantum simulation of Hamiltonians in solid mechanics. VBQC applies voxel grids to discretize the spatial domain, thereby enabling the system matrix to exhibit the tridiagonal fractal property. Based on this property, the system matrix can be decomposed into three groups of fundamental matrices, $\mathbf{k}_{n}$, $\mathbf{c}_{n}$, and $\mathbf{q}_{n}$. This decomposition process is referred to as the KCQ decomposition. By integrating the KCQ decomposition with the quantum Fourier transform and the quantum multiplexer, VBQC enables efficient quantum simulation of Hamiltonians in solid mechanics. Three specific solid problems with different dimensions and numbers of variables are applied to preliminarily verify the correctness of the proposed VBQC for solid mechanics problems.

We answer a question posed by Poggiolesi concerning a syntactic decidability proof for GL in the tree-hypersequent system CSGL, and resolve a challenge identified by Maggesi and Perini Brogi, who sought a PSPACE proof-search algorithm for GL in expressive sequent-based formalisms. We work with a notational variant of CSGL formulated in terms of (labeled) tree sequents. Our answer is complexity-optimal: we present a proof-search algorithm that decides the (in)validity of formulae and runs in PSPACE, matching the known PSPACE-completeness of GL. To achieve this, we introduce a "linearization method," which constructs only a single branch of a derivation and of a tree sequent at a time, avoiding the exponential blowup typical of naive proof-search in sequent formalisms. We show how to systematically combine fragments of tree sequents generated during proof-search to extract finite counter-models, which serves as a theoretical device for establishing the correctness of the algorithm when proof-search fails. Finally, we show that every valid formula admits a proof consisting solely of line sequents, which correspond to linear nested sequents. This establishes a connection between depth-first proof-search and linear nested sequent calculi. Our results not only answer the aforementioned questions, but also provide new insights into proof-search and correctness arguments in tree sequent systems for modal logics.

We introduce and investigate non-wellfounded and cyclic linear nested sequent calculi, and, as a case study, develop such systems for linear temporal logic (LTL). The paper addresses two central problems, which we call 'cycle recognition' and 'unraveling.' Cycle recognition concerns identifying cycles in non-wellfounded proofs in order to extract corresponding cyclic proofs, while unraveling studies the converse transformation, from cyclic proofs to non-wellfounded ones. Although these processes are well understood for Gentzen sequents, they have received little attention for more expressive sequent formalisms and become more challenging in the linear nested sequent setting. To address cycle recognition, we show the completeness of non-wellfounded proofs relative to a particular normal form exhibiting a property we call 'saturation recurrence,' which enables the systematic extraction of cyclic proofs. To address unraveling, we introduce a specialized procedure that shifts rule applications forward along linear nested sequents, allowing non-wellfounded proofs to be reconstructed from cyclic ones. Overall, our work provides new proof-theoretic techniques for cycle recognition and unraveling in expressive multisequent formalisms.

We identify two constructions from different mathematical traditions. In linear logic and realisability, logical types are generated rather than fixed in advance: one begins with a universe of realisers equipped with execution, uses orthogonality to test their interactions, and takes types to be the biorthogonally closed subsets. In enriched Isbell duality, a quantitative relation induces an adjunction whose fixed points form a category, its nucleus. These constructions proceed by different means; we show that, in the present setting, they produce the same objects. The shared datum is minimal: an associative product, called execution, and a real-valued measurement, with no compatibility assumed between them. The failure of the measurement to be additive is at once the relation defining orthogonality and the quantitative relation whose Isbell nucleus we form, and the types cut out by orthogonality are exactly the fixed points of the associated adjunction. The identification pays off in both directions. The most natural product of types fails to be associative; repairing this failure forces a different notion of type, sensitive to both sides of a composite, on which the induced product is associative and, when execution has units, carries two residuals. What emerges is a noncommutative Lambek calculus, derived directly from execution and orthogonality rather than imposed. In the reverse direction, each such type, read on the categorical side, generates a quantitative relation of its own, and with it a derived adjunction and a further generation of types; these derived types are again types of the original situation, computed by the residuals of the Lambek calculus. We also prove a coherence theorem for the threefold arrangements of this construction and, in the finite-dimensional case, give explicit formulas for the product.

We present a framework to generalize the standard b-ary Gray code to get the k-bonacci ones obtained in [5] as well as many others by using theoretical tools that allow to make calculations on lists. We introduce the notion of Z-Gray product, from which we deduce sequences of lists of finite words avoiding a predefinite list Z of factors and which satisfy a power-associativity property as well a generalizations of the classical flipping digit property.

Neural operators learn mappings between infinite-dimensional function spaces and provide a data-driven surrogate modeling paradigm for parametric partial differential equations (PDEs). Existing architectures typically obtain expressivity by parameterizing integral kernels in prescribed transform domains or by applying attention-like interactions over discretized spatial points. While these approaches have achieved substantial progress, they often face a persistent trade-off among physical interpretability, nonlocal spatial communication, mesh scalability, and computational cost. We propose a Light-inspired neural operator(LiNO), an operator-learning architecture whose latent evolution is decomposed into three mechanisms motivated by elementary light transport: reflection, refraction, and scattering. Reflection and refraction act as adaptive pointwise transformations in latent feature space, enabling local feature reorientation and anisotropic modulation, whereas scattering performs input-dependent nonlocal propagation over the physical domain. We first formulate scattering as a normalized pairwise kernel with relative positional bias, and then develop an efficient scattering variant that replaces explicit pairwise interactions with positive-feature global propagation and a local diffusion branch, reducing the dominant spatial complexity from quadratic to linear. This yields a structured neural operator that separates local feature modulation from global spatial communication while retaining a modular and interpretable latent evolution.

Automatic-differentiation-based inverse analysis methods, including physics-informed neural networks (PINNs) and differentiable programming, have recently shown great promise due to their ability to compute accurate gradients and convergence efficiency. However, their applicability to falling weight deflectometer (FWD) backcalculation remains unexplored. This study critically evaluates PINN-based inverse analysis for a multilayer pavement system and investigates differentiable finite element method (DiffFEM) as an alternative based on a synthetic benchmark. The standard PINN does not recover layer moduli because of the sharp domain discontinuities inherent to layered pavement systems. Although we use an extended PINN with domain decomposition (XPINN), which shows better performance on discontinuous domains, its performance remains highly sensitive to loss weighting and network architecture, and degrades under measurement noise. By contrast, DiffFEM consistently achieves more accurate, stable, and computationally efficient inversion results. These results indicate that DiffFEM, which enforces the governing physics as a hard constraint, yields better accuracy, robustness, and computational efficiency than PINN-based approaches, in which the governing physics is imposed as a soft constraint through the loss function. More broadly, the findings suggest that the choice between PINN- and DiffFEM-based inverse analysis needs careful consideration, with DiffFEM offering practical advantages when an efficient and robust differentiable forward solver is available.

The Membership Problem for Pedigree Polytope (M3P) asks, given $X\in\mathbb{Q}^{\binom{n}{3}}$, whether $X\in\mathrm{conv}(P_n)$, where $P_n$ is the set of all pedigrees. A pedigree is a structured encoding of a Hamiltonian cycle construction in $K_n$. We establish that M3P is solvable in strongly polynomial time via a recursively constructed layered network $(N_k, R_k, μ)$ and a multicommodity flow problem MCF$(k)$. The necessary and sufficient condition for membership established is that the optimal total flow in MCF$(n-1)$ equals the maximum possible flow $z_{\max}$. The complexity analysis, grounded in Tardos's strongly polynomial algorithm for combinatorial linear programs (1986), shows that this condition can be checked in strongly polynomial time in the dimension of the matrix involved. By sufficiency, this implies M3P~$\in$~P. Since the Symmetric Travelling Salesman Problem (STSP) reduces to M3P via the Multistage Insertion (MI) formulation (Arthanari 1983), STSP is solvable in polynomial time, and the P vs.NP question is resolved. The proofs leading to this result are fully machine-verified in Lean~4/Mathlib4, with zero unresolved \texttt{sorry}s in the main proof chain. The main contribution is the Lean~4 machine verification of all proofs in the main chain, resulting in \texttt{theorem p\_equals\_np}: P = NP. The Lean~4 formal verification covers the sufficiency of MCF(n-1) for membership in $\mathrm{conv}(P_n)$, and the P = NP chain via Maurras (2002), Grötschel--Lovász--Schrijver (1988), Cook (1971), and Karp (1972). The complete lean project (36 Lean~4 files, 2968/2968 build targets clean) is available at https://github.com/TiruArt/Pedigree-Polytopes-Lean4.

Understanding how structured internal structure emerges during neural network training is central to the study of deep learning. We investigate this phenomenon through the group composition task, where a two-layer neural network is trained to predict $g_1 \star g_2$ for elements of a finite group $G$. By lifting the projected gradient flow to the Fourier domain, we demonstrate that the training dynamics are governed by a Riemannian gradient ascent on a representation-theoretic energy functional. We prove that, under random initialization, this flow drives each neuron to converge almost surely toward a single irreducible representation, while the cross-layer Fourier coefficients achieve a rotational rank-one alignment. This framework provides a representation-theoretic account of feature learning and characterizes a novel low-rank compression phenomenon for matrix-valued group representations. Moreover, for Abelian groups, we provide a complete population-level description: random initialization promotes uniform diversification across nontrivial representations and induces Haar-uniform phases, jointly approximating the indicator via a majority-vote mechanism. We further prove that both phase alignment and representation competition emerge with exponential convergence rates.

This paper examines three approaches for modeling the dynamics of a flexible-link 2-DoF robotic arm to address unmodeled dynamics not captured by rigid-body models. Two physics informed models combine rigid-body dynamics (RBD) formulations with a Gaussian Mixture Model (GMM) to capture residual model errors and linkage flexibility. A kinematics-based regression model serves as a purely data-driven baseline. Using an open-source dataset, torque predictions are first estimated using Ridge regression on kinematic features, while the physicsbased baseline is constructed from published specifications, and ordinary least-squares regression is subsequently used to estimate the same parameter set directly from data. Results show that the physics-based parameters yield the poorest accuracy, while regularized and least-squares estimators align more closely with measured torques. Residual analysis and error metrics highlight the limitations of purely parametric models for flexible-link systems and underscore the value of regularization and data-driven identification, supporting developments of semi-parametric residual learning methods.

Public scientific and metrology releases can leak the hidden settings that produced them. We formalize and quantify this risk as a profiled statistical side-channel audit: a release map exposes finite-band statistics of a power spectral density (PSD), a profiled observer trains labeled template spectra under an explicit budget, and a challenge release is drawn from one of two utility-equivalent recipes separated by a protected coordinate. Averaged PSD bins follow a gamma channel, replaced by a covariance-weighted log-spectrum channel when the bins are correlated; this yields exact Kullback-Leibler divergences, Chernoff exponents, protected-bit advantage bounds, and finite-training, finite-library, finite-compute, and model-mismatch corrections. Our headline result is a finite-band transport-leakage law: after amplitude and blur are eliminated, the protected acid-transport information obeys $I_{λ|α,β}(K) = (64/1225)\, w λ^{6} K^{9} + O(w λ^{8} K^{11})$ for $Kλ\ll 1$, a ninth-order exponent with a closed-form safe band. A step-by-step protocol turns a measured release into these numbers, and a fixed-seed reproducibility package regenerates every table and figure. We instantiate the audit on screened extreme-ultraviolet (EUV) roughness spectra as a model-conditioned case study, with deployment on measured releases the next step.

Symmetric nonnegative matrix factorization (Symmetric NMF) approximates a matrix as $WW^T$ with nonnegative rectangular factor $W$. It has broad applications in graph clustering and machine learning. In contrast to the NMF, projected gradient methods for the symmetric problem had been associated with slow convergence. To address this, we introduce SNMPBB, the first adaptation of nonmonotone projected Barzilai-Borwein methods to Symmetric NMF, demonstrating that gradient algorithms are significantly more effective than previously understood. We further extend SNMPBB to graph clustering using the graph Laplacian regularization (Graph-SNMPBB) and to large problems with low-rank approximations (LAI-SNMPBB). For all variants we prove global convergence to first-order stationary points and also that Barzilai-Borwein curvature information is preserved with randomized approximations. On synthetic data, SNMPBB achieves 6 times speedup over the alternative SymANLS for similar residuals, with advantages growing at higher ranks. Across six real-world clustering benchmarks, Graph-SNMPBB matches or exceeds SymANLS accuracy. Lastly, LAI-SNMPBB outperforms state-of-the-art LAI-SymPGNCG on 34 SuiteSparse matrices in both runtime and residual quality.

For fans of Gabriel's "Worse is Better" it may be ironic that C++, by way of MLIR, serves as the scaffold for compiling an ML-family language whose correctness properties are structural. A crucial intersection in our Composer compiler initiates its lowering with a fixed-point combinator that preserves the dimensional, grade, escape, and numeric-representation structure from the Program Semantic Graph. And the MLIR that's witnessed from the PSG is no passive host. Its use of static single assignment, attribute system and dialects carry that structure materially. We show that our compiler middle end uses categorical construction for lowering code with companion verification to that strata: a functor from the compilation poset to a target category, subject to the compositionality equation. The grounding of our approach comes from three sources, each on its own algebraic object: Ohori's machine-code proof theory grounds the compilation axis, parametricity grounds the content at the base, and adjoint mode logic grounds the traversal between our verification tiers. To extend the thesis we introduce compact-closed negative and fractional types, and show the type machinery can be carried with preserved structure and realized through tooling MLIR provides. More broadly, the same fixed-point primitive that preserves types through compilation also supplies proof terms that can continue to be exercised in MLIR to verify its integrity as lowering proceeds through the pipeline. We argue that this foundation is a unique additional point anticipated by our framework that includes dimensional types, Tarau's groupoid, and cellular sheaves. Throughout, the formalism is instrumented as an internal scaffold: the abstractions support the compiler's mechanics, where a developer is never required to reach for category theory in order to rely on the guarantees the compiler provides.

Deep neural networks learn representations where individual features often lack interpretable meaning; a single neuron may activate for scattered, unrelated inputs. We introduce coherence, a geometric property inspired by neural coding in the brain, where neurons like grid cells and head direction cells respond to contiguous regions of state space. A non-negative matrix is coherent if each row (sample) attends to geometrically clustered columns (features) and vice versa, and in addition every sample is well described by some feature and every feature is needed by some sample. We prove that coherent matrices induce a bounded interleaving between the Vietoris-Rips filtrations of samples and features, guaranteeing that both spaces share compatible topological structure. This geometric constraint facilitates interpretability. For example, if data lies on a circle, coherent features must tile that circle into contiguous arcs. We introduce Coh, a differentiable objective function based on Fréchet variance that enforces coherence during training. Unlike sparsity, which bounds how many samples a feature activates on, coherence bounds which samples, requiring geometric connectivity rather than only rarity. This yields not just interpretable features but an interpretable feature space. We validate Coh in an auto-encoder using synthetic and rotated MNIST datasets and in a token embedding of BERT using language data.