Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Rational Numbers Form an Archimedean Ordered Field Containing the Integers
lemmalem:rationals-nbg-2026aAlgebraSet TheoryThe rational numbers form an Archimedean ordered field whose strict order is the strict relation of its order; the integers embed into it preserving 0, 1, the operations and the order, two fractions are equal exactly when their cross products agree, and each fraction times its de…- Defines the rational numbers as the classes [x, m] of pairs of an integer and a natural number (thought of as x/m), with the sum, product, negation and order of the construction lemma, the rationals 0 and 1, and the embedding x ↦ [x, 1] of the integers.
Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order
lemmalem:rational-construction-nbg-2026aAlgebraSet TheoryPairs (x, m) of an integer and a natural number, thought of as x/m, with (x, m) ≈ (y, n) when x·n = y·m, form an equivalence relation; on the classes [x, m] there are unique sum, product, negation and order given by the usual formulas.The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements
lemmalem:integers-nbg-2026aAlgebraSet TheoryThe integers form an ordered commutative ring; negation behaves as expected; the embedding of N is injective and preserves 1, sums, products and the order; [a, b] = ι(a) − ι(b); every integer is positive (the image of N), zero or negative; and there are no zero divisors, so nonze…- Defines the integers as the classes [a, b] of pairs of natural numbers (thought of as a − b), with the sum, product, negation and order of the construction lemma, the integers 0 = [1, 1] and 1 = [2, 1], and the embedding n ↦ [n + 1, 1] of N.
Construction of the Integers: Pairs of Natural Numbers up to Equal Differences, with Sum, Product, Negation and Order
lemmalem:integer-construction-nbg-2026aAlgebraSet TheoryPairs (a, b) of natural numbers, thought of as a − b, with (a, b) ~ (c, d) when a + d = b + c, form an equivalence relation; on the classes [a, b] there are unique sum, product, negation and order given by the usual formulas.- Defines an ordered field as a field with a total order that makes it an ordered ring.
- Defines a field as a commutative ring with 0 ≠ 1 in which every nonzero element has a multiplicative inverse.
- Defines a commutative ring (with identity) as a set with two binary operations and two distinguished elements 0 and 1 satisfying the associative, commutative, identity, additive-inverse and distributive laws.
Rotations and Cyclic Derivatives of Words in Unitary Letters
definitiondef:nc-unitary-cyclic-derivative-2026aAlgebraProbabilityThe i-th cyclic derivative of a word is the word polynomial summing, over the occurrences of the i-th unitary or its inverse, the rotation of the word starting at the insertion point, with coefficient i times the sign of the letter.Evaluation of Word Polynomials by a Unitary Law
definitiondef:nc-unitary-law-evaluation-2026aAlgebraProbabilityA unitary law is extended linearly to word polynomials: lambda(X) is the sum of X(w) lambda(w) over a support set of X.The Truncated Cyclic Gradient of a Gauge Vector
definitiondef:nc-unitary-cyclic-gradient-2026aAlgebraProbabilityFor a gauge vector p and a length n, the i-th truncated cyclic gradient is the self-adjoint part of the sum of c_w times conj(p(w)) times the i-th cyclic derivative of w, over cyclically reduced words of length at most n.Word Polynomials under a Unitary Law: Linearity, Traciality, Positivity, the Cauchy-Schwarz Inequality and the l1 Bound
lemmalem:nc-unitary-word-polynomials-2026aAlgebraProbabilityEvaluation of word polynomials by a unitary law is linear, tracial and compatible with adjoints; it is positive on X*X, satisfies the Cauchy-Schwarz inequality, and is bounded by the l1 norm, which is submultiplicative.Word Polynomials in Unitary Letters: the Normed *-Algebra of Finitely Supported Word Functions
definitiondef:nc-unitary-word-polynomials-2026aAlgebraProbabilityWord polynomials are finitely supported complex functions on words in unitary letters, with pointwise linear structure, the concatenation product, the adjoint and the l1 norm.Reduced and Cyclically Reduced Words in Unitary Letters
definitiondef:nc-unitary-reduced-words-2026aAlgebraDefines reduced words (no adjacent inverse letters) and cyclically reduced words (also first and last letters not inverse to each other).Unitary Laws: Adjoints, the Bound One, and Reduction to Cyclically Reduced Words
lemmalem:nc-unitary-laws-basic-2026aAlgebraProbabilityUnitary laws satisfy lambda(w*) = conj lambda(w) and |lambda| <= 1, reduce to cyclically reduced words, are determined by them, and the constant law 1 exists.- A unitary law of d-tuples is a function on words that is normalised, cyclic, invariant under cancelling adjacent inverse letters, and gives positive semidefinite kernels.
Words in Unitary Letters: Generators, Signs, Inverse Letters, Lengths and Adjoint Words
definitiondef:nc-unitary-words-2026aAlgebraLetters 1,...,2d encode unitaries and their inverses; defines generators, signs, inverse letters, word lengths and adjoint words.Evaluation of Noncommutative Polynomials at Bounded Operators: a Unital Homomorphism Compatible with Adjoints, Substitution, Representations and the GNS Multiplication Operators
lemmalem:nc-polynomial-evaluation-operators-2026aAnalysisAlgebraEvaluation at a tuple of bounded operators is a unital algebra homomorphism that respects adjoints for self-adjoint tuples, commutes with substitution and with unital multiplicative linear maps, turns GNS left multiplications into L_p, and obeys the bound R^k on words of length k…Evaluation of Noncommutative Polynomials at a Tuple of Bounded Operators
definitiondef:nc-polynomial-evaluation-operators-2026aAnalysisAlgebraDefines the value p(T) of a noncommutative polynomial at a tuple T of bounded operators on a complex Hilbert space, sending each monomial to the product of the operators along its word.