13.2. The trust model: what is checked, what is authored🔗

The negative pole — kinds in the name only. In an unkinded model every quantity is a bare numeric: a vegetation-attenuation kernel reads attenuation (b ndvi : Float) : Float, and the kind of each argument lives only in its name. The type system then cannot see any of the kind algebra: the swapped call attenuation ndvi b elaborates and silently computes the role-swapped exponent; a damping lam : Float adds to a Gram-diagonal entry jtj : Float whatever the entry's kind; a fitted gain from one forward model substitutes for the differently-kinded gain of another. Dimension checking does not recover the distinctions: attenuations, damping factors, and vegetation indices are all dimension one, so a dimensional type system waves every one of these confusions through (the torque-versus-energy instance above is the same failure at dimension \mathrm{M\,L^2\,T^{-2}}). Name-only kinds are documentation; nothing enforces them.

The positive pole — the kind algebra is explicit. The same kernel written over Quantity makes the kind a type index and gates every kind-changing operation on a witness: attenuationQ (b : Quantity paramB α) (ndvi : Quantity vegetationIndex α) rejects the swapped call at compile time, the cross-kind sum jtj + lam fails to elaborate because addition is defined only at a shared kind (there is deliberately no opt-in for heterogeneous addition), and each product or exponential names its edge in full — ProductKind.ofRatio paramB vegetationIndex attenuationExponent — where it is used. Downstream models certify the rejections as build artifacts: a #check_failure probe succeeds only if the forbidden term fails to elaborate, so the build proves the negative examples stay negative.

Definition13.2.1

groupuses 0used by 0✓L∃∀N

The liberal certificate authority. ProductKind.ofRatio k₁ k₂ k signs any three ratio-scale kinds: the scale gate is checked, the kind equation is not. This is deliberate — the same dimension-one ratio can legitimately land in different kinds by role (a quotient of two backscatters is an attenuation in one column of a Jacobian and a pure number in another), so the landing kind is curation the calculus must let the author state. The cost is the trust model above: an edge's truth is a reviewed claim. The guarantee that remains is that the claim must be written, in full, where it is used — a wrong edge is not impossible, it is impossible to write silently.

Lean code for Definition13.2.1●1 theorem

theoremdefined in PropertyKindCalculus/QuantityClassification.lean

complete

theorem PropertyKindCalculus.ProductKind.ofRatio
  (k₁ k₂ k : PropertyKindCalculus.KindOfProperty)
  (h₁ : k₁.IsRational := by rfl) (h₂ : k₂.IsRational := by rfl)
  (h : k.IsRational := by rfl) :
  PropertyKindCalculus.ProductKind k₁ k₂ k

theorem PropertyKindCalculus.ProductKind.ofRatio
  (k₁ k₂ k :
    PropertyKindCalculus.KindOfProperty)
  (h₁ : k₁.IsRational := by rfl)
  (h₂ : k₂.IsRational := by rfl)
  (h : k.IsRational := by rfl) :
  PropertyKindCalculus.ProductKind k₁ k₂ k

**Smart constructor.** Build a product law from three *named* ratio-scale kinds, the
ratio-scale gate discharged by `rfl` for any concrete kinds. Reads as the kind equation it
stands for at the call site (`ProductKind.ofRatio k₁ k₂ k`), with the dimensional content
certified in the application's `Dimension` layer.

Deliberately liberal: it signs *any* ratio-scale triple — whether `k` truly is the product
kind of `k₁` and `k₂` is the author's claim, not a checked fact (the trust model in this
module's header). The guarantee is that the claim must be *written*, in full, where it is
used.

Proof for Definition 13.2.1

uses 0

Realized in QuantityClassification ("The trust model" in that module's header): the witness Props (ProductKind, QuotientKind, TranscendentalKind) carry only the ratio-scale gates, ofRatio discharges them by rfl for any concrete kinds, and Quantity.mul/div/exp refuse to operate without the witness.

Definition13.2.2

groupuses 0used by 0✓L∃∀N

Narrowing by instance table. KindMul k₁ k₂ k (with k an outParam) and its division dual KindDiv re-house authored edges as typeclass instances: a model registers at most one signed edge per operand pair next to its kind declarations, and adopting call sites use scoped *// whose result kind is resolved — not chosen — at each use. Where the table is adopted, an unlisted edge is no longer merely unwritten; it is unresolvable.

Lean code for Definition13.2.2●1 definition

class(1 method)defined in PropertyKindCalculus/OperatorTable.lean

complete

class PropertyKindCalculus.KindMul
  (k₁ k₂ : PropertyKindCalculus.KindOfProperty)
  (k : outParam PropertyKindCalculus.KindOfProperty) : Prop

class PropertyKindCalculus.KindMul
  (k₁ k₂ :
    PropertyKindCalculus.KindOfProperty)
  (k :
    outParam
      PropertyKindCalculus.KindOfProperty) :
  Prop

**A curated product-table entry.** The product of a `k₁`- and a `k₂`-quantity is
sanctioned and lands in `k`, witnessed by the same kind-level law `Quantity.mul` takes.
`k` is an `outParam`: instance search computes the result kind from the operand kinds, so
a chained product finds its interior kinds without annotation. Applications register
instances next to their kind declarations — at most one per `(k₁, k₂)` pair.

Methods

law : PropertyKindCalculus.ProductKind k₁ k₂ k

The kind-level product law backing this table entry.

Proof for Definition 13.2.2

uses 1

Realized in OperatorTable: the instance classes wrap the curated ternary product as resolution-driven registrations, with hmul_eq_mul bridging the scoped operator back to the witness-passing Quantity.mul by rfl.

The audit is mechanical. A witness is to the kind algebra what an axiom is to a proof, and the analogy extends to the tooling: soundness is judged by enumerating the trusted base, never by the absence of errors. Three queries cover it. Instance-table registrations are listed by the stock #instances KindMul command. Named witness theorems are found by scanning the environment for declarations whose type mentions the witness Props. And every call-site witness is lifted by Lean into an auxiliary theorem whose type is the edge (attenuationQ._proof_2 : ProductKind paramB vegetationIndex attenuationExponent), so one environment scan over constant types — internal names attributed to their parents — enumerates the complete authored edge set of a kind, named and inline alike: the kind-algebra analog of #print axioms.