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 type is τ.subst σ, and Ty.shape_subst is a theorem. It appears once more at mcons, where a row's space is a map over the column space and List.length_map is likewise a theorem.

From the paper's long form: Accumulated Ratios, and a Decidable Diagnostic

The paper's tag long-form carries this section in full; it is reproduced here, converted to Markdown, so the documentation develops what the paper now summarizes. Section references name the module that carries the section; theorem references name the declaration.

With the abstraction theorems in hand, we now ask what many conversions accumulate to. The theorem “Single-conversion invariance” (cvt_rel_iff_coherent, Fundamental.lean) 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 every program its accumulated conversion ratio, 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.

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.

(Figure omitted here; see the ratio calculus (Shape, Tw, SemTw, and Tw.eval in Ratio.lean). Its caption: The ratio calculus Tw (top), the semantic ratios at each shape (middle), and evaluation (bottom), transcribed from the artifact's Shape, Tw, SemTw, and Tw.eval. 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; the shape of Q u is scalar, the shape of a unit quantifier is bind applied to its body's shape, and a dimension binder leaves the shape unchanged. Evaluation reads a ratio under a rescaling ψ and an environment ρ of semantic ratios; (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). The two conses and two projections are distinguished by their shapes, and the vector and matrix formers evaluate componentwise. 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).)

the ratio calculus (Shape, Tw, SemTw, and Tw.eval in Ratio.lean) presents the resulting calculus Tw of ratio expressions and its interpretation, transcribed from the artifact. 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. No substitution lemma for ratios exists.

A judgment Twist relates a typing derivation to its ratio, and the scaling law generalizes the theorem “Abstraction, convert-free” (fundamental_free, Fundamental.lean) 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 constant 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 theorem “Abstraction, convert-free” (fundamental_free, Fundamental.lean); 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 +, and at map application and composition per output component, the analysis compares ratio terms up to β-reduction and the unit algebra (Tw.normEq): each ratio is first normalized (Tw.norm, a fueled β-normalizer that preserves evaluation, Tw.eval_norm), and each scalar normal form flattens to an exponent vector holding all of its unit constants, merged by the group operations, together with a finitely supported assignment of rational exponents to atoms, opaque subratios the flattening cannot evaluate; the comparison is vector against vector and assignment against assignment. Reordered, reassociated, and differently placed conversions are therefore 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. A first-order program's ratios consequently carry no atoms, and there the comparison is exact in both directions: for atom-free ratios, syntactic agreement coincides with equal evaluation under every rescaling (Tw.normEq_iff_eval_eq), so a once both summands have been assigned atom-free ratios, 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.

Under binders the analysis reduces every ratio redex it can see, so a visible application analyzes as its redex (betaShared), and the comparison normalizes the ratios it compares, so a redex that substitution creates is reduced as well (hoSum). What remains is a boundary: two distinct bound atoms are never identified, because whether two arguments will drift alike is a fact about call sites, which a compositional analysis refuses to consult.

The analysis declines one term form unconditionally: 1_u, which the theorem “Abstraction, convert-free” (fundamental_free, Fundamental.lean) places outside the invariance theory. The decline also keeps the report single-voiced. 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. Tracking it is possible (the relation forces the ratio u^(-1/2): the defect is incurred once where conversion's is incurred twice, hence the half exponent), but 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 a closed program's compiled output (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
• 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)))
• 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 β-normalizes as it builds: 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, which is the entire design working as intended.

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, the instantiation they performed already.

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: the program 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.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, and it says precisely what "conversion is the only thing that pays" means: the payment is the accumulated ratio, and unrestricted parametricity charges for exactly that and nothing else. The condition on the right is semantic; Tw.nfOne decides it syntactically, via Tw.nfOne_eq_one_iff.

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. It 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, which normalizes both ratios and compares the normal forms): 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. Under the frees-at-one assignment the program's own context variables contribute the literal ratio 1 rather than atoms, so the ratio of a first-order program without abstractions of its own is atom-free and the ratio-equality check is exact there (Tw.normEq_iff_eval_eq). Once all operands have ratios, the comparison at add, mapp and comp declines only on a genuine ratio disagreement, 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 that atoms are identified only with themselves. Atoms arise under lam binders only; an abstraction applied inside the program leaves none behind, since the comparison reduces every redex, the ones substitution creates included (LambdaS.Examples.hoSum is accepted). 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 decides equality. 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 we compare 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 distinct atoms: an atom is the ratio of a lam-bound variable, standing for a future argument, and nothing relates two arguments' ratios. The program's own context variables produce no atoms at all under the frees-at-one assignment, which is what makes the comparison complete at first order (Tw.scalarEq_complete, lifted to normal forms by Tw.normEq_iff_eval_eq). 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

With the frees-at-one assignment, a first-order program's ratios contain no atoms at all: every context variable contributes the literal ratio 1, so the flat form is a bare exponent vector. On that fragment the comparison is complete, not merely sound. 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 this is the ratio of every first-order program without abstractions of its own: lam-bound variables are the only variables there are, and the comparison normalizes away every redex an internal application leaves (Tw.normN_of_atomFree).

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. With the frees-at-one assignment this covers every first-order program without abstractions of its own, and for those the conditional declines at add, mapp and comp are exactly the genuine drift disagreements.

The comparison on normal forms

A redex that substitution creates (a lam-bound variable in head position, instantiated by an abstraction) is an app node to Tw.flat, hence an atom. Comparing normal forms (Tw.norm) removes every such residue: after normalization the only atoms left are lam-bound variables themselves and their projections, which stand for arguments not yet supplied.

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

The branch comparison, run on β-normal forms.

Equations

• a.normEq b = 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 θρ

normEq is sound: normalization preserves evaluation, and scalarEq is sound on the normal forms.

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 θρ

The comparison on normal forms is exact on the atom-free fragment: Tw.scalarEq_iff_eval_eq, since normalization fixes an atom-free ratio.

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: branch ratios are β-normalized (Tw.norm) and their normal forms compare with their unit constants merged into one exponent vector and their atoms as coordinates of a free ℚ-vector space, one total exponent per atom, so the same conversions reordered, reassociated, split into different rational powers, and canceled against themselves across the fraction bar are all accepted; the positive scalar carrier is what makes x / x = 1 sound. What the check never does is identify distinct atoms, since nothing relates two arguments' ratios; but atoms arise only under lam binders, so a first-order ratio has none and the check is exact there (Tw.normEq_iff_eval_eq). 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 whose branch 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.

twistOf never wanted a scalar context; only unitDrift's wrapper did, and only because twRelEnv_scaleEnv constructs the rescaled environment and knows how to do that at scalar types alone. Taking the environment relation as a hypothesis instead removes the restriction without proving anything new: the relation is the specification of "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 map-valued one has a drift table, because TwRel at .lin charges each entry separately. Reporting a single ratio would be a lie unless the entries happened to agree, so this reports the table and lets the caller ask what it wants of it. Invariance is the table constantly 1, which is scaleLaw_lin_of_driftFree below.

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.

The context restriction is gone. 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 puts the linear-algebra section and the diagnostic in the same room. 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.

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 first-order type, 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 the compiled program: 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.