Step 1 — Start from the measurement principle: declare the kinds

Name what each quantity is by the examination that produces it. Each is a bare KindOfProperty, named for the instrument or principle that examines it — the radar backscatter σ⁰, the optical vegetation index, the surface reflectivity, and the three Mironov-2009 dielectric fit constants used in Step 3.

def PropertyKindCalculus.Examples.MiniWriteOnce.backscatter : KindOfProperty

Radar backscatter coefficient σ⁰.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.backscatter = { id := "backscatter coefficient", scale := PropertyKindCalculus.ScaleType.ratio }

def PropertyKindCalculus.Examples.MiniWriteOnce.ndvi : KindOfProperty

Optical normalized vegetation index.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.ndvi = { id := "vegetation index", scale := PropertyKindCalculus.ScaleType.ratio }

def PropertyKindCalculus.Examples.MiniWriteOnce.reflectivity : KindOfProperty

Surface reflectivity.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.reflectivity = { id := "reflectivity", scale := PropertyKindCalculus.ScaleType.ratio }

Theorems about this kind

• PropertyKindCalculus.Examples.MiniWriteOnce.cholRowQ_magnitudes

def PropertyKindCalculus.Examples.MiniWriteOnce.refractiveIndexKind : KindOfProperty

Mironov dry refractive index n.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.refractiveIndexKind = { id := "refractive index (n)", scale := PropertyKindCalculus.ScaleType.ratio, examPrinciple := some "refractive-mixing" }

def PropertyKindCalculus.Examples.MiniWriteOnce.relaxTimeKind : KindOfProperty

Mironov dielectric relaxation time τ.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.relaxTimeKind = { id := "dielectric relaxation time", scale := PropertyKindCalculus.ScaleType.ratio, examPrinciple := some "debye-relaxation" }

def PropertyKindCalculus.Examples.MiniWriteOnce.conductivityKind : KindOfProperty

Mironov ionic conductivity σ.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.conductivityKind = { id := "ionic conductivity", scale := PropertyKindCalculus.ScaleType.ratio, examPrinciple := some "ionic-conduction" }

def PropertyKindCalculus.Examples.MiniWriteOnce.reflMonostatic : KindOfProperty

A different examination principle forces a different kind, even when the name, scale, and dimension all agree: monostatic and bistatic reflectivity share id "reflectivity" and ratio scale, yet are distinct kinds because the principle that examines them differs (§7.5).

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.reflMonostatic = { id := "reflectivity", scale := PropertyKindCalculus.ScaleType.ratio, examPrinciple := some "monostatic" }

def PropertyKindCalculus.Examples.MiniWriteOnce.reflBistatic : KindOfProperty

Bistatic reflectivity — same name and scale, different examination principle.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.reflBistatic = { id := "reflectivity", scale := PropertyKindCalculus.ScaleType.ratio, examPrinciple := some "bistatic" }

Step 2 — Pair each kind with its dimension

The quantities that carry the retrieval are almost all dimension one — a volume fraction, a mass fraction, a reflectivity, an index. Dimension equates them all; the kind layer keeps them apart. Volumetric and gravimetric water content are the textbook case: both volume/volume resp. mass/mass, hence dimension one, yet a units library alone would silently accept one for the other. Here they are distinct kinds, so that confusion is a type error.

(The literal dim-functor collapse — dim vwc = dim gwc = 1 — is the Mathlib-backed dimension layer, demonstrated in the Units / Dimension chapters; this Mathlib-free example makes the point one level up, at the kind.)

def PropertyKindCalculus.Examples.MiniWriteOnce.vwc : KindOfProperty

Volumetric water content (water volume / soil volume) — dimension one.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.vwc = { id := "volumetric water content", scale := PropertyKindCalculus.ScaleType.ratio, examPrinciple := some "ratio of volumes" }

def PropertyKindCalculus.Examples.MiniWriteOnce.gwc : KindOfProperty

Gravimetric water content (water mass / dry-soil mass) — also dimension one.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.gwc = { id := "gravimetric water content", scale := PropertyKindCalculus.ScaleType.ratio, examPrinciple := some "ratio of masses" }

Step 3 — Build kind-differentiated quantities

Write the model's constants as a record of typed quantities, each field its own kind. Authored over an abstract carrier α, the whole record re-represents at any carrier by one map, every kind preserved. This miniature keeps three of the Mironov-2009 fit constants — the pattern is the same for the full table.

structure PropertyKindCalculus.Examples.MiniWriteOnce.MiniMironovCoeffs (α : Type) : Type

A miniature Mironov fit table: three constants, each of its own kind, over a carrier α. The elaborator refuses to pass a relaxation time where a conductivity is wanted, even though all three erase to the same α.

• ndA0 : Quantity refractiveIndexKind α

  Dry refractive index.

• taub0 : Quantity relaxTimeKind α

  Dielectric relaxation time.

• sigbF0 : Quantity conductivityKind α

  Ionic conductivity.

def PropertyKindCalculus.Examples.MiniWriteOnce.MiniMironovCoeffs.map {α β : Type} (f : α → β) (c : MiniMironovCoeffs α) : MiniMironovCoeffs β

Re-represent the whole table at a new carrier, each constant keeping its kind.

Equations

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

def PropertyKindCalculus.Examples.MiniWriteOnce.coeffsInt : MiniMironovCoeffs Int

A concrete table at the Int carrier.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.coeffsInt = { ndA0 := { magnitude := 1 }, taub0 := { magnitude := 7 }, sigbF0 := { magnitude := 3 } }

Step 4 — Differentiate shared kinds: dedicate, or index by named field

Two cases, on two different axes.

(a) Same kind, different component — dedicate

When two quantities should differ because their measurement target differs — same relative-permittivity kind, different water phase — make them distinct with a dedicated kind: holding the component apart is enough to force distinct kinds, without inventing identity strings.

def PropertyKindCalculus.Examples.MiniWriteOnce.soilWater : SortOfSystem

The sort of system under examination.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.soilWater = { id := "soil water" }

def PropertyKindCalculus.Examples.MiniWriteOnce.boundWater : Component

One pertinent component.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.boundWater = { id := "bound water" }

def PropertyKindCalculus.Examples.MiniWriteOnce.freeWater : Component

A second pertinent component.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.freeWater = { id := "free water" }

def PropertyKindCalculus.Examples.MiniWriteOnce.relPermKind : KindOfProperty

One generic kind-of-property, shared by both phases.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.relPermKind = { id := "relative permittivity", scale := PropertyKindCalculus.ScaleType.ratio }

def PropertyKindCalculus.Examples.MiniWriteOnce.boundStaticPerm : DedicatedKind

Bound-water static permittivity = the permittivity kind dedicated to soil-water / bound water.

Equations

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

def PropertyKindCalculus.Examples.MiniWriteOnce.freeStaticPerm : DedicatedKind

Free-water static permittivity = the same kind dedicated to soil-water / free water.

Equations

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

(b) Genuinely shared kind — carry position on named fields

When the algebra forces one kind, the leftover distinction is positional, not metrological. A row of a lower-triangular Cholesky factor L (from A = L·Lᵀ) is row-homogeneous: every entry of a row lands at the same kind, here reflectivity, regardless of column — a kind that separated the columns would make the factorization's own row sums ill-typed. The remaining "which slot" distinction is held by the named fields, not by the kind and not by a Fin n-indexed array, and is checked off the kind axis by an erasure rfl against a bare-Float kernel.

(The genuine Cholesky entries also carry sqrt/division arithmetic; that — and the Gram-matrix kind bookkeeping — is the omitted detail. Kept here: the within-kind update shape, which is what exhibits the row-homogeneity and the erasure.)

structure PropertyKindCalculus.Examples.MiniWriteOnce.CholRowQ (α : Type) : Type

One row of the lower-triangular factor: three same-kind named fields.

• l20 : Quantity reflectivity α

  column 0

• l21 : Quantity reflectivity α

  column 1

• l22 : Quantity reflectivity α

  column 2 (the diagonal)

def PropertyKindCalculus.Examples.MiniWriteOnce.CholRowQ.magnitudes {α : Type} (r : CholRowQ α) : α × α × α

Project the kinded row to its bare magnitudes — the erasure .magnitude per slot.

Equations

• r.magnitudes = (r.l20.magnitude, r.l21.magnitude, r.l22.magnitude)

def PropertyKindCalculus.Examples.MiniWriteOnce.bareCholRow (a b c : Float) : Float × Float × Float

The bare-Float kernel a hand-written factorization would run: the within-kind row update on raw numbers.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.bareCholRow a b c = (a, b - a, c - a)

def PropertyKindCalculus.Examples.MiniWriteOnce.cholRowQ (a b c : Quantity reflectivity Float) : CholRowQ Float

The kinded row, built with the computational - (the executable-kernel spelling), every entry staying at reflectivity.

Equations

• PropertyKindCalculus.Examples.MiniWriteOnce.cholRowQ a b c = { l20 := a, l21 := b - a, l22 := c - a }

theorem PropertyKindCalculus.Examples.MiniWriteOnce.cholRowQ_magnitudes (a b c : Quantity reflectivity Float) : (cholRowQ a b c).magnitudes = bareCholRow a.magnitude b.magnitude c.magnitude

Erasure parity. The kinded factor's magnitudes are definitionally the bare kernel's outputs — .magnitude erases the whole kind overlay and the number that runs is the one a hand-written kernel would compute, bit for bit.