pith. sign in

arxiv: 2606.30868 · v1 · pith:6SWKM56Xnew · submitted 2026-06-29 · 🧮 math.NA · cs.NA· hep-lat· math-ph· math.MP

Vector alignment in matrix Lie groups

Congzhou M Sha This is my paper

Pith reviewed 2026-07-01 01:39 UTC · model grok-4.3

classification 🧮 math.NA cs.NAhep-latmath-phmath.MP
keywords vector alignmentmatrix Lie groupsLie algebra projectionmatrix logarithmNewton correctiongauge transformationKabsch algorithmspecial orthogonal group
0
0 comments X

The pith

The four-step Lie algebra procedure recovers the exact group element aligning paired vector observations in any classical matrix Lie group when data is noiseless.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Recovering the gauge difference between two observers as a group element from paired vector observations can be useful in both theory and experiment. The paper gives explicit formulas for applying the Lie algebra method to the classical matrix Lie groups over real and complex fields, using the four steps of pseudoinverse, matrix logarithm, projection onto the Lie algebra, and matrix exponential. These steps are exact without noise. The projection is the unique least-squares optimal element of the Lie algebra whenever its image lies in the algebra and its residual is orthogonal to it. For noisy data the basic method is only optimal to leading order, so a Newton-style correction is added that matches the uncorrected method without noise and direct least-squares optimization with noise.

Core claim

The central claim is that the four-step procedure of pseudoinverse, matrix logarithm, projection onto the Lie algebra, and matrix exponential recovers the exact aligning group element in the noiseless case for every classical matrix Lie group. The projection step produces the unique least-squares optimal element of the Lie algebra whenever its image lies in the algebra and its residual is orthogonal to it. The Lie algebra method is optimal only to leading order for noisy data, but the added Newton-style correction matches the Lie algebra method without noise and direct least-squares optimization with noise.

What carries the argument

The projection of the matrix logarithm (after pseudoinverse) onto the Lie algebra, which is shown to be the unique least-squares optimal element under the image-and-orthogonal-residual condition.

If this is right

  • In the noiseless case the procedure returns the exact group element for every listed matrix Lie group.
  • The Newton-style correction yields accuracy between the uncorrected Lie algebra method and direct least-squares optimization when noise is present.
  • Explicit projection formulas are supplied for each classical matrix Lie group over both real and complex fields.
  • The optimality of the projection and the identity underlying the correction are formally proven in Lean 4 with Mathlib.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same four-step structure supplies a uniform route to alignment across Galilean and Lorentzian settings.
  • The closed-form projections may enable faster computation than iterative optimization in applications that repeatedly solve alignment problems.
  • The Lean formalization indicates the method can be mechanically verified when embedded in larger geometric or physical computations.

Load-bearing premise

After the pseudoinverse and logarithm the resulting matrix has image lying in the Lie algebra and residual orthogonal to the Lie algebra.

What would settle it

A side-by-side comparison, on synthetic noisy paired observations for a group such as SO(3), of the corrected method's output against the result of direct nonlinear least-squares optimization over the group.

Figures

Figures reproduced from arXiv: 2606.30868 by Congzhou M Sha.

Figure 1
Figure 1. Figure 1: Median relative recovery error ∥gest − gGT∥/∥gGT∥ (log scale) in the noiseless case across the classical groups, for six methods: the Lie algebra method estimate, the correction of §2.4, and automatic-differentiation Newton in four configurations (finite-difference vs. exact forward-over-reverse Hessian, each warm-started from the closed-form estimate or cold-started from the identity). All six reproduce t… view at source ↗
Figure 2
Figure 2. Figure 2: Median wall-clock time per alignment across the classical groups (log scale), for the same six methods as [PITH_FULL_IMAGE:figures/full_fig_p013_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: SE(3) recovery error ∥Gest−GGT∥F for two routes, both refined by the correction of §2.4: the homogeneous method on the full group (blue) and the classical centroid+SO(3) recipe (orange), at three noise levels (overlaid histograms, log scale). Note that the histograms overlap perfectly at ϵ = 0.01 and ϵ = 0.05. At ϵ = 0, both distributions are near double precision (∼ 10−16). 13 [PITH_FULL_IMAGE:figures/fu… view at source ↗
Figure 4
Figure 4. Figure 4: Per-group recovery-error histograms (Figs. 4–14). For each classical group, the [PITH_FULL_IMAGE:figures/full_fig_p014_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: SL(4,R), 1000 trials. 15 [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: SO(5), 1000 trials. 16 [PITH_FULL_IMAGE:figures/full_fig_p016_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: U(3), 1000 trials. 17 [PITH_FULL_IMAGE:figures/full_fig_p017_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: SU(3), 1000 trials. 18 [PITH_FULL_IMAGE:figures/full_fig_p018_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: SO(3,1), 1000 trials. 19 [PITH_FULL_IMAGE:figures/full_fig_p019_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: SO(2,3), 1000 trials. 20 [PITH_FULL_IMAGE:figures/full_fig_p020_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Sp(4,R), 1000 trials. 21 [PITH_FULL_IMAGE:figures/full_fig_p021_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Sp(4,C), 1000 trials. 22 [PITH_FULL_IMAGE:figures/full_fig_p022_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Spin(5), 1000 trials. 23 [PITH_FULL_IMAGE:figures/full_fig_p023_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: SE(3,1), 1000 trials. 24 [PITH_FULL_IMAGE:figures/full_fig_p024_14.png] view at source ↗
read the original abstract

The difference in gauge between two observers of the same physical system can be thought of as a group element acting on their common vector representations. Recovering that group element from a finite, noisy list of paired observations may be of use in both theory and experiment. The Kabsch and Horn algorithms efficiently align point clouds in $\mathbb R^3$, reconciling rotated frames of reference in Galilean relativity (i.e. $SO(3)$). In a previous work, we proposed an alternative Lie algebra method which extends to the Lorentz group $SO(3,1)_+$, and putatively to all Lie groups. In this work, we report the explicit formulae for applying the Lie algebra method to the classical matrix Lie groups (general linear $GL(n)$, special linear $SL(n)$, special orthogonal $SO(n)$, unitary $U(n)$, indefinite special orthogonal $SO(p,q)$, symplectic $Sp(n)$, spin $Spin(n)$, special Euclidean $SE(n)$) over both the real and complex fields. The four steps (pseudoinverse, matrix logarithm, projection onto the Lie algebra, matrix exponential) are exact in the noiseless case. The only group-dependent step is the projection, which we show produces the unique least squares-optimal element of the Lie algebra whenever its image lies in $\mathfrak g$ and its residual is orthogonal to $\mathfrak g$. Additionally, the Lie algebra method is optimal only to leading order for noisy data, so we refine it with a Newton-style correction. This correction matches the Lie algebra method in the noiseless case and direct least squares optimization in the noisy case, with performance between that of the Lie algebra method without correction and naive least squares optimization. The projections, their optimality, and the identity underlying the correction are formally proven in Lean~4.31.0 (with Mathlib 4.31.0), and numerical experiments are benchmarked in Julia.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript develops explicit formulae for a four-step Lie-algebra method (pseudoinverse, matrix logarithm, projection onto the Lie algebra, matrix exponential) to recover group elements from paired noisy vector observations, applicable to the classical matrix Lie groups GL(n), SL(n), SO(n), U(n), SO(p,q), Sp(n), Spin(n), and SE(n) over R and C. The projection step is shown to be the unique least-squares optimal element of the Lie algebra whenever its image lies in g and the residual is orthogonal to g; a Newton-style correction is introduced that recovers the Lie-algebra solution in the noiseless case and matches direct least-squares in the noisy case. All projections, the conditional optimality statement, and the correction identity are formally proven in Lean 4.31.0; numerical performance is benchmarked in Julia.

Significance. The combination of group-general explicit projections, machine-checked proofs of the central identities, and a correction that interpolates between the algebraic and direct least-squares regimes constitutes a substantive contribution to numerical methods on Lie groups. The Lean formalization supplies a level of verification uncommon in the field and directly addresses reproducibility concerns for the optimality claims.

major comments (2)
  1. [§3] §3 (Projection formulae): the optimality theorem is stated only under the explicit hypothesis that the post-logarithm matrix satisfies image-in-g and residual-orthogonality; the manuscript should clarify whether this hypothesis is automatically satisfied for all listed groups when the input is exactly a group element, or whether additional verification is required for each group.
  2. [§5] §5 (Newton correction): the claim that the correction 'matches direct least squares optimization in the noisy case' is supported by numerical benchmarks but lacks an analytic error bound or convergence-rate statement; a short derivation showing the order of the residual after one Newton step would strengthen the result.
minor comments (2)
  1. [Table 1] Table 1: the column headings for the complex-field cases are not aligned with the real-field rows; a small formatting adjustment would improve readability.
  2. The Lean repository URL is given only in the abstract; it should also appear in the main text or a dedicated reproducibility section.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive evaluation and the recommendation of minor revision. The two major comments are addressed below; both will be incorporated into the revised manuscript.

read point-by-point responses

  1. Referee: [§3] §3 (Projection formulae): the optimality theorem is stated only under the explicit hypothesis that the post-logarithm matrix satisfies image-in-g and residual-orthogonality; the manuscript should clarify whether this hypothesis is automatically satisfied for all listed groups when the input is exactly a group element, or whether additional verification is required for each group.

    Authors: The optimality theorem is stated conditionally, as noted. When the input consists of exact group elements (noiseless case), the matrix logarithm of any element of the listed groups lies in the corresponding Lie algebra by definition, so the image-in-g condition holds automatically. The residual-orthogonality condition is likewise satisfied because the projection employed is the orthogonal projection onto the Lie algebra with respect to the Frobenius inner product; this property is uniform across the classical matrix Lie groups and is already covered by the general Lean formalization without requiring separate per-group verification. A clarifying paragraph will be added to §3. revision: yes

  2. Referee: [§5] §5 (Newton correction): the claim that the correction 'matches direct least squares optimization in the noisy case' is supported by numerical benchmarks but lacks an analytic error bound or convergence-rate statement; a short derivation showing the order of the residual after one Newton step would strengthen the result.

    Authors: We agree that an analytic statement would strengthen the result. A short derivation establishes that a single Newton step reduces the residual to O(ε²) in the noise level ε, which explains the observed numerical agreement with direct least-squares optimization. This derivation will be included in the revised §5. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The derivation consists of four standard matrix operations (pseudoinverse, logarithm, projection onto the Lie algebra, exponential) whose exactness in the noiseless case follows directly from the definitions of matrix Lie groups and their algebras. Optimality of the projection is stated only conditionally ('whenever its image lies in g and its residual is orthogonal to g') and is formally proven in Lean within the present paper, not imported from prior work. The Newton correction is shown by direct identity to match the Lie-algebra method when noise vanishes and least-squares when noise is present; no parameter is fitted and then renamed as a prediction. The single reference to 'a previous work' merely introduces the Lie-algebra approach; the explicit formulae, conditional optimality theorem, and Lean proofs for the current classical groups are self-contained and do not reduce to that citation. No self-definitional loops, ansatz smuggling, or uniqueness theorems imported from the same authors appear.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard mathematical properties of matrix Lie groups and the matrix logarithm/exponential; no free parameters, ad-hoc constants, or new postulated entities are introduced.

axioms (2)
  • standard math Standard properties of the matrix logarithm and exponential maps on matrix Lie groups
    Invoked in the four-step procedure.
  • domain assumption Existence of a unique least-squares projection onto the Lie algebra when the image lies in g and the residual is orthogonal to g
    Required for the optimality claim of the projection step.

pith-pipeline@v0.9.1-grok · 5880 in / 1511 out tokens · 64242 ms · 2026-07-01T01:39:56.509542+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

13 extracted references · 12 canonical work pages

  1. [1]

    M. E. Peskin, D. V. Schroeder, An Introduction to Quantum Field Theory, Addison-Wesley, Reading, USA, 1995. doi:10.1201/9780429503559

    work page doi:10.1201/9780429503559 1995

  2. [2]

    Kabsch, A solution for the best rotation to relate two sets of vectors, Acta Crystallogr

    W. Kabsch, A solution for the best rotation to relate two sets of vectors, Acta Crystallogr. Sect. A32(1976) 922–923. doi:10.1107/S0567739476001873

    work page doi:10.1107/s0567739476001873 1976

  3. [3]

    B. K. P. Horn, Closed-form solution of absolute orientation using unit quaternions, J. Opt. Soc. Am. A4(1987) 629. doi:10.1364/josaa.4.000629

    work page doi:10.1364/josaa.4.000629 1987

  4. [4]

    C. M. Sha, Optimal alignment of Lorentz orientation and generalization to matrix Lie groups, J. Comput. Appl. Math.485(2026) 117482. doi:10.1016/j.cam.2026.117482

    work page doi:10.1016/j.cam.2026.117482 2026

  5. [5]

    de Moura, S

    L. de Moura, S. Ullrich, The Lean 4 theorem prover and programming language, in: Automated Deduction – CADE 28, Lecture Notes in Computer Science, vol. 12699, Springer, Cham, 2021, pp. 625–635. doi:10.1007/978-3-030-79876-5_37

    work page doi:10.1007/978-3-030-79876-5_37 2021

  6. [6]

    R. J. de la Cruz, A. T. Paras, Sums of orthogonal, symmetric, and skew-symmetric matrices, Electron. J. Linear Algebra38(2022) 655–660

    2022

  7. [7]

    Begović, Finding the closest normal structured matrix, Linear Algebra Appl.617(2021) 49–77

    E. Begović, Finding the closest normal structured matrix, Linear Algebra Appl.617(2021) 49–77. arXiv:2003.06391. doi:10.1016/j.laa.2021.01.019. 16Lean:exp_commutes_realEmbedding, obtained from Lemma 3 (the ring-homomorphism bun- dlerealEmbeddingRingHom) together with continuity ofφ(realEmbedding_continuous, from LinearMap.continuous_of_finiteDimensional) ...

    work page doi:10.1016/j.laa.2021.01.019 2021

  8. [8]

    Abuaf, A

    R. Abuaf, A. Boralevi, Orthogonal bundles and skew-Hamiltonian matrices, Canad. J. Math. 67(2015) 961–989. arXiv:1312.0963. doi:10.4153/CJM-2014-034-9

    work page doi:10.4153/cjm-2014-034-9 2015

  9. [9]

    The mathlib Community, The Lean mathematical library, in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, New Orleans, LA, USA, 2020, pp. 367–381. doi:10.1145/3372885.3373824

    work page doi:10.1145/3372885.3373824 2020

  10. [10]

    Fletcher, Conjugate direction methods, in: Practical Methods of Optimization, John Wiley & Sons, Ltd, 2000, Ch

    R. Fletcher, Conjugate direction methods, in: Practical Methods of Optimization, John Wiley & Sons, Ltd, 2000, Ch. 4, pp. 80–94. doi:10.1002/9781118723203.ch4

    work page doi:10.1002/9781118723203.ch4 2000

  11. [11]

    A. H. Al-Mohy, N. J. Higham, A new scaling and squaring algorithm for the matrix exponential, SIAM J. Matrix Anal. Appl.31(3) (2009) 970–989. doi:10.1137/09074721X

    work page doi:10.1137/09074721x 2009

  12. [12]

    Levin, A

    Y. Levin, A. Ben-Israel, A Newton method for systems ofmequations innvariables, Nonlinear Anal. Theory Methods Appl.47(3) (2001) 1961–1971. doi:10.1016/S0362-546X(01)00325-X

    work page doi:10.1016/s0362-546x(01)00325-x 2001

  13. [13]

    A. H. Al-Mohy, N. J. Higham, Improved inverse scaling and squaring algorithms for the matrix logarithm, SIAM J. Sci. Comput.34(2012). doi:10.1137/110852553. 11 Figures Figure 1: Median relative recovery error∥g est −g GT∥/∥gGT∥(log scale) in the noiseless case across the classical groups, for six methods: the Lie algebra method estimate, the correction of...

    work page doi:10.1137/110852553 2012