The work develops a structure theory for Radon measures on parabolic space-time R^n x R with the parabolic distance. It extends the Euclidean rectifiable Reifenberg and square-function characterizations of rectifiability (Edelen–Naber–Valtorta, Azzam–Tolsa, David–Semmes) to the parabolic setting.

Parabolic Jones beta numbers measure distance to horizontal and vertical flat models, and their square functions are used to prove a parabolic rectifiable Reifenberg decomposition, qualitative and quantitative (corona-type) characterizations of regular parabolic rectifiability, and sharp results for L^p beta numbers. All stated results are proved in Lean 4 with Mathlib, with LLMs writing the Lean code under the author's direction. A Mathlib-only specification file restates the results with sorry'd proofs. Comparator checks that the library proves exactly these statements, replaying proofs in Lean's kernel and in the independent nanoda checker.

Regular parabolic rectifiability is characterized by finiteness of the square function together with density conditions, and measures decompose canonically into horizontal, vertical and purely unrectifiable parts. Only p=2 gives a characterization among L^p beta numbers. The formalization has 957 modules, about 176,000 lines and 14,534 declarations, covers 104 results, and uses only the standard axioms.