ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The orthogonal group is a regular level set of dimension $n (n - 1) / 2$

Example

Let $n \geq 1$ . Identify $M_{n} (R)$ with $R^{n^{2}}$ entrywise, and identify the symmetric $n \times n$ real matrices with $R^{n (n + 1) / 2}$ by listing the entries in the positions $(i, j)$ with $i \leq j$ . Under these identifications let $f : M_{n} (R) \to {Sym}_{n} (R), f (A) = A^{T} A,$ so that $f$ is a map between Euclidean spaces of dimensions $n^{2}$ and $n (n + 1) / 2$ .

Then $f$ is $C^{\infty}$ , its derivative is $D f (A) H = A^{T} H + H^{T} A$ , and $I_{n}$ is a regular value of $f$ . Consequently $O (n) = {A \in M_{n} (R) : A^{T} A = I_{n}} = f^{- 1} (I_{n})$ is a regular level set: near each of its points it is a $C^{\infty}$ graph of dimension $n^{2} - \frac{n (n + 1)}{2} = \frac{n (n - 1)}{2},$ and its tangent space at $A \in O (n)$ is $T_{A} O (n) = {A K : K \in M_{n} (R), K^{T} = - K},$ of dimension $n (n - 1) / 2$ .

At $n = 1$ the target dimension equals the source dimension, $O (1) = {1, - 1}$ , and the graph dimension is $0$ : the two points are isolated.

Facts & Assumptions

Given: A natural number $n \geq 1$ , the entrywise identifications above, and the map $f$ with components $f_{i j} (A) = \sum_{k < n} a_{k i} a_{k j}$ for $i \leq j$ .

[L1]

Each component $f_{i j}$ is a polynomial in the entries of $A$ , so its partial derivatives of every order exist and are again polynomials, hence continuous (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ). A map each of whose components is $C^{k}$ for every $k$ is $C^{\infty}$ ( $C^{k}$ Euclidean maps and diffeomorphisms), and a map whose partial derivatives exist near a point and are continuous there is totally differentiable there (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

[L2]

If $f$ is totally differentiable at $A$ , then the directional derivative $D_{H} f (A)$ exists for every $H$ and equals $D f (A) H$ (A total derivative computes every directional derivative, and its matrix is the Jacobian).

[L3]

A $C^{1}$ map is a submersion at a point when its derivative there is surjective, and a value is regular when every point of its fibre is a submersion point (Submersions and immersions between Euclidean open sets, Regular and critical points, regular and critical values, and level sets).

[L4]

Near each of its points a regular level set of a $C^{k}$ map $U \subseteq R^{m} \to R^{N}$ is a $C^{k}$ graph of dimension $m - N$ , and its tangent space at such a point is the kernel of the derivative (A regular level set is locally a $C^{k}$ graph of dimension $m - n$ , The tangent space to a regular level set).

[L5]

A linear map is injective exactly when its kernel is trivial, and for a linear map on a finite-dimensional space the dimension of the space is the sum of the dimensions of the kernel and the image (The kernel and image are linear subspaces, and a linear map is injective if and only if its kernel is trivial, Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

Verification

technique · direct

1.1givenL1

By [L1], $f$ is $C^{\infty}$ and totally differentiable at every $A$ .

1.2givenL5algebra

Let $A \in f^{- 1} (I_{n})$ , so $A^{T} A = I_{n}$ . If $A x = 0$ then $x = I_{n} x = A^{T} A x = 0$ , so by [L5] the map $x \mapsto A x$ is injective and therefore, its kernel being trivial, surjective on $R^{n}$ ; hence $A$ is invertible and $A^{- 1} = A^{T}$ , so also $A A^{T} = I_{n}$ .

2.1step 1.1givenL2algebra

Fix $A, H \in M_{n} (R)$ . Then $(A + t H)^{T} (A + t H) = A^{T} A + t (A^{T} H + H^{T} A) + t^{2} H^{T} H$ , a polynomial in $t$ with matrix coefficients, so its derivative at $t = 0$ is $A^{T} H + H^{T} A$ . By [L2] this directional derivative is $D f (A) H$ , so $D f (A) H = A^{T} H + H^{T} A$ . This matrix is symmetric, as the target requires.

3.1step 2.1step 1.2algebra

Let $S$ be symmetric and put $H = \frac{1}{2} A S$ . Then $A^{T} H = \frac{1}{2} A^{T} A S = \frac{1}{2} S$ , and $H^{T} = \frac{1}{2} S A^{T}$ gives $H^{T} A = \frac{1}{2} S A^{T} A = \frac{1}{2} S$ . By step 2.1, $D f (A) H = S$ , so $D f (A)$ is surjective onto ${Sym}_{n} (R)$ .

4.1step 3.1L3

By [L3], every point of $f^{- 1} (I_{n})$ is a submersion point, so $I_{n}$ is a regular value and $f^{- 1} (I_{n}) = O (n)$ is a regular level set.

5.1step 4.1L4algebra

By [L4] with $m = n^{2}$ and $N = n (n + 1) / 2$ , near each of its points $O (n)$ is a $C^{\infty}$ graph of dimension $n^{2} - n (n + 1) / 2 = n (n - 1) / 2$ , and $T_{A} O (n) = \ker D f (A) = {H : A^{T} H + H^{T} A = 0}$ .

6.1step 5.1step 1.2algebra

If $K^{T} = - K$ and $H = A K$ , then by step 1.2 $A^{T} H = K$ and $H^{T} A = K^{T} A^{T} A = K^{T} = - K$ , so $H \in \ker D f (A)$ . Conversely, if $A^{T} H + H^{T} A = 0$ , put $K = A^{T} H$ ; then $K^{T} = H^{T} A = - K$ and $A K = A A^{T} H = H$ by step 1.2. Hence $T_{A} O (n) = {A K : K^{T} = - K}$ .

7.1step 6.1step 1.2L5algebra

The map $K \mapsto A K$ is linear and injective, because $A$ is invertible by step 1.2, so by [L5] its image has the dimension of its domain. A skew-symmetric matrix is determined freely by its entries strictly above the diagonal and has zero diagonal, so the skew-symmetric matrices have dimension $n (n - 1) / 2$ , and $\dim T_{A} O (n) = n (n - 1) / 2$ .

8.1step 5.1step 7.1algebra∎

At $n = 1$ the source and target both have dimension $1$ , $f (a) = a^{2}$ , and $f^{- 1} (1) = {1, - 1}$ , on which $f^{'} (a) = 2 a \neq 0$ ; the graph dimension $n (n - 1) / 2$ is $0$ , so each point is isolated, and the skew-symmetric $1 \times 1$ matrices are ${0}$ , in agreement with step 7.1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

52 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

L. W. Tu, An Introduction to Manifolds, Example 11.3 (the orthogonal group) (standard reference, not scraped)
J. M. Lee, Introduction to Smooth Manifolds, Section 8 (standard reference, not scraped)

The orthogonal group is a regular level set of dimension n(n−1)/2n(n−1)/2