Accumulated conversion ratios, over first-order syntax

LambdaS.Definability proves that a single conversion is detectable, and that a term whose conversions are all inert is invariant under every scaling. Between those lies the general question: a term may convert many times, and what matters is whether the conversions cancel.

Twist assigns a term its accumulated ratio, an element of Tw, the first-order ratio syntax of LambdaS.Ratio. Multiplication multiplies ratios, division divides them, addition forces its branches to agree, and convert u v contributes u/v. Abstraction binds a ratio variable and application applies one, which is what carries the analysis past first order.

Ratio variables enter in one place only: at a lam binder, whose future argument may carry any ratio. The free variables of the program itself are measurements, and the certified theorems only ever instantiate their ratios at 1 (the inputs rescale ideally), so the analysis assigns them the literal ratio 1 rather than an atom: the frees-at-one assignment, carried by the pin marker p below. Asking the add agreement to hold at arbitrary ratios for the program's own inputs would answer a stronger question than the theorems ask, and would wrongly decline (x in ft) + (y in ft) for distinct measurements x y : Q m.

What the first-order ratios buy here

Unit and dimension abstraction are covered, which a function-space ratio could not do (see LambdaS.Ratio): Λu. e has the ratio of its body one unit scope out, and e[μ] records the instantiation.

The ratio context Θ is an index of the relation rather than a function of Γ. That is deliberate: Ctx.shapes Γ.weaken = Ctx.shapes Γ is a theorem, not a definitional equality, so tying Θ to Γ would put a transport in every binder rule. Keeping it free puts the correspondence in the var rule, where it is one hypothesis.

Tw.castShape appears at uapp and dapp for the same reason in the other index: the result types are τ.subst σ and τ.substDim d, and Ty.shape_subst and Ty.shape_substDim are theorems. It appears also at mcons and mrow, where a row's space is a map over the column space and List.length_map is likewise a theorem.

Accumulated Ratios, and a Decidable Diagnostic

With the abstraction theorems in hand, we now ask what many conversions accumulate to. The single-conversion invariance theorem (cvt_rel_iff_coherent) characterizes one conversion, but programs convert many times: a meter-to-feet round trip is harmless, a one-way conversion is not. In this section we assign a program its accumulated conversion ratio where the analysis succeeds, prove that the ratio measures the program's departure from scale-invariance, and show that the resulting condition is decidable, which turns the abstraction theory into a compiler diagnostic. The analysis is conservative: at a sum, a comparison, mapp, comp, log and exp it can decline to assign a ratio, and it always declines a unit constant; a decline is not a verdict of non-invariance.

Ratios as Syntax

The ratio of a first-order program is an element of the unit group: multiplication multiplies ratios, division divides them, a conversion from u to v contributes u/v, and addition forces its branches to agree, which is what makes the ratio a property of a program rather than of a path through it. At higher type the ratio of a function must be a function: λ x. x · x squares its argument's ratio while λ x. x + x preserves it, and nothing in their common type distinguishes them. Our first formulation represented these function ratios as metalanguage functions, and a metalanguage function can be applied but neither traversed nor inspected: unit instantiation, which is a substitution, had nowhere to send the ratio of a polymorphic term, and triviality of a ratio could be defined but not decided. We therefore make ratios first-order syntax.

The definitions are Shape, Tw, SemTw and Tw.eval, all in Ratio.lean. Read them in that order; the notation needed here is this. A ratio is indexed by a unit scope, a context of shapes (one ratio variable, a de Bruijn index, per term variable), and a shape. Evaluation reads a ratio under a rescaling ψ and an environment ρ of semantic ratios, where (a,ρ) extends the environment and (ψ,a) extends the rescaling, assigning log-factor a to the newly bound unit variable. The clause for t [u] performs the recorded instantiation semantically, reading the family at logψ(u). Semantic ratios are positive reals: every ratio denotes a product of scale factors, and positivity is what makes cancellation across the fraction bar sound (Tw.scalarEq).

Tw is the calculus of ratio expressions and Tw.eval its interpretation. Ratios are indexed not by the program's type but by its shape: the type's skeleton, which records where the ratio is a unit expression (scalar), where it maps ratios to ratios (an arrow), where it is a vector or matrix of ratios (vec and mat: the ratio of a vector is a vector of ratios, one per component, and likewise per entry for a matrix), and where a unit binder was crossed (bind). Only the lengths of the spaces survive into the shape, so shape stays blind to units: instantiating a quantifier preserves it, so a ratio indexed by a type equally indexes every instantiation of that type, and no transport is needed. Unit instantiation is then recorded by the syntax rather than performed: t [u] stores the instantiating unit, and the interpretation reads the ratio family at that unit's log-factor. So the Twist rules apply no unit substitution to a ratio; twistOf performs a recorded instantiation only to reduce a redex (Tw.uappE). Reduction of a ratio application is ordinary syntactic substitution (Tw.subst0, interpreted by Tw.eval_subst0).

A judgment Twist relates a typing derivation to its ratio, and the scaling law generalizes the convert-free abstraction theorem (fundamental_free) with the ratio as the measured defect:

Theorem (The scaling law, twisted; Twist.scaling). The law has two parameters. Under a rescaling φ of the valuation the conversion factors are drawn from and a rescaling ψ of the program's inputs, a program of type Q u whose conversions accumulate to ratio t rescales by ψ(u)·φ(t)·ψ(t); we write ψ(t) for the ratio's value ⟦t⟧_(ψ,ρ) with every ratio variable held at the trivial ratio 1.

Each conversion pays the factor once to each parameter: once under ψ because the converted value rescales with its source unit rather than the target its type advertises, and once under φ because the conversion factor itself rescales with the valuation. At φ = ψ the ratio appears squared. For example, doubling the meter while fixing the foot, in both the values and the valuation, multiplies x in ft by four: the input x, a length in meters, doubles, and the conversion factor V(m)/V(ft) doubles with it, while the result type Q ft promises only ψ(ft) = 1; the excess 2² is ψ(m/ft)². At trivial ratio this is the convert-free abstraction theorem (fundamental_free); the extra factor is visible to every rescaling, not only the incoherent ones. Holding one parameter trivial in turn gives the two statements a drift diagnosis is for (unitDrift_law): with the values fixed, a program of drift w is multiplied by φ(w) when the valuation is rescaled by φ (den_comp_of_drift), so drift 1 is declaration independence (den_indep_of_driftFree); with the valuation fixed, a program of drift 1 obeys the unrestricted scaling law (scaleLaw_of_driftFree). The converse direction gives the characterization: for a first-order program with nonzero denotation, invariance under all rescalings holds exactly when its ratio evaluates to 1 under every rescaling (Twist.invariant_iff). The nonzero hypothesis is the standing zero exception, in the same place Atkey et al. [2013] patch their relational interpretation for polymorphic zero. This characterization assumes the analysis assigns a ratio. A decline is conservative: 0 * (x in ft) + y is invariant because it denotes y, but its branch ratios disagree and the analysis declines. No completeness theorem for the decline verdict is claimed.

Deciding Triviality

The condition “evaluates to 1 under every rescaling” is semantic. It is also decidable, and rational exponents are what make the decision clean. A ratio normalizes to a single unit-group element. The normalizer is a standard environment-passing evaluator: it interprets Tw into a symbolic model whose scalar case is the unit group itself, reading the program's unit variables through an environment into one fixed scope; “Mechanization notes” (LambdaS.lean) reports why this avoids indexing the model by scopes. Rescalings separate units: two group elements scale alike under every rescaling only if they are equal. Since the group is a ℚ-vector space, triviality of the normal form is one coordinatewise comparison of rationals.

The decision is one a compiler can act on: a build system can refuse to link a routine whose conversions do not cancel (its result depends on whether lengths were declared in feet or in meters), or warn at its call sites, wherever declaration-independence is part of the interface. The diagnostic certifies declaration-independence the way a purity analysis certifies effect-freedom, at the cost of one group computation per derivation and one equality of exponent vectors.

Theorem (Decidability; Tw.nfOne_eq_one_iff). A ratio evaluates to 1 under every rescaling, its ratio variables held at the trivial ratio, iff its normal form is the group unit 1; consequently, for a first-order program with nonzero denotation whose ratio the analysis computes, scale-invariance is decided by one equality of exponent vectors.

We package the analysis as a function unitDrift from typing derivations to normal ratios (its specification is unitDrift_spec) and call its output the program's drift. For example, for x : Q m consider three programs, written here with the in form of “Types and Terms” (Typing.lean); their core elaborations are checked at build time in the artifact:

(x in ft) in m,  x in ft,  (x in ft) + (x in ft).

The round trip has drift 1: its two factors cancel, whatever magnitudes the declarations assign m and ft. The one-way conversion has drift m/ft, and the diagnostic names it. The sum also has drift m/ft: both branches carry the same variable's ratio times m/ft, so the agreement demanded at + holds and the branches' shared drift is the program's.

At +, at a comparison, and at map application and composition per output component, the analysis compares ratio terms up to β-reduction and the unit algebra (Tw.normEq). At a first-order ratio context, Tw.openNF evaluates structurally with an independent fresh coordinate for every scalar input component. It has no fuel and handles arbitrary internal higher-order applications and unit binders. Equality of its exponent vectors is exact (Tw.normEq_firstOrder_iff). At contexts containing unknown functions or unit families, the bounded Tw.norm reducer and opaque-atom algebra serve as a sound conservative fallback. In that fallback, unit constants merge into one exponent vector and opaque subratios carry rational exponents. In either mode, reordered, reassociated, and differently placed conversions are accepted: the artifact's addAssoc converts a product of meters once at m² in one branch and factor by factor in the other, and the analysis reports the drift the branches share. An atom also cancels against itself across the fraction bar, and soundly: semantic ratios are positive reals, so x/x = 1 holds, and the atoms, like the units, form a free ℚ-vector space, with t^q scaling their exponents.

How exact is the comparison? A program's free variables are its inputs, and inputs are measurements: they rescale exactly with their units, so the analysis assigns them the trivial ratio, and unitDriftLam extends the same reading to a program's leading λ-binders, which are inputs spelled with a binder. The trivial ratio is not an assumption about callers; it is the hypothesis of the property the diagnostic decides, since the scaling law rescales each input by its unit's factor by definition of the question. Nor does a caller that passes an already-converted value escape: at a visible application the argument's actual ratio flows into the body's family, so a conversion is charged where it is visible, and the input reading applies only at the program's own boundary. Atoms therefore arise only at variables bound inside the term under analysis, whose future arguments may genuinely drift. A ratio variable stands for the accumulated ratio of whatever term an application site will supply, and accumulated ratios are products of scale factors, so the positive carrier excludes nothing the scaling law can instantiate. At first-order ratio contexts, comparison is exact in both directions for all scalar ratio syntax: agreement coincides with equal evaluation under every rescaling and every positive input drift (Tw.normEq_firstOrder_iff). For atom-free ratios, comparison is exact at arbitrary contexts (Tw.normEq_iff_eval_eq). Once both summands have ratios in either exact fragment, the sum is declined precisely when those ratios disagree. A summand whose own analysis declines also makes the sum decline. The artifact checks both sides of the line: (x in ft) + (y in ft) over two meter inputs is accepted at drift m/ft (addTwoVars), while (x in ft) + y against a foot input is declined (addMixed). Its executable Float guard illustrates sensitivity to two constant oracles, not a kernel theorem about valuation-induced rescalings. Exact ratio comparison does not imply that a declined whole program fails invariance: a mismatched branch can be multiplied by zero, or two conditional arms can denote the same value.

Unknown function and unit-family inputs select the bounded fallback, whose fuel is not proved sufficient; Tw.normEq_of_legacy shows that, at every context, Tw.normEq accepts each pair that comparison accepts. Distinct input components remain independent: agreeing at a particular call site is weaker than the universal agreement that the compositional analysis requires.

The analysis declines one term form unconditionally: 1_u, which the convert-free abstraction theorem (fundamental_free) places outside the invariance theory. The decline also keeps a reported drift meaning one thing. A unit constant's defect is a failure of covariance, not a dependence on the declarations: 1_u/1_u depends on nothing, and x · 1_u never consults the valuation. The ratio u^(-1/2) would track it only on the diagonal φ = ψ, where the valuation and the inputs are rescaled together: the twisted law's factor is ψ(u)·φ(w)·ψ(w), which at w = u^(-1/2) is ψ(u)^(1/2)·φ(u)^(-1/2), equal to 1 exactly when φ(u) = ψ(u). The law's two parameters are independent, so no single ratio in the unit group accepts 1_u in general. Even were one available, tracking it would make the exhibited ratio mean two different things. With 1_u declined, conversion remains the only analyzed construct that reads the valuation, so a reported drift names dependence on the declared magnitudes and nothing else.

log and exp accept an argument whose ratio is trivial, since a drift-free value is unmoved by every rescaling and so is its logarithm; the artifact accepts log of a round-trip ratio at drift 1 (logRoundTrip) and declines log of a drifting one (logDrifting). Beyond drift-free arguments the defect leaves the multiplicative group. exp's would depend on the value, not only the rescaling. log's, though value-independent, is additive, turning a ratio into a shift. An additive drift slot would not survive multiplication, so tracking log further would only move the decline to ·. Every other form has a rule. A power lifts its argument's ratio to the exponent. The introduction forms of “Types and Terms” (Typing.lean) build ratio vectors and matrices componentwise, with no side condition, and indexing projects. Map application and composition are accepted under the same agreement condition as +, stated per output component: the summands of (M ⊙ x)_j must share one ratio, and the shared ratio is the component's drift.

The diagnostic scales past one-liners. The artifact's ballistics kernel (Ballistics in Examples.lean) takes a distance in feet and a time in seconds, converts to meters, and computes the kinetic energy per unit mass v²/2, in four reporting variants, each verdict decided at build time. Reporting back in ft²/s² is certified drift-free: the input conversion cancels against the output conversion through the square. Reporting in metric carries drift exactly ft²/m², the one foot-to-meter conversion squared through v², and the diagnostic names it. Computing the energy two ways in one sum, convert-then-square against square-then-convert, is accepted with the shared drift. And recovering the speed by a square root carries drift ft/m: the energy's ft²/m² through the root, which halves the drift's exponent along with the unit's.

The diagnostic also works through the quantifiers. The generic caster of “The Calculus” (Typing.lean) has, before any instantiation, the open drift u/v: an exponent vector with unit-variable coordinates, read off the ratio family its binders denote (caster). Instantiated at meters and feet it is m/ft; at meters twice, 1. And the polymorphic round trip, converting out to v and back to u, is certified drift-free without instantiation (casterRound): the variable coordinates cancel in the free ℚ-vector space, so one certificate covers every future instantiation at once.

Programs with drift 1 satisfy a strong guarantee. A program with drift 1, open or closed and at any unit, denotes at every environment the same number under every valuation of the base units (den_indep_of_driftFree): its output provably does not depend on how the units it converts through are declared. By the adequacy theorem of “Adequacy and Erasure” (Erasure.lean), the same holds of the real-valued evaluation of a closed program at Q 1 (evalC_indep_of_driftFree). The declared factors along any closed conversion loop cancel, which restates “Unit Declarations” (Declare.lean)'s consistency criterion as a theorem about programs. With the valuation held fixed instead, the same program obeys the unrestricted scaling law (scaleLaw_of_driftFree), which is the hypothesis the Pi theorem consumes (den_mulScaleLaw_driftFree, PiTheorem.lean), now supplied by the drift analysis rather than by the absence of conversion.

inductive LambdaS.Twist {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {τ : Ty B D j k} (p : ℕ) (Θ : List Shape) : HasTy Δ Γ e τ → Tw B k Θ τ.shape → Prop

The conversion-ratio semantics. A second reading of Λs, valued in the ratio syntax, running alongside den.

Addition forces its branches to agree, which is what makes the ratio a property of a term rather than of a path through it.

The index p is the frees-at-one assignment, in de Bruijn form. Because lam always prepends its ratio variable, the genuine atoms are exactly the positions below p and the program's own context variables are the positions at p and beyond. A lam-bound variable stands for a future argument, which may carry any ratio, so it enters as an atom (var); a context variable is a measurement, which rescales ideally, so it enters at the trivial ratio (varOne). The exported diagnostic runs at p = 0: every free variable of the program is pinned at 1, and atoms arise only under binders.

• var {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {τ : Ty B D j k} {n p : ℕ} {Θ : List Shape} (h : Γ[n]? = some τ) (h' : Θ[n]? = some τ.shape) (hp : n < p) : Twist p Θ (HasTy.var h) (Tw.var n h')

  A lam-bound variable, below the pin marker: a genuine atom.

• varOne {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {τ : Ty B D j k} {n p : ℕ} {Θ : List Shape} (h : Γ[n]? = some τ) (h' : Θ[n]? = some τ.shape) (hp : p ≤ n) : Twist p Θ (HasTy.var h) (Tw.one τ.shape)

  A context variable of the program, at or beyond the pin marker: its ratio is 1 at every shape, because inputs are measurements and measurements rescale ideally.

• lam {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {σ τ : Ty B D j k} {e : Tm B D j k} {p : ℕ} {Θ : List Shape} {d : HasTy Δ (σ :: Γ) e τ} {t : Tw B k (σ.shape :: Θ) τ.shape} : Twist (p + 1) (σ.shape :: Θ) d t → Twist p Θ d.lam t.lam
• app {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {σ τ : Ty B D j k} {f a : Tm B D j k} {p : ℕ} {Θ : List Shape} {df : HasTy Δ Γ f (σ.arrow τ)} {da : HasTy Δ Γ a σ} {tf : Tw B k Θ (σ.arrow τ).shape} {ta : Tw B k Θ σ.shape} : Twist p Θ df tf → Twist p Θ da ta → Twist p Θ (df.app da) (tf.app ta)
• lit {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {q : ℚ} {p : ℕ} {Θ : List Shape} : Twist p Θ HasTy.lit (Tw.unit 1)
• mul {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {u v : UExp B k} {a b : Tm B D j k} {p : ℕ} {Θ : List Shape} {da : HasTy Δ Γ a (Ty.Q u)} {db : HasTy Δ Γ b (Ty.Q v)} {s t : Tw B k Θ Shape.scalar} : Twist p Θ da s → Twist p Θ db t → Twist p Θ (da.mul db) (s.mul t)
• div {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {u v : UExp B k} {a b : Tm B D j k} {p : ℕ} {Θ : List Shape} {da : HasTy Δ Γ a (Ty.Q u)} {db : HasTy Δ Γ b (Ty.Q v)} {s t : Tw B k Θ Shape.scalar} : Twist p Θ da s → Twist p Θ db t → Twist p Θ (da.div db) (s.div t)
• add {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {u : UExp B k} {a b : Tm B D j k} {p : ℕ} {Θ : List Shape} {da : HasTy Δ Γ a (Ty.Q u)} {db : HasTy Δ Γ b (Ty.Q u)} {s t : Tw B k Θ Shape.scalar} (heq : ∀ (ψ : Scaling B k) (θρ : TwEnv Θ), Tw.eval ψ s θρ = Tw.eval ψ t θρ) : Twist p Θ da s → Twist p Θ db t → Twist p Θ (da.add db) s

  Addition: the two summands' ratios must have equal value under every scaling and environment (heq), and the sum carries that shared ratio. twistOf discharges heq with Tw.normEq.

• ifle {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {u : UExp B k} {a b t f : Tm B D j k} {τ : Ty B D j k} {p : ℕ} {Θ : List Shape} {da : HasTy Δ Γ a (Ty.Q u)} {db : HasTy Δ Γ b (Ty.Q u)} {dt : HasTy Δ Γ t τ} {df : HasTy Δ Γ f τ} {sa sb : Tw B k Θ Shape.scalar} {st sf : Tw B k Θ τ.shape} (hab : ∀ (ψ : Scaling B k) (θρ : TwEnv Θ), Tw.eval ψ sa θρ = Tw.eval ψ sb θρ) (htf : ∀ (ψ : Scaling B k) (θρ : TwEnv Θ), Tw.eval ψ st θρ = Tw.eval ψ sf θρ) : Twist p Θ da sa → Twist p Θ db sb → Twist p Θ dt st → Twist p Θ df sf → Twist p Θ (da.ifle db dt df) st

  Compare and branch: the add agreement, twice over. The scrutinees must carry the same ratio, or the branch taken would depend on the conversion table, which is a control-flow bug from a wrong declaration and not merely a wrong number. The branches must carry the same ratio, or the result has no single ratio to report. Either failure declines.

• convert {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {u v : UExp B k} {a : Tm B D j k} {p : ℕ} {Θ : List Shape} {da : HasTy Δ Γ a (Ty.Q u)} {s : Tw B k Θ Shape.scalar} (h : SameDim Δ u v) : Twist p Θ da s → Twist p Θ (da.convert h) (s.mul ((Tw.unit u).div (Tw.unit v)))

  Conversion from u to v multiplies the operand's ratio by u/v: the value still moves with u where its type now predicts v.

• pow {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {q : ℚ} {e : Tm B D j k} {u : UExp B k} {p : ℕ} {Θ : List Shape} {de : HasTy Δ Γ e (Ty.Q u)} {s : Tw B k Θ Shape.scalar} : Twist p Θ de s → Twist p Θ de.pow (s.qpow q)
• log {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {p : ℕ} {Θ : List Shape} {de : HasTy Δ Γ e (Ty.Q 1)} {s : Tw B k Θ Shape.scalar} (hone : ∀ (ψ : Scaling B k) (θρ : TwEnv Θ), Tw.eval ψ s θρ = 1) : Twist p Θ de s → Twist p Θ de.log (Tw.unit 1)

  log of a trivial-ratio argument, with the add-style side condition that the argument's ratio is worth 1 under every scaling and environment. A trivial-ratio argument is unmoved by every rescaling: the typing rule pins it at Q 1, so the type's factor is ψ(1) = 1 and the ratio is 1, hence its logarithm is unmoved too and the result carries the trivial ratio. Beyond drift-1 arguments the defect leaves the multiplicative group: log turns a multiplicative discrepancy into an additive one, which no ratio expresses, and the decline in twistOf stands.

• exp {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {p : ℕ} {Θ : List Shape} {de : HasTy Δ Γ e (Ty.Q 1)} {s : Tw B k Θ Shape.scalar} (hone : ∀ (ψ : Scaling B k) (θρ : TwEnv Θ), Tw.eval ψ s θρ = 1) : Twist p Θ de s → Twist p Θ de.exp (Tw.unit 1)

  exp of a trivial-ratio argument, under the same side condition and for the same reason: an argument at Q 1 with ratio 1 is unmoved by every rescaling, so its exponential is unmoved too. Beyond drift-1 arguments the defect leaves the multiplicative group: how exp moves would depend on the argument's value, not merely its unit, and the decline in twistOf stands.

• ulam {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {d : DExp D j} {τ : Ty B D j (k + 1)} {e : Tm B D j (k + 1)} {p : ℕ} {Θ : List Shape} {db : HasTy (DCtx.cons d Δ) Γ.weaken e τ} {t : Tw B (k + 1) Θ τ.shape} : Twist p Θ db t → Twist p Θ db.ulam t.ulam
• uapp {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {f : Tm B D j k} {d : DExp D j} {τ : Ty B D j (k + 1)} {σ : UExp B k} {p : ℕ} {Θ : List Shape} {df : HasTy Δ Γ f (Ty.all d τ)} {t : Tw B k Θ (Ty.all d τ).shape} (hd : dimOf Δ σ = d) : Twist p Θ df t → Twist p Θ (df.uapp hd) (Tw.castShape ⋯ (t.uapp σ))
• dlam {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {τ : Ty B D (j + 1) k} {e : Tm B D (j + 1) k} {p : ℕ} {Θ : List Shape} {db : HasTy Δ.weakenDim Γ.weakenDim e τ} {t : Tw B k Θ τ.shape} : Twist p Θ db t → Twist p Θ db.dlam t
• dapp {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {f : Tm B D j k} {τ : Ty B D (j + 1) k} {p : ℕ} {Θ : List Shape} {d : DExp D j} {df : HasTy Δ Γ f τ.allDim} {t : Tw B k Θ τ.shape} : Twist p Θ df t → Twist p Θ df.dapp (Tw.castShape ⋯ t)
• vnil {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {p : ℕ} {Θ : List Shape} : Twist p Θ HasTy.vnil Tw.vecnil

  The empty vector: the empty drift vector.

• vcons {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e v : Tm B D j k} {u : UExp B k} {V : Sp B k} {p : ℕ} {Θ : List Shape} {de : HasTy Δ Γ e (Ty.Q u)} {dv : HasTy Δ Γ v (Ty.vec V)} {s : Tw B k Θ Shape.scalar} {t : Tw B k Θ (Shape.vec (List.length V))} : Twist p Θ de s → Twist p Θ dv t → Twist p Θ (de.vcons dv) (s.veccons t)

  Consing a scalar onto a vector conses its drift onto the drift vector. No side condition: the relation at vector shapes carries one ratio per component, so a drifting component is reported rather than declined.

• mnil {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {V : Sp B k} {p : ℕ} {Θ : List Shape} : Twist p Θ HasTy.mnil Tw.matnil

  The zero-row matrix: the zero-row drift matrix.

• mcons {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {w : UExp B k} {r M : Tm B D j k} {V W : Sp B k} {p : ℕ} {Θ : List Shape} {dr : HasTy Δ Γ r (Ty.vec (List.map (fun (u : Term B (Fin k)) => Term.div w u) V))} {dM : HasTy Δ Γ M (Ty.lin V W)} {tr : Tw B k Θ (Shape.vec (List.map (fun (u : Term B (Fin k)) => Term.div w u) V).length)} {tM : Tw B k Θ (Shape.mat (List.length V) (List.length W))} : Twist p Θ dr tr → Twist p Θ dM tM → Twist p Θ (dr.mcons dM) ((Tw.castShape ⋯ tr).matcons tM)

  Consing a row onto a matrix conses the row's drift vector onto the drift matrix. The row lives at the mapped space, whose length equals the column space's by List.length_map, so its drift vector is retyped along that equality.

• idx {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {V : Sp B k} {i : ℕ} {u : UExp B k} {p : ℕ} {Θ : List Shape} {de : HasTy Δ Γ e (Ty.vec V)} {t : Tw B k Θ (Shape.vec (List.length V))} (hu : V[i]? = some u) : Twist p Θ de t → Twist p Θ (de.idx hu) (t.proj ⟨i, ⋯⟩)

  Indexing projects the component's drift out of the drift vector.

• mrow {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {V W : Sp B k} {i : ℕ} {w : UExp B k} {p : ℕ} {Θ : List Shape} {de : HasTy Δ Γ e (Ty.lin V W)} {t : Tw B k Θ (Shape.mat (List.length V) (List.length W))} (hw : W[i]? = some w) : Twist p Θ de t → Twist p Θ (de.mrow hw) (Tw.castShape ⋯ (t.row ⟨i, ⋯⟩))

  Row extraction reads the row's drift vector out of the drift matrix. Extraction converts nothing, so the row carries exactly the drift its entries had. The row space is a map over the column space, so the shape is retyped along List.length_map, in the direction opposite to mcons.

• mapp {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {f x : Tm B D j k} {V W : Sp B k} {p : ℕ} {Θ : List Shape} {df : HasTy Δ Γ f (Ty.lin V W)} {dx : HasTy Δ Γ x (Ty.vec V)} {tf : Tw B k Θ (Shape.mat (List.length V) (List.length W))} {tx : Tw B k Θ (Shape.vec (List.length V))} {tw : Tw B k Θ (Shape.vec (List.length W))} (heq : ∀ (ψ : Scaling B k) (θρ : TwEnv Θ) (a : Fin (List.length W)) (i : Fin (List.length V)), Tw.eval ψ tf θρ a i * Tw.eval ψ tx θρ i = Tw.eval ψ tw θρ a) : Twist p Θ df tf → Twist p Θ dx tx → Twist p Θ (df.mapp dx) tw

  Matrix application. The add-style agreement condition, per output row a: the product of the entry drift at (a, i) with the argument drift at i must be worth the output drift at a, for every column i, in every scaling and environment. Over the empty domain the condition is vacuous and any output drift is sound, since the output is the zero vector.

• comp {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {f g : Tm B D j k} {U V W : Sp B k} {p : ℕ} {Θ : List Shape} {df : HasTy Δ Γ f (Ty.lin V W)} {dg : HasTy Δ Γ g (Ty.lin U V)} {tf : Tw B k Θ (Shape.mat (List.length V) (List.length W))} {tg : Tw B k Θ (Shape.mat (List.length U) (List.length V))} {tw : Tw B k Θ (Shape.mat (List.length U) (List.length W))} (heq : ∀ (ψ : Scaling B k) (θρ : TwEnv Θ) (a : Fin (List.length W)) (i : Fin (List.length U)) (b : Fin (List.length V)), Tw.eval ψ tf θρ a b * Tw.eval ψ tg θρ b i = Tw.eval ψ tw θρ a i) : Twist p Θ df tf → Twist p Θ dg tg → Twist p Θ (df.comp dg) tw

  Composition. The analogous agreement condition per entry (a, i), across the middle index b.

• ratio {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {τ : Ty B D j k} {p : ℕ} {Θ : List Shape} {d : HasTy Δ Γ e τ} {t t' : Tw B k Θ τ.shape} (heq : ∀ (ψ : Scaling B k) (θρ : TwEnv Θ), Tw.eval ψ t θρ = Tw.eval ψ t' θρ) : Twist p Θ d t → Twist p Θ d t'

  Ratio conversion: a ratio may be replaced by one of equal value under every scaling and environment. This is how twistOf reduces the redexes it forms while building: app on a literal lam emits the substituted body (Tw.appE), uapp on a literal ulam performs the recorded instantiation (Tw.uappE), idx reduces projections of vector literals (Tw.projE), and mrow reduces rows of matrix literals (Tw.rowE), each justified by its evaluation lemma.

The scaling law with a twist

inductive LambdaS.TwRelEnv {B D : Type} [Fintype B] {j k : ℕ} (φ ψ : Scaling B k) (Γ : Ctx B D j k) (Θ : List Shape) : TwEnv Θ → TwEnv Θ → Env Γ → Env Γ → Prop

Environments related at given ratios, pointwise, under a valuation rescaling φ and a value rescaling ψ, with one ratio environment per reading. The cons rule carries an equation of shapes rather than demanding a definitional match, because under ulam the context is Γ.weaken and Ty.shape (Ty.weaken τ) = Ty.shape τ is a theorem. Localizing the transport here keeps it out of every other rule.

• nil {B D : Type} [Fintype B] {j k : ℕ} {φ ψ : Scaling B k} {θρ θρ' : TwEnv []} {ρ ρ' : Env []} : TwRelEnv φ ψ [] [] θρ θρ' ρ ρ'
• cons {B D : Type} [Fintype B] {j k : ℕ} {φ ψ : Scaling B k} {τ : Ty B D j k} {Γ : Ctx B D j k} {s : Shape} {Θ : List Shape} {θρ θρ' : TwEnv (s :: Θ)} {ρ ρ' : Env (τ :: Γ)} (hs : s = τ.shape) : TwRel τ (hs ▸ θρ.1) (hs ▸ θρ'.1) φ ψ ρ.1 ρ'.1 → TwRelEnv φ ψ Γ Θ θρ.2 θρ'.2 ρ.2 ρ'.2 → TwRelEnv φ ψ (τ :: Γ) (s :: Θ) θρ θρ' ρ ρ'

theorem LambdaS.twRelEnv_lookup {B D : Type} [Fintype B] {j k : ℕ} {φ ψ : Scaling B k} {Γ : Ctx B D j k} {Θ : List Shape} {θρ θρ' : TwEnv Θ} {ρ ρ' : Env Γ} : TwRelEnv φ ψ Γ Θ θρ θρ' ρ ρ' → ∀ {τ : Ty B D j k} (n : ℕ) (h : Γ[n]? = some τ) (h' : Θ[n]? = some τ.shape), TwRel τ (TwEnv.lookup n h' θρ) (TwEnv.lookup n h' θρ') φ ψ (Env.lookup n h ρ) (Env.lookup n h ρ')

Looking up related environments.

theorem LambdaS.twRelEnv_weaken {B D : Type} [Fintype B] {j k : ℕ} {φ ψ : Scaling B k} (s s' : ℝ) {Γ : Ctx B D j k} {Θ : List Shape} {θρ θρ' : TwEnv Θ} {ρ ρ' : Env Γ} : TwRelEnv φ ψ Γ Θ θρ θρ' ρ ρ' → TwRelEnv (φ.cons s) (ψ.cons s') Γ.weaken Θ θρ θρ' ρ.weaken ρ'.weaken

Weakening related environments under a unit binder. The value environments are retyped by Env.weaken; the ratio environments are untouched, because shape is blind to units (Ty.shape_weaken).

theorem LambdaS.twRelEnv_weakenDim {B D : Type} [Fintype B] {j k : ℕ} {φ ψ : Scaling B k} {Γ : Ctx B D j k} {Θ : List Shape} {θρ θρ' : TwEnv Θ} {ρ ρ' : Env Γ} : TwRelEnv φ ψ Γ Θ θρ θρ' ρ ρ' → TwRelEnv φ ψ Γ.weakenDim Θ θρ θρ' ρ.weakenDim ρ'.weakenDim

The same under a dimension binder, where nothing at all moves.

theorem LambdaS.Twist.scaling {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {τ : Ty B D j k} {p : ℕ} {Θ : List Shape} {d : HasTy Δ Γ e τ} {t : Tw B k Θ τ.shape} : Twist p Θ d t → ∀ (V φ ψ : Scaling B k) (θρ θρ' : TwEnv Θ), TwEnv.OnesFrom p θρ → TwEnv.OnesFrom p θρ' → ∀ {ρ ρ' : Env Γ}, TwRelEnv φ ψ Γ Θ θρ θρ' ρ ρ' → TwRel τ (Tw.eval φ t θρ) (Tw.eval ψ t θρ') φ ψ (den V d ρ) (den (V.comp φ) d ρ')

The scaling law with a twist. Rescale the valuation by φ and the values by ψ: a term whose conversions accumulate to t rescales by its type's factor under ψ times t's value under φ times t's value under ψ. The two readings of the ratio are the two things a conversion pays for: its factor V(u)/V(v) moves with the valuation, and the converted value moves with its source unit where its type promises the target. At φ = ψ the ratio appears squared; at trivial ratio the conclusion is that of fundamental_free, the unrestricted law under every rescaling, now for terms that convert but accumulate nothing.

The value environments are related at the evaluation of the assignment: the ratio environments are arbitrary at the atoms (positions below p, the lam-bound variables) and pinned at 1 from p on (TwEnv.OnesFrom), which is where the varOne rule reads its trivial ratio back. The exported theorems instantiate at p = 0 and the all-ones environments.

Proved at the whole calculus; the binder cases are the ones a function-space ratio could not state.

The characterization at first order

A term of scalar type over a context of scalars: a program computing a number from numbers, whatever abstraction and application it uses inside. Its ratio is a closed scalar Tw, and the characterization says: a program with nonzero denotation obeys the unrestricted scaling law exactly when that ratio's value is 1 under every scaling. The next section makes that condition syntactic, and hence decidable.

@[simp]

theorem LambdaS.shapes_scalarCtx {B D : Type} {j k : ℕ} (us : List (UExp B k)) : (scalarCtx us).shapes = List.map (fun (x : UExp B k) => Shape.scalar) us

Scalar contexts and their shape lists.

theorem LambdaS.twRelEnv_scaleEnv {B D : Type} [Fintype B] {j k : ℕ} (φ ψ : Scaling B k) (us : List (UExp B k)) (ρ : Env (scalarCtx us)) : TwRelEnv φ ψ (scalarCtx us) (List.map (fun (x : UExp B k) => Shape.scalar) us) (oneTwEnv (List.map (fun (x : UExp B k) => Shape.scalar) us)) (oneTwEnv (List.map (fun (x : UExp B k) => Shape.scalar) us)) ρ (scaleEnv ψ us ρ)

A scalar environment is related to its own rescaling at trivial ratios, under any rescaling of the valuation.

theorem LambdaS.Twist.law {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {u : UExp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.Q u)} {t : Tw B k (List.map (fun (x : UExp B k) => Shape.scalar) us) Shape.scalar} (ht : Twist 0 (List.map (fun (x : UExp B k) => Shape.scalar) us) d t) (V φ ψ : Scaling B k) (ρ : Env (scalarCtx us)) : den (V.comp φ) d (scaleEnv ψ us ρ) = ψ.scale u * (↑(Tw.eval φ t (oneTwEnv (List.map (fun (x : UExp B k) => Shape.scalar) us))) * ↑(Tw.eval ψ t (oneTwEnv (List.map (fun (x : UExp B k) => Shape.scalar) us)))) * den V d ρ

The twisted scaling law at first order. Rescale the valuation by φ and the arguments by ψ: the result rescales by its unit's factor under ψ times the accumulated ratio's value under φ times its value under ψ. The two exported specializations are φ = ψ (the ratio squared; the characterization below) and the two axes held trivial in turn (scaleLaw_of_driftFree, den_indep_of_driftFree).

theorem LambdaS.Twist.law_lin {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {V W : Sp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.lin V W)} {t : Tw B k (List.map (fun (x : UExp B k) => Shape.scalar) us) (Shape.mat (List.length V) (List.length W))} (ht : Twist 0 (List.map (fun (x : UExp B k) => Shape.scalar) us) d t) (V₀ φ ψ : Scaling B k) (ρ : Env (scalarCtx us)) (a : Fin (List.length W)) (i : Fin (List.length V)) : den (V₀.comp φ) d (scaleEnv ψ us ρ) a i = ψ.scale (List.get W a) / ψ.scale (List.get V i) * (↑(Tw.eval φ t (oneTwEnv (List.map (fun (x : UExp B k) => Shape.scalar) us)) a i) * ↑(Tw.eval ψ t (oneTwEnv (List.map (fun (x : UExp B k) => Shape.scalar) us)) a i)) * den V₀ d ρ a i

The twisted scaling law at a matrix result. The same law as Twist.law, over a context of scalars but a program that returns a map. The conclusion is TwRel at .lin unfolded: entry (a,i) rescales by the factor its type predicts, ψ(W a) / ψ(V i), times that entry's own ratio under each axis. Hart's rank-one form is what makes the prediction a ratio of two space factors rather than a table.

Nothing new is proved here. Twist.scaling was always stated at an arbitrary context and type; this is its instantiation at the shape the linear-algebra section is about, which Twist.law never took.

theorem LambdaS.Twist.law_vec {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {U : Sp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.vec U)} {t : Tw B k (List.map (fun (x : UExp B k) => Shape.scalar) us) (Shape.vec (List.length U))} (ht : Twist 0 (List.map (fun (x : UExp B k) => Shape.scalar) us) d t) (V₀ φ ψ : Scaling B k) (ρ : Env (scalarCtx us)) (i : Fin (List.length U)) : den (V₀.comp φ) d (scaleEnv ψ us ρ) i = ψ.scale (List.get U i) * (↑(Tw.eval φ t (oneTwEnv (List.map (fun (x : UExp B k) => Shape.scalar) us)) i) * ↑(Tw.eval ψ t (oneTwEnv (List.map (fun (x : UExp B k) => Shape.scalar) us)) i)) * den V₀ d ρ i

The twisted scaling law at a vector result. The same law as Twist.law, over a context of scalars but a program that returns a vector. The conclusion is TwRel at .vec unfolded: component i rescales by the factor its type predicts, ψ(U i), times that component's own ratio under each axis. Like Twist.law_lin, it is Twist.scaling instantiated at one shape.

theorem LambdaS.Twist.eq_one_of_invariant {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {u : UExp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.Q u)} {t : Tw B k (List.map (fun (x : UExp B k) => Shape.scalar) us) Shape.scalar} (ht : Twist 0 (List.map (fun (x : UExp B k) => Shape.scalar) us) d t) (V : Scaling B k) {ρ : Env (scalarCtx us)} (hne : den V d ρ ≠ 0) (hinv : ∀ (ψ : Scaling B k), den (V.comp ψ) d (scaleEnv ψ us ρ) = ψ.scale u * den V d ρ) (ψ : Scaling B k) : Tw.eval ψ t (oneTwEnv (List.map (fun (x : UExp B k) => Shape.scalar) us)) = 1

Invariance under all scalings forces the ratio's value to 1.

The general converse for any term of scalar type over a context of scalars, higher-order structure and unit polymorphism inside the term included. A nonzero denotation obeying the scaling law for every scaling has a ratio worth 1 under every scaling.

Compare fundamental, which gives the law for coherent scalings and no conclusion at all about the ratio: coherence is precisely blind to conversion, which is why the two theorems are the two halves of one story.

theorem LambdaS.Twist.invariant_of_eq_one {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {u : UExp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.Q u)} {t : Tw B k (List.map (fun (x : UExp B k) => Shape.scalar) us) Shape.scalar} (ht : Twist 0 (List.map (fun (x : UExp B k) => Shape.scalar) us) d t) (hone : ∀ (ψ : Scaling B k), Tw.eval ψ t (oneTwEnv (List.map (fun (x : UExp B k) => Shape.scalar) us)) = 1) (V ψ : Scaling B k) (ρ : Env (scalarCtx us)) : den (V.comp ψ) d (scaleEnv ψ us ρ) = ψ.scale u * den V d ρ

Cancelling conversions are invisible. A term whose ratio is worth 1 under every scaling obeys the unrestricted scaling law, exactly as a convert-free term does, even though it may convert repeatedly along the way.

theorem LambdaS.Twist.invariant_iff {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {u : UExp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.Q u)} {t : Tw B k (List.map (fun (x : UExp B k) => Shape.scalar) us) Shape.scalar} (ht : Twist 0 (List.map (fun (x : UExp B k) => Shape.scalar) us) d t) (V : Scaling B k) {ρ : Env (scalarCtx us)} (hne : den V d ρ ≠ 0) : (∀ (ψ : Scaling B k), den (V.comp ψ) d (scaleEnv ψ us ρ) = ψ.scale u * den V d ρ) ↔ ∀ (ψ : Scaling B k), Tw.eval ψ t (oneTwEnv (List.map (fun (x : UExp B k) => Shape.scalar) us)) = 1

The characterization. For a term of scalar type over a context of scalars with nonzero denotation, invariance under every scaling holds exactly when its accumulated ratio is worth 1 under every scaling.

This is cvt_invariant_iff_eq for arbitrary terms rather than a single conversion: under unrestricted rescaling, the accumulated ratio is the only defect. The condition on the right is semantic; Tw.nfOne decides it syntactically (Tw.nfOne_eq_one_iff, Twist.invariant_iff_nfOne).

The decision

def LambdaS.Tw.nfOne {B : Type} {k : ℕ} {Θ : List Shape} (t : Tw B k Θ Shape.scalar) : UExp B k

The normal ratio: the unit expression a scalar ratio is worth, at the all-ones environment, with unit variables read as themselves.

Equations

• t.nfOne = LambdaS.Tw.nf (LambdaS.idU B k) t (LambdaS.SynEnv.ones Θ)

theorem LambdaS.Tw.eval_oneTwEnv {B : Type} [Fintype B] {k : ℕ} {Θ : List Shape} (t : Tw B k Θ Shape.scalar) (ψ : Scaling B k) : ↑(eval ψ t (oneTwEnv Θ)) = ψ.scale t.nfOne

At the all-ones environment a ratio is worth the scale of its normal form: the value of Tw.nfOne under ψ.

theorem LambdaS.Tw.nfOne_eq_one_iff {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} (t : Tw B k Θ Shape.scalar) : t.nfOne = 1 ↔ ∀ (ψ : Scaling B k), eval ψ t (oneTwEnv Θ) = 1

Triviality of a ratio is decidable. A scalar ratio, with its ratio variables held at 1, is worth 1 under every scaling exactly when its normal form is the unit of the group: an equality in a free ℚ-vector space, decided coordinatewise.

This is the theorem that turns the characterization into an algorithm.

theorem LambdaS.Twist.invariant_iff_nfOne {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {u : UExp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.Q u)} {t : Tw B k (List.map (fun (x : UExp B k) => Shape.scalar) us) Shape.scalar} (ht : Twist 0 (List.map (fun (x : UExp B k) => Shape.scalar) us) d t) (V : Scaling B k) {ρ : Env (scalarCtx us)} (hne : den V d ρ ≠ 0) : (∀ (ψ : Scaling B k), den (V.comp ψ) d (scaleEnv ψ us ρ) = ψ.scale u * den V d ρ) ↔ t.nfOne = 1

The decidable characterization. For a first-order program with nonzero denotation, unrestricted scale invariance holds exactly when the normal form of its accumulated ratio is the unit of the group: one equality of exponent vectors, decided coordinatewise.

The compiler diagnostic, as a theorem: check Tw.nfOne t = 1 and either conclude the program's result is independent of the unit system, or exhibit the nontrivial ratio as the reason it is not.

Computing the ratio

Twist is a relation; the compiler needs a function. twistOf computes, for a derivation, a ratio together with its Twist derivation, or none.

It fails in exactly two circumstances, and they are different in kind. At add the two branches' ratios must agree up to β-reduction and the unit algebra (Tw.normEq, exact symbolic evaluation at first-order contexts and the conservative bounded fallback at higher-order contexts): unit constants merge into one exponent vector and atoms into one rational exponent each, so reordered, reassociated and differently split conversions are accepted. The same check runs per output component at mapp and comp, whose sums mix one drift per summand: the products along the summed index must agree, and the common value is the component's drift; disagreement declines, exactly as at add. ifle runs it on the two compared quantities and, per component (Tw.agree), on the two branches. Under the frees-at-one assignment the program's own context variables contribute the literal ratio 1 rather than atoms. At a first-order ratio context, once all operands have ratios, the comparison at add, mapp and comp declines only on a genuine ratio disagreement (Tw.normEq_firstOrder_iff), such as (x in ft) + y. A decline inside an operand propagates, and a disagreement need not imply a dependence of the whole denotation: multiplication by zero can erase it. Another source of incompleteness is the treatment of unknown higher-order inputs. Scalar, vector, and matrix argument drifts under lam binders are independent coordinates; their comparison is exact even with internal applications (Tw.normEq_firstOrder_iff). Contexts with unknown functions or unit families retain bounded normalization, whose fuel is not proved sufficient. At log and exp the same check runs against the literal ratio 1: a trivial-ratio argument at Q 1 is unmoved by every rescaling, so its logarithm or exponential is unmoved too, and the result carries the trivial ratio (log ((x in ft)/(x in ft)) is declaration-independent, and is accepted). Beyond drift-1 arguments the two forms are nonlinear and no ratio of any kind describes how they move: log turns a multiplicative defect into an additive one, and exp's would have to depend on the argument's value, not merely its unit, so a nontrivial argument ratio declines. The one unconditional decline is ucon, which names a unit, and that is outside the invariance theory: no scaling story survives naming a magnitude.

The vector and matrix forms are accepted, at the vec and mat shapes, with no side conditions at the introductions: the drift of a vector is a vector of drifts, the drift of a matrix is a matrix of drifts, and a drifting literal component is reported rather than declined. idx projects a drift back out, and mrow reads a row of drifts back out. pow is accepted too: the drift of e ^ q is the drift of e lifted to the q by Tw.qpow, which the positive scalar carrier makes sound.

def LambdaS.Tw.beq {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} {s : Shape} : Tw B k Θ s → Tw B k Θ s → Bool

Decidable equality of ratio terms at matching indices. Proof fields are propositions, so var compares only its index.

Equations

• (LambdaS.Tw.var n a).beq (LambdaS.Tw.var m a_1) = (n == m)
• (LambdaS.Tw.unit u).beq (LambdaS.Tw.unit v) = (u == v)
• (a.mul b).beq (a'.mul b') = (a.beq a' && b.beq b')
• (a.div b).beq (a'.div b') = (a.beq a' && b.beq b')
• (t.qpow q).beq (t'.qpow q') = (t.beq t' && q == q')
• t_1.lam.beq t'.lam = t_1.beq t'
• (f.app a).beq (f'.app a') = if h : s₁ = s₂ then (h ▸ f).beq f' && (h ▸ a).beq a' else false
• LambdaS.Tw.vecnil.beq LambdaS.Tw.vecnil = true
• (a.veccons v).beq (a'.veccons v') = (a.beq a' && v.beq v')
• (v.proj i).beq (v'.proj i') = if h : n₁ = n₂ then (h ▸ v).beq v' && ↑i == ↑i' else false
• LambdaS.Tw.matnil.beq LambdaS.Tw.matnil = true
• (r.matcons M).beq (r'.matcons M') = (r.beq r' && M.beq M')
• (M.row j).beq (M'.row j') = if h : m₁ = m₂ then (h ▸ M).beq M' && ↑j == ↑j' else false
• t.ulam.beq t'.ulam = t.beq t'
• (t.uapp μ).beq (t'.uapp μ') = (t.beq t' && μ == μ')
• x✝¹.beq x✝ = false

theorem LambdaS.Tw.beq_sound {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} {s : Shape} (t t' : Tw B k Θ s) : t.beq t' = true → t = t'

beq is sound (Tw.beq_refl gives the converse). Proof fields vanish by proof irrelevance; the app case pattern-matches the existential shape.

Comparing branch ratios up to the unit algebra

Tw.beq is syntactic. At a sum, syntactic comparison rejects branches whose ratios are the same conversions written in a different order, so the bounded fallback of Tw.normEq compares a flattened form instead: a scalar ratio splits into its unit-constant part (one exponent vector, merged by the group operations) and a list of opaque atoms each carrying a rational exponent, a vector in the free ℚ-vector space the atoms generate, exactly as the units themselves are vectors over the base units. Multiplication appends, division negates the exponents, and qpow scales them. Two ratios compare equal when their unit parts agree and every atom carries the same total exponent on both sides. What the comparison never does is identify syntactically distinct atoms. An atom is usually the ratio of a lam-bound variable, standing for a future argument, and nothing relates two arguments' ratios; a residual application, projection, or unit instantiation is also an atom (Tw.flat). The program's own context variables produce no atoms under the frees-at-one assignment. Comparison is complete when the resulting ratios are atom-free (Tw.scalarEq_complete). At first-order contexts Tw.normEq does not use this comparison and is exact for all ratio syntax (Tw.normEq_firstOrder_iff). Soundness of the exponent arithmetic needs every atom's value positive, which the carrier SemScalar provides: x ^ p · x ^ q = x ^ (p + q) already fails at x = 0.

theorem LambdaS.Tw.beq_refl {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} {s : Shape} (t : Tw B k Θ s) : t.beq t = true

t.beq t holds. With Tw.beq_sound, beq is a lawful equality test.

@[instance_reducible]

instance LambdaS.instBEqTw {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} {s : Shape} : BEq (Tw B k Θ s)

Equations

• LambdaS.instBEqTw = { beq := LambdaS.Tw.beq }

instance LambdaS.instLawfulBEqTw {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} {s : Shape} : LawfulBEq (Tw B k Θ s)

@[instance_reducible]

instance LambdaS.instDecidableEqTw {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} {s : Shape} : DecidableEq (Tw B k Θ s)

Equations

• LambdaS.instDecidableEqTw a b = if h : a.beq b = true then isTrue ⋯ else isFalse ⋯

@[irreducible]

def LambdaS.Tw.flat {B : Type} {k : ℕ} {Θ : List Shape} : Tw B k Θ Shape.scalar → UExp B k × List (Tw B k Θ Shape.scalar × ℚ)

Flatten a scalar ratio into its unit-constant part and its atoms, each with a rational exponent. Unit constants merge into one exponent vector; everything else is an atom at exponent 1, negated under the fraction bar and scaled under qpow.

Equations

• (LambdaS.Tw.unit u).flat = (u, [])
• (a.mul b).flat = (LambdaS.Term.mul a.flat.1 b.flat.1, a.flat.2 ++ b.flat.2)
• (a.div b).flat = (LambdaS.Term.div a.flat.1 b.flat.1, a.flat.2 ++ List.map (fun (p : LambdaS.Tw B x✝¹ x✝ LambdaS.Shape.scalar × ℚ) => (p.1, -p.2)) b.flat.2)
• (t.qpow q).flat = (LambdaS.Term.rpow t.flat.1 q, List.map (fun (p : LambdaS.Tw B x✝¹ x✝ LambdaS.Shape.scalar × ℚ) => (p.1, q * p.2)) t.flat.2)
• x✝.flat = (1, [(x✝, 1)])

theorem LambdaS.Tw.flat_eval {B : Type} [Fintype B] {k : ℕ} {Θ : List Shape} (ψ : Scaling B k) (θρ : TwEnv Θ) (t : Tw B k Θ Shape.scalar) : ↑(eval ψ t θρ) = ψ.scale t.flat.1 * (List.map (fun (p : Tw B k Θ Shape.scalar × ℚ) => ↑(eval ψ p.1 θρ) ^ ↑p.2) t.flat.2).prod

Flattening preserves the value: a scalar ratio evaluates to its unit-constant part's scale times the product of its atoms' values raised to their exponents. Everything in sight is positive, which is what licenses the exponent arithmetic.

def LambdaS.Tw.keyMult {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} (L : List (Tw B k Θ Shape.scalar × ℚ)) (a : Tw B k Θ Shape.scalar) : ℚ

The total exponent an atom carries in a flattened atom list.

Equations

• LambdaS.Tw.keyMult L a = (List.map (fun (p : LambdaS.Tw B k Θ LambdaS.Shape.scalar × ℚ) => if (p.1 == a) = true then p.2 else 0) L).sum

def LambdaS.Tw.scalarEq {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} (a b : Tw B k Θ Shape.scalar) : Bool

Decides whether two scalar ratios are equal up to the unit algebra: equal unit-constant parts (one exponent-vector comparison), and equal total exponents on every atom either side mentions. Sound, and strictly wider than Tw.beq: it accepts the same conversions reassociated, reordered, with their unit constants combined differently, and with atom exponents split differently.

Equations

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

theorem LambdaS.Tw.scalarEq_sound {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} (a b : Tw B k Θ Shape.scalar) (h : a.scalarEq b = true) (ψ : Scaling B k) (θρ : TwEnv Θ) : eval ψ a θρ = eval ψ b θρ

scalarEq is sound: it implies evaluation equality in every scaling and every environment: the hypotheses Twist.add, Twist.mapp and Twist.comp carry.

Completeness on the atom-free fragment

The frees-at-one assignment gives each context variable the literal ratio 1. For ratios built from unit expressions, multiplication, division, and rational powers, the flat form is a bare exponent vector. On this atom-free fragment, comparison is complete as well as sound. Unit variables are permitted; unknown argument drifts and residual applications, projections, or unit instantiations are excluded. The separating lemma is scale_eq_iff: scalings tell apart any two distinct exponent vectors, by scaling a base where they differ.

def LambdaS.Tw.AtomFree {B : Type} {k : ℕ} {Θ : List Shape} (t : Tw B k Θ Shape.scalar) : Prop

A scalar ratio is atom-free when its flat form carries no atoms: the ratio is built from unit, mul, div and qpow alone. Under the frees-at-one assignment, context variables contribute 1. Unit variables remain permitted in unit expressions. Unknown argument drifts and residual applications, projections, or unit instantiations fall outside this fragment. Tw.normN_of_atomFree proves that bounded normalization fixes an already atom-free ratio; it does not prove that normalization removes every atom from arbitrary generated ratios.

Equations

• t.AtomFree = (t.flat.2 = [])

theorem LambdaS.Tw.scalarEq_complete {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} (a b : Tw B k Θ Shape.scalar) (ha : a.AtomFree) (hb : b.AtomFree) (h : ∀ (ψ : Scaling B k), eval ψ a (oneTwEnv Θ) = eval ψ b (oneTwEnv Θ)) : a.scalarEq b = true

The comparison is complete on the atom-free fragment. Two atom-free scalar ratios that evaluate equal under every scaling compare equal: each value is ψ.scale of the flat form's unit part, and scalings separate distinct exponent vectors (scale_eq_iff), so agreement in every scaling forces the unit parts to be the same vector, which Tw.scalarEq accepts.

theorem LambdaS.Tw.scalarEq_iff_eval_eq {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} (a b : Tw B k Θ Shape.scalar) (ha : a.AtomFree) (hb : b.AtomFree) : a.scalarEq b = true ↔ ∀ (ψ : Scaling B k) (θρ : TwEnv Θ), eval ψ a θρ = eval ψ b θρ

The comparison is exact on the atom-free fragment: for atom-free scalar ratios, Tw.scalarEq answers true precisely when the two ratios evaluate equal under every scaling and every environment. Tw.normEq_iff_eval_eq carries this to Tw.normEq, the comparison twistOf runs.

Exact first-order branch comparison

For a first-order context, openNF reflects independent unknown components and performs structural symbolic evaluation. All internal applications and unit binders are supported. When the context contains an unknown function or unit family, the bounded normalizer Tw.norm and sound opaque-atom algebra provide a conservative comparison. Only that higher-order-context fallback uses fuel.

def LambdaS.Tw.normEq {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} (a b : Tw B k Θ Shape.scalar) : Bool

The ratio comparison twistOf runs. At first-order contexts it compares Tw.openNF normal forms, which is exact (Tw.normEq_firstOrder_iff); otherwise it compares Tw.norm forms by Tw.scalarEq, which is sound but not proved complete.

Equations

• a.normEq b = if LambdaS.ratioFirstOrder Θ = true then decide (a.openNF = b.openNF) else a.norm.scalarEq b.norm

theorem LambdaS.Tw.normEq_sound {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} (a b : Tw B k Θ Shape.scalar) (h : a.normEq b = true) (ψ : Scaling B k) (θρ : TwEnv Θ) : eval ψ a θρ = eval ψ b θρ

Every accepted comparison holds at arbitrary scalings and ratio environments.

theorem LambdaS.Tw.normEq_firstOrder_iff {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} (a b : Tw B k Θ Shape.scalar) (hΘ : ratioFirstOrder Θ = true) : a.normEq b = true ↔ ∀ (ψ : Scaling B k) (ρ : TwEnv Θ), eval ψ a ρ = eval ψ b ρ

Exactness for first-order contexts, including open independent scalar drifts and arbitrary internal higher-order and unit-polymorphic ratio syntax.

theorem LambdaS.Tw.normEq_of_legacy {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} (a b : Tw B k Θ Shape.scalar) (h : a.norm.scalarEq b.norm = true) : a.normEq b = true

Tw.normEq accepts every pair that the bounded comparison Tw.scalarEq a.norm b.norm accepts: at first-order contexts by exactness, elsewhere by definition.

theorem LambdaS.Tw.normN_of_atomFree {B : Type} {k : ℕ} {Θ : List Shape} (n : ℕ) (t : Tw B k Θ Shape.scalar) : t.AtomFree → normN n t = t

Normalization fixes an atom-free ratio: there is nothing to reduce in a term built from unit, mul, div and qpow.

theorem LambdaS.Tw.normEq_iff_eval_eq {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} (a b : Tw B k Θ Shape.scalar) (ha : a.AtomFree) (hb : b.AtomFree) : a.normEq b = true ↔ ∀ (ψ : Scaling B k) (θρ : TwEnv Θ), eval ψ a θρ = eval ψ b θρ

Exactness for atom-free ratios, in any context. At first-order contexts Tw.normEq_firstOrder_iff drops the atom-freeness hypotheses.

def LambdaS.Tw.agree {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} {s : Shape} : Tw B k Θ s → Tw B k Θ s → Bool

Agreement of two ratios at a shape, the check ifle runs on its branches. At scalar shape it is Tw.normEq, the add check; at vector and matrix shapes it is Tw.normEq per component, exactly as mapp and comp check per output component, with entries extracted by projE/rowE so that literals compare by their components; at the function and binder shapes, which have no first-order normal form, it is syntactic identity.

Equations

• a.agree b = a.normEq b
• a_1.agree b = decide (∀ (i : Fin a), (a_1.projE i).normEq (b.projE i) = true)
• a_2.agree b = decide (∀ (j : Fin a_1) (i : Fin a), ((a_2.rowE j).projE i).normEq ((b.rowE j).projE i) = true)
• a_2.agree b = a_2.beq b
• a_1.agree b = a_1.beq b

theorem LambdaS.Tw.agree_sound {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} {s : Shape} (a b : Tw B k Θ s) : a.agree b = true → ∀ (ψ : Scaling B k) (θρ : TwEnv Θ), eval ψ a θρ = eval ψ b θρ

Ratios that agree evaluate equally, in every scaling and environment.

def LambdaS.mappDrift {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} {n m : ℕ} (tf : Tw B k Θ (Shape.mat n m)) (tx : Tw B k Θ (Shape.vec n)) : Option ((tw : Tw B k Θ (Shape.vec m)) ×' ∀ (ψ : Scaling B k) (θρ : TwEnv Θ) (a : Fin m) (i : Fin n), Tw.eval ψ tf θρ a i * Tw.eval ψ tx θρ i = Tw.eval ψ tw θρ a)

The drift of a matrix application, when the analysis can name one. Per output row a, the products of an entry drift with the matching argument drift must agree across the row up to β-reduction and the unit algebra (Tw.normEq, exactly the add check), and the representative at column 0 is the row's output drift. Entries are extracted with projE/rowE so that literal rows compare by their components rather than as opaque projections. Over the empty domain the sum is empty and the output is the zero vector, so the output drift is 1 per component.

Equations

• One or more equations did not get rendered due to their size.
• LambdaS.mappDrift x x_1 = some ⟨LambdaS.Tw.vecOfFn fun (x : Fin m) => LambdaS.Tw.unit 1, ⋯⟩

def LambdaS.compDrift {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {Θ : List Shape} {p n m : ℕ} (tf : Tw B k Θ (Shape.mat n m)) (tg : Tw B k Θ (Shape.mat p n)) : Option ((tw : Tw B k Θ (Shape.mat p m)) ×' ∀ (ψ : Scaling B k) (θρ : TwEnv Θ) (a : Fin m) (i : Fin p) (b : Fin n), Tw.eval ψ tf θρ a b * Tw.eval ψ tg θρ b i = Tw.eval ψ tw θρ a i)

The drift of a composition, when the analysis can name one: the analogue of mappDrift per entry (a, i), with agreement across the middle index and the representative taken at middle index 0.

Equations

• One or more equations did not get rendered due to their size.
• LambdaS.compDrift x x_1 = some ⟨LambdaS.Tw.matOfFn fun (x : Fin m) => LambdaS.Tw.vecOfFn fun (x : Fin p) => LambdaS.Tw.unit 1, ⋯⟩

def LambdaS.twistOf {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {τ : Ty B D j k} (p : ℕ) (Θ : List Shape) (hΘ : Θ = Γ.shapes) (d : HasTy Δ Γ e τ) : Option ((t : Tw B k Θ τ.shape) ×' Twist p Θ d t)

Computing the ratio. For a derivation, the accumulated conversion ratio together with its Twist derivation, or none where the analysis does not apply. The pin marker p is the frees-at-one assignment: a variable below p is lam-bound and enters as an atom, a variable at or beyond p is a context variable of the program and enters at the literal ratio 1. The exported diagnostic runs at p = 0.

The add check is Tw.normEq. For first-order ratio contexts it compares fuel-free symbolic normal forms with an independent coordinate for every input component (Tw.normEq_firstOrder_iff). Internal functions and unit binders are evaluated structurally without a reduction bound. The unit algebra merges conversions that are reordered, reassociated, or split into rational powers; positivity makes cancellation sound. Unknown function or unit-family inputs select the bounded Tw.norm and opaque-atom comparison, which is sound but not proved complete. Atom-free ratios compare exactly in any context (Tw.normEq_iff_eval_eq). ifle runs the check on its compared quantities and, per component (Tw.agree), on its branches. mapp and comp run the same check per output component, across the summed index, and log and exp run it against the literal ratio 1, accepting exactly the arguments whose ratio is identifiably trivial. Everything downstream of the checks is complete: Tw.nfOne decides triviality of the resulting ratio exactly.

The diagnostic, end to end

def LambdaS.unitDrift {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {u : UExp B k} {e : Tm B D j k} (d : HasTy Δ (scalarCtx us) e (Ty.Q u)) : Option (UExp B k)

Unit drift: the normal form of a program's accumulated conversion ratio, computed from its derivation. some 1 means the conversions cancel; some w with w ≠ 1 exhibits the drift; none means the analysis does not apply (a ucon; a log or exp whose argument ratio is not identifiably trivial; or an add, ifle, mapp or comp whose compared ratios Tw.normEq cannot identify).

Equations

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

def LambdaS.unitDriftGen {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {V W : Sp B k} {e : Tm B D j k} (d : HasTy Δ Γ e (Ty.lin V W)) : Option (Fin (List.length W) → Fin (List.length V) → UExp B k)

Unit drift at a matrix result over an arbitrary context: one normal ratio per entry, or none.

unitDriftLin takes a scalar context only because its theorem uses twRelEnv_scaleEnv, which constructs the rescaled environment and can do so only at scalar types. scaleLaw_lin_of_driftFree_gen instead takes the environment relation as a hypothesis: the relation specifies "each argument rescaled as its type prescribes", and constructing one is the caller's business.

Equations

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

def LambdaS.unitDriftLin {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {V W : Sp B k} {e : Tm B D j k} (d : HasTy Δ (scalarCtx us) e (Ty.lin V W)) : Option (Fin (List.length W) → Fin (List.length V) → UExp B k)

Unit drift at a matrix result: one normal ratio per entry.

A scalar program has a drift, a vector-valued one a drift vector (unitDriftVec), and a map-valued one a drift table, because TwRel at .lin charges each entry separately. A single ratio would be wrong unless the entries happened to agree, so this reports the table and lets the caller ask what it wants of it. A table constantly 1 gives the type's scaling law (scaleLaw_lin_of_driftFree, below); no converse is proved here.

Equations

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

noncomputable def LambdaS.scaleLinVal {B : Type} [Fintype B] {k : ℕ} {V W : Sp B k} (ψ : Scaling B k) (A : Fin (List.length W) → Fin (List.length V) → ℝ) : Fin (List.length W) → Fin (List.length V) → ℝ

Rescale a map-valued argument the way its type prescribes: entry (a,i) by ψ(W a) / ψ(V i), which is Hart's rank-one factor.

Equations

• LambdaS.scaleLinVal ψ A a i = ψ.scale (List.get W a) / ψ.scale (List.get V i) * A a i

theorem LambdaS.twRelEnv_scaleLinVal {B D : Type} [Fintype B] {j k : ℕ} (φ ψ : Scaling B k) {V W : Sp B k} (A : Fin (List.length W) → Fin (List.length V) → ℝ) (u : PUnit.{1}) : TwRelEnv φ ψ [Ty.lin V W] [Shape.mat (List.length V) (List.length W)] (oneTwEnv [Shape.mat (List.length V) (List.length W)]) (oneTwEnv [Shape.mat (List.length V) (List.length W)]) (A, u) (scaleLinVal ψ A, u)

A one-map environment is related to its own rescaling at trivial ratios.

The map-valued analogue of twRelEnv_scaleEnv, and the piece that lets scaleLaw_lin_of_driftFree_gen be applied to a kernel that takes a matrix rather than its entries.

theorem LambdaS.scaleLaw_lin_of_driftFree_gen {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {V W : Sp B k} {e : Tm B D j k} {d : HasTy Δ Γ e (Ty.lin V W)} {w : Fin (List.length W) → Fin (List.length V) → UExp B k} (hd : unitDriftGen d = some w) (h1 : ∀ (a : Fin (List.length W)) (i : Fin (List.length V)), w a i = 1) (V₀ ψ : Scaling B k) {ρ ρ' : Env Γ} (hr : TwRelEnv Scaling.zero ψ Γ Γ.shapes (oneTwEnv Γ.shapes) (oneTwEnv Γ.shapes) ρ ρ') (a : Fin (List.length W)) (i : Fin (List.length V)) : den V₀ d ρ' a i = ψ.scale (List.get W a) / ψ.scale (List.get V i) * den V₀ d ρ a i

The scaling law at a matrix result, over any context at all.

With the valuation held fixed, rescale the arguments however their types prescribe, which is what TwRelEnv at trivial ratios says, and a drift-free map moves entry (a,i) by exactly ψ(W a) / ψ(V i).

scaleLaw_lin_of_driftFree is this with the environment relation supplied by twRelEnv_scaleEnv, which is available only at scalar arguments. A caller with a map-valued argument proves the relation for it directly; at first order that is the entrywise equation and nothing more.

theorem LambdaS.scaleLaw_lin_of_driftFree {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {V W : Sp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.lin V W)} {w : Fin (List.length W) → Fin (List.length V) → UExp B k} (hd : unitDriftLin d = some w) (h1 : ∀ (a : Fin (List.length W)) (i : Fin (List.length V)), w a i = 1) (V₀ ψ : Scaling B k) (ρ : Env (scalarCtx us)) (a : Fin (List.length W)) (i : Fin (List.length V)) : den V₀ d (scaleEnv ψ us ρ) a i = ψ.scale (List.get W a) / ψ.scale (List.get V i) * den V₀ d ρ a i

A drift-free map obeys its type's scaling law, entry by entry.

The matrix analogue of scaleLaw_of_driftFree, and the theorem that connects the diagnostic to dimensioned linear algebra (Section 9 of the paper). When every entry of the drift table is trivial, rescaling the arguments moves entry (a,i) by exactly ψ(W a) / ψ(V i), the factor Hart's rank-one form assigns it, and by nothing else.

def LambdaS.unitDriftVecGen {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {U : Sp B k} {e : Tm B D j k} (d : HasTy Δ Γ e (Ty.vec U)) : Option (Fin (List.length U) → UExp B k)

Unit drift at a vector result over an arbitrary context: one normal ratio per component, or none.

The vector counterpart of unitDriftGen. TwRel at .vec charges each component separately, so a vector-valued program has a drift vector rather than a single drift; scaleLaw_vec_of_driftFree_gen is its scaling law.

Equations

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

def LambdaS.unitDriftVec {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {U : Sp B k} {e : Tm B D j k} (d : HasTy Δ (scalarCtx us) e (Ty.vec U)) : Option (Fin (List.length U) → UExp B k)

Unit drift at a vector result: one normal ratio per component, over a context of scalars. The vector counterpart of unitDriftLin; its scaling law is scaleLaw_vec_of_driftFree.

Equations

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

noncomputable def LambdaS.scaleVecVal {B : Type} [Fintype B] {k : ℕ} {U : Sp B k} (ψ : Scaling B k) (v : Fin (List.length U) → ℝ) : Fin (List.length U) → ℝ

Rescale a vector-valued argument the way its type prescribes: component i by ψ(U i).

Equations

• LambdaS.scaleVecVal ψ v i = ψ.scale (List.get U i) * v i

theorem LambdaS.twRelEnv_scaleVecVal {B D : Type} [Fintype B] {j k : ℕ} (φ ψ : Scaling B k) {U : Sp B k} (v : Fin (List.length U) → ℝ) (u : PUnit.{1}) : TwRelEnv φ ψ [Ty.vec U] [Shape.vec (List.length U)] (oneTwEnv [Shape.vec (List.length U)]) (oneTwEnv [Shape.vec (List.length U)]) (v, u) (scaleVecVal ψ v, u)

A one-vector environment is related to its own rescaling at trivial ratios: the vector-valued analogue of twRelEnv_scaleLinVal, which lets scaleLaw_vec_of_driftFree_gen be applied to a program that takes a vector.

theorem LambdaS.scaleLaw_vec_of_driftFree_gen {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {U : Sp B k} {e : Tm B D j k} {d : HasTy Δ Γ e (Ty.vec U)} {w : Fin (List.length U) → UExp B k} (hd : unitDriftVecGen d = some w) (h1 : ∀ (i : Fin (List.length U)), w i = 1) (V₀ ψ : Scaling B k) {ρ ρ' : Env Γ} (hr : TwRelEnv Scaling.zero ψ Γ Γ.shapes (oneTwEnv Γ.shapes) (oneTwEnv Γ.shapes) ρ ρ') (i : Fin (List.length U)) : den V₀ d ρ' i = ψ.scale (List.get U i) * den V₀ d ρ i

The scaling law at a vector result, over any context at all.

The vector counterpart of scaleLaw_lin_of_driftFree_gen. With the valuation held fixed, rescale the arguments however their types prescribe (TwRelEnv at trivial ratios), and a program whose drift vector is trivial moves component i by exactly ψ(U i), the factor its type predicts.

theorem LambdaS.scaleLaw_vec_of_driftFree {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {U : Sp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.vec U)} {w : Fin (List.length U) → UExp B k} (hd : unitDriftVec d = some w) (h1 : ∀ (i : Fin (List.length U)), w i = 1) (V₀ ψ : Scaling B k) (ρ : Env (scalarCtx us)) (i : Fin (List.length U)) : den V₀ d (scaleEnv ψ us ρ) i = ψ.scale (List.get U i) * den V₀ d ρ i

A drift-free vector obeys its type's scaling law, component by component. The vector counterpart of scaleLaw_lin_of_driftFree: when every component of the drift vector is trivial, rescaling the scalar arguments moves component i by exactly ψ(U i), and by nothing else.

theorem LambdaS.unitDrift_spec {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {u : UExp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.Q u)} {w : UExp B k} (hw : unitDrift d = some w) (V : Scaling B k) {ρ : Env (scalarCtx us)} (hne : den V d ρ ≠ 0) : (∀ (ψ : Scaling B k), den (V.comp ψ) d (scaleEnv ψ us ρ) = ψ.scale u * den V d ρ) ↔ w = 1

The diagnostic is exact. When unitDrift answers, invariance under every rescaling holds precisely when the answer is 1, for a term whose denotation at the given environment is nonzero (hne: the zero function is invariant whatever its ratio, so it is the one term the drift cannot see).

This is the compiler check: one group computation per derivation, one equality of exponent vectors, and the program's dependence on the declared unit magnitudes is decided, with unit polymorphism, higher-order structure and conversion chains all handled by the one computation.

Top-level abstractions as inputs

A first-order kernel is as often written λx. λy. e as it is written as an open term over a context. The two spellings name the same inputs, so the diagnostic should give them the same verdict.

def LambdaS.unitDriftLam {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {τ : Ty B D j k} : HasTy Δ Γ e τ → Option (UExp B k)

Unit drift, through leading abstractions. Strips the leading lam binders and analyzes the body over the extended context with the all-ones assignment (p = 0): every stripped binder is a program input, pinned at ratio 1 exactly as a context variable is, so a lambda-wrapped kernel receives the same verdict as its open-term spelling. Abstractions in non-leading position keep their atoms. Answers at quantity-typed bodies and returns none elsewhere, exactly as unitDrift.

Equations

• One or more equations did not get rendered due to their size.
• LambdaS.unitDriftLam db.lam = LambdaS.unitDriftLam db
• LambdaS.unitDriftLam x✝ = none

theorem LambdaS.twistOf_nfOne_irrel {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {u : UExp B k} (d : HasTy Δ Γ e (Ty.Q u)) {Θ Θ' : List Shape} (hΘ : Θ = Γ.shapes) (hΘ' : Θ' = Γ.shapes) : Option.map (fun (p : (t : Tw B k Θ (Ty.Q u).shape) ×' Twist 0 Θ d t) => p.fst.nfOne) (twistOf 0 Θ hΘ d) = Option.map (fun (p : (t : Tw B k Θ' (Ty.Q u).shape) ×' Twist 0 Θ' d t) => p.fst.nfOne) (twistOf 0 Θ' hΘ' d)

The verdict read off a ratio does not depend on how the shape list was presented: the two proofs that it is the context's are interchangeable.

theorem LambdaS.unitDriftLam_eq_unitDrift {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {u : UExp B k} {e : Tm B D j k} (d : HasTy Δ (scalarCtx us) e (Ty.Q u)) : unitDriftLam d = unitDrift d

The stripped kernel is analyzed as an open term. At a quantity type over a scalar context, unitDriftLam is unitDrift.

theorem LambdaS.unitDriftLam_spec {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {σ u : UExp B k} {e : Tm B D j k} {db : HasTy Δ (scalarCtx (σ :: us)) e (Ty.Q u)} {w : UExp B k} (hw : unitDriftLam db.lam = some w) (V : Scaling B k) {ρ : Env (scalarCtx us)} {x : ℝ} (hne : den V db.lam ρ x ≠ 0) : (∀ (ψ : Scaling B k), den (V.comp ψ) db.lam (scaleEnv ψ us ρ) (ψ.scale σ * x) = ψ.scale u * den V db.lam ρ x) ↔ w = 1

Through a leading abstraction. The verdict on λx:Q σ. e is the verdict on e over the context extended by x (definitionally), and the diagnostic is exact for the abstraction applied to any input: for x with (λx. e) x ≠ 0, rescaling the input by σ's factor together with the context rescales the output by u's factor, under every rescaling, exactly when the drift is 1. Each further leading binder is the same step again, since unitDriftLam (.lam db) = unitDriftLam db by definition and the denotation of an abstraction is the function it denotes.

Closing the loop with the declarations

The twisted law has two parameters, and holding each at the trivial scaling in turn yields the two statements a drift diagnosis is for. With the values held fixed, a program's dependence on the declared unit magnitudes is exactly its drift: drift 1 is declaration independence at any result unit, for open programs as for closed ones. With the valuation held fixed, a drift-free program obeys the unrestricted scaling law of scaleLaw, which is the hypothesis the Pi theorem consumes, now supplied by the drift analysis rather than by the absence of conversion. Composed with adequacy, the first statement holds of evaluation with real arithmetic for a closed program at Q 1: its output is invariant across every consistent extension of the declaration set. This is the ratio-level analogue of evalC_convert_declared: Twist joined to Declare the way eval_adeq joined Dynamics to Declare.

theorem LambdaS.Scaling.comp_sub {B : Type} {k : ℕ} (V V' : Scaling B k) : V.comp { base := fun (b : B) => V'.base b - V.base b, vars := fun (i : Fin k) => V'.vars i - V.vars i } = V'

Any scaling is reachable from any other by composition: log-space is a group.

theorem LambdaS.unitDrift_law {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {u : UExp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.Q u)} {w : UExp B k} (hw : unitDrift d = some w) (V φ ψ : Scaling B k) (ρ : Env (scalarCtx us)) : den (V.comp φ) d (scaleEnv ψ us ρ) = ψ.scale u * (φ.scale w * ψ.scale w) * den V d ρ

The drift law. A program with unit drift w rescales, under a rescaling φ of the valuation and ψ of its arguments, by its unit's factor under ψ times w's factor under each: Twist.law with the ratio's two values read off its normal form (Tw.eval_oneTwEnv).

theorem LambdaS.den_comp_of_drift {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {u : UExp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.Q u)} {w : UExp B k} (hw : unitDrift d = some w) (V φ : Scaling B k) (ρ : Env (scalarCtx us)) : den (V.comp φ) d ρ = φ.scale w * den V d ρ

Declared magnitudes enter through the drift alone. With the arguments held fixed, rescaling the valuation by φ multiplies a program of drift w by φ(w): the drift the diagnostic exhibits is the program's exact dependence on the unit system.

theorem LambdaS.den_indep_of_driftFree {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {u : UExp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.Q u)} (h1 : unitDrift d = some 1) (V V' : Scaling B k) (ρ : Env (scalarCtx us)) : den V d ρ = den V' d ρ

Drift-free programs are declaration-independent. A program with canceling conversions denotes, at every environment, the same number under every valuation, however the units it converts between are declared. Open programs at any unit included: the drift is the only route by which a declared magnitude reaches the result.

theorem LambdaS.scaleLaw_of_driftFree {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {u : UExp B k} {e : Tm B D j k} {d : HasTy Δ (scalarCtx us) e (Ty.Q u)} (h1 : unitDrift d = some 1) (V ψ : Scaling B k) (ρ : Env (scalarCtx us)) : den V d (scaleEnv ψ us ρ) = ψ.scale u * den V d ρ

Drift-free programs obey the unrestricted scaling law. With the valuation held fixed, rescaling the arguments of a drift-free program by their units' factors rescales its result by its own: the conclusion of scaleLaw for a program that converts, provided its conversions cancel. The hypothesis the Pi theorem consumes, supplied by the drift analysis (den_mulScaleLaw_driftFree).

theorem LambdaS.evalC_indep_of_driftFree {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {e : Tm B D 0 0} {d : HasTy (DCtx.nil D) [] e (Ty.Q 1)} (h1 : unitDrift d = some 1) (V V' : Scaling B 0) : ∃ (n : ℕ) (n' : ℕ) (m : ℝ), evalC (conv V) n [] e = some (Val.scalar { mag := m, unit := 1 }) ∧ evalC (conv V') n' [] e = some (Val.scalar { mag := m, unit := 1 })

The program is declaration-independent, drift-free case. The evaluator's output (a scalar at the trivial unit, at carrier ℝ) is the same number under every valuation, hence under every consistent set of unit declarations that the conversion oracle is drawn from. The theorem the diagnostic justifies; the binary runs the same evaluator at Float.