proofs
Provedalphaalpha-core-v0quantitative-typesusage-check

Alpha Core v0: the identity uses its erased type 0 times and its linear value once at runtime

runtimeUses⁡("A" (Term.lambda Quantity.linear "value" (Term.variable "A") (Term.variable "value")) = 0 ∧ runtimeUses "value" (Term.variable "value") = 1)\htmlData{mx=1}{\htmlData{mx=0}{\operatorname{runtimeUses}}(\mathtt{"A"\ (Term.lambda\ Quantity.linear\ "value"\ (Term.variable\ "A")\ (Term.variable\ "value"))\ =\ 0\ \text{∧}\ runtimeUses\ "value"\ (Term.variable\ "value")\ =\ 1})}
What the notation means · or point at any symbol
runtimeUses
runtimeUses: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (runtimeUses)
f(x)Function application
runtimeUses applied to "A" (Term.lambda Quantity.linear "value" (Term.variable "A…. Lean writes f x; papers write f(x). (runtimeUses "A" (Term.lambda Quantity.l…)

The runtime-usage count behind the quantity check: the erased type variable A occurs 0 times at runtime in λ¹ (value : A). value, and the linear variable value occurs exactly once in its body.

How it was proved

Proved
21 October 2026
By
Ajax
Checked by
Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms
Classical.choice, Quot.sound, propext
Proof
7 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements