论文库

We develop a mathematical abstraction for uniformly exploiting symmetries in programming and reasoning based on the mathematical proof principle `without-loss-of-generality' (w.l.o.g.). Given: group actions that describe symmetries of the input and the output; and a canoniser, which captures how arbitrary inputs get sent to canonical ones, our construction extends any function from the canonical inputs to the whole domain. We characterise the conditions on the canonisers which guarantee that the construction gives the unique equivariant (i.e. symmetry-preserving) extension. Furthermore, we adapt the construction to a dependently-typed setting, where it captures traditional symmetric w.l.o.g. arguments via the Curry-Howard correspondence. Finally, we extend the construction to algebraic data types, where the symmetries of the constructors both uniquely determine the symmetries of the data type and pave the way for efficient execution.

Discovering continuous symmetries directly from differential-equation data can reveal geometric structure for model reduction and scientific machine learning without symbolic determining equations or a closed-form representation of the governing system. We formulate intrinsic Lie point-symmetry discovery as an operator-theoretic problem on sampled jet-space data. Admissible generators are identified from a sampled determining operator and separated from redundant, solution-dependent, and geometrically trivial directions. The framework combines prolongation, sequential subspace restrictions, and a fixed nonlinear dictionary linear in trainable coefficients. A rank-stabilization preflight test diagnoses systems whose represented intrinsic symmetry algebra does not stabilize under dictionary refinement. On a controlled differential-equation benchmark with an analytically known 11-dimensional represented intrinsic symmetry algebra, the method recovers the complete represented generator set, reproduces its Lie-bracket structure to numerical precision, and approximates a known generator beyond the training domain. Here we show that explicit intrinsic continuous-symmetry generators can be recovered from data obtained from exact or approximate differential systems.

The \textit{boxicity} of an undirected graph $Γ$, denoted as $\operatorname{box}(Γ)$, is the smallest non-negative integer $d$ such that $Γ$ can be represented as the intersection graph of axis-parallel rectangular boxes in $\mathbb{R}^d$. The \emph{power graph} of a group $G$, denoted as $\operatorname{Pow}(G)$, is an undirected graph whose vertex set is the group itself, with two elements being adjacent if one is a power of the other. We determine the exact boxicity of power graphs of finite nilpotent groups. For a cyclic group of order $n=\prod_{i=1}^{r}p_i^{e_i}>1$, where the $p_i$ are distinct primes, we prove that its power graph has boxicity $\sum_{i=1}^{r}e_i-\max_i e_i$. For a finite nilpotent group $G$, let the number of noncyclic odd Sylow subgroups be denoted by $t(G)$. If $G$ has odd order or if $G$ has a cyclic Sylow $2$-subgroup, then $\operatorname{box}(\operatorname{Pow}(G))=\operatorname{box}(\operatorname{Pow}(\mathbb{Z}_{\operatorname{exp}(G)}))+t(G)$, where $\operatorname{exp}(G)$ denotes the \emph{exponent} of a group $G$. When the Sylow $2$-subgroup is noncyclic, and the odd part is nontrivial, the boxicity equals this value or one more, and we characterise precisely when each of these values is attained. The boxicity of power graphs of arbitrary finite groups and the exact boxicity of the comparability graph of the Boolean lattice were posed as open questions in Discrete Mathematics, 349(7):115017, 2026. As a consequence of our results, we answer the latter question completely and the former question partially, by computing the exact boxicity of the power graphs of nilpotent groups.