33.10. The generated indexes🔗

What these tables index. Every table in this section is scoped to PropertyKindCalculus.Examples — the calculus's own worked examples, which are what this package has to index. They are not the soil-moisture model: that model is a separate downstream repository, and its technical reference renders the same eight tables over its own namespaces, populated with its real kinds and crossings.

The rows nonetheless read as soil-moisture material, and it is worth saying why rather than letting it look like a leak. The calculus's worked examples deliberately run on the domain that motivated it: a vegetation-attenuation forward model, Mironov coefficients, soil and soil-water as systems. That is the point of a worked example — it has to be of something — and the alternative, examples over invented quantities, would demonstrate the machinery while hiding whether it survives contact with a real model. The generic examples are here too, in the same tables: length and width as distinct kinds, a blood group as a nominal scale, Mohs hardness as an ordinal one, the principle/method/procedure examination chain.

So the reading to avoid is that these tables document the model. They document the examples this package ships, and they exist here for the same reason the boundary probe does: a derived table nobody renders is a table nobody notices has broken.

33.10.1. Kinds and their algebra🔗

The column that earns this table is Algebra. A kind's authored edges are the complete statement of what may be done with it — multiplied by what, divided into what, raised to what power — because the calculus infers none of them. A kind whose Algebra cell is empty supports no arithmetic at all, and being able to see that is the point.

Kind	Identity	Scale	Algebra	Theorems
`attenExponent`	AVS attenuation exponent	ratio	produced (1) `paramB · vegetationIndex → attenExponent` consumed (1) `transcendental : attenExponent → attenuationK`	`attenuation_roles_distinct`
`attenuationK`	AVS vegetation attenuation	ratio	produced (1) `transcendental : attenExponent → attenuationK` consumed (3) `jacB · attenuationK → jacB` `attenuationK · paramC → paramC` `attenuationK · reflectivity → reflectivity`	`attenuation_roles_distinct`
`backscatter`	AVS backscatter coefficient σ⁰	ratio	produced (2) `paramA · vegetationIndex → backscatter` `paramC · reflectivity → backscatter`
`jacB`	AVS backscatter times NDVI	ratio	produced (2) `jacB · attenuationK → jacB` `jacBPartial · reflectivity → jacB`
`jacBPartial`	AVS NDVI times gain c	ratio	produced (1) `vegetationIndex · paramC → jacBPartial` consumed (1) `jacBPartial · reflectivity → jacB`
`paramA`	AVS gain a (σ⁰ per NDVI)	ratio	consumed (1) `paramA · vegetationIndex → backscatter`
`paramB`	AVS rate b (inverse NDVI)	ratio	produced (1) `pureNumber · paramB → paramB` consumed (1) `paramB · vegetationIndex → attenExponent`
`paramC`	AVS gain c (σ⁰ per reflectivity)	ratio	produced (1) `attenuationK · paramC → paramC` consumed (2) `paramC · reflectivity → backscatter` `vegetationIndex · paramC → jacBPartial`
`pureNumber`	AVS pure number	ratio	consumed (2) `pureNumber · paramB → paramB` `pureNumber · vegetationIndex → vegetationIndex`	`attenuation_roles_distinct`
`reflectivity`	AVS surface reflectivity	ratio	produced (1) `attenuationK · reflectivity → reflectivity` consumed (2) `paramC · reflectivity → backscatter` `jacBPartial · reflectivity → jacB`
`vegetationIndex`	AVS vegetation index	ratio	produced (1) `pureNumber · vegetationIndex → vegetationIndex` consumed (3) `paramB · vegetationIndex → attenExponent` `paramA · vegetationIndex → backscatter` `vegetationIndex · paramC → jacBPartial`
`length`	length	ratio	produced (1) `speed · time → length`	`length_is_speed_times_time`
`speed`	speed	ratio	consumed (1) `speed · time → length`	`length_is_speed_times_time`
`time`	time	ratio	consumed (1) `speed · time → length`	`length_is_speed_times_time`
`massFraction`	mass fraction	ratio
`volumeFraction`	volume fraction	ratio	produced (1) `volumeFraction ± volumeFraction → volumeFraction`
`dl`	1	ratio	produced (2) `dl · dl → dl` `transcendental : dl → dl`	`pk`, `tk`
`height`	height	ratio
`length`	length	ratio
`width`	width	ratio
`mass`	mass	ratio		`mass_extensive`
`lengthK`	length	ratio
`massK`	mass	ratio		`instAssemblesGridSMassK`
`length`	length	ratio		`hLen`
`mass`	mass	ratio		`hMass`
`lengthKind`	length	ratio	produced (1) `lengthKind ± lengthKind → lengthKind`	`hLen`
`displacement`	displacement	ratio	produced (2) `displacement ± displacement → displacement` `factor · displacement → displacement` consumed (1) `displacement · displacement → displacementSq`	`doubled_east`, `hDisp`, `hScale`, `hSquare`, `vector_add_comm`
`displacementSq`	displacement squared	ratio	produced (1) `displacement · displacement → displacementSq`	`hSquare`
`factor`	scale factor	ratio	consumed (1) `factor · displacement → displacement`	`hScale`
`backscatter`	backscatter coefficient	ratio
`conductivityKind`	ionic conductivity	ratio
`gwc`	gravimetric water content	ratio
`ndvi`	vegetation index	ratio
`reflBistatic`	reflectivity	ratio
`reflMonostatic`	reflectivity	ratio
`reflectivity`	reflectivity	ratio		`cholRowQ_magnitudes`
`refractiveIndexKind`	refractive index (n)	ratio
`relPermKind`	relative permittivity	ratio
`relaxTimeKind`	dielectric relaxation time	ratio
`vwc`	volumetric water content	ratio
`bloodGroup`	abo-blood-group	nominal
`length`	length	ratio
`mass`	mass	ratio
`mohsHardness`	mohs-hardness	ordinal
`bloodGroup`	abo-blood-group	nominal
`length`	length	ratio
`mass`	mass	ratio
`height`	height	ratio
`length`	length	ratio
`width`	width	ratio

33.10.2. The ontology🔗

The Dybkær spine is inhabited by ordinary definitions, so nothing marks them as a family: the criterion is simply "a constant whose type is that structure". The dedicated-kind table renders each one as the System — Component ; kind-of-property triple it is — the System slot naming the sort — cross-linked to the sort and component tables rather than repeating their identity strings. The systems table lists the particulars; nothing dedicates to a particular, so it carries no dedicated-kinds column.

Sort	Identity	Dedicated kinds	Theorems
`soil`	soil	`airContent`, `gwc`, `vwc`
`gridS`	four-cell grid		`instAssemblesGridSMassK`
`soilWater`	soil water	`boundStaticPerm`, `freeStaticPerm`

System	Identity	Theorems

Component	Identity	Dedicated kinds
`air`	air	`airContent`
`water`	water	`gwc`, `vwc`
`boundWater`	bound water	`boundStaticPerm`
`freeWater`	free water	`freeStaticPerm`

Dedicated kind	Sort of system	Component	Kind of property
`airContent`	`soil`	`air`	`volumeFraction`
`gwc`	`soil`	`water`	`massFraction`
`vwc`	`soil`	`water`	`volumeFraction`
`boundStaticPerm`	`soilWater`	`boundWater`	`relPermKind`
`freeStaticPerm`	`soilWater`	`freeWater`	`relPermKind`

Two dedicated kinds that share a kind-of-property are held apart only by their sort and component, and the Theorems column lists what proves it. A dedicated kind with no distinctness theorem is one that nothing yet relies on separating.

The examination chain needs no annotation either: a method is based on the principle it cites and a procedure on the method it cites, so BasedOn is structural, and the table below is the generating edges of the Refines closure.

Examination	Layer	Based on	Principle
`widthPrinciple`	principle	—	caliper-perpendicular
`widthMethod`	method	`widthPrinciple`	iso-width-method
`widthProcedure`	procedure	`widthMethod`	iso-width-procedure-v1

33.10.3. Kinded records and operations🔗

Neither table needs an annotation to decide membership. A kinded record is a structure at least one of whose fields is a registered carrier applied to a kind; a kinded operation is a definition whose result type is one. @[kindCarrier] is the only opt-in, and it is already required for the audit.

For a record the useful column is the notation, because the fields are where @[pkc_math_symbol] attaches and a rendered equation's readability is decided.

Record	Field	Carrier	Kind
`AvsConfig`	`two`	`Quantity`	`pureNumber`
`Bounds`	`hi`	`Quantity`	`dl`
	`lo`	`Quantity`	`dl`
`DemoConfig`	`scale`	`Quantity`	`dl`
`CholRowQ`	`l20`	`Quantity`	`reflectivity`
	`l21`	`Quantity`	`reflectivity`
	`l22`	`Quantity`	`reflectivity`
`MiniMironovCoeffs`	`ndA0`	`Quantity`	`refractiveIndexKind`
	`taub0`	`Quantity`	`relaxTimeKind`
	`sigbF0`	`Quantity`	`conductivityKind`

For an operation it is the kind signature together with the authored crossings its body routes through — which makes the row a contract rather than a signature, since an operation that changes kind must reach a sanctioned crossing to do it.

Field projections are excluded. MironovNK.nd satisfies the criterion literally, its result type being Quantity nIndexKind α, but it is the record's accessor rather than an operation on kinds and is already a row of the table above.

Operation	Argument kinds	Result kind
`attenuationQ`	`paramB`, `vegetationIndex`	`attenuationK`
`lavsForwardQ`	`paramA`, `paramB`, `paramC`, `backscatter`, `vegetationIndex`, `reflectivity`	`backscatter`
`lavsResidualQ`	`paramA`, `paramB`, `paramC`, `backscatter`, `vegetationIndex`, `reflectivity`, `backscatter`	`backscatter`
`d`		`length`
`dFake`		`length`
`v`		`speed`
`τ`		`time`
`avsForward`	`dl`, `dl`, `dl`, `dl`, `dl`, `dl`	`dl`
`byPolarization`	`dl`, `dl`	`dl`
`combined`	`dl`, `dl`	`dl`
`decay`	`dl`	`dl`
`gain`	`dl`	`dl`
`grad`	`dl`	`dl`
`letExample`	`dl`	`dl`
`model`	`dl`, `dl`	`dl`
`noted`	`dl`, `dl`	`dl`
`ofN`		`dl`
`residual`	`dl`, `dl`, `dl`	`dl`
`scaled`	`dl`	`dl`
`scaledByTwo`	`dl`	`dl`
`shared`	`dl`, `dl`	`dl`
`twiceBound`	`dl`, `dl`	`dl`
`lenA`		`length`
`lenB`		`length`
`lenF`		`length`
`massA`		`mass`
`a`		`lengthKind`
`aSpec`		`lengthKind`
`b`		`lengthKind`
`bSpec`		`lengthKind`
`doubled`		`displacement`
`east`		`displacement`
`up`		`displacement`