The Pi theorem

Kennedy's Pi theorem (POPL 1997, Theorem 3): when A X = b is solvable over ℤ, a first-order unit-polymorphic type is isomorphic, for positive values, to one with n − r dimensionless arguments, where r is the rank of the exponent matrix. His WMM 2008 slides list formalizing its proof as work in progress.

This module mechanizes equivalences with scale-invariant functions on n arguments (piEquiv, piEquivSigned), including both inverse laws. It separately reduces those invariants to n − rank A orbit coordinates (invariant_descends). The equivalences themselves do not have reduced-coordinate functions as their codomains. The paper's Pi theorem (Theorem 8.1), for programs with conversion, is den_pi_coherent_dichotomy in LambdaS.PiCoherent.

The route taken

Kennedy proves it by reducing the exponent matrix through a sequence of syntactic type isomorphisms: column operations C1–C3, row operations R1–R3, then r instances of an elimination isomorphism D. That route needs the isomorphism witnesses to be terms, hence a term-level rational power x^q, hence positivity.

This file takes the semantic route instead. The fundamental theorem (fundamental_free) already gives every parametric convert-free term an unrestricted scaling law. Working directly from that law (in logarithmic coordinates, where the scaling action is a translation), the theorem becomes a statement in linear algebra and no term witnesses are needed.

Concretely, in log coordinates ξ = log x the action of a scaling ψ is ξ ↦ ξ + Aᵀψ, and the scaling law reads F(ξ + Aᵀψ) = F(ξ) + ⟨b, ψ⟩. Given a solution X of A X = b (Kennedy's solvability hypothesis), subtracting the linear functional ⟨X, ·⟩ produces a function invariant under the entire action. That invariant function is exactly the "function of the dimensionless groups", and

f(x) = (∏ xᵢ^{Xᵢ}) · g(Π₁, …, Π_{n−r})

is Buckingham's conclusion.

Why ℚ helps

Kennedy's ℤ-exponent proof reduces the matrix to Smith normal form. Here the orbit subspace is range Aᵀ over a field, its dimension is rank A, and invariant_descends obtains n − r coordinates from a rational basis of the kernel, using linear extension with values in ℝ to separate the orbits. The coordinate count is rank-nullity (Mathlib's).

Dimensional Analysis

The abstraction theorems of “The Price of Conversion” (Fundamental.lean) have two further consequences, which the programmer never asks for but a numerical library wants: a non-definability theorem and the Pi theorem of dimensional analysis.

First, non-definability. For any nontrivial u (u ≠ 1: some base or variable exponent nonzero), no term of Λs built from variables, rational literals, and the field operations computes square root at type Q u² → Q u (sqrt_not_definable_tm), so the powers of “The Calculus” (Typing.lean) must be primitive. (The full calculus does inhabit the type, by naming a unit, λ x. 1_u; the Newton paragraph below prices that seed.) Note that the scaling law alone cannot deliver this. Applied to a hypothetical f : Q u² → Q u, the convert-free abstraction theorem (fundamental_free) gives f(k² x) = k · f(x), an equation square root satisfies; parametricity says that any such f is a constant multiple of square root, not that none exists. What excludes the function is a span argument on the syntax. From an argument at u² and dimensionless literals, closure under the field operations reaches exactly the integer powers of u²: multiplication and division add and subtract exponent vectors, so the reachable units form the ℤ-span of the argument's unit, and u = (u²)^(1/2) requires the ℚ-span. For such u, the type Q u² → Q u is therefore uninhabited by arithmetic terms, a conclusion stronger than uncomputability (sqrt_not_definable, over a self-contained arithmetic grammar; arith_of_hasTy lifts the statement to the calculus's own typing derivations). The primitive is also a permitted one: powers are parametric, so the convert-free abstraction theorem (fundamental_free) covers them (sqrt_scales, instantiated at λ x. √x). Atkey et al. [2013] prove stronger results of this kind (cube root remains undefinable even given square root); we include ours because the exponent-vector representation makes it a two-line span argument, and because it justifies a constructor of Λs.

Recursion would not rescue definability. Newton's iteration x_(n+1) = (x_n + a/x_n)/2 is unit-correct at every step; what it lacks is the seed x₀ : Q u, and manufacturing one from a : Q u² is the non-definability theorem itself (no_newton_seed; at the term grammar, no_newton_seed_tm). The full calculus offers the seed 1_u, at a price the theory names: every finite run of the constant-seeded program depends on the unit system (an absolute tolerance written as a literal times 1_(u²) is not writable parametrically, though one supplied as an input is), while a seed passed as an argument rescales with everything else and restores parametricity wholesale. LambdaS.NonDefinability develops seeds, tolerances, and the unmechanized piecewise-rational argument that no recursive program computes square root exactly. Its content is that the square root cannot be computed: what the power primitive buys is exactness, a denotation that commutes with rescaling.

Second, the Pi theorem, which we motivate with its classical example before stating it. What determines the period of a pendulum? List everything the period could plausibly depend on: the mass m of the bob, the length ℓ of the arm, the gravitational acceleration g, and the release amplitude θ, so that T = f(m, ℓ, g, θ) for some unknown f. Dimensional analysis extracts the form of f from the units alone, before any mechanics. Record the exponents of each argument's unit over the base units of mass, length, and time as the columns of a matrix A (g is an acceleration, at L/T²; the amplitude is an angle, dimensionless, hence a zero column):

	m	ℓ	g	θ
M	1	0	0	0
L	0	1	1	0
T	0	0	-2	0

The matrix has rank 3, so the dimensionless power products m^c₁ℓ^c₂g^c₃θ^c₄ of the arguments, whose exponent vectors form the kernel of A, make up a space of dimension 4 - 3 = 1; solving Ac = 0 forces c₁ = c₂ = c₃ = 0 and leaves c₄ free, so the amplitude is the only dimensionless combination of the arguments. The output T has exponent vector b = (0, 0, 1), and AX = b has the solution X = (0, 1/2, -1/2, 0): the power product ℓ^(1/2) g^(-1/2) = √(ℓ/g). The Pi theorem says that these two computations determine f up to one unknown function of one variable:

T  =  √(ℓ/g) · G(θ).

Equivalently, the ratio T√(g/ℓ) is the problem's single dimensionless invariant. Note what the mass row has already decided: mass occurs in exactly one argument and not in the output, so every solution of AX = b has zero in the mass coordinate, and so does every kernel vector; f cannot depend on the bob's mass. The period's independence from mass, a fact usually credited to the mechanics, follows from the type of f. Mechanics contributes only the function G, with G(θ) → 2π in the small-amplitude limit.

The general statement is the scaling law of the convert-free abstraction theorem (fundamental_free) handed to linear algebra, and the artifact carries the handoff as theorems. For a first-order program (n scalar arguments, one scalar result), instantiating the scaling law at every rescaling of the unit symbols in scope, base units and unit variables alike, says that multiplying each argument by its unit's power product of factors multiplies the result by its own (den_mulScaleLaw). The program's dependence on the unit system is then governed by the exponent matrix A (one row per unit symbol, one column per argument) together with the output's exponent vector b; we call the pair (A, b) the program's signature. Taking logarithms turns the multiplicative action into translation (scaleLaw_of_mulScaleLaw); the logarithm of the output needs positivity, but the positivity belongs to that presentation, not to the theorem, and the factorization below is stated without it. The invariance theory becomes linear algebra: the invariants of the translation action are exactly the dimensionless power products of the arguments, a space of dimension n - rank A, and every function obeying the scaling law factors through them.

Theorem (Pi, for a signature; pi_theorem). Let (A, b) be a signature whose output's exponents are solvable from the arguments (AX = b for some X). A function obeying its scaling law factors as an explicit power product times a function invariant under every rescaling; the invariant monomials form a space of dimension n - rank A, and the factorization is an equivalence.

The artifact states the clauses separately: invariant_iff_dimensionless characterizes the invariant monomials, pi_count counts them, mulScaleLaw_factorization gives the factorization in multiplicative coordinates with an invariant factor of arbitrary sign (the zero function is the factorization at H = 0), and piEquiv with piEquivSigned package the equivalences, in additive and in signed multiplicative form. Solvability of AX = b is half of a dichotomy (mulScaleLaw_dichotomy): when no X solves it, some combination of rescalings fixes every argument while moving the output, so the only function obeying the scaling law is identically zero (mulScaleLaw_eq_zero_of_unsolvable; its single-base-unit case over scalar environments is scaleLaw_forces_zero). An unsolvable signature is dimensional inconsistency.

For the pendulum, the power product is √(ℓ/g), the invariant space is spanned by the amplitude, and the factorization is the displayed equation above. The artifact runs this instance: pendulum is the 3 × 4 matrix above, with output exponents (0, 0, 1) and the exhibited solution (0, 1/2, -1/2, 0) (pendulum_period_solution), and the mass conclusion follows (pendulum_mass_absent): a base unit occurring in exactly one argument and absent from the output forces that argument's exponent to zero in every solution (solution_eq_zero_of_appears_once) and in every invariant (eq_zero_of_appears_once). Note also what the theorem offers a programmer: it bounds what any unit-polymorphic first-order function can depend on, an interface-narrowing result that costs nothing. Whatever a function of the pendulum's signature computes, it can depend on its four arguments only through √(ℓ/g) and θ.

The counting is Buckingham's [1914], in the modern rank formulation, obtained here as a corollary of parametricity, as Kennedy [1997] showed on paper. Atkey et al. [2013] derive a one-variable instance; their Coq development states the instance ∀s. real⟨s⟩ → real⟨s⟩ ≅ real⟨1⟩ in a comment, with its proof unfinished. Ours is the general n-variable statement with the rank condition, mechanized and connected to the calculus; we claim the mechanization, not the mathematics. The unit-level statement's standing hypotheses are those of the convert-free abstraction theorem (fundamental_free): the program must be parametric (no unit constants) and convert-free; solvability's failure is the dichotomy's other half, settled above. Neither syntactic hypothesis is redundant. A program that converts obeys the scaling law only for coherent rescalings, so it can fail the unit-level law, which quantifies over all rescalings; it still obeys the dimension-level law of LambdaS.PiCoherent. The drift analysis (Twist.lean) supplies a sharper unit-level hypothesis, drift-free rather than convert-free: den_mulScaleLaw_driftFree, below, reaches the same conclusion for a program whose conversions cancel, with no separate parametricity hypothesis because the analysis declines unit constants. It does not subsume the convert-free statement, since the two are incomparable: a drift-free program may convert, and a convert-free one may be declined by the analysis. Parametricity cannot be dropped even for convert-free terms: λ x. (x/1_u)·1_v is convert-free, denotes the identity at Q u → Q v, and violates the unrestricted law.

def LambdaS.Pi.act {m n : ℕ} (A : ExpMatrix m n) (ψ : Fin m → ℝ) (i : Fin n) : ℝ

The displacement a scaling induces on the log-arguments. In log coordinates the scaling action is translation by Aᵀψ.

Equations

• LambdaS.Pi.act A ψ i = ∑ v : Fin m, ↑(A v i) * ψ v

def LambdaS.Pi.ScaleLaw {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (F : (Fin n → ℝ) → ℝ) : Prop

The scaling law of a first-order signature, in log coordinates.

F is log ∘ f ∘ exp; rescaling the units translates the arguments and shifts the value by the output's own scale. This is what fundamental_free delivers for a parametric convert-free term, transported to logs; the transport needs a positive output (scaleLaw_of_mulScaleLaw).

Equations

• LambdaS.Pi.ScaleLaw A b F = ∀ (ψ : Fin m → ℝ) (ξ : Fin n → ℝ), (F fun (i : Fin n) => ξ i + LambdaS.Pi.act A ψ i) = F ξ + ∑ v : Fin m, ↑(b v) * ψ v

theorem LambdaS.Pi.sum_act_eq {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (X : Fin n → ℝ) (hX : ∀ (v : Fin m), ∑ i : Fin n, ↑(A v i) * X i = ↑(b v)) (ψ : Fin m → ℝ) : ∑ i : Fin n, X i * act A ψ i = ∑ v : Fin m, ↑(b v) * ψ v

The exchange identity at the heart of the reduction: a solution of A X = b turns the argument displacement into exactly the output shift.

This is where Kennedy's solvability hypothesis does its work.

theorem LambdaS.Pi.pi_theorem {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (X : Fin n → ℝ) (hX : ∀ (v : Fin m), ∑ i : Fin n, ↑(A v i) * X i = ↑(b v)) {F : (Fin n → ℝ) → ℝ} (hF : ScaleLaw A b F) : ∃ (G : (Fin n → ℝ) → ℝ), (∀ (ψ : Fin m → ℝ) (ξ : Fin n → ℝ), (G fun (i : Fin n) => ξ i + act A ψ i) = G ξ) ∧ ∀ (ξ : Fin n → ℝ), F ξ = ∑ i : Fin n, X i * ξ i + G ξ

The Pi theorem.

In log coordinates: given a solution X of A X = b, any function satisfying the scaling law is the linear functional ⟨X, ·⟩ plus a function that is invariant under every rescaling, hence a function of the dimensionless groups alone (invariant_descends), of which there are n − r.

In the original coordinates this reads f(x) = (∏ xᵢ^{Xᵢ}) · g(Π₁, …, Π_{n−r}), which is Buckingham's conclusion and Kennedy's isomorphism.

theorem LambdaS.Pi.invariant_iff_dimensionless {m n : ℕ} (A : ExpMatrix m n) (c : Fin n → ℝ) : (∀ (ψ : Fin m → ℝ), ∑ i : Fin n, c i * act A ψ i = 0) ↔ ∀ (v : Fin m), ∑ i : Fin n, ↑(A v i) * c i = 0

The invariants are exactly the dimensionless groups.

A monomial ∏ xᵢ^{cᵢ} (a linear functional ⟨c, ·⟩ in log coordinates) is invariant under every rescaling precisely when c lies in the kernel of the exponent matrix, which is Dimensionless A.

This characterizes linear invariants only. invariant_descends separately proves that every invariant function descends to coordinates in a rational basis of the kernel; finrank_dimensionless_add_rank gives their count.

theorem LambdaS.Pi.pi_count {m n : ℕ} (A : ExpMatrix m n) : Module.finrank ℚ ↥(Dimensionless A) + Matrix.rank A = n

The count. The dimensionless groups form a space of dimension n − r, and invariant_descends shows that every invariant is a function of that many coordinates (piCoordinates). Particular functions may ignore some or all of them.

Restated here from finrank_dimensionless_add_rank to keep the theorem's two halves (the factorization and the count) in one place.

The isomorphism

Kennedy states the theorem as a type isomorphism. Here it is, as an actual bijection: the functions satisfying a signature's scaling law correspond exactly to the scale-invariant functions, and the correspondence is adding and subtracting the power-product ∏ xᵢ^{Xᵢ}.

def LambdaS.Pi.Invariant {m n : ℕ} (A : ExpMatrix m n) (G : (Fin n → ℝ) → ℝ) : Prop

A function invariant under every rescaling: a function of the dimensionless groups alone, as invariant_descends proves below.

Equations

• LambdaS.Pi.Invariant A G = ∀ (ψ : Fin m → ℝ) (ξ : Fin n → ℝ), (G fun (i : Fin n) => ξ i + LambdaS.Pi.act A ψ i) = G ξ

Descent to finitely many dimensionless coordinates

noncomputable def LambdaS.Pi.dimensionlessBasis {m n : ℕ} (A : ExpMatrix m n) : Module.Basis (Fin (n - Matrix.rank A)) ℚ ↥(Dimensionless A)

A rational basis of the dimensionless power products, indexed by the Buckingham count. Choosing it is noncomputable; each exponent is rational.

Equations

• LambdaS.Pi.dimensionlessBasis A = Module.finBasisOfFinrankEq ℚ ↥(LambdaS.Pi.Dimensionless A) ⋯

noncomputable def LambdaS.Pi.piCoordinates {m n : ℕ} (A : ExpMatrix m n) (ξ : Fin n → ℝ) (j : Fin (n - Matrix.rank A)) : ℝ

The logarithms of the independent dimensionless power products.

Equations

• LambdaS.Pi.piCoordinates A ξ j = ∑ i : Fin n, ↑(↑((LambdaS.Pi.dimensionlessBasis A) j) i) * ξ i

theorem LambdaS.Pi.exists_act_of_annihilates {m n : ℕ} (A : ExpMatrix m n) (δ : Fin n → ℝ) (hδ : ∀ (c : ↥(Dimensionless A)), ∑ i : Fin n, ↑(↑c i) * δ i = 0) : ∃ (ψ : Fin m → ℝ), act A ψ = δ

If a real vector annihilates every rational dependency among the columns, it is an orbit displacement. Rational linear extension with real values avoids any appeal to an unproved scalar-extension identity for kernels.

theorem LambdaS.Pi.exists_act_of_piCoordinates_eq {m n : ℕ} (A : ExpMatrix m n) {ξ η : Fin n → ℝ} (h : piCoordinates A ξ = piCoordinates A η) : ∃ (ψ : Fin m → ℝ), (fun (i : Fin n) => η i + act A ψ i) = ξ

The independent dimensionless coordinates separate scaling orbits.

theorem LambdaS.Pi.invariant_descends {m n : ℕ} (A : ExpMatrix m n) {H : (Fin n → ℝ) → ℝ} (hH : Invariant A H) : ∃ (G : (Fin (n - Matrix.rank A) → ℝ) → ℝ), ∀ (ξ : Fin n → ℝ), H ξ = G (piCoordinates A ξ)

Arity descent. Every arbitrary (not necessarily linear or continuous) invariant is a function of n - rank A rational dimensionless power products, in logarithmic coordinates. This supplies the descent missing from the invariant-factor theorem alone.

theorem LambdaS.Pi.scaleLaw_add_linear {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (X : Fin n → ℝ) (hX : ∀ (v : Fin m), ∑ i : Fin n, ↑(A v i) * X i = ↑(b v)) {G : (Fin n → ℝ) → ℝ} (hG : Invariant A G) : ScaleLaw A b fun (ξ : Fin n → ℝ) => ∑ i : Fin n, X i * ξ i + G ξ

Adding the power-product back turns an invariant function into one obeying the scaling law. The inverse direction of pi_theorem.

noncomputable def LambdaS.Pi.piEquiv {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (X : Fin n → ℝ) (hX : ∀ (v : Fin m), ∑ i : Fin n, ↑(A v i) * X i = ↑(b v)) : { F : (Fin n → ℝ) → ℝ // ScaleLaw A b F } ≃ { G : (Fin n → ℝ) → ℝ // Invariant A G }

Kennedy's isomorphism, as a bijection.

Functions obeying the scaling law of the signature (A, b) are in bijection with scale-invariant functions. The separate invariant_descends theorem expresses each invariant in n − r rational dimensionless coordinates; this equivalence itself retains the invariant-function subtype as its codomain.

Equations

• One or more equations did not get rendered due to their size.

The multiplicative bridge

ScaleLaw lives in log coordinates. The law the calculus itself delivers (scaleLaw in LambdaS.Fundamental) is multiplicative: rescaling each argument by the scale factor of its unit multiplies the result by the scale factor of the result unit. This section states that multiplicative law as a predicate on functions and factors any function satisfying it, on the positive orthant, as the power product ∏ xᵢ^{Xᵢ} times an invariant function of the log magnitudes.

No positivity of the function is assumed anywhere in the factorization: only the arguments pass through exp and log, and the invariant factor carries whatever sign the function has (the zero function is carried by the zero invariant). Positivity enters only in scaleLaw_of_mulScaleLaw below, which additionally takes the logarithm of the output to present the law additively; that is a presentation choice, not a hypothesis of the theorem.

def LambdaS.Pi.MulScaleLaw {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (f : (Fin n → ℝ) → ℝ) : Prop

The multiplicative scale law. Scaling each row symbol v (a base unit, unit variable, or dimension) by a positive factor κ v scales argument i by ∏ v, κ v ^ A v i and the result by ∏ v, κ v ^ b v. This is the form of the scaling law a Λs term actually satisfies (den_mulScaleLaw below); ScaleLaw is its image in log coordinates. Exponents are rational, so the powers are Real.rpow under a cast.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LambdaS.Pi.logConj {n : ℕ} (f : (Fin n → ℝ) → ℝ) (ξ : Fin n → ℝ) : ℝ

The log conjugate log ∘ f ∘ exp of a function on magnitudes. This is the F that ScaleLaw and pi_theorem speak about, produced from the multiplicative function the calculus provides.

Equations

• LambdaS.Pi.logConj f ξ = Real.log (f fun (i : Fin n) => Real.exp (ξ i))

theorem LambdaS.Pi.prod_exp_rpow {m : ℕ} (ψ : Fin m → ℝ) (c : Fin m → ℚ) : ∏ v : Fin m, Real.exp (ψ v) ^ ↑(c v) = Real.exp (∑ v : Fin m, ↑(c v) * ψ v)

A product of real powers of exponentials is the exponential of a dot product. The computation that carries the multiplicative law into log coordinates and back.

def LambdaS.Pi.ExpScaleLaw {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (g : (Fin n → ℝ) → ℝ) : Prop

The scale law in exponential coordinates. The multiplicative law transported to log coordinates on the arguments only: the output is scaled, not logged, so the predicate makes sense for functions of any sign. This is the signed carrier of the Pi reduction; ScaleLaw is its image under a further logarithm on the values, available only for positive functions.

Equations

• LambdaS.Pi.ExpScaleLaw A b g = ∀ (ψ : Fin m → ℝ) (ξ : Fin n → ℝ), (g fun (i : Fin n) => ξ i + LambdaS.Pi.act A ψ i) = Real.exp (∑ v : Fin m, ↑(b v) * ψ v) * g ξ

theorem LambdaS.Pi.sum_act_shift {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (X : Fin n → ℝ) (hX : ∀ (v : Fin m), ∑ i : Fin n, ↑(A v i) * X i = ↑(b v)) (ψ : Fin m → ℝ) (ξ : Fin n → ℝ) : ∑ i : Fin n, X i * (ξ i + act A ψ i) = ∑ i : Fin n, X i * ξ i + ∑ v : Fin m, ↑(b v) * ψ v

The displacement of the linear functional ⟨X, ·⟩ along the scaling action is exactly the output shift: sum_act_eq packaged with the splitting of the sum, since every use below needs the two together.

theorem LambdaS.Pi.expScaleLaw_of_mulScaleLaw {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) {f : (Fin n → ℝ) → ℝ} (hmul : MulScaleLaw A b f) : ExpScaleLaw A b fun (ξ : Fin n → ℝ) => f fun (i : Fin n) => Real.exp (ξ i)

A function satisfying the multiplicative law, precomposed with exp, satisfies the exponential-coordinates law. No hypothesis on the function beyond the law itself: the exponentials are all on the argument side.

noncomputable def LambdaS.Pi.piEquivSigned {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (X : Fin n → ℝ) (hX : ∀ (v : Fin m), ∑ i : Fin n, ↑(A v i) * X i = ↑(b v)) : { g : (Fin n → ℝ) → ℝ // ExpScaleLaw A b g } ≃ { H : (Fin n → ℝ) → ℝ // Invariant A H }

Kennedy's isomorphism at the multiplicative level. Functions obeying the exponential-coordinates scale law of the signature (A, b) are in bijection with the scale-invariant functions, of any sign: the correspondence multiplies and divides by the exponential of the linear functional ⟨X, ·⟩, which is the power product ∏ xᵢ^{Xᵢ} in the original coordinates. The additive piEquiv is the same bijection read after a further logarithm on the values, which is where positivity would enter and why it is not needed here.

Equations

• One or more equations did not get rendered due to their size.

theorem LambdaS.Pi.mulScaleLaw_factorization {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (X : Fin n → ℝ) (hX : ∀ (v : Fin m), ∑ i : Fin n, ↑(A v i) * X i = ↑(b v)) {f : (Fin n → ℝ) → ℝ} (hmul : MulScaleLaw A b f) : ∃ (H : (Fin n → ℝ) → ℝ), Invariant A H ∧ ∀ (x : Fin n → ℝ), (∀ (i : Fin n), 0 < x i) → f x = (∏ i : Fin n, x i ^ X i) * H fun (i : Fin n) => Real.log (x i)

Buckingham's factorization for multiplicative data, signed. A function satisfying the multiplicative scale law factors, on the positive orthant, as the power product ∏ i, x i ^ X i times a function of the log magnitudes that is invariant under every rescaling, hence a function of the dimensionless groups alone (invariant_descends). The explicit reduced-arity statement is mulScaleLaw_factorization_reduced.

No positivity of f is assumed and none survives in the conclusion: H is real-valued of whatever sign f takes, and the zero function is carried by H = 0. The factorization needs only the solvability witness X; when the system is unsolvable there is nothing to factor, because f is forced to vanish (mulScaleLaw_eq_zero_of_unsolvable).

theorem LambdaS.Pi.mulScaleLaw_factorization_reduced {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (X : Fin n → ℝ) (hX : ∀ (v : Fin m), ∑ i : Fin n, ↑(A v i) * X i = ↑(b v)) {f : (Fin n → ℝ) → ℝ} (hmul : MulScaleLaw A b f) : ∃ (G : (Fin (n - Matrix.rank A) → ℝ) → ℝ), ∀ (x : Fin n → ℝ), (∀ (i : Fin n), 0 < x i) → f x = (∏ i : Fin n, x i ^ X i) * G (piCoordinates A fun (i : Fin n) => Real.log (x i))

Buckingham factorization with the reduced arity. On positive inputs, a function of arbitrary output sign satisfying the multiplicative scaling law is a power product times a function of n - rank A rational dimensionless combinations. piCoordinates A (log x) lists their logarithms.

The solvability dichotomy

Kennedy's hypothesis that A X = b be solvable is not bookkeeping either, but its failure mode is total collapse rather than a missing factorization: an unsolvable signature admits only the zero function. Unsolvability over ℝ means b is separated from the column space of A by a linear functional; instantiating the multiplicative law along the one-parameter family of scalings in that functional's direction leaves every argument fixed while multiplying the output by a nonconstant factor, which forces the value to zero. Everywhere, not just on the positive orthant: the law itself quantifies over all argument vectors.

theorem LambdaS.Pi.exists_act_annihilator_of_unsolvable {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (hb : ¬∃ (X : Fin n → ℝ), ∀ (v : Fin m), ∑ i : Fin n, ↑(A v i) * X i = ↑(b v)) : ∃ (ψ : Fin m → ℝ), (∀ (i : Fin n), act A ψ i = 0) ∧ ∑ v : Fin m, ↑(b v) * ψ v ≠ 0

Unsolvability is witnessed by an annihilator. If A X = b has no real solution, some direction ψ annihilates every column of A (so the induced scaling moves no argument) while pairing nontrivially with b (so it moves the output). The linear geometry behind the dichotomy: b outside the column space of A is separated from it by a dual functional, and a functional on Fin m → ℝ is again a vector.

theorem LambdaS.Pi.mulScaleLaw_eq_zero_of_unsolvable {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (hb : ¬∃ (X : Fin n → ℝ), ∀ (v : Fin m), ∑ i : Fin n, ↑(A v i) * X i = ↑(b v)) {f : (Fin n → ℝ) → ℝ} (hmul : MulScaleLaw A b f) (x : Fin n → ℝ) : f x = 0

Unsolvable signatures force zero. When A X = b has no real solution, the only function satisfying the multiplicative scale law is the zero function, on the whole space. The scaling built from the annihilator fixes every argument pointwise while scaling the output by a factor other than 1, and the only value that survives is 0.

scaleLaw_forces_zero in LambdaS.Definability is the single-base-unit special case of this collapse, stated over scalar environments (forced_zero is its form for terms): there the result unit mentions a base unit no argument mentions, so the row of that base unit is zero in the matrix while its entry in b is not, and the annihilator is the coordinate direction itself.

theorem LambdaS.Pi.mulScaleLaw_dichotomy {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) {f : (Fin n → ℝ) → ℝ} (hmul : MulScaleLaw A b f) : (∃ (X : Fin n → ℝ), (∀ (v : Fin m), ∑ i : Fin n, ↑(A v i) * X i = ↑(b v)) ∧ ∃ (H : (Fin n → ℝ) → ℝ), Invariant A H ∧ ∀ (x : Fin n → ℝ), (∀ (i : Fin n), 0 < x i) → f x = (∏ i : Fin n, x i ^ X i) * H fun (i : Fin n) => Real.log (x i)) ∨ ∀ (x : Fin n → ℝ), f x = 0

The dichotomy. A signature either admits a solution of A X = b, and then every function satisfying its multiplicative law factors through the dimensionless groups with the solution as exponent vector, or it admits none, and then the zero function is the only one satisfying the law. There is no third case: Kennedy's solvability hypothesis is not a gap in the theorem but the boundary between factorization and collapse.

The additive presentation

theorem LambdaS.Pi.scaleLaw_of_mulScaleLaw {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) {f : (Fin n → ℝ) → ℝ} (hmul : MulScaleLaw A b f) (hpos : ∀ (x : Fin n → ℝ), (∀ (i : Fin n), 0 < x i) → 0 < f x) : ScaleLaw A b (logConj f)

The additive presentation of the bridge. A function satisfying the multiplicative scale law and positive on positive inputs has a log conjugate satisfying the additive ScaleLaw with the same exponent matrix and result vector, which is the form pi_theorem and piEquiv consume.

Positivity is a presentation choice, not a hypothesis of the factorization: mulScaleLaw_factorization needs no sign information, because it exponentiates only the arguments. Only this statement, which also takes the logarithm of the output, must know the output is in the logarithm's domain. The zero function shows the hypothesis cannot be dropped from this presentation: it satisfies every multiplicative law, and its log conjugate is the constant log 0 = 0, which satisfies ScaleLaw A b only when b = 0.

theorem LambdaS.Pi.mulScaleLaw_factorization_pos {m n : ℕ} (A : ExpMatrix m n) (b : Fin m → ℚ) (X : Fin n → ℝ) (hX : ∀ (v : Fin m), ∑ i : Fin n, ↑(A v i) * X i = ↑(b v)) {f : (Fin n → ℝ) → ℝ} (hmul : MulScaleLaw A b f) (hpos : ∀ (x : Fin n → ℝ), (∀ (i : Fin n), 0 < x i) → 0 < f x) : ∃ (G : (Fin n → ℝ) → ℝ), Invariant A G ∧ ∀ (x : Fin n → ℝ), (∀ (i : Fin n), 0 < x i) → f x = (∏ i : Fin n, x i ^ X i) * Real.exp (G fun (i : Fin n) => Real.log (x i))

The positive corollary of mulScaleLaw_factorization: when f is positive on positive inputs, the invariant factor is positive everywhere and can be written as an exponential, recovering the classical form f(x) = (∏ xᵢ^{Xᵢ}) · exp(G(log x)). Derived from the signed factorization rather than proved separately: positivity only repackages H as Real.exp ∘ G.

From terms to the multiplicative law

The last gap: scaleLaw in LambdaS.Fundamental speaks about environments and Scalings, while MulScaleLaw speaks about vectors of magnitudes and a matrix of exponents. This section closes it. For a first-order term over n scalar arguments, the denotation as a function of the argument magnitudes satisfies MulScaleLaw with the matrix whose column i collects the exponents of argument i's unit and the vector of the result unit's exponents. The row index runs over every rescalable symbol in scope, base units and unit variables alike, enumerated by an equivalence Fin m ≃ B ⊕ Fin k: a Scaling B k carries an independent factor for each, and scaleLaw quantifies over all of them, so the exponent matrix must have a row for each or the bridge would silently restrict the scaling group.

def LambdaS.Pi.envOf {B D : Type} {j k : ℕ} (us : List (UExp B k)) : (Fin us.length → ℝ) → Env (scalarCtx us)

The environment of a first-order scalar signature, assembled from a vector of argument magnitudes. Inverse to reading the magnitudes off the environment.

Equations

• LambdaS.Pi.envOf [] x_2 = PUnit.unit
• LambdaS.Pi.envOf (head :: us) x_2 = (x_2 0, LambdaS.Pi.envOf us fun (i : Fin us.length) => x_2 i.succ)

theorem LambdaS.Pi.scaleEnv_envOf {B D : Type} [Fintype B] {j k : ℕ} (ψ : Scaling B k) (us : List (UExp B k)) (x : Fin us.length → ℝ) : scaleEnv ψ us (envOf us x) = envOf us fun (i : Fin us.length) => ψ.scale (us.get i) * x i

Rescaling the environment of a scalar signature is rescaling each magnitude by the scale factor of its unit. Connects scaleEnv, which walks the context, to the componentwise scaling MulScaleLaw quantifies over.

noncomputable def LambdaS.Pi.scalingOfFactors {m : ℕ} {B : Type} {k : ℕ} (e : Fin m ≃ B ⊕ Fin k) (κ : Fin m → ℝ) : Scaling B k

The scaling whose factors are a given vector of positive reals, read through an enumeration of the base units and the unit variables in scope. The witness that instantiates scaleLaw at the scalings MulScaleLaw quantifies over: one independent factor for every symbol a scaling can move.

Equations

• LambdaS.Pi.scalingOfFactors e κ = { base := fun (b : B) => Real.log (κ (e.symm (Sum.inl b))), vars := fun (i : Fin k) => Real.log (κ (e.symm (Sum.inr i))) }

theorem LambdaS.Pi.scale_scalingOfFactors {m : ℕ} {B : Type} [Fintype B] {k : ℕ} (e : Fin m ≃ B ⊕ Fin k) (κ : Fin m → ℝ) (hκ : ∀ (v : Fin m), 0 < κ v) (u : UExp B k) : (scalingOfFactors e κ).scale u = ∏ v : Fin m, κ v ^ ↑(Sum.elim u.base u.vars (e v))

The scale factor of scalingOfFactors e κ on a unit is the power product of the factors against the unit's full exponent vector, base and variable exponents both. Positivity of the factors is required: scale exponentiates the logs of κ, and log collapses nonpositive inputs.

theorem LambdaS.Pi.den_mulScaleLaw {B D : Type} [Fintype B] [UnitSys B D] {j k m : ℕ} {Δ : DCtx D j k} {e : Tm B D j k} {us : List (UExp B k)} {u₀ : UExp B k} (d : HasTy Δ (scalarCtx us) e (Ty.Q u₀)) (hp : e.Parametric) (hf : e.ConvertFree) (V : Scaling B k) (eqv : Fin m ≃ B ⊕ Fin k) : MulScaleLaw (Matrix.of fun (v : Fin m) (i : Fin us.length) => Sum.elim (us.get i).base (us.get i).vars (eqv v)) (fun (v : Fin m) => Sum.elim u₀.base u₀.vars (eqv v)) fun (x : Fin us.length → ℝ) => den V d (envOf us x)

The term-level multiplicative scale law. The denotation of a first-order parametric convert-free term, as a function of its argument magnitudes, satisfies MulScaleLaw for the matrix of its arguments' exponents and the vector of its result unit's exponents, with one row for every rescalable symbol in scope: base units and unit variables alike, enumerated by Fin m ≃ B ⊕ Fin k.

Together with mulScaleLaw_factorization this closes the chain from a well-typed Λs term to Buckingham's factorization on positive inputs, with no sign restriction on the output. The term supplies the multiplicative law, and the factorization is signed. mulScaleLaw_dichotomy adds the other half: a signature whose system is unsolvable forces the denotation to vanish.

The law quantifies over the full scaling group of the signature: a rescaling may move base units and unit variables independently, which is exactly the freedom scaleLaw itself provides. In closed unit scope (k = 0) the Fin k summand is empty and the matrix is the base-unit matrix.

theorem LambdaS.Pi.den_mulScaleLaw_driftFree {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} [DecidableEq B] {m : ℕ} {Δ : DCtx D j k} {e : Tm B D j k} {us : List (UExp B k)} {u₀ : UExp B k} {d : HasTy Δ (scalarCtx us) e (Ty.Q u₀)} (h1 : unitDrift d = some 1) (V : Scaling B k) (eqv : Fin m ≃ B ⊕ Fin k) : MulScaleLaw (Matrix.of fun (v : Fin m) (i : Fin us.length) => Sum.elim (us.get i).base (us.get i).vars (eqv v)) (fun (v : Fin m) => Sum.elim u₀.base u₀.vars (eqv v)) fun (x : Fin us.length → ℝ) => den V d (envOf us x)

The term-level multiplicative scale law, drift-free case. The same conclusion as den_mulScaleLaw with the convert-free hypothesis replaced by a drift diagnosis of 1: a program may convert as it likes, provided its conversions cancel (scaleLaw_of_driftFree). Parametricity is not assumed separately, because a unit constant is a ucon node and the drift analysis declines it. The two hypotheses are incomparable, so both theorems stay: (λx. λy. x + y) a b is convert-free but its drift is undetermined, since the two branches' ratios are atoms under distinct binders.

The pendulum, again

The mass conclusion, stated here so the full pipeline can see it, in both halves. The mass exponent is zero in every solution (Pi.pendulum_period_independent_of_mass), so the power product ∏ xᵢ^{Xᵢ} does not mention the mass; and it is zero in every dimensionless group (Pi.pendulum_mass_drops_out), so G cannot mention it either. The period is independent of the mass, and both factors of the factorization say so.

theorem LambdaS.Pi.pendulum_mass_absent : (∀ {X : Fin 4 → ℚ}, Matrix.mulVec pendulum X = ![0, 0, 1] → X 0 = 0) ∧ ∀ {x : Fin 4 → ℚ}, x ∈ Dimensionless pendulum → x 0 = 0

The pendulum's period does not depend on the mass. The mass exponent is zero in every solution of pendulum.mulVec X = ![0, 0, 1] and in every dimensionless group, so neither factor of the factorization mentions the mass.