Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01
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.

Sard on the infinitely flat critical stratum

Statement

Let n≥1 and r≥1, let U⊆Rm be open, and let f:U→Rn be Cr with rn≥m. Let

Cr:={x∈U:Dαf(x)=0 for every multi-index 1≤∣α∣≤r}.

If K⊆Cr is compact, then f(K) is null in Rn.

Facts & Assumptions

Given: Integers n,r≥1, a Cr map f:U→Rn with rn≥m, and a compact set K⊆Cr.

[L1]

The multivariable Taylor formula with Lagrange remainder expresses the order-r remainder using the order-r derivatives at points of the joining segment (Multivariable Taylor formula with a Lagrange remainder along a line segment).

[L2]

A continuous map on a compact metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[F1]

Euclidean nullity is proved by box covers of arbitrarily small total volume (Measure zero and content zero in Rm by countable and finite cube covers).

Proof

technique · direct
1.1F1givenchoosecases

If m=0, then K has at most one point and f(K) is finite, hence null in Rn by cubes of arbitrarily small side. Assume henceforth that m≥1. For each x∈K, choose nested closed cubes Qx⊆Q^x⊆U with x∈int⁡(Qx) and Q^x having Qx in its interior. Compactness gives finitely many inner cubes Q1,…,Qs whose interiors cover K. It suffices to prove that each f(K∩Qi) is null, because finite unions of Euclidean null sets are null directly from the cube-cover definition [F1].

2.1L1L2step 1.1algebra

Fix one pair Q⊆Q^, let KQ:=K∩Q, and let λ be the side length of Q. The finitely many order-r partial derivatives of the components of f are uniformly continuous on the compact cube Q^ by [L2]. Since they vanish at every x∈KQ, applying [L1] componentwise with degree r−1 shows that for every η>0 there is a single δ>0 such that ∣f(y)−f(x)∣≤η∥y−x∥r whenever x∈KQ, y∈Q, and ∥y−x∥<δ.

3.1step 2.1choosealgebra

Fix ε>0. If rn=m, choose η>0 so small that (2η)nmrn/2λrn<ε; if rn>m, choose any η>0. Let δ be furnished by step 2.1, and choose N so large that the congruent subcubes in the subdivision of Q into Nm cubes have diameter below δ. Use the following target cubes. [step 2.1, choose, cases] For each subcube Qν meeting KQ, choose a point xν∈KQ∩Qν. If y∈KQ∩Qν, then ∥y−xν∥≤m λ/N, so step 2.1 gives ∣f(y)−f(xν)∣≤η(m λN)r. Hence f(KQ∩Qν) lies in an n-cube of side length at most 2η(m λN)r.

4.1F1step 3.1casesalgebra

The union of those target cubes covers f(KQ), and its total n-volume has the following bound. [F1, step 3.1, cases, algebra] It is at most Nm(2η(m λN)r)n=(2η)nmrn/2λrnNm−rn. If rn>m, increase N until this quantity is below ε; if rn=m, the choice of η in step 3.1 already makes it smaller than ε. In either case the total covering volume is below ε. Therefore [F1] implies that f(KQ) is null.

5.1F1step 1.1step 4.1∎

Applying step 4.1 to the finite cover from step 1.1 shows that f(K) is null. Thus the infinitely flat critical stratum has null image.

Depends on

Used by

Dependency tree · two levels

24 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