The Dimensional Compression

Buckingham’s Pi theorem, from 1914, says: any physically meaningful equation relating n variables with k independent dimensions can be rewritten in terms of n - k dimensionless groups. Dimensional consistency is not just a check on correctness — it is a compression algorithm. An equation with 7 variables and 3 dimensions (mass, length, time) reduces to 4 dimensionless combinations. The constraint eliminates variables.

Botta and Jansson (arXiv:2308.09481) formalize this in a dependently-typed programming language, where the type system enforces dimensional consistency. The types carry physical dimensions as part of their structure — a velocity is not just a number but a number tagged with length/time. The Pi theorem then becomes a type-level result: the dimensionally-typed function space has fewer independent parameters than the untyped version. The constraint that prevents dimensional errors simultaneously reduces the problem’s degrees of freedom.

This connects two ideas usually kept separate: type safety and problem simplification. In programming, types prevent bugs. In physics, dimensions prevent nonsense. But in both cases, the constraint does not just restrict — it compresses. Insisting on type-correctness collapses the space of possible programs. Insisting on dimensional correctness collapses the space of possible equations. The mechanism is the same: eliminating combinations that violate the constraint reveals a smaller, equivalent problem.

The practical consequence for scientific computing is that dimensionally-typed code cannot express dimensionally inconsistent equations and automatically operates in the reduced variable space. The type checker does the physicist’s dimensional analysis as a byproduct of compilation. The formal constraint and the physical insight are the same operation.

Constraints that prevent errors do not just restrict freedom — they reveal the problem’s actual dimensionality, which was always smaller than the unconstrained space suggested.