33.8. How a definition reads — the rendering family🔗

@[pkc_math] renders a Quantity definition to LaTeX and writes it into that declaration's own docstring. Nothing else in the toolchain has to know: doc-gen4 typesets the docstring with MathJax and the InfoView renders the same markdown on hover, so one annotation reaches both surfaces.

Every rendering is faithful — it denotes exactly what the definition computes. Substitution is delta-expansion and keeping a let is a naming choice; neither asserts algebra the definition does not perform. The full policy, and the escape hatch for the cases it cannot serve, are in RENDERING.md.

33.8.1. `@[pkc_math]` — render this definition🔗

/-- The vegetation attenuation `τ = exp(−2·b·ndvi)`, kind `attenuationK`. -/
@[pkc_math]
def attenuationQ (cfg : AvsConfig α) (b : Quantity paramB α)
    (ndvi : Quantity vegetationIndex α) : Quantity attenuationK α := …

The effect, appended to that declaration's docstring and typeset on its doc-gen4 page:

\tau = e^{-2\,b\,\mathrm{NDVI}}

Two clauses control the shape. keeping binds a definition's lets as named auxiliary equations below the main one instead of inlining them — right when a model shares one subexpression across several outputs, where inlining both explodes the LaTeX and hides the structure the author wrote. substituting adds a derivation: one further equation per clause, each inlining the named helpers, so a reader sees the equation as written and then the same equation expanded.

33.8.2. `@[pkc_math_symbol]` — fix the notation🔗

Overrides every naming heuristic for one token.

attribute [pkc_math_symbol "n_{d}"]  MironovNK.nd
attribute [pkc_math_symbol "m_{vt}"] MironovNK.mvt

This is not always cosmetic. The rendering heuristic maps a Greek-letter spelling to its letter, so a refractive-index field named nu would typeset as \nu — an angular frequency. Notation stated once, on the field, wins over every heuristic, and the index below is therefore a table of the places where a heuristic was deliberately overruled.

Declaration	Renders as	Layout
`avsForward`	`\sigma^0`	function head
`byPolarization`	`P`	function head
`columns`	`J`	function head
`combined`	`D`	function head
`decay`	`\tau`	function head
`grad`	`\nabla`	prefix operator
`letExample`	`q`	function head
`model`	`F`	function head
`noted`	`\gamma`	function head
`residual`	`R`	function head
`scaled`	`g`	function head
`scaledByTwo`	`u`	function head
`shared`	`S`	function head
`twiceBound`	`T`	function head

33.8.3. `@[pkc_math_config]` — a configuration type🔗

A projection of an ordinary structure renders as a function applied to its receiver: \mathrm{two}\left(\mathrm{cfg}\right), which is the field name stripped of the type it belongs to plus a spurious application. Tagging the structure makes its projections render as the qualified constant \mathrm{AvsConfig.two} instead, with the configuration value elided.

@[pkc_math_config]
structure AvsConfig (α : Type) where
  two : Quantity pureNumber α

The type must opt in: a blanket "drop the receiver" rule would wreck Prod.fst and Prod.snd. Note what this does not do — it does not render cfg.two as 2, which would assert something about a def parameter rather than report what the definition computes.

Type	What it is
`AvsConfig`	The AVS forward's configuration: the two-way optical-path factor `2`, as a kinded quantity — the sole numeral of the model.
`DemoConfig`	A configuration type: one dimensionless scale factor, the demo's sole configured constant.

33.8.4. `@[pkc_math_transparent]` — a notational wrapper🔗

Marks a wrapper the renderer should see through, so the wrapped term is rendered in place of a call to it. The carrier's numeral injection is the motivating case: without this, every literal in a rendered equation appears wrapped in a helper nobody wants to read.

Wrapper	What it is
`ofN`	The carrier's numeral injection: a transparent wrapper.

33.8.5. The rendered definitions🔗

Every @[pkc_math] application in the worked examples, with the clauses each requested.

Definition	Rendering mode	What it is
`attenuationQ`	plain	The vegetation attenuation `τ = exp(−2·b·ndvi)`, kind `attenuationK`.
`lavsForwardQ`	substituting (1 step(s))	The LAVS forward `σ⁰ = a·ndvi + (τ·c)·r + d`, kind `backscatter`.
`lavsJacResidualQ`	substituting (1 step(s))	The four analytic Jacobian columns `∂residual/∂(a,b,c,d)`, each at its forced kind.
`lavsResidualQ`	substituting (2 step(s))	The LAVS residual `s0 − σ⁰`, kind `backscatter` (subtraction forces the shared kind).
`avsForward`	plain	The AVS-style backscatter forward model, rendered on its doc page as `σ⁰ = a·ndvi + exp(−2·b·ndvi)·c·r + d`.
`byPolarization`	plain	Case analysis on the polarization, written vertical-first.
`columns`	plain	Three columns returned as a triple: exercises the `Prod.mk` flattening and both head layouts.
`combined`	plain	Consumes a destructured pair.
`model`	substituting (1 step(s))	One derivation step.
`noted`	plain	Base backscatter.
`residual`	substituting (2 step(s))	The residual of `model`: two cumulative steps, so the reader sees the call, then the call expanded, then the constant it bottoms out in.
`scaled`	plain	Reads a configuration constant.
`scaledByTwo`	plain	Doubling through the numeral injection.
`shared`	keeping	A model with a shared intermediate: `d` is used by both `s` and the sum.
`spread`	plain	A record-valued model: renders as the system `hi = a·b`, `lo = a − b`.
`twiceBound`	keeping	A definition that binds `u` twice, for different values.

33.8. How a definition reads — the rendering family🔗

33.8.1. @[pkc_math] — render this definition🔗

33.8.2. @[pkc_math_symbol] — fix the notation🔗

33.8.3. @[pkc_math_config] — a configuration type🔗

33.8.4. @[pkc_math_transparent] — a notational wrapper🔗

33.8.5. The rendered definitions🔗

33.8.1. `@[pkc_math]` — render this definition🔗

33.8.2. `@[pkc_math_symbol]` — fix the notation🔗

33.8.3. `@[pkc_math_config]` — a configuration type🔗

33.8.4. `@[pkc_math_transparent]` — a notational wrapper🔗