A Property Kind Calculus for Measurement Metrology

14.2. Complex-valued carriers🔗

Definition14.2.1
Group: A quantity carries a magnitude in some numbers ; many physical quantities take that magnitude in the complex numbers. The key observation is metrological, not numerical: complex-ness is a property of the carrier, not of the kind . A complex permittivity (a real part plus j times an imaginary part) is one kind of quantity — a relative permittivity, dimension one, ratio-scale — whose value is complex. It is not two real quantities, and not a new dimension. In the two-index design it is exactly Quantity k (Complex R) : the same kind layer over a complexified carrier, so the algebraic calculus applies verbatim, now computing complex products and quotients. (2)
Group member previews
Preview
Definition 14.2.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
Tagsproved

\mathrm{Complex}\ R is the complexification of a carrier — the functor R \mapsto \mathrm{Complex}\ R that, given the real arithmetic of R, equips (\mathrm{re}, \mathrm{im}) with the complex arithmetic. A complex-valued quantity is \mathrm{Quantity}\ k\ (\mathrm{Complex}\ R); the carrier varies (\mathbb{R} to prove, Float to run) while the kind k does not.

This is a fourth point on the representation axis (R10): the three scalar carriers (\mathbb{R} to prove, a binary32 rounding spec to certify, Float to run) are all real, and \mathrm{Complex}\ R lifts each of them — \mathrm{Complex}\ \mathbb{R} to prove, \mathrm{Complex}\ (\mathrm{binary32}) to certify rounding, \mathrm{Complex}\ \mathrm{Float} to run. It is a Carrier, and a LawfulCarrier whenever R is (complex addition is componentwise, so the additivity laws lift for free); it carries a full field +\,-\,\times\,\div but is unordered, so — unlike the real carriers — it sits outside the ordinal/interval/ratio carrier tower: complex magnitudes are compared by modulus, not ranked.

Lean code for Definition14.2.1●1 definition
  • structure(2 fields)defined in PropertyKindCalculus/Complex.lean
    complete
    structure PropertyKindCalculus.Complex (R : Type) : Type
    structure PropertyKindCalculus.Complex (R : Type) :
  Type
    **A complex number `(re, im)` over a carrier `R` — the complexification of `R`.**
The value type of a complex-valued quantity: `Quantity k (Complex R)` is a quantity of
kind `k` whose magnitude is complex. `R` ranges over any real carrier (`ℝ` to prove,
`Float` to run), so the same complex quantity elaborates at every representation.

    Fields

    re : R
    The real part. 
    im : R
    The imaginary part.
Proof for Definition 14.2.1
uses 0

Realized as Complex R with the toolchain instances (+, -, \times, \div, negation, zero, one), a Carrier instance, and |z|^2 / |z|. Why parametric rather than Mathlib's \mathbb{C}? For the same reason the carrier is a parameter at all: \mathbb{C} is noncomputable (its parts are \mathbb{R}, which does not reduce — no \mathbb{C}-valued program runs or compiles, yet the executable carrier must be Float-backed), and it is hardwired to \mathbb{R} (there is no "\mathbb{C} over Float"), whereas the representation axis needs complex over Float, over a binary32 rounding spec, and over \mathbb{R} from one definition. As with the reals — where \mathbb{R} is one instance of the carrier, not the universal one — Mathlib's \mathbb{C} is the natural proof-carrier target: a ring isomorphism \mathrm{Complex}\ \mathbb{R} \simeq \mathbb{C} (its home the Dimension layer) transports any property of complex quantities at \mathbb{R} to \mathbb{C} and borrows its analysis library, while the run side stays on \mathrm{Complex}\ \mathtt{Float}.

Definition14.2.2
Group: A quantity carries a magnitude in some numbers ; many physical quantities take that magnitude in the complex numbers. The key observation is metrological, not numerical: complex-ness is a property of the carrier, not of the kind . A complex permittivity (a real part plus j times an imaginary part) is one kind of quantity — a relative permittivity, dimension one, ratio-scale — whose value is complex. It is not two real quantities, and not a new dimension. In the two-index design it is exactly Quantity k (Complex R) : the same kind layer over a complexified carrier, so the algebraic calculus applies verbatim, now computing complex products and quotients. (2)
Group member previews
Preview
Definition 14.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N
Tagsproved

The principal complex square root. The algebraic operations are total and single-valued, so they are plain instances; the square root is the exception — it has a branch cut along the negative real axis. Selecting the principal branch needs exactly one sign decision (the sign of the imaginary part, with \operatorname{sign} 0 = +), isolated as the one-field capability NegTest so the branch-free complex algebra needs only the toolchain.

Lean code for Definition14.2.2●1 definition
  • defdefined in PropertyKindCalculus/Complex.lean
    complete
    def PropertyKindCalculus.Complex.sqrt {R : Type} [One R] [Add R] [Sub R]
  [Mul R] [Div R] [Neg R] [PropertyKindCalculus.MathCarrier R]
  [PropertyKindCalculus.Complex.NegTest R]
  (z : PropertyKindCalculus.Complex R) : PropertyKindCalculus.Complex R
    def PropertyKindCalculus.Complex.sqrt
  {R : Type} [One R] [Add R] [Sub R]
  [Mul R] [Div R] [Neg R]
  [PropertyKindCalculus.MathCarrier R]
  [PropertyKindCalculus.Complex.NegTest R]
  (z : PropertyKindCalculus.Complex R) :
  PropertyKindCalculus.Complex R
    **The principal complex square root** (numpy's branch, `sign 0 = +`):
`√z = √((|z|+re)/2) + sign(im)·√((|z|−re)/2)·j`. The real and imaginary magnitudes are
two real square roots; the imaginary *sign* is the one branch decision, taken by
`NegTest`. The divisor `2` is `1 + 1` (toolchain), which at every real carrier is the
literal `2`.
Proof for Definition 14.2.2
uses 1

Realized as Complex.sqrt: \sqrt{z} = \sqrt{\tfrac{|z|+\mathrm{re}}{2}} \;+\; \operatorname{sign}(\mathrm{im})\,\sqrt{\tfrac{|z|-\mathrm{re}}{2}}\,j, the real and imaginary magnitudes two real square roots and the imaginary sign the one NegTest decision (Float deciding it computably, \mathbb{R} classically). Complex is deliberately not made a full MathCarrier: a complex \exp/\log/\sin suite would drag in a quadrant-aware angle and an unprovable lawfulness story the metrology does not need — the one transcendental the electromagnetic forward model uses is given directly and honestly as its own branch-tracked constructor.

Theorem14.2.3
Group: A quantity carries a magnitude in some numbers ; many physical quantities take that magnitude in the complex numbers. The key observation is metrological, not numerical: complex-ness is a property of the carrier, not of the kind . A complex permittivity (a real part plus j times an imaginary part) is one kind of quantity — a relative permittivity, dimension one, ratio-scale — whose value is complex. It is not two real quantities, and not a new dimension. In the two-index design it is exactly Quantity k (Complex R) : the same kind layer over a complexified carrier, so the algebraic calculus applies verbatim, now computing complex products and quotients. (2)
Group member previews
Preview
Definition 14.2.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 kind-tracked complex square root. The complex analogue of Quantity.sqrt, licensed by the same PowerKind (1/2): the complex square root of a (dimension-one) relative permittivity is a (dimension-one) refractive index — a checked half-power crossing of kinds, now over a complex carrier. The complexification leaves the kind layer untouched, so this is the only new kind-level constructor the complex numbers require.

Lean code for Theorem14.2.3●1 definition
  • defdefined in PropertyKindCalculus/Complex.lean
    complete
    def PropertyKindCalculus.Quantity.csqrt
  {k₁ k : PropertyKindCalculus.KindOfProperty} {R : Type} [One R]
  [Add R] [Sub R] [Mul R] [Div R] [Neg R]
  [PropertyKindCalculus.MathCarrier R]
  [PropertyKindCalculus.Complex.NegTest R]
  (_h : PropertyKindCalculus.PowerKind (1 / 2) k₁ k)
  (a :
    PropertyKindCalculus.Quantity k₁ (PropertyKindCalculus.Complex R)) :
  PropertyKindCalculus.Quantity k (PropertyKindCalculus.Complex R)
    def PropertyKindCalculus.Quantity.csqrt
  {k₁ k :
    PropertyKindCalculus.KindOfProperty}
  {R : Type} [One R] [Add R] [Sub R]
  [Mul R] [Div R] [Neg R]
  [PropertyKindCalculus.MathCarrier R]
  [PropertyKindCalculus.Complex.NegTest R]
  (_h :
    PropertyKindCalculus.PowerKind (1 / 2)
      k₁ k)
  (a :
    PropertyKindCalculus.Quantity k₁
      (PropertyKindCalculus.Complex R)) :
  PropertyKindCalculus.Quantity k
    (PropertyKindCalculus.Complex R)
    **Kind-tracked principal complex square root.** The complex analogue of
`Quantity.sqrt`, licensed by the same `PowerKind (1/2) k₁ k`: `√` carries a
`k₁`-quantity to a `k`-quantity, now over a complex carrier. Named `csqrt` because the
complex square root is a genuinely distinct operation — it has a branch cut — even though
its kind discipline is identical to the real half-power's.
Proof for Theorem 14.2.3
uses 1

Realized as Quantity.csqrt, the smart constructor wrapping the principal complex square root under the same PowerKind (1/2) certificate as the real half-power; named csqrt because the complex root is a genuinely distinct operation (it has a branch cut) even though its kind discipline is identical.