Paper
Iterative Berechnung der reziproken Matrix, 1933. ZAMM 13(1), pp. 57–59. Read a later research treatment, §3.
Connection to the paper
The publisher lists Schulz’s 1933 paper with the spelling “Berechung.” The full original was inaccessible. The update was checked against Leplat et al., “Iterative Methods for Computing the Moore–Penrose Pseudoinverse of Quaternion Matrices, with Applications” (2025), §3. This file proves its algebraic core in any ring.
The result
Every iteration squares both the left and right inverse residual. After n steps, either residual is the initial residual raised to 2ⁿ. If the right residual has vanished at that power, the iterate is an exact right inverse.
Xₙ₊₁ = Xₙ(2I − AXₙ) I − AXₙ = (I − AX₀)^(2ⁿ) I − XₙA = (I − X₀A)^(2ⁿ)
Proof in plain English
- Expand without commuting. Keep all multiplication factors in their original order.
- Square the residual. Subtracting the updated product from the identity gives the old residual squared.
- Iterate. Induction doubles the exponent at every step.
Scope & assumptions
6 checked theorems. Left/right one-step identities, both arbitrary-iteration formulas, exactness for a nilpotent right residual, and fixed points at right inverses. No norm convergence, initialization rule, or pseudoinverse result.
An associative ring with identity; multiplication need not commute. Square matrices are an instance. Nilpotent exactness assumes (1 − ax₀)^(2ⁿ) = 0. A right inverse is not silently promoted to a two-sided inverse in a general ring.
Notation in Lean
| Meaning | Lean |
|---|---|
| Iteration | iterate |
| Right residual | right_error_exact |
| Left residual | left_error_exact |
| Finite exactness | nilpotent_right_exact |
Prior work
No matching named formalization was located in the bounded search of two Mathlib revisions and indexed web results on 2026-09-10. Related library ingredients already exist. First-formalization status is unconfirmed; this does not establish priority.
Read the search recordLean proof
import Mathlib.Algebra.Ring.Basic
import Mathlib.Tactic.NoncommRing
/-! Schulz (1933): algebraic error squaring for inverse iteration.
Works in any unital ring, including square matrices. No commutativity,
invertibility, convergence, or floating-point stability is assumed. -/
namespace PaperToLean.Schulz
variable {R : Type*} [Ring R]
def step (a x : R) : R := x * (2 - a * x)
def iterate (a x : R) : ℕ → R
| 0 => x
| n + 1 => step a (iterate a x n)
theorem right_error_square (a x : R) :
1 - a * step a x = (1 - a * x) ^ 2 := by
simp only [step, ← one_add_one_eq_two, mul_sub, mul_add, mul_one]
noncomm_ring
theorem left_error_square (a x : R) :
1 - step a x * a = (1 - x * a) ^ 2 := by
simp only [step, ← one_add_one_eq_two, mul_sub, mul_add, mul_one,
sub_mul, add_mul]
noncomm_ring
theorem right_error_exact (a x : R) (n : ℕ) :
1 - a * iterate a x n = (1 - a * x) ^ (2 ^ n) := by
induction n with
| zero => simp [iterate]
| succ n ih =>
rw [iterate, right_error_square, ih, ← pow_mul, pow_succ]
theorem left_error_exact (a x : R) (n : ℕ) :
1 - iterate a x n * a = (1 - x * a) ^ (2 ^ n) := by
induction n with
| zero => simp [iterate]
| succ n ih =>
rw [iterate, left_error_square, ih, ← pow_mul, pow_succ]
theorem nilpotent_right_exact (a x : R) (n : ℕ)
(h : (1 - a * x) ^ (2 ^ n) = 0) : a * iterate a x n = 1 := by
have he := right_error_exact a x n
rw [h, sub_eq_zero] at he
exact he.symm
theorem inverse_fixed (a x : R) (h : a * x = 1) : step a x = x := by
simp [step, h, ← one_add_one_eq_two]
#print axioms right_error_square
#print axioms left_error_square
#print axioms right_error_exact
#print axioms left_error_exact
#print axioms nilpotent_right_exact
#print axioms inverse_fixed
end PaperToLean.Schulz
Inspect the verification record
Every listed theorem is audited individually. These proofs use only propext. No custom axioms, sorry placeholders, or native_decide proofs.
Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Schulz.lean
SHA-256: 351aa72c80b8e5f906ca2b9ba3b61aa49a64d7ccfce336c3ec69febd53535009
Result: passed
'PaperToLean.Schulz.right_error_square' depends on axioms: [propext]
'PaperToLean.Schulz.left_error_square' depends on axioms: [propext]
'PaperToLean.Schulz.right_error_exact' depends on axioms: [propext]
'PaperToLean.Schulz.left_error_exact' depends on axioms: [propext]
'PaperToLean.Schulz.nilpotent_right_exact' depends on axioms: [propext]
'PaperToLean.Schulz.inverse_fixed' depends on axioms: [propext]
SHA-256: 351aa72c80b8e5f906ca2b9ba3b61aa49a64d7ccfce336c3ec69febd53535009
Run it
Install Lean with elan and Git. Download the project ZIP, extract it, and run these commands in that folder. The first command downloads the pinned Mathlib dependencies.
python3 prepare.py
lake env lean -DwarningAsError=true Schulz.lean