Cumulus · The Top 100 Theorems

Foundational mathematics in Grace17, from sets to working proofs.

52/100 verified entries

Numbering follows Freek Wiedijk's Formalizing 100 Theorems.

At a glance#

Statements and proofs#

1. Irrationality of √2#

Informal. √2 is irrational.

Scope. Irrational(√2), where Irrational(x) says that no rational q ∈ ℚ is sent to x by the embedding rationalCut of ℚ into ℝ: the textbook √2 ∉ ℚ, with ℚ read as its copy inside ℝ. The set form √2 ∉ rationalReals (the image of the embedding), the pointwise form √2 ≠ rationalCut(q), and the quotient form √2 ≠ p/q for naturals p and q ≠ 0 are stated as well. The proof shows the embedding is additive, carries multiplication by a natural, and sends a rational (a − b)/m to a real with rationalCut(q)·m = a − b; squaring reduces to the natural-number statement that no p and positive q satisfy p² = 2q², proved by descent from the least such p.

Proof: sqrtTwo.irrational

theorem sqrtTwo.irrational
  shows Irrational(√2)

Proof: sqrtTwo.not_rational

theorem sqrtTwo.not_rational
  shows √2 ∉ rationalReals

Proof: sqrtTwo.ne_rationalCut

theorem sqrtTwo.ne_rationalCut (q : Rational)
  shows √2 ≠ rationalCut(q)

Proof: sqrtTwo.ne_quotient

theorem sqrtTwo.ne_quotient (p q : Nat)
  requires positive : q ≠ 0
  shows √2 ≠ realNat(p) / realNat(q)

Proof: rootTwo.irrational

theorem rootTwo.irrational (p q : Nat)
  requires positive : q ≠ 0
  shows p * p ≠ 2 * (q * q)

Back to overview

2. Fundamental theorem of algebra#

Informal. Every nonconstant complex polynomial has a complex root.

Scope. Root existence for every nonconstant polynomial over the concrete Dedekind-real complex field: in the monic form complexes.fundamental_theorem_of_algebra, in the general form with an explicit nonzero leading coefficient (hornerAt with lower coefficients cs ≠ []), and in the single-coefficient-list form where some coefficient of index at least one is nonzero. The general forms divide by the leading coefficient and reduce to the monic case. The proof inherits Global Choice through minimum attainment. Counting roots with multiplicity is a separate theorem, not proved here.

Proof: complexes.fundamental_theorem_of_algebra

theorem complexes.fundamental_theorem_of_algebra (cs : List(ℂ))
  requires nonconstant : cs ≠ []
  shows ∃ a ∈ ℂ, monicValue(ℂ, identity(ℂ), ℂ, a, cs) = ℂ[0]

Proof: complexes.fundamental_theorem_of_algebra_general

theorem complexes.fundamental_theorem_of_algebra_general (c : Set) (cs : List(ℂ))
  requires leading : c ∈ ℂ
  requires nonzero : c ≠ ℂ[0]
  requires nonconstant : cs ≠ []
  shows ∃ a ∈ ℂ, hornerAt{ℂ}(complexAdd, complexMul, c, a, cs) = ℂ[0]

Proof: complexes.fundamental_theorem_of_algebra_coefficients

theorem complexes.fundamental_theorem_of_algebra_coefficients (cs : List(complexCarrier)) (n : Nat)
  requires nonconstant : listCoefficient{complexCarrier}(complexZero, cs, n + 1) ≠ complexZero
  shows ∃ a ∈ complexCarrier,
    hornerAt{complexCarrier}(complexAdd, complexMul, complexZero, a, cs) = complexZero

Proof: complexes.algebraically_closed

theorem complexes.algebraically_closed
  shows IsAlgebraicallyClosed(ℂ)

Back to overview

3. Denumerability of the rationals#

Informal. The rational numbers are countable.

Scope. Countable(ℚ) means an injection from ℚ into ℕ exists. The proof injects ℕ × ℕ into ℕ by (a, b) ↦ 2^a(2b + 1), shows countability passes to subsets, products, and images under surjections (choosing the least code, without Choice), and applies this to the quotient construction of ℚ from pairs of naturals and a positive denominator.

Proof: rationals.countable

theorem rationals.countable
  shows Countable(ℚ)

Proof: Countable.of_surjection

theorem Countable.of_surjection (f A B : Set)
  requires countable : Countable(A)
  requires surjection : SurjectiveBetween(f, A, B)
  shows Countable(B)

Proof: naturalPairing.injective

theorem naturalPairing.injective
  shows InjectiveBetween(naturalPairing, ℕ × ℕ, ℕ)

Back to overview

4. Pythagorean theorem#

Informal. In a right triangle, c² = a² + b².

Scope. Squared Euclidean distances over Dedekind reals; orthogonality expresses the right angle. Includes degenerate configurations. No square-root distance is needed.

Proof: pythagoras

theorem pythagoras (a₁ a₂ b₁ b₂ c₁ c₂ : Real)
  requires right : RightAt(a₁, a₂, b₁, b₂, c₁, c₂)
  shows distanceSquared(a₁, a₂, b₁, b₂) =
    distanceSquared(a₁, a₂, c₁, c₂) + distanceSquared(b₁, b₂, c₁, c₂)

Back to overview

10. Euler's generalization of Fermat's little theorem#

Informal. If gcd(a, n) = 1 then a^φ(n) ≡ 1 (mod n); for a prime p and p ∤ a, a^(p−1) ≡ 1 (mod p).

Scope. For naturals a and n > 1 with gcd(a, n) = 1, a^φ(n) % n = 1, where φ(n) is the length of the list of residues below n coprime to n. The proof scales that list by a: the scaled entries have the same multiplicities as the original list (an inverse of a exists by a counting argument on residues), so their products agree, and the product of units is coprime to n, so it cancels. Fermat's little theorem a^(p−1) % p = 1 for a prime p ∤ a follows from φ(p) = p − 1. The totient is defined by this count rather than by a product formula, and its multiplicativity is not proved.

Proof: euler.theorem

theorem euler.theorem (a n : Nat)
  requires aboveOne : 1 < n
  requires coprime : gcd(a, n) = 1
  shows (a ^ totient(n)) % n = 1

Proof: fermat.little

theorem fermat.little (a p : Nat)
  requires prime : Prime(p)
  requires notDivides : ¬(p ∣ a)
  shows a ^ (p - 1) % p = 1

Back to overview

11. Infinitude of primes#

Informal. For every natural bound there is a larger prime; the set of primes is infinite.

Scope. Both order-unboundedness and the set-theoretic non-finiteness conclusion are proved.

Proof: primes.order_unbounded

theorem primes.order_unbounded (n : Nat)
  shows ∃ p ∈ primes, n < p

Proof: primes.infinite

theorem primes.infinite
  shows ¬Finite(primes)

Back to overview

15. Fundamental theorem of integral calculus#

Informal. For continuous f, differentiating x ↦ ∫ₐˣ f recovers f. A continuous derivative integrates to the endpoint difference.

Scope. Riemann integration on real closed intervals. FTC-I is an interior derivative statement; the second displayed theorem assumes a continuous integrand and the stated local derivative hypotheses. No Lebesgue-integral generality is claimed.

Proof: FTC.derivative_of_integral

theorem FTC.derivative_of_integral (f : Set) (A B X : Real)
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires left : A < X
  requires right : X < B
  shows HasDerivativeAt(integralFrom(f, A, B), f(X), X)

Proof: FTC.continuous_derivative

theorem FTC.continuous_derivative (f : ℝ → ℝ) (F : Set) (A B : Real)
  requires ordered : A ≤ B
  requires continuousF : ContinuousOn(F, closedInterval(A, B))
  requires derivative : ∀ X ∈ ℝ, A < X → X < B →
    HasDerivativeAt(F, f(X), X)
  requires continuousf : ContinuousOn(f, closedInterval(A, B))
  shows HasRiemannIntegral(f, A, B, F(B) - F(A))

Back to overview

22. Non-denumerability of the continuum#

Informal. The real numbers cannot be enumerated by the natural numbers.

Scope. The carrier is the constructed Dedekind reals. The proof embeds the powerset of the naturals into the reals and uses Cantor diagonalization.

Proof: reals.uncountable

theorem reals.uncountable
  shows Uncountable(ℝ)

Back to overview

23. Formula for Pythagorean triples#

Informal. The primitive Pythagorean triples are exactly (m² − n², 2mn, m² + n²) with m > n > 0 coprime and of opposite parity, up to the order of the legs; every Pythagorean triple is a multiple of a primitive one.

Scope. A Pythagorean triple is a triple of positive naturals with a ^ 2 + b ^ 2 = c ^ 2, primitive when gcd(a, b) = 1; "opposite parity" is Odd(m + n). Both directions are proved over the naturals: pythagorean.of_parameters and pythagorean.primitive_of_parameters give the triples of the parametrization, pythagorean.one_even shows a primitive triple has exactly one even leg, and pythagorean.primitive_form recovers m and n for every primitive triple with b even, so every primitive triple up to swapping the legs. pythagorean.form writes any triple as gcd(a, b) times a primitive one. The arithmetic heart, that coprime factors of a square are squares, is IsSquare.of_coprime_mul, proved by the cofactor argument on gcd(a, c) without prime factorization. Everything is in ZF.

Proof: pythagorean.primitive_form

theorem pythagorean.primitive_form (a b c : Nat)
  requires primitive : PrimitivePythagorean(a, b, c)
  requires even : Even(b)
  shows ∃ m, Nat(m) ∧ ∃ n, Nat(n) ∧
    0 < n ∧ n < m ∧ gcd(m, n) = 1 ∧ Odd(m + n) ∧
    a = m ^ 2 - n ^ 2 ∧ b = 2 * m * n ∧ c = m ^ 2 + n ^ 2

Proof: pythagorean.primitive_of_parameters

theorem pythagorean.primitive_of_parameters (m n : Nat)
  requires positive : 0 < n
  requires below : n < m
  requires coprime : gcd(m, n) = 1
  requires parity : Odd(m + n)
  shows PrimitivePythagorean(m ^ 2 - n ^ 2, 2 * m * n, m ^ 2 + n ^ 2)

Proof: pythagorean.of_parameters

theorem pythagorean.of_parameters (m n : Nat)
  requires positive : 0 < n
  requires below : n < m
  shows Pythagorean(m ^ 2 - n ^ 2, 2 * m * n, m ^ 2 + n ^ 2)

Proof: pythagorean.one_even

theorem pythagorean.one_even (a b c : Nat)
  requires primitive : PrimitivePythagorean(a, b, c)
  shows Odd(a + b)

Proof: pythagorean.form

theorem pythagorean.form (a b c : Nat)
  requires triple : Pythagorean(a, b, c)
  shows ∃ x, Nat(x) ∧ ∃ y, Nat(y) ∧ ∃ z, Nat(z) ∧
    PrimitivePythagorean(x, y, z) ∧
    a = gcd(a, b) * x ∧ b = gcd(a, b) * y ∧ c = gcd(a, b) * z

Proof: IsSquare.of_coprime_mul

theorem IsSquare.of_coprime_mul (a b c : Nat)
  requires coprimeAB : gcd(a, b) = 1
  requires product : a * b = c * c
  shows IsSquare(a) ∧ IsSquare(b)

Back to overview

25. Schröder–Bernstein Theorem#

Informal. If there are injections from A into B and from B into A, then there is a bijection between A and B.

Scope. Sets A and B with injective functions as graphs in both directions, written A ≼ B and B ≼ A. The bijection is built from the back-and-forth chain: f on the points of A reached from the complement of the image of g by iterating g ∘ f, and the inverse of g elsewhere.

Proof: Equipotent.of_mutual_dominance

theorem Equipotent.of_mutual_dominance (A B : Set)
  requires hAB : A ≼ B
  requires hBA : B ≼ A
  shows A ≃ B

Back to overview

30. The ballot problem#

Informal. If A receives a votes and B receives b < a votes, the orderings of the ballots in which A is strictly ahead throughout the count are (a − b)/(a + b) of all orderings.

Scope. A ballot is 0 (a vote for A) or 1 (a vote for B), an ordering is a list over 2 read in the order of the count, ballots(n) is the set of such lists of length n, and ballotSequences(a, b) the lists of length a + b with a zeros along which every nonempty prefix holds more zeros than ones (AlwaysAhead). ballot.count gives (a + b) * cardinality(ballotSequences(a, b)) = (a - b) * ((a + b) choose a) for b < a, from the additive form ballotSequences.count_succ, cardinality(ballotSequences(a + 1, b)) + ((a + b) choose (a + 1)) = (a + b) choose a for b ≤ a, and the absorption identities of the binomial coefficients. The proof is the recursion by the first ballot: the orderings with a zeros and b ones along which A stays ahead by more than k split, by their first ballot, into the cons images of the families at (k + 1, a − 1, b) and (k − 1, a, b − 1), and leadSequences.closed_form verifies cardinality + (n choose (a + k + 1)) = n choose a by induction on n = a + b with Pascal's rule; the ballot sequences are the case of a first ballot 0 followed by a lead above one. orderings.count gives cardinality(orderings(a, b)) = (a + b) choose a for all orderings, and ballot.probability the probability form prob(uniformWeight(orderings(a, b)), ballotSequences(a, b)) = realNat(a - b) / realNat(a + b) on the uniform space of all orderings. The counting module is in ZF.

Proof: ballot.count

theorem ballot.count (a b : Nat)
  requires lead : b < a
  shows (a + b) * cardinality(ballotSequences(a, b)) =
    (a - b) * ((a + b) choose a)

Proof: ballotSequences.count_succ

theorem ballotSequences.count_succ (a b : Nat)
  requires le : b ≤ a
  shows cardinality(ballotSequences(a + 1, b)) + ((a + b) choose (a + 1)) =
    (a + b) choose a

Proof: orderings.count

theorem orderings.count (a b : Nat)
  shows cardinality(orderings(a, b)) = (a + b) choose a

Proof: leadSequences.closed_form

theorem leadSequences.closed_form (n k a b : Nat)
  requires total : a + b = n
  requires bound : b ≤ a + k
  shows cardinality(leadSequences(k + 1, a, b)) + (n choose (a + k + 1)) =
    n choose a

Proof: ballot.probability

theorem ballot.probability (a b : Nat)
  requires lead : b < a
  shows prob(uniformWeight(orderings(a, b)), ballotSequences(a, b)) =
    (realNat(a - b):R) / (realNat(a + b):R)

Back to overview

31. Ramsey's theorem#

Informal. For every n, every infinite set S, and every colouring of the n-element subsets of S with finitely many colours, some infinite subset of S has all its n-element subsets the same colour; and among any six people, three are mutual acquaintances or three are mutual strangers.

Scope. The infinite Ramsey theorem in full: for every natural n, every infinite set S, and every function C from the n-element subsets of S into a finite set of colours, there is an infinite H ⊆ S and a colour c with C(U) = c for every n-element subset U of H (ramsey.infinite_colours); ramsey.infinite is the two-colour form and ramsey.infinite_numeral the form for a numeral of colours. The proof is the classical induction on n: a chain of nested infinite sets, each homogeneous for the colouring induced by a chosen point, is built by recursion on ℕ with global choice, the infinite pigeonhole principle picks a colour that recurs infinitely often, and the least index of an (n + 1)-subset of the chosen points reduces it to the previous stage. The finite case R(3, 3) ≤ 6 is proved separately for simple graphs.

Proof: ramsey.infinite_colours

theorem ramsey.infinite_colours (n : Nat) (S C K : Set)
  requires infinite : Infinite(S)
  requires finite : Finite(K)
  requires colouring : C : subsetsOfSize(S, n) → K
  shows ∃ H, H ⊆ S ∧ Infinite(H) ∧
    ∃ c ∈ K, ∀ U ∈ subsetsOfSize(H, n), C(U) = c

Proof: ramsey.infinite

theorem ramsey.infinite (n : Nat) (S C : Set)
  requires infinite : Infinite(S)
  requires colouring : C : subsetsOfSize(S, n) → 2
  shows ∃ H, H ⊆ S ∧ Infinite(H) ∧
    ∃ c ∈ 2, ∀ U ∈ subsetsOfSize(H, n), C(U) = c

Proof: ramsey.three_three

theorem ramsey.three_three (V E : Set)
  requires graph : SimpleGraph(V, E)
  requires six : HasCardinality(V, 6)
  shows ∃ x ∈ V, ∃ y ∈ V, ∃ z ∈ V,
    x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ MonochromaticTriangle(E, x, y, z)

Back to overview

34. Divergence of the harmonic series#

Informal. The series 1 + 1/2 + 1/3 + ⋯ diverges.

Scope. The harmonic terms 1/(k+1) form a real sequence whose partial sums pass every real number and therefore have no limit. The proof is the classical doubling bound 2·S(2m) ≥ 2·S(m) + 1, iterated to 2·S(mₖ) ≥ 2 + k, combined with the Archimedean property of the Dedekind reals, which is proved here from the cut structure (Real.below_natural). Divergence is stated both as unboundedness of the partial sums and as nonconvergence of the sequence of prefix sums.

Proof: harmonicSeries.diverges

theorem harmonicSeries.diverges
  shows ¬∃ L ∈ ℝ, ConvergesTo(prefixSums(harmonicTerms), L)

Proof: harmonicSeries.unbounded

theorem harmonicSeries.unbounded (M : Real)
  shows ∃ N, Nat(N) ∧ M < ∑ i < N, harmonicTerms(i)

Back to overview

35. Taylor's theorem#

Informal. If f is n + 1 times differentiable on [a, b], then f(b) = ∑_{k ≤ n} f⁽ᵏ⁾(a)(b − a)ᵏ/k! + f⁽ⁿ⁺¹⁾(ξ)(b − a)ⁿ⁺¹/(n + 1)! for some ξ strictly between a and b.

Scope. The Lagrange remainder form on a closed interval [A, B] with A < B, for (f : ℝ → ℝ). The derivative is the function f′ chosen from HasDerivativeAt, and f⁽ᵏ⁾ is that derivative applied k times; the hypothesis is ∀ k ≤ n, ∀ X ∈ closedInterval(A, B), DifferentiableAt(f⁽ᵏ⁾, X), and the conclusion is written as on paper, f(B) = ∑ k ≤ n, f⁽ᵏ⁾(A) * (B - A) ^ k / k! + f⁽ⁿ⁺¹⁾(C) * (B - A) ^ (n + 1) / (n + 1)!, the factorials read as reals and the sum being the library's ∑ over the term sequence taylorTerms(f, A, B). Proved for every n by induction on the derivative of the Taylor approximant and the Cauchy mean value theorem; the n = 0 instance is checked to read as the mean value theorem, f(B) = f(A) + f′(C) * (B - A). The case B < A is not stated separately.

Proof: Taylor.theorem

theorem Taylor.theorem (f : ℝ → ℝ) (A B : Real, n : Nat)
  requires ordered : A < B
  requires smooth : ∀ k ≤ n,
    ∀ X ∈ closedInterval(A, B), DifferentiableAt(f⁽ᵏ⁾, X)
  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧
    f(B) = ∑ k ≤ n, f⁽ᵏ⁾(A) * (B - A) ^ k / k! +
      f⁽ⁿ⁺¹⁾(C) * (B - A) ^ (n + 1) / (n + 1)!

Proof: Taylor.mean_value

theorem Taylor.mean_value (f : ℝ → ℝ) (A B : Real)
  requires ordered : A < B
  requires differentiable : ∀ X ∈ closedInterval(A, B), DifferentiableAt(f, X)
  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧ f(B) = f(A) + f′(C) * (B - A)

Proof: taylorApproximant.derivative

theorem taylorApproximant.derivative (f : Set) (B X : Real, n : Nat)
  requires function : f : ℝ → ℝ
  shows (∀ k ≤ n, DifferentiableAt(f⁽ᵏ⁾, X)) →
    HasDerivativeAt(taylorApproximant(f, B, n),
      f⁽ⁿ⁺¹⁾(X) * (B - X) ^ n / n!, X)

Back to overview

36. Brouwer fixed point theorem#

Informal. Every continuous map from a closed ball (here the cube [0, 1]ⁿ) to itself has a fixed point.

Scope. Every continuous self-map of the unit cube [0, 1]ⁿ in the sup metric has a fixed point, for every dimension n, and the same for the product of simplices cut out of the cube by a block map (the strategy spaces of a finite game). The cube theorem is proved from Kuhn's cubical version of Sperner's lemma: the points of dyadic grids are labelled by comparing each with its image, Kuhn's lemma gives a completely labelled cell at every scale, and a coordinatewise convergent subsequence of the cells squeezes the limit into a fixed point. The transfer to products of simplices uses an explicit continuous retraction of the cube. General compact convex sets are not treated.

Proof: brouwer.cube

theorem brouwer.cube (n : Nat) (f : Set)
  requires continuous : CubeContinuous(f, n)
  shows ∃ x ∈ unitCube(n), f(x) = x

Proof: brouwer.simplexProduct

theorem brouwer.simplexProduct (n : Nat) (m a f : Set) (blk : n → m)
  requires ha : a ∈ simplexProduct(n, m, blk)
  requires continuous : ProductContinuous(f, n, m, blk)
  shows ∃ x ∈ simplexProduct(n, m, blk), f(x) = x

Back to overview

37. Solution of a cubic#

Informal. Cardano's formula: the roots of a cubic are given by radicals.

Scope. Cardano's formula over the concrete Dedekind-real complex field. For the depressed cubic x³ + px + q, cubic.cardano_root shows s + t is a root whenever s³ + t³ = −q and 3st = −p, and cubic.cardano_pair constructs such a pair for every p and q: s is a cube root of a root of the resolvent quadratic W² + 27qW − 27p³ and t = −p/(3s), or p = 0 and t is a cube root of −q. cubic.solution depresses a general monic cubic by x = y − a·v with 3v = 1 and returns a root of that form. Division is written through explicit inverses, and the cube and square roots come from the quadratic-root theorem and the fundamental theorem of algebra.

Proof: cubic.solution

theorem cubic.solution (a b c : Set)
  requires aIn : a ∈ ℂ
  requires bIn : b ∈ ℂ
  requires cIn : c ∈ ℂ
  shows ∃ x ∈ ℂ, ℂ[x * x * x + a * (x * x) + b * x + c] = ℂ[0] ∧ ∃ v ∈ ℂ, ∃ y ∈ ℂ, ℂ[3 * v] = ℂ[1] ∧ x = ℂ[y + -(a * v)] ∧ ∃ s ∈ ℂ, ∃ t ∈ ℂ, y = ℂ[s + t] ∧ ℂ[s * s * s + t * t * t] = ℂ[-(c + -(a * b * v) + 2 * (a * a * a * (v * v * v)))] ∧ ℂ[3 * (s * t)] = ℂ[-(b + -(a * a * v))]

Proof: cubic.cardano_root

theorem cubic.cardano_root (p q s t : Set)
  requires pIn : p ∈ ℂ
  requires qIn : q ∈ ℂ
  requires sIn : s ∈ ℂ
  requires tIn : t ∈ ℂ
  requires cubes : ℂ[s * s * s + t * t * t] = ℂ[-q]
  requires product : ℂ[3 * (s * t)] = ℂ[-p]
  shows ℂ[(s + t) * (s + t) * (s + t) + p * (s + t) + q] = ℂ[0]

Proof: cubic.cardano_pair

theorem cubic.cardano_pair (p q : Set)
  requires pIn : p ∈ ℂ
  requires qIn : q ∈ ℂ
  shows ∃ s ∈ ℂ, ∃ t ∈ ℂ, ℂ[s * s * s + t * t * t] = ℂ[-q] ∧ ℂ[3 * (s * t)] = ℂ[-p]

Back to overview

38. Arithmetic mean/geometric mean#

Informal. For nonnegative reals a and b, √(ab) ≤ (a + b)/2.

Scope. The two-variable inequality over the Dedekind reals, with the real square root from the least-upper-bound property. The general n-variable form is not proved.

Proof: sqrt.le_mean

theorem sqrt.le_mean (a b : Real)
  requires nonnegativeA : 0 ≤ a
  requires nonnegativeB : 0 ≤ b
  shows √(a * b) ≤ (a + b) / 2

Proof: realMulValue.le_square_of_mean

theorem realMulValue.le_square_of_mean (a b : Real)
  shows a * b ≤ half(a + b) * half(a + b)

Back to overview

42. Sum of the reciprocals of the triangular numbers#

Informal. 1/1 + 1/3 + 1/6 + ⋯ + 1/T_n = 2n/(n + 1), where T_k = k(k + 1)/2.

Scope. Both the finite and the infinite forms over the Dedekind reals. The summands are the real sequence triangularReciprocals with term k equal to 2/((k + 1)(k + 2)) = 1/T_{k+1}; the partial sum of the first n terms is 2n/(n + 1), proved by telescoping, and triangularReciprocals.sums_to states that the series sums to 2, as the limit of the partial sums, from n/(n + 1) → 1.

Proof: realPartialSum.triangular_reciprocals

theorem realPartialSum.triangular_reciprocals (n : Nat)
  shows ∑ i < n, triangularReciprocals(i) = (2:R) * (realNat(n):R) / (realNat(n) + 1)

Proof: triangularReciprocals.sums_to

theorem triangularReciprocals.sums_to
  shows SumsTo(triangularReciprocals, (2:R))

Back to overview

44. The binomial theorem#

Informal. (a + b)ⁿ = Σₖ C(n, k) aᵏ bⁿ⁻ᵏ.

Scope. For real A, B and every natural n, (A + B)^n equals the partial sum over k < n + 1 of the terms choose(n, k)·A^k·B^(n − k), with the binomial coefficient defined by Pascal's rule and the exponent n − k as truncated subtraction. The proof is by induction on n: Pascal's rule holds term by term, so splitting off the first term and reindexing the shifted sum turns the row n + 1 into A times the row n plus B times the row n, where the extra top term vanishes because the coefficient above the diagonal is zero.

Proof: binomial.theorem

theorem binomial.theorem (A B : Real) (n : Nat)
  shows (A + B) ^ n = ∑ i < n + 1, binomialTerm(A, B, n)(i)

Proof: binomialTerm.pascal

theorem binomialTerm.pascal (A B : Real) (n k : Nat)
  shows binomialTerm(A, B, succ(n))(succ(k)) = A * binomialTerm(A, B, n)(k) + B * binomialTerm(A, B, n)(succ(k))

Back to overview

46. Solution of the general quartic equation#

Informal. Ferrari's method: the roots of a quartic are given by radicals through a resolvent cubic.

Scope. Ferrari's method over the concrete complex field. quartic.ferrari_identity is the factorisation 4(y⁴ + py² + qy + r) = (2y² + p + 2m)² − (2αy − γ)² under α² = 2m, αγ = q, γ² = 4m² + 4pm + p² − 4r; quartic.depressed_solution produces m from the resolvent cubic 8m³ + 8pm² + 2p²m − 8rm − q² = 0 through the cubic theorem, α and γ as above, and a root y of the quadratic 2y² − 2αy + (p + 2m + γ) = 0, which is then a root of the quartic. quartic.solution depresses a general monic quartic by x = y − a·e with 4e = 1. The statements give a root in formula form; the four roots with multiplicity are not enumerated.

Proof: quartic.solution

theorem quartic.solution (a b c d : Set)
  requires aIn : a ∈ ℂ
  requires bIn : b ∈ ℂ
  requires cIn : c ∈ ℂ
  requires dIn : d ∈ ℂ
  shows ∃ x ∈ ℂ, ℂ[x * x * x * x + a * (x * x * x) + b * (x * x) + c * x + d] = ℂ[0] ∧ ∃ e ∈ ℂ, ∃ y ∈ ℂ, ℂ[2 * 2 * e] = ℂ[1] ∧ x = ℂ[y + -(a * e)] ∧ ℂ[y * y * y * y + (b + -((3 + 3) * (a * a * (e * e)))) * (y * y) + (c + -(2 * (a * b * e)) + 2 * 2 * 2 * (a * a * a * (e * e * e))) * y + (d + -(a * c * e) + a * a * b * (e * e) + -(3 * (a * a * a * a * (e * e * e * e))))] = ℂ[0]

Proof: quartic.depressed_solution

theorem quartic.depressed_solution (p q r : Set)
  requires pIn : p ∈ ℂ
  requires qIn : q ∈ ℂ
  requires rIn : r ∈ ℂ
  shows ∃ y ∈ ℂ, ℂ[y * y * y * y + p * (y * y) + q * y + r] = ℂ[0] ∧ ∃ m ∈ ℂ, ∃ α ∈ ℂ, ∃ γ ∈ ℂ, ℂ[2 * 2 * 2 * (m * m * m) + 2 * 2 * 2 * (p * (m * m)) + 2 * (p * p * m) + -(2 * 2 * 2 * (r * m)) + -(q * q)] = ℂ[0] ∧ ℂ[α * α] = ℂ[2 * m] ∧ ℂ[α * γ] = q ∧ ℂ[2 * (y * y) + -(2 * (α * y)) + (p + 2 * m + γ)] = ℂ[0]

Proof: quartic.ferrari_identity

theorem quartic.ferrari_identity (p q r m α γ y : Set)
  requires pIn : p ∈ ℂ
  requires qIn : q ∈ ℂ
  requires rIn : r ∈ ℂ
  requires mIn : m ∈ ℂ
  requires alphaIn : α ∈ ℂ
  requires gammaIn : γ ∈ ℂ
  requires yIn : y ∈ ℂ
  requires alphaSquare : ℂ[α * α] = ℂ[2 * m]
  requires gamma : ℂ[α * γ] = q
  requires gammaSquare : ℂ[γ * γ] = ℂ[2 * 2 * (m * m) + 2 * 2 * (p * m) + p * p + -(2 * 2 * r)]
  shows ℂ[2 * 2 * (y * y * y * y + p * (y * y) + q * y + r)] = ℂ[(2 * (y * y) + p + 2 * m) * (2 * (y * y) + p + 2 * m) + -((2 * (α * y) + -γ) * (2 * (α * y) + -γ))]

Back to overview

49. The Cayley–Hamilton theorem#

Informal. Every square matrix satisfies its own characteristic polynomial.

Scope. For a square matrix M : R ^ n × n over a bundled commutative ring CommRing(R), the characteristic polynomial charpoly(M), the element det(X·1 − M) of polynomialRing(R, {0}), evaluates at M to the zero matrix: evalAt(M)(charpoly(M)) = matrixRing(R, n)[0], where evalAt(M) is the evaluation homomorphism polynomialRing(R, {0}) →+* commutant(R, n, M) sending X to M and the constants to the scalar matrices, and commutant(R, n, M) is the commutative subring of the matrix ring matrixRing(R, n) generated by M and the scalars, the bicommutant of {M}. The proof reads the adjugate identity of the characteristic matrix over that commutative ring entry by entry and contracts it against the columns of M. Everything is in ZF.

Proof: Matrix.cayley_hamilton

theorem Matrix.cayley_hamilton (M : R ^ n × n)
  shows evalAt(M)(charpoly(M)) = matrixRing(R, n)[0]

Proof: charpoly.evaluate

theorem charpoly.evaluate (M : R ^ n × n)
  shows evalAt(M)(charpoly(M)) = determinant(n, Ring.carrier(commutant(R, n, M)),
    Ring.add(commutant(R, n, M)), Ring.zero(commutant(R, n, M)),
    Ring.neg(commutant(R, n, M)), Ring.mul(commutant(R, n, M)),
    Ring.one(commutant(R, n, M)), charMatrix(R, n, M))

Proof: matrixEvaluation.hom

theorem matrixEvaluation.hom (M : R ^ n × n)
  shows evalAt(M) : polynomialRing(R, {0}) →+* commutant(R, n, M)

Proof: matrixRing.ring

instance matrixRing.ring
  shows Ring(matrixRing(R, n))

Back to overview

51. Wilson's theorem#

Informal. (p − 1)! ≡ −1 (mod p) for every prime p.

Scope. Both directions. For every prime p, ((p − 1)! + 1) % p = 0, stated in natural numbers, where p - 1 is truncated subtraction; conversely a natural n > 1 with ((n − 1)! + 1) % n = 0 is prime, and wilson.characterization states the equivalence for every n > 1. The residues 2, …, p − 2 are paired with their modular inverses, chosen by uniqueness: a residue is its own inverse only when it is 1 or p − 1, so the product of the middle residues is 1 modulo p by induction on the length of such paired lists, and the remaining factor p − 1 contributes −1; the case p = 2 is computed directly. For the converse, a proper divisor d of n divides (n − 1)! and hence 1.

Proof: wilson.theorem

theorem wilson.theorem (p : Nat)
  requires prime : Prime(p)
  shows ((p - 1)! + 1) % p = 0

Proof: wilson.converse

theorem wilson.converse (n : Nat)
  requires aboveOne : 1 < n
  requires congruence : ((n - 1)! + 1) % n = 0
  shows Prime(n)

Proof: wilson.characterization

theorem wilson.characterization (n : Nat)
  requires aboveOne : 1 < n
  shows Prime(n) ↔ ((n - 1)! + 1) % n = 0

Back to overview

52. Number of subsets of a set#

Informal. A set with n elements has 2^n subsets.

Scope. HasCardinality(A, n) gives HasCardinality(𝒫(A), 2 ^ n), by induction on n: adjoining a fresh element x to A puts 𝒫(insert(x, A)) in bijection with the tagged disjoint union 𝒫(A) ⊎ 𝒫(A), through the map that records whether x is in a subset, so the count doubles.

Proof: powerset.cardinality

theorem powerset.cardinality (A : Set) (n : Nat)
  requires counted : HasCardinality(A, n)
  shows HasCardinality(𝒫(A), 2 ^ n)

Proof: Equipotent.powerset_insert

theorem Equipotent.powerset_insert (A x : Set)
  requires fresh : ¬(x ∈ A)
  shows 𝒫(insert(x, A)) ≃ 𝒫(A) ⊎ 𝒫(A)

Back to overview

54. Königsberg bridges problem#

Informal. No walk crosses each of the seven Königsberg bridges exactly once.

Scope. Actual bridge identities and endpoint table, including parallel bridges; derived from a general finite multigraph parity obstruction. Indexed paths replace the source list presentation.

Proof: no_euler_trail_exists

theorem no_euler_trail_exists
  shows ¬(∃ n ∈ ℕ, ∃ edges, ∃ vertices,
    Multigraph.EulerTrail(4, 7, leftEnd, rightEnd, edges, vertices, n))

Back to overview

55. Product of segments of chords#

Informal. If two chords AB and CD of a circle meet at P, then PA·PB = PC·PD.

Scope. Euclidean plane with coordinates. The point P lies on each chord's line as P = A + t(B − A), so the statement covers intersections inside and outside the circle alike. Proved through the power of a point: the dot product of the two segments at P equals the squared distance to the center less the squared radius, and the product of the segment lengths is the square root of the product of their squares.

Proof: chord.products

theorem chord.products (a b c d p center through : Point) (t u : Real)
  requires onA : OnCircle(a, center, through)
  requires onB : OnCircle(b, center, through)
  requires onC : OnCircle(c, center, through)
  requires onD : OnCircle(d, center, through)
  requires firstLine : OnLine(p, a, b, t)
  requires secondLine : OnLine(p, c, d, u)
  shows distance(p, a) * distance(p, b) = distance(p, c) * distance(p, d)

Proof: chord.power

theorem chord.power (a b p center through : Point) (t : Real)
  requires onA : OnCircle(a, center, through)
  requires onB : OnCircle(b, center, through)
  requires onLine : OnLine(p, a, b, t)
  shows angleDot(a, p, b) =
    distanceSquared(p, center) - distanceSquared(a, center)

Back to overview

57. Heron's formula#

Informal. The area of a triangle with side lengths a, b, c and semiperimeter s = (a + b + c)/2 is √(s(s − a)(s − b)(s − c)).

Scope. Euclidean plane with coordinates. The area is half the absolute value of the cross product of two sides, the side lengths are square roots of squared distances, and the semiperimeter is half their sum. Proved through the squared form 16·area² = 2a²b² + 2b²c² + 2c²a² − a⁴ − b⁴ − c⁴, a polynomial identity in the coordinates.

Proof: heron

theorem heron (a b c : Point)
  shows area(a, b, c) =
    √(semiperimeter(a, b, c) *
      (semiperimeter(a, b, c) - distance(b, c)) *
      (semiperimeter(a, b, c) - distance(c, a)) *
      (semiperimeter(a, b, c) - distance(a, b)))

Proof: heron.squared

theorem heron.squared (a b c : Point)
  shows (16:R) * (area(a, b, c) * area(a, b, c)) =
    2 * distanceSquared(a, b) * distanceSquared(b, c) +
    2 * distanceSquared(b, c) * distanceSquared(c, a) +
    2 * distanceSquared(c, a) * distanceSquared(a, b) -
    distanceSquared(a, b) * distanceSquared(a, b) -
    distanceSquared(b, c) * distanceSquared(b, c) -
    distanceSquared(c, a) * distanceSquared(c, a)

Back to overview

58. Formula for the number of combinations#

Informal. An n-element set has C(n, k) subsets with k elements.

Scope. A finite set with n elements has exactly choose(n, k) subsets with k elements, where choose is defined by Pascal's rule and subsetsOfSize(A, k) is the set of subsets of A of cardinality k. The proof is by induction on n: the k + 1 element subsets of insert(a, B) are sent by the powerset split of entry 52 onto the disjoint sum of the k + 1 element subsets of B (those avoiding a) and the k element subsets of B (those containing a, with a removed), and Pascal's rule adds the two counts. The symmetric identity choose(n, k) = choose(n, n − k) is not included.

Proof: combinations.count

theorem combinations.count (A : Set) (k : Nat)
  requires finite : Finite(A)
  shows cardinality(subsetsOfSize(A, k)) = choose(cardinality(A), k)

Proof: subsetsOfSize.cardinality

theorem subsetsOfSize.cardinality (n : Nat)
  shows ∀ A, HasCardinality(A, n) → ∀ k, Nat(k) → HasCardinality(subsetsOfSize(A, k), choose(n, k))

Back to overview

60. Bézout's theorem#

Informal. For any integers a, b, there are integers u, v with ua + vb = gcd(a, b).

Scope. Nonnegative GCD is returned as a natural and embedded into the quotient integers. Natural-input coefficients are also computed and proved correct. No equivalence with the source program is asserted.

Proof: integerGCD.bezout

theorem integerGCD.bezout (x y : Integer)
  shows ∃ u, Integer(u) ∧ ∃ v, Integer(v) ∧ u * x + v * y = integerOfNat(integerGCD(x, y))

Proof: bezout.correct

theorem bezout.correct (a b : Nat)
  shows integerLinearCombination(bezoutLeft(a, b), bezoutRight(a, b), a, b) = integerOfNat(gcd(a, b))

Back to overview

63. Cantor's theorem#

Informal. No function from a set onto its powerset exists.

Scope. For every set A and every f, f is not a surjection from A onto 𝒫(A). Proved by the diagonal set. The uncountability of 𝒫(ℕ) and of the reals (entry 22) build on it.

Proof: Cantor.no_surjection_onto_powerset

theorem Cantor.no_surjection_onto_powerset (f A : Set)
  shows ¬SurjectiveBetween(f, A, 𝒫(A))

Back to overview

64. L'Hôpital's rule#

Informal. If f(a) = g(a) = 0, f and g are differentiable near a with g′ ≠ 0 away from a, and f′(x)/g′(x) → L as x → a, then f(x)/g(x) → L.

Scope. The 0/0 form at a point, for (f g : ℝ → ℝ), with limits as the library's punctured limit TendsToAt and quotients as pointwiseDiv: from f(A) = 0, g(A) = 0, g′ ≠ 0 away from A, and TendsToAt(pointwiseDiv(f′, g′), L, A) follows TendsToAt(pointwiseDiv(f, g), L, A). Differentiability is assumed on an open ball around A, including A; the Cauchy mean value theorem CauchyMeanValue.theorem, f′(C) * (g(B) - g(A)) = g′(C) * (f(B) - f(A)), proved from Rolle's theorem, gives for each x on either side of A a point strictly between where f/g equals f′/g′. The ∞/∞ form and limits at infinity are not covered.

Proof: LHopital.theorem

theorem LHopital.theorem (f g : ℝ → ℝ) (A L W : Real)
  requires radius : 0 < W
  requires differentiableF : ∀ X ∈ openBall(A, W), DifferentiableAt(f, X)
  requires differentiableG : ∀ X ∈ openBall(A, W), DifferentiableAt(g, X)
  requires nonzero : ∀ X ∈ openBall(A, W), X ≠ A → g′(X) ≠ (0:R)
  requires zeroF : f(A) = 0
  requires zeroG : g(A) = 0
  requires limit : TendsToAt(pointwiseDiv(f′, g′), L, A)
  shows TendsToAt(pointwiseDiv(f, g), L, A)

Proof: CauchyMeanValue.theorem

theorem CauchyMeanValue.theorem (f g : ℝ → ℝ) (A B : Real)
  requires ordered : A < B
  requires continuousF : ContinuousOn(f, closedInterval(A, B))
  requires continuousG : ContinuousOn(g, closedInterval(A, B))
  requires differentiableF : ∀ C ∈ ℝ, A < C → C < B → DifferentiableAt(f, C)
  requires differentiableG : ∀ C ∈ ℝ, A < C → C < B → DifferentiableAt(g, C)
  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧
    f′(C) * (g(B) - g(A)) = g′(C) * (f(B) - f(A))

Back to overview

65. Isosceles triangle theorem#

Informal. Equal legs give equal base angles.

Scope. Euclidean plane. The cosine of an unoriented angle is the normalized dot product of its rays, proved to lie in [-1, 1]; an angle in [0, π] is determined by its cosine, so equal cosines are equal angles. The theorem states that the two base angles have equal cosines. The earlier root-free algebraic encoding (EqualAngle) is retained.

Proof: isosceles.cosines

theorem isosceles.cosines (a b c : Point)
  requires base : a ≠ b
  requires leg : a ≠ c
  requires equalLegs : Euclidean.distanceSquared(a, c) = Euclidean.distanceSquared(b, c)
  shows cosAngle(c, a, b) = cosAngle(c, b, a)

Proof: isosceles

theorem isosceles (a b c : Point)
  requires base : a ≠ b
  requires leg : a ≠ c
  requires equalLegs : Euclidean.distanceSquared(a, c) = Euclidean.distanceSquared(b, c)
  shows EqualAngle(c, a, b, c, b, a)

Back to overview

66. Sum of a geometric series#

Informal. 1 + x + x² + ⋯ + xⁿ⁻¹ = (1 − xⁿ)/(1 − x) for x ≠ 1.

Scope. Finite and infinite geometric sums over the Dedekind reals, as realPartialSum of the sequence of powers: the product form (1 − x)·Σ = 1 − xⁿ for every real x, the quotient form when 1 − x ≠ 0, and geometricSeries.sums_to: for |x| < 1 the series sums to 1/(1 − x), as the limit of the partial sums, from xⁿ → 0 by Bernoulli's inequality and the Archimedean property.

Proof: realPartialSum.geometric_quotient

theorem realPartialSum.geometric_quotient (X : Real, n : Nat)
  requires nonzero : ((1:R) - X) ≠ (0:R)
  shows ∑ i < n, geometricTerms(X)(i) =
    ((1:R) - X ^ n) / ((1:R) - X)

Proof: realPartialSum.geometric

theorem realPartialSum.geometric (X : Real, n : Nat)
  shows ((1:R) - X) * (∑ j < n, geometricTerms(X)(j):R) =
    (1:R) - X ^ n

Proof: geometricSeries.sums_to

theorem geometricSeries.sums_to (X : Real)
  requires small : abs(X) < 1
  shows SumsTo(geometricTerms(X), (1:R) / ((1:R) - X))

Back to overview

68. Sum of an arithmetic series#

Informal. 2·∑ₖ₌₀ⁿ (A + kD) = (n + 1)(2A + nD).

Scope. Arbitrary real first term and common difference; the doubled formula avoids division, and a quotient-form corollary is also available.

Proof: arithmeticSeries.inclusive

theorem arithmeticSeries.inclusive (A D : Real, n : Nat)
  shows (2:R) * (∑ i < n + 1, arithmeticTerms(A, D)(i):R) =
    ((realNat(n):R) + (1:R)) * ((2:R) * A + (realNat(n):R) * D)

Back to overview

69. Greatest common divisor algorithm#

Informal. The Euclidean algorithm returns the greatest common divisor.

Scope. Structurally recursive remainder-based algorithm on arbitrary natural inputs, including zero. The integer wrapper uses absolute values. No running-time bound is claimed.

Proof: gcd.correct

theorem gcd.correct (a b : Nat)
  shows IsGCD(a, b, gcd(a, b))

Proof: integerGCD.correct

theorem integerGCD.correct (x y : Integer)
  shows IsIntegerGCD(x, y, integerGCD(x, y))

Back to overview

70. The perfect number theorem#

Informal. If 2^p − 1 is prime then 2^(p−1)(2^p − 1) is perfect (Euclid), and every even perfect number has this form (Euler).

Scope. sigma(n) is the sum of the divisors of n, natSum(divisors(n), identity(ℕ)) over the naturals, and PerfectNumber(n) says 0 < n ∧ sigma(n) = 2 * n. perfectNumber.of_mersenne gives Euclid's direction for every p (primality of 2 ^ p - 1 already forces p ≥ 2), perfectNumber.even_form gives Euler's converse as ∃ p ∈ ℕ, Prime(2 ^ p - 1) ∧ n = 2 ^ (p - 1) * (2 ^ p - 1), and perfectNumber.even_iff combines them. Underneath: sigma.multiplicative, sigma(m * n) = sigma(m) * sigma(n) for gcd(m, n) = 1, proved through the bijection (d, e) ↦ d · e from divisors(m) × divisors(n) onto divisors(m * n) and the sum of products over a product set; sigma.prime_iff, σ(p) = p + 1 characterises the primes above 1; and sigma.two_pow, σ(2 ^ k) = 2 ^ (k + 1) - 1, from divisors(2 ^ (k + 1)) being 1 together with the doubles of divisors(2 ^ k). Euler's direction writes n = 2 ^ k · m with m odd, reads (2 ^ (k + 1) − 1) σ(m) = 2 ^ (k + 1) m, and bounds the sum of the divisors strictly between 1 and m. Everything is in ZF.

Proof: perfectNumber.of_mersenne

theorem perfectNumber.of_mersenne (p : Nat)
  requires prime : Prime(2 ^ p - 1)
  shows PerfectNumber(2 ^ (p - 1) * (2 ^ p - 1))

Proof: perfectNumber.even_form

theorem perfectNumber.even_form (n : Nat)
  requires perfect : PerfectNumber(n)
  requires even : Even(n)
  shows ∃ p ∈ ℕ, Prime(2 ^ p - 1) ∧ n = 2 ^ (p - 1) * (2 ^ p - 1)

Proof: perfectNumber.even_iff

theorem perfectNumber.even_iff (n : Nat)
  requires even : Even(n)
  shows PerfectNumber(n) ↔
    ∃ p ∈ ℕ, Prime(2 ^ p - 1) ∧ n = 2 ^ (p - 1) * (2 ^ p - 1)

Proof: sigma.multiplicative

theorem sigma.multiplicative (m n : Nat)
  requires coprime : gcd(m, n) = 1
  shows sigma(m * n) = sigma(m) * sigma(n)

Proof: sigma.prime_iff

theorem sigma.prime_iff (p : Nat)
  requires aboveOne : 1 < p
  shows Prime(p) ↔ sigma(p) = p + 1

Proof: sigma.two_pow

theorem sigma.two_pow (k : Nat)
  shows sigma(2 ^ k) = 2 ^ (k + 1) - 1

Back to overview

71. Order of a subgroup#

Informal. Lagrange's theorem: the order of a subgroup of a finite group divides the order of the group.

Scope. For a finite group G (one set with carrier, operation, unit, and inverse) and a subgroup H, cardinality(H) divides order(G), the size of the carrier, and order(G) = index(G, H) · cardinality(H) with the index the number of left cosets leftCosets(G, H). The proof is the textbook one: the cosets g • H partition the group (leftCoset.eq_or_disjoint, leftCosets.cover), each is in bijection with H by the translation h ↦ g * h (leftCoset.cardinality), and a disjoint union of equal blocks is counted by cardinality.big_union_constant. Independently of finiteness, g ↦ (gH, rep(gH)⁻¹ · g) is a bijection from the carrier onto leftCosets(G, H) × H (Group.equipotent_cosets_product); its representative is chosen with Global Choice. Normal subgroups and quotient groups are developed in their own modules.

Proof: lagrange.theorem

theorem lagrange.theorem
  requires finite : Finite(G)
  shows cardinality(H) ∣ order(G)

Proof: lagrange

theorem lagrange
  requires finite : Finite(G)
  shows order(G) = index(G, H) * cardinality(H)

Back to overview

72. Sylow's theorem#

Informal. A finite group of order p^k·m with p prime not dividing m has a subgroup of order p^k; every p-subgroup lies in a conjugate of it, any two Sylow p-subgroups are conjugate, and the number of Sylow p-subgroups divides m and is congruent to 1 modulo p.

Scope. Over a bundled group Group(G) with Finite(G), Prime(p), ¬(p ∣ m), and order(G) = p ^ k * m: sylow.exists_subgroup gives ∃ P, Subgroup(P, G) ∧ cardinality(P) = p ^ k; sylow.subset_conjugate gives ∃ g ∈ G, Q ⊆ conjugateSet(G, g, P) for every PSubgroup(Q, G, p) and SylowSubgroup(P, G, p); sylow.conjugate gives ∃ g ∈ G, Q = conjugateSet(G, g, P) for two Sylow p-subgroups; sylow.count_dvd and sylow.count_mod give cardinality(sylowSubgroups(G, p)) ∣ m and cardinality(sylowSubgroups(G, p)) % p = 1. The proofs use group actions act : G ↷ X with orbits, stabilizers, and the orbit–stabilizer theorem cardinality(orbit(x)) * cardinality(stabilizer(x)) = order(G): existence by the translation action on the subsets of size p^k, whose number (p ^ k * m) choose (p ^ k) is prime to p by Lucas' congruence; conjugacy by a p-subgroup acting on the cosets of a Sylow subgroup; the count by a Sylow subgroup acting on the Sylow subgroups by conjugation, with the class equation and the normalizer alongside.

Proof: sylow.exists_subgroup

theorem sylow.exists_subgroup (p k m : Nat)
  requires finite : Finite(G)
  requires prime : Prime(p)
  requires notDivides : ¬(p ∣ m)
  requires count : order(G) = p ^ k * m
  shows ∃ P, Subgroup(P, G) ∧ cardinality(P) = p ^ k

Proof: sylow.subset_conjugate

theorem sylow.subset_conjugate (P Q : Set) (p : Nat)
  requires finite : Finite(G)
  requires prime : Prime(p)
  requires sylow : SylowSubgroup(P, G, p)
  requires pSubgroup : PSubgroup(Q, G, p)
  shows ∃ g ∈ G, Q ⊆ conjugateSet(G, g, P)

Proof: sylow.conjugate

theorem sylow.conjugate (P Q : Set) (p : Nat)
  requires finite : Finite(G)
  requires prime : Prime(p)
  requires sylowP : SylowSubgroup(P, G, p)
  requires sylowQ : SylowSubgroup(Q, G, p)
  shows ∃ g ∈ G, Q = conjugateSet(G, g, P)

Proof: sylow.count_dvd

theorem sylow.count_dvd (p k m : Nat)
  requires finite : Finite(G)
  requires prime : Prime(p)
  requires notDivides : ¬(p ∣ m)
  requires count : order(G) = p ^ k * m
  shows cardinality(sylowSubgroups(G, p)) ∣ m

Proof: sylow.count_mod

theorem sylow.count_mod (p k m : Nat)
  requires finite : Finite(G)
  requires prime : Prime(p)
  requires notDivides : ¬(p ∣ m)
  requires count : order(G) = p ^ k * m
  shows cardinality(sylowSubgroups(G, p)) % p = 1

Proof: orbit_stabilizer

theorem orbit_stabilizer (x : Set)
  requires hx : x ∈ X
  requires finite : Finite(G)
  shows cardinality(orbit(x)) * cardinality(stabilizer(x)) = order(G)

Proof: class_equation

theorem class_equation
  requires finite : Finite(G)
  shows order(G) = cardinality(center(G)) +
    natSum(noncentralClasses(G), sizeMap(noncentralClasses(G)))

Back to overview

73. Ascending or descending sequences#

Informal. Every sequence of mn + 1 distinct elements of a linear order has an increasing subsequence of length m + 1 or a decreasing one of length n + 1.

Scope. The Erdős–Szekeres theorem. For a bundled linear order LinearOrder(P) and an injective f : m * n + 1 → points(P), there is an index set S ∈ subsetsOfSize(m * n + 1, m + 1) with IncreasingOn(P, f, S) or one in subsetsOfSize(m * n + 1, n + 1) with DecreasingOn(P, f, S), where IncreasingOn says f(i) ≤ f(j) for indices i < j of S. The proof labels each index with the length of the longest increasing run and of the longest decreasing run ending there, the latter as a run of the dual order; a later larger term lengthens the first label and a later smaller term the second, so the label pairs are distinct, and there are only m·n of them.

Proof: erdos_szekeres

theorem erdos_szekeres (P f : Set) (m n : Nat)
  requires order : LinearOrder(P)
  requires distinct : InjectiveBetween(f, m * n + 1, points(P))
  shows (∃ S ∈ subsetsOfSize(m * n + 1, m + 1), IncreasingOn(P, f, S)) ∨
    (∃ S ∈ subsetsOfSize(m * n + 1, n + 1), DecreasingOn(P, f, S))

Proof: rise.step

theorem rise.step (P f : Set, N i j : Nat)
  requires order : LinearOrder(P)
  requires function : f : N → points(P)
  requires hi : i ∈ N
  requires hj : j ∈ N
  requires below : i < j
  requires le : Le(P, f(i), f(j))
  shows rise(P, f, i) < rise(P, f, j)

Back to overview

74. Principle of mathematical induction#

Informal. A set of natural numbers that contains 0 and is closed under successor contains every natural number.

Scope. Stated for subsets of ℕ and proved by the least counterexample, using the least-element construction leastNatural. Structural induction on naturals is also a primitive kernel rule; this theorem derives the set-theoretic principle from Foundation.

Proof: natural.induction

theorem natural.induction (S : Set)
  requires base : 0 ∈ S
  requires step : ∀ n ∈ ℕ, n ∈ S → n + 1 ∈ S
  shows ∀ n ∈ ℕ, n ∈ S

Back to overview

75. Mean value theorem#

Informal. A real function continuous on [a, b] and differentiable inside has a point where its derivative equals its secant slope.

Scope. Ordinary local derivative over the Dedekind reals. The formal conclusion uses multiplication by B-A instead of division.

Proof: MeanValue.theorem

theorem MeanValue.theorem (F : Set) (A B : Real)
  requires ordered : A < B
  requires continuous : ContinuousOn(F, closedInterval(A, B))
  requires differentiable : ∀ C ∈ ℝ, A < C → C < B → ∃ D ∈ ℝ, HasDerivativeAt(F, D, C)
  shows ∃ C ∈ ℝ, A < C ∧ C < B ∧ ∃ D ∈ ℝ, HasDerivativeAt(F, D, C) ∧ D * (B - A) = F(B) - F(A)

Back to overview

77. Sum of kth powers#

Informal. Closed forms for 1ᵏ + 2ᵏ + ⋯ + nᵏ.

Scope. Closed forms for the sums of the first n squares and cubes as real partial sums of realNat terms: 6·Σ i² = n(n+1)(2n+1) and 4·Σ i³ = n²(n+1)², in multiplied-out form so no division is needed, together with Nicomachus's identity that the sum of the first n cubes is the square of the sum of the first n naturals (the latter is entry 68). Proofs are inductions closed by linear_combination. The general Faulhaber formula with Bernoulli numbers is not proved.

Proof: powerSum.squares_inclusive

theorem powerSum.squares_inclusive (n : Nat)
  shows (6:R) * (∑ i < n + 1, squareTerms(i):R) =
    (realNat(n):R) * ((realNat(n):R) + (1:R)) * ((2:R) * (realNat(n):R) + (1:R))

Proof: powerSum.cubes_inclusive

theorem powerSum.cubes_inclusive (n : Nat)
  shows (4:R) * (∑ i < n + 1, cubeTerms(i):R) =
    (realNat(n):R) * (realNat(n):R) * ((realNat(n):R) + (1:R)) * ((realNat(n):R) + (1:R))

Proof: powerSum.cubes_eq_square_of_sum

theorem powerSum.cubes_eq_square_of_sum (n : Nat)
  shows ∑ i < n + 1, cubeTerms(i) =
    (∑ i < n + 1, arithmeticTerms(realZero, realOne)(i):R) *
      (∑ i < n + 1, arithmeticTerms(realZero, realOne)(i):R)

Back to overview

78. Cauchy–Schwarz inequality#

Informal. For finite-dimensional real vectors, ⟨u, v⟩² ≤ ⟨u, u⟩⟨v, v⟩.

Scope. Arbitrary finite dimension, including zero, over real sequences restricted to their first n coordinates. Squared formulation with an exact equality criterion: the second vector has zero norm, or the first is a real scalar multiple of it on that prefix. No square-root norm is used.

Proof: dotProduct.cauchy_schwarz

theorem dotProduct.cauchy_schwarz (u v : Set, n : Nat)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  shows (dotProduct(u, v, n):R) * (dotProduct(u, v, n):R) ≤
    (squaredNorm(u, n):R) * (squaredNorm(v, n):R)

Proof: dotProduct.cauchy_schwarz_scalar_equality

theorem dotProduct.cauchy_schwarz_scalar_equality (v : Set, C : Real, n : Nat)
  requires sequence : RealSequence(v)
  shows (dotProduct(mulSequence(constantSequence(C), v), v, n):R) *
      (dotProduct(mulSequence(constantSequence(C), v), v, n):R) =
    (squaredNorm(mulSequence(constantSequence(C), v), n):R) * (squaredNorm(v, n):R)

Proof: dotProduct.cauchy_schwarz_equality_iff

theorem dotProduct.cauchy_schwarz_equality_iff (u v : Set, n : Nat)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  shows (dotProduct(u, v, n):R) * (dotProduct(u, v, n):R) =
      (squaredNorm(u, n):R) * (squaredNorm(v, n):R) ↔
    (squaredNorm(v, n) = (0:R) ∨
      (∃ C ∈ ℝ, (∀ i ∈ ℕ, i < n → u[i] = C * (v[i]:R))))

Back to overview

79. Intermediate value theorem#

Informal. A continuous function on a closed interval takes every value between its values at the endpoints.

Scope. Real functions f : ℝ → ℝ continuous on closedInterval(A, B) with A ≤ B. Both the strict form f(A) < V < f(B) and the form with ≤ are proved, together with the zero-crossing corollary; the point is the least upper bound of the set where f stays below V, so only Dedekind completeness is used. The symmetric case f(A) > V > f(B) follows by applying the theorem to −f and is not stated separately.

Proof: closedInterval.intermediate_value

theorem closedInterval.intermediate_value (f : Set) (A B V : Real)
  requires ordered : A ≤ B
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires below : (f(A):R) < V
  requires above : V < (f(B):R)
  shows ∃ C ∈ closedInterval(A, B), f(C) = V

Proof: closedInterval.intermediate_value_le

theorem closedInterval.intermediate_value_le (f : Set) (A B V : Real)
  requires ordered : A ≤ B
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires below : (f(A):R) ≤ V
  requires above : V ≤ (f(B):R)
  shows ∃ C ∈ closedInterval(A, B), f(C) = V

Proof: closedInterval.zero_of_sign_change

theorem closedInterval.zero_of_sign_change (f : Set) (A B : Real)
  requires ordered : A ≤ B
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires negative : (f(A):R) < 0
  requires positive : 0 < (f(B):R)
  shows ∃ C ∈ closedInterval(A, B), f(C) = (0:R)

Back to overview

80. Fundamental theorem of arithmetic#

Informal. Every positive natural number is a product of primes, and the factorization is unique up to reordering.

Scope. A factorization is a list of primes with product ∏ xs; n = 1 has the empty factorization. Uniqueness is stated as equality of multisets: two prime lists with the same product give every prime the same multiplicity. Euclid's lemma is derived through the integer Bézout identity. Everything is in ZF.

Proof: primeFactorization.fundamental_theorem

theorem primeFactorization.fundamental_theorem (n : Nat)
  requires nonzero : n ≠ 0
  shows (∃ xs, List(ℕ, xs) ∧ PrimeList(xs) ∧ ∏ xs = n) ∧
    (∀ xs, List(ℕ, xs) → ∀ ys, List(ℕ, ys) → PrimeList(xs) → PrimeList(ys) →
      ∏ xs = n → ∏ ys = n →
      ∀ q, Nat(q) → multiplicity(q, xs) = multiplicity(q, ys))

Proof: primeFactorization.exists

theorem primeFactorization.exists (n : Nat)
  requires nonzero : n ≠ 0
  shows ∃ xs, List(ℕ, xs) ∧ PrimeList(xs) ∧ ∏ xs = n

Proof: primeFactorization.unique

theorem primeFactorization.unique (xs : List(ℕ))
  shows ∀ ys, List(ℕ, ys) → PrimeList(xs) → PrimeList(ys) →
    ∏ xs = ∏ ys →
    ∀ q, Nat(q) → multiplicity(q, xs) = multiplicity(q, ys)

Back to overview

85. Divisibility by 3 rule#

Informal. A natural number is divisible by 3 exactly when the sum of its decimal digits is.

Scope. Numbers are given by their decimal digits, least significant first, with digitsValue reading the list and digitSum adding it. The rule holds for any list of naturals, not only digits below ten, because every power of ten is one more than a multiple of three.

Proof: digitsValue.three_divides_iff

theorem digitsValue.three_divides_iff (ds : List(ℕ))
  shows 3 ∣ digitsValue(ds) ↔ 3 ∣ digitSum(ds)

Back to overview

88. Derangements formula#

Informal. The number of permutations of n objects with no fixed point is d(n) = n! ∑{k ≤ n} (−1)^k / k!, equivalently d(n) = ∑{k ≤ n} (−1)^k (n choose k)(n − k)!, with d(n + 2) = (n + 1)(d(n + 1) + d(n)).

Scope. derangements(I) is the set of permutations of I without a fixed point. derangements.natural_count gives cardinality(derangements(n)) = derangement(n) for the recurrence-defined sequence 1, 0, 1, 2, 9, 44, …, derangements.recurrence the textbook recurrence for the counts themselves, and derangements.formula the inclusion–exclusion sum in the integers, integerOfNat(cardinality(derangements(n))) = derangementSum(n, n + 1) with derangementSum(n, k + 1) = derangementSum(n, k) + (−1)^k · (n choose k) · (n − k)!, the integer form of n! ∑ (−1)^k/k!. The count is proved by the classical bijection: a derangement sends a chosen point a to some b, and either returns b to a, leaving a derangement of the other n − 2 points, or not, where composing with the transposition (a b) and forgetting a leaves a derangement of n − 1 points. The formula follows from the one-step recurrence d(n + 1) = (n + 1)d(n) + (−1)^(n + 1).

Proof: derangements.natural_count

theorem derangements.natural_count (n : Nat)
  shows cardinality(derangements(n)) = derangement(n)

Proof: derangements.recurrence

theorem derangements.recurrence (n : Nat)
  shows cardinality(derangements(n + 2)) =
    (n + 1) * (cardinality(derangements(n + 1)) + cardinality(derangements(n)))

Proof: derangements.formula

theorem derangements.formula (n : Nat)
  shows integerOfNat(cardinality(derangements(n))) = derangementSum(n, n + 1)

Proof: derangement.closed_form

theorem derangement.closed_form (n : Nat)
  shows integerOfNat(derangement(n)) = derangementSum(n, n + 1)

Back to overview

89. The factor and remainder theorems#

Informal. Dividing a polynomial p by X − a leaves the remainder p(a); a is a root exactly when X − a divides p.

Scope. For a polynomial over any commutative ring, given by its Horner coefficient list, remainder.theorem is the synthetic-division identity p(x) = p(a) + (x − a)·q(x) with q the synthetic quotient, so the remainder on division by X − a is p(a); factor.theorem specialises it at a root to p(x) = (x − a)·q(x), and factor.root recovers the root from such a factorisation. Polynomials are concrete coefficient lists evaluated by Horner's rule, not elements of an abstract polynomial ring.

Proof: factor.theorem

theorem factor.theorem (a x c : Set) (cs : List(A))
  requires center : a ∈ R
  requires element : x ∈ R
  requires coefficient : c ∈ R
  requires root : hornerAt{A}(add, mul, leading, a, c :: cs) = R[0]
  shows hornerAt{A}(add, mul, leading, x, c :: cs) = R[(x - a) * hornerAt{A}(add, mul, leading, x, hornerQuotient{A}(add, mul, leading, a, cs))]

Proof: remainder.theorem

theorem remainder.theorem (a x c : Set) (cs : List(A))
  requires center : a ∈ R
  requires element : x ∈ R
  requires coefficient : c ∈ R
  shows hornerAt{A}(add, mul, leading, x, c :: cs) = R[hornerAt{A}(add, mul, leading, a, c :: cs) + (x - a) * hornerAt{A}(add, mul, leading, x, hornerQuotient{A}(add, mul, leading, a, cs))]

Back to overview

91. Triangle inequality#

Informal. ‖a − c‖ ≤ ‖a − b‖ + ‖b − c‖, and for real numbers |a + b| ≤ |a| + |b|.

Scope. Euclidean norm form in the plane: the distance between points is the square root of the squared distance, and the triangle inequality is proved from Cauchy–Schwarz. The real absolute-value and real-line metric forms are also checked. Higher-dimensional Euclidean space is not covered.

Proof: distance.triangle

theorem distance.triangle (a b c : Point)
  shows distance(a, c) ≤ distance(a, b) + distance(b, c)

Proof: abs.triangle

theorem abs.triangle (A B : Real)
  shows abs(A + B) ≤ abs(A) + abs(B)

Proof: dist.triangle

theorem dist.triangle (A B C : Real)
  shows dist(A, C) ≤ dist(A, B) + dist(B, C)

Back to overview

93. The birthday problem#

Informal. Among 23 people with independent, uniformly random birthdays in a year of 365 days, the probability that two share a birthday exceeds 1/2; for n people and d days it is 1 − d(d − 1)⋯(d − n + 1)/dⁿ.

Scope. An assignment of birthdays to the people of A from the days of B is a function A → B, and sharedBirthday(A, B) is the set of assignments outside injections(A, B); sharedBirthday.membership reads it as the assignments under which two distinct people get the same day. birthday.counting is the arithmetic core, 2 * fallingFactorial(365, 23) < 365 ^ 23, certified by the kernel's closed-term evaluator through the equation 2 · 365·364⋯343 + 1 + c = 365²³ for the explicit 58-digit gap c. birthday.injections transfers it to any finite sets of 23 people and 365 days through injections.count and functionSpace.count: fewer than half of the assignments are injective. sharedBirthday.probability is the general formula on the uniform probability space of all assignments, prob(uniformWeight(functionSpace(A, B)), sharedBirthday(A, B)) = 1 − realNat(fallingFactorial(|B|, |A|)) / realNat(|B| ^ |A|) for finite A and finite nonempty B, from the complement rule of the uniform distribution; birthday.problem specializes it and bounds the quotient below 1/2 from the counting fact, giving 1/2 < prob(…) as a real inequality. Every theorem's axiom audit lists only ZF axioms.

Proof: birthday.counting

theorem birthday.counting
  shows 2 * fallingFactorial(365, 23) < 365 ^ 23

Proof: birthday.injections

theorem birthday.injections (A B : Set)
  requires finiteA : Finite(A)
  requires finiteB : Finite(B)
  requires people : cardinality(A) = 23
  requires days : cardinality(B) = 365
  shows 2 * cardinality(injections(A, B)) < cardinality(functionSpace(A, B))

Proof: sharedBirthday.probability

theorem sharedBirthday.probability (A B : Set)
  requires finiteA : Finite(A)
  requires finiteB : Finite(B)
  requires inhabited : Nonempty(B)
  shows prob(uniformWeight(functionSpace(A, B)), sharedBirthday(A, B)) =
    (1:R) - (realNat(fallingFactorial(cardinality(B), cardinality(A))):R) /
      (realNat(cardinality(B) ^ cardinality(A)):R)

Proof: birthday.problem

theorem birthday.problem (A B : Set)
  requires finiteA : Finite(A)
  requires finiteB : Finite(B)
  requires people : cardinality(A) = 23
  requires days : cardinality(B) = 365
  shows (1:R) / 2 <
    (prob(uniformWeight(functionSpace(A, B)), sharedBirthday(A, B)):R)

Back to overview

94. Law of cosines#

Informal. c² = a² + b² − 2ab·cos γ.

Scope. Euclidean plane, with side lengths that are square roots of squared distances and the cosine of the angle at the vertex defined as the normalized dot product of its rays, which is proved to lie in [-1, 1]. Requires the two rays to be nondegenerate. The root-free dot-product identity is retained.

Proof: law_of_cosines

theorem law_of_cosines (a b c : Point)
  requires firstRay : a ≠ b
  requires secondRay : c ≠ b
  shows Euclidean.distanceSquared(a, c) =
    Euclidean.distanceSquared(a, b) + Euclidean.distanceSquared(b, c) - 2 * (distance(a, b) * distance(b, c) * cosAngle(a, b, c))

Proof: cosine_identity

theorem cosine_identity (a b c : Point)
  shows distanceSquared(a, c) + angleDot(a, b, c) + angleDot(a, b, c) =
    distanceSquared(a, b) + distanceSquared(b, c)

Back to overview

96. Principle of inclusion/exclusion#

Informal. For finite sets, |A ∪ B| + |A ∩ B| = |A| + |B|.

Scope. Two finite sets, with cardinality the natural number counting a finite set. The union splits as A with B ∖ A and B as A ∩ B with B ∖ A, two disjoint unions whose sizes add.

Proof: cardinality.inclusion_exclusion

theorem cardinality.inclusion_exclusion (A B : Set)
  requires finiteA : Finite(A)
  requires finiteB : Finite(B)
  shows cardinality(A ∪ B) + cardinality(A ∩ B) =
    cardinality(A) + cardinality(B)

Back to overview

97. Cramer's rule#

Informal. A solution of a square linear system is given by ratios of determinants.

Scope. Over a bundled commutative ring CommRing(R), for a square matrix M : R ^ n × n and a solution x of the row system x · M = b (rowProduct(R, n, x, M)(j) = b(j) for every column j), det(M) * x(i) = det(N) where N is M with row i replaced by b; no division is assumed, so the statement holds over every commutative ring and gives x(i) = det(N) / det(M) over a field. The adjugate identity M * adj(M) = det(M) · 1 is stated in the matrix ring matrixRing(R, n), and when det(M) has an inverse u, M * scalarMultiple(R, n, u, adj(M)) = matrixRing(R, n)[1]. The column form and the two-sided inverse await the invariance of the determinant under transposition. Everything is in ZF.

Proof: Matrix.cramer

theorem Matrix.cramer (M N : R ^ n × n) (x b i : Set)
  requires vector : x : n → R.carrier
  requires solution : ∀ j ∈ n, rowProduct(R, n, x, M)(j) = b(j)
  requires row : i ∈ n
  requires replaced : ∀ j ∈ n, N[i, j] = b(j)
  requires outside : ∀ k ∈ n, k ≠ i → ∀ j ∈ n, N[k, j] = M[k, j]
  shows det(M) * x(i) = det(N)

Proof: Matrix.mul_adj

theorem Matrix.mul_adj (M : R ^ n × n)
  shows M * adj(M) = scalarMultiple(R, n, det(M), matrixRing(R, n)[1])

Proof: Matrix.mul_inverse

theorem Matrix.mul_inverse (M : R ^ n × n) (u : R)
  requires inverse : u * det(M) = R[1]
  shows M * scalarMultiple(R, n, u, adj(M)) = matrixRing(R, n)[1]

Back to overview

Beyond the numbered list#

The library also grows in ways the scoreboard does not count. The two-modulus Chinese remainder theorem is one example: for coprime integers m,n and arbitrary residues a,b, a simultaneous solution exists and is unique modulo m*n. Its explicit construction uses Bézout coefficients.

Proof: ChineseRemainder.exists

theorem ChineseRemainder.exists (m n a b : Integer)
  requires coprime : IntegerCoprime(m, n)
  shows ∃ x, Integer(x) ∧ IntegerCongruent(m, x, a) ∧ IntegerCongruent(n, x, b)

Proof: ChineseRemainder.unique

theorem ChineseRemainder.unique (m n a b x y : Integer)
  requires coprime : IntegerCoprime(m, n)
  requires xm : IntegerCongruent(m, x, a)
  requires xn : IntegerCongruent(n, x, b)
  requires ym : IntegerCongruent(m, y, a)
  requires yn : IntegerCongruent(n, y, b)
  shows IntegerCongruent(m * n, x, y)

Orthogonal projection onto a line is constructed for arbitrary finite real vectors with a nonzero direction. Its residual is orthogonal, and the projection uniquely minimizes squared distance along that line. Its residual also gives a Pythagorean decomposition, and projection is idempotent.

Proof: lineProjection.orthogonal

theorem lineProjection.orthogonal (u v : Set, n : Nat)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  requires nonzero : squaredNorm(v, n) ≠ (0:R)
  shows Orthogonal(subSequence(u, lineProjection(u, v, n)), v, n)

Proof: lineProjection.minimum

theorem lineProjection.minimum (u v : Set, C : Real, n : Nat)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  requires nonzero : squaredNorm(v, n) ≠ (0:R)
  shows lineDistanceSquared(u, v, projectionCoefficient(u, v, n), n) ≤
    lineDistanceSquared(u, v, C, n)

Proof: lineProjection.unique_minimizer

theorem lineProjection.unique_minimizer (u v : Set, C : Real, n : Nat)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  requires nonzero : squaredNorm(v, n) ≠ (0:R)
  requires minimizing : lineDistanceSquared(u, v, C, n) ≤
    lineDistanceSquared(u, v, projectionCoefficient(u, v, n), n)
  shows C = projectionCoefficient(u, v, n)

Proof: orthogonalResidual.pythagorean

theorem orthogonalResidual.pythagorean (u v : Set, n : Nat)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  requires nonzero : squaredNorm(v, n) ≠ (0:R)
  shows squaredNorm(u, n) = squaredNorm(lineProjection(u, v, n), n) +
    squaredNorm(orthogonalResidual(u, v, n), n)

Proof: lineProjection.idempotent

theorem lineProjection.idempotent (u v : Set, n : Nat)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  requires nonzero : squaredNorm(v, n) ≠ (0:R)
  shows lineProjection(lineProjection(u, v, n), v, n) = lineProjection(u, v, n)

Try ProjectionStarter.g17.

Successive removals along perpendicular directions preserve earlier orthogonality and commute coordinatewise. The two-direction Bessel bound also proves that the captured squared lengths cannot exceed the original squared length. See OrthogonalizationStarter.g17.

Try ChineseRemainderStarter.g17. Other developments include verified Dijkstra, executable Gaussian elimination, Euclidean centers, compactness, uniform continuity, and modular inverses. See cumulus.md.

Maintaining this page#

1. Add or update the scope audit in top-100.json.
2. Give every completed or scoped entry an existing theorem and source path.
3. Run npm run docs:top100; the formal statements and line links regenerate together.
4. Run npm run docs:top100:check and the relevant proof and replay checks.