Ambient coordinate carriers

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. This port keeps only the coordinate carrier needed by the weak-derivative API and uses the CKN namespace.

@[reducible, inline]

abbrev CKN.Vec (d : ℕ) : Type

The native coordinate model of a finite-dimensional real vector space.

Equations

• CKN.Vec d = (Fin d → ℝ)