A Property Kind Calculus for Measurement Metrology

14.1. Functions on quantities🔗

Definition14.1.1
Group: The algebraic calculus rides on the toolchain classes for multiplication, division, and reciprocal. There is no toolchain class for exp , sin , or square root, so the one genuinely new artifact is a carrier capability — the function-layer analogue of the numeric carrier — and a family of smart constructors that each carry their own metrological discipline. The functions split into five families with genuinely different kind signatures: kind-preserving ( abs , min , max ); powers and roots (the dimension scales by the exponent); dimensionless transcendentals ( exp , log — pure number in, pure number out); the trigonometric functions (a plane angle in, a number out — curated so that sin of a reflectivity stays a category error); and logarithmic levels (dB, neper — where log of a ratio demotes the scale, so the product calculus correctly refuses it). (4)
Group member previews
Preview
Definition 14.1.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

\mathrm{MathCarrier}\ R is the function operation surface a kind-indexed magnitude needs — \exp, \log, \sin, \cos, the hyperbolic functions, \sqrt{\,}, |\cdot|, and the constant \pi — supplied once per representation type R. It is the function-layer analogue of the numeric carrier Carrier, and is by construction the same surface as the underlying tensor toolchain's elementary functions, so every carrier that supports them — \mathbb{R}, Float, the binary32 carriers — is a clean \mathrm{MathCarrier}.

Lean code for Definition14.1.1●1 definition
  • class(10 methods)defined in PropertyKindCalculus/QuantityFunction.lean
    complete
    class PropertyKindCalculus.MathCarrier (R : Type) : Type
    class PropertyKindCalculus.MathCarrier
  (R : Type) : Type
    **The function operation surface.** The transcendental and root operations a
kind-indexed magnitude needs, supplied once per representation type `R`. This is the
function-layer analogue of `Carrier`, and is deliberately the *same* surface as
TorchLean's `MathFunctions α`, so any carrier supporting `MathFunctions` (`ℝ`, `Float`,
binary32) instantiates it cleanly.

    Methods

    exp : R → R
    Natural exponential. 
    log : R → R
    Natural logarithm. 
    sin : R → R
    Sine. 
    cos : R → R
    Cosine. 
    sinh : R → R
    Hyperbolic sine. 
    cosh : R → R
    Hyperbolic cosine. 
    tanh : R → R
    Hyperbolic tangent. 
    sqrt : R → R
    Square root. 
    abs : R → R
    Absolute value. 
    pi : R
    The constant `π`.
Proof for Definition 14.1.1
uses 0

Realized as the MathCarrier class. The richer surface (\tan, the inverse trig, \operatorname{atan2}, cube root, rounding, rational power) is split off into MathCarrierExt, so the executable binary32 carrier — whose function vocabulary is deliberately smaller — is a MathCarrier without being a MathCarrierExt. The algebraic identities (\sin^2+\cos^2=1, \exp(a+b)=\exp a\cdot\exp b) live in LawfulMathCarrier, which holds at \mathbb{R} and fails in floating point — the same exec/spec gap the lawful numeric carrier draws for +. The Float instance is computable (the run carrier); the \mathbb{R} instance is the noncomputable proof carrier in the PhysLib-backed Dimension layer.

Definition14.1.2
Group: The algebraic calculus rides on the toolchain classes for multiplication, division, and reciprocal. There is no toolchain class for exp , sin , or square root, so the one genuinely new artifact is a carrier capability — the function-layer analogue of the numeric carrier — and a family of smart constructors that each carry their own metrological discipline. The functions split into five families with genuinely different kind signatures: kind-preserving ( abs , min , max ); powers and roots (the dimension scales by the exponent); dimensionless transcendentals ( exp , log — pure number in, pure number out); the trigonometric functions (a plane angle in, a number out — curated so that sin of a reflectivity stays a category error); and logarithmic levels (dB, neper — where log of a ratio demotes the scale, so the product calculus correctly refuses it). (4)
Group member previews
Preview
Definition 14.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 3
Reverse dependency previews
Preview
Definition 14.1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

\mathrm{PowerKind}\ p\ k_1\ k records that raising a k_1-quantity to the rational power p yields a k-quantity (k = k_1^{\,p}). In the core it carries only the ratio-scale gate (Dybkær §13.3.5 — only ratio quantities have powers); the dimension layer strengthens it to the exponent-scaling certificate \dim k = (\dim k_1)^{p}. This is the one function family that is not dimension-one-in-out — the dimension-scaling extension of multiplication and division.

Lean code for Definition14.1.2●1 definition
  • structure(2 fields)defined in PropertyKindCalculus/QuantityFunction.lean
    complete
    structure PropertyKindCalculus.PowerKind (p : ℚ)
  (k₁ k : PropertyKindCalculus.KindOfProperty) : Prop
    structure PropertyKindCalculus.PowerKind (p : ℚ)
  (k₁ k :
    PropertyKindCalculus.KindOfProperty) :
  Prop
    **A kind-level power law.** `k` is the `p`-th power kind of `k₁` (`k = k₁^p`): both
ratio-scale. The `Dimension` layer strengthens this with `k.dim = (k₁.dim)^p`.

    Fields

    ratio₁ : k₁.IsRational
    The base is ratio-scale. 
    ratioPow : k.IsRational
    The power is ratio-scale.
Proof for Definition 14.1.2
uses 1

Realized as the PowerKind structure (two ratio-scale fields), with the smart constructors Quantity.sqrt (the half-power), Quantity.cbrt, and Quantity.rpow. The exponent-scaling refinement is DimPowerKind, well-defined because PhysLib's Dimension carries \mathbb{Q} exponents (Pow Dimension ℚ), making a half-power a genuine group element.

Definition14.1.3
Group: The algebraic calculus rides on the toolchain classes for multiplication, division, and reciprocal. There is no toolchain class for exp , sin , or square root, so the one genuinely new artifact is a carrier capability — the function-layer analogue of the numeric carrier — and a family of smart constructors that each carry their own metrological discipline. The functions split into five families with genuinely different kind signatures: kind-preserving ( abs , min , max ); powers and roots (the dimension scales by the exponent); dimensionless transcendentals ( exp , log — pure number in, pure number out); the trigonometric functions (a plane angle in, a number out — curated so that sin of a reflectivity stays a category error); and logarithmic levels (dB, neper — where log of a ratio demotes the scale, so the product calculus correctly refuses it). (4)
Group member previews
Preview
Definition 14.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 14.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 5
Reverse dependency previews
Preview
Definition 14.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsproved

\mathrm{Quantity.sqrt} is the verified half-power, the canonical PowerKind (1/2) smart constructor: \sqrt{\,} of a k_1 yields a k, its magnitude \sqrt{a} taken in the carrier. It rides on the base MathCarrier (not the extended surface), so it runs even on the binary32 executable carrier.

Lean code for Definition14.1.3●1 definition
  • defdefined in PropertyKindCalculus/QuantityFunction.lean
    complete
    def PropertyKindCalculus.Quantity.sqrt
  {k₁ k : PropertyKindCalculus.KindOfProperty} {R : Type}
  [PropertyKindCalculus.MathCarrier R]
  (_h : PropertyKindCalculus.PowerKind (1 / 2) k₁ k)
  (a : PropertyKindCalculus.Quantity k₁ R) :
  PropertyKindCalculus.Quantity k R
    def PropertyKindCalculus.Quantity.sqrt
  {k₁ k :
    PropertyKindCalculus.KindOfProperty}
  {R : Type}
  [PropertyKindCalculus.MathCarrier R]
  (_h :
    PropertyKindCalculus.PowerKind (1 / 2)
      k₁ k)
  (a :
    PropertyKindCalculus.Quantity k₁ R) :
  PropertyKindCalculus.Quantity k R
    **Square root** — the half-power, available from the base `MathCarrier` (so it runs
even on the binary32 exec carrier). `sqrt` of an area is a length.
Proof for Definition 14.1.3
uses 0

Realized as Quantity.sqrt, taking a PowerKind (1/2) k₁ k and returning ⟨\mathrm{MathCarrier.sqrt}\ a.\mathrm{magnitude}⟩; the projection sqrt_magnitude is rfl, so an erased computation is exactly the carrier's \sqrt{\,}.

Theorem14.1.4
Group: The algebraic calculus rides on the toolchain classes for multiplication, division, and reciprocal. There is no toolchain class for exp , sin , or square root, so the one genuinely new artifact is a carrier capability — the function-layer analogue of the numeric carrier — and a family of smart constructors that each carry their own metrological discipline. The functions split into five families with genuinely different kind signatures: kind-preserving ( abs , min , max ); powers and roots (the dimension scales by the exponent); dimensionless transcendentals ( exp , log — pure number in, pure number out); the trigonometric functions (a plane angle in, a number out — curated so that sin of a reflectivity stays a category error); and logarithmic levels (dB, neper — where log of a ratio demotes the scale, so the product calculus correctly refuses it). (4)
Group member previews
Preview
Definition 14.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 14.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
EffortsmallTagsproved

The square root of an area is a length — checked, not annotated. The half-power of the area dimension \mathrm{L}^2 is the length dimension \mathrm{L}: \dim(\sqrt{\mathrm{area}}) = (\dim \mathrm{area})^{1/2} = \mathrm{L}. The certificate Quantity.sqrt carries, here discharged in the PhysLib Dimension group. Builds on the power law.

Lean code for Theorem14.1.4●1 theorem
  • theoremdefined in PropertyKindCalculus/Function.lean
    complete
    theorem PropertyKindCalculus.sqrt_area_coherent :
  PropertyKindCalculus.DimPowerKind (1 / 2) PropertyKindCalculus.areaK
    PropertyKindCalculus.lengthKind
    theorem PropertyKindCalculus.sqrt_area_coherent :
  PropertyKindCalculus.DimPowerKind
    (1 / 2) PropertyKindCalculus.areaK
    PropertyKindCalculus.lengthKind
    **`sqrt` of an area is a length — checked, not annotated.** The half-power of the
area dimension `L²` is the length dimension `L`: `dim(√area) = (dim area)^(1/2) = L`.
This is the certificate the core `Quantity.sqrt` carries, here discharged in the
`Dimension` group.
Proof for Theorem 14.1.4
uses 0

Proved in the Function module: areaK is declared with dimension \mathrm{L}^2 and the goal lengthKind.dim = areaK.dim ^ (1/2 : ℚ) is closed component-wise by norm_num over the rational exponents of the Dimension group.

Definition14.1.5
Group: The algebraic calculus rides on the toolchain classes for multiplication, division, and reciprocal. There is no toolchain class for exp , sin , or square root, so the one genuinely new artifact is a carrier capability — the function-layer analogue of the numeric carrier — and a family of smart constructors that each carry their own metrological discipline. The functions split into five families with genuinely different kind signatures: kind-preserving ( abs , min , max ); powers and roots (the dimension scales by the exponent); dimensionless transcendentals ( exp , log — pure number in, pure number out); the trigonometric functions (a plane angle in, a number out — curated so that sin of a reflectivity stays a category error); and logarithmic levels (dB, neper — where log of a ratio demotes the scale, so the product calculus correctly refuses it). (4)
Group member previews
Preview
Definition 14.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 11.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

\mathrm{TranscendentalKind}\ k_1\ k licenses the smart constructors for \exp, \log, the hyperbolic and trigonometric functions. The core records the ratio-scale gate; the dimension layer strengthens it to "argument and result are dimension one" (Families C), and — for the trigonometric functions — to a curated algebra (the unary analogue of the interaction algebra) that keeps \sin on plane angles only. That a plane angle is dimension one yet a distinct kind is exactly why \sin of an angle is fine while \sin of a reflectivity is the category error a dimension-only system cannot forbid.

Lean code for Definition14.1.5●1 definition
  • structure(2 fields)defined in PropertyKindCalculus/QuantityFunction.lean
    complete
    structure PropertyKindCalculus.TranscendentalKind
  (k₁ k : PropertyKindCalculus.KindOfProperty) : Prop
    structure PropertyKindCalculus.TranscendentalKind
  (k₁ k :
    PropertyKindCalculus.KindOfProperty) :
  Prop
    **A kind-level transcendental law.** Applying a transcendental to `k₁` yields `k`;
both ratio-scale. The `Dimension` layer strengthens this to `dim k₁ = dim k = 1` and,
for the trigonometric functions, curates exactly which `(k₁, k)` edges are sanctioned.

    Fields

    ratio₁ : k₁.IsRational
    The argument kind is ratio-scale. 
    ratioResult : k.IsRational
    The result kind is ratio-scale.
Proof for Definition 14.1.5
uses 0

Realized as TranscendentalKind with the constructors Quantity.exp / log / sin / cos / tanh (base surface) and tan / asin / acos / atan / atan2 (extended surface). The dimensional strengthening is DimTranscendental (tanh_lossTangent_coherent is the worked edge: the conductive-loss \tanh argument is dimensionless and so is its value), and the trigonometric curation is the Dimension-layer trig algebra.