$\tfrac{n(n+1)}{2} + \tfrac{n(n-1)}{2} = n^2$

Proved

PassivityUn.symm_antisymm_dim

by ShapeZero · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebramatrices

For every natural number $n$ ,

\frac{n(n+1)}{2} + \frac{n(n-1)}{2} = n^2 .

The two summands are the dimensions of the spaces of symmetric and of antisymmetric real $n\times n$ matrices, so this is the arithmetic that turns the block description of the admissible class into the count $n^2$ .

Formalization Note The identity is stated in $\mathbb{N}$ with floor division and truncated subtraction; both are exact here, since $n(n\pm1)$ is always even and $n\cdot(n-1) = 0$ at $n = 0$ .

Preamble

import Mathlib

Formal statement

namespace PassivityUn
theorem symm_antisymm_dim (n : ℕ) :
    n * (n + 1) / 2 + n * (n - 1) / 2 = n ^ 2 := by sorry
end PassivityUn

Source

Shape Zero LLC, "Formal Proofs of the C1 Verification Package" (August 2026), §6, Theorem 6.1: https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ShapeZero_C1_Formal_Proofs.pdf ; corrected in "Errata — C1 Formal Proofs (Sections 3 and 6)", Corrected Theorem 6.1(b) (dimension count): https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ERRATUM_Theorem_6.1.md

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

PassivityUn.symm_antisymm_dim. For every natural number $n \in \mathbb{N} = \{0, 1, 2, \dots\}$ , the following equation holds in the natural numbers:

\left\lfloor \frac{n(n+1)}{2} \right\rfloor + \left\lfloor \frac{n \cdot (n \mathbin{\dot-} 1)}{2} \right\rfloor = n^2 .

The notation works as follows:

Division: both divisions are natural-number division, which rounds down. They are written with floor brackets above.
Subtraction: $n \mathbin{\dot-} 1$ is truncated natural-number subtraction. It equals $n-1$ when $n \ge 1$ and $0$ when $n = 0$ .

For every $n$ , both $n(n+1)$ and $n(n-1)$ are products of two consecutive integers, so they are even. The floors therefore never discard a remainder. In the case $n = 0$ , the truncated subtraction gives $0 \cdot 0 = 0$ , which matches $0 \cdot (0-1) = 0$ in ordinary arithmetic. So the equation says the same as $\frac{n(n+1)}{2} + \frac{n(n-1)}{2} = n^2$ over the integers, for every $n \ge 0$ , including $n = 0$ , where both sides are $0$ .

The statement has no hypotheses and no other variables. It is a purely arithmetic identity about $n$ . It does not mention matrices, vector spaces, dimensions, or symmetric or antisymmetric objects; those words appear only in the declaration's name.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by ShapeZero · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

n(n+1)2+n(n−1)2=n2\tfrac{n(n+1)}{2} + \tfrac{n(n-1)}{2} = n^22n(n+1)​+2n(n−1)​=n2

$\tfrac{n(n+1)}{2} + \tfrac{n(n-1)}{2} = n^2$