2.11. Ergonomics and erasure (R21, R25)🔗

R21 — The kind layer erases: the ceremony is pure. The standing objection to any kind layer is authoring cost, and the honest answer is not that the cost is zero — the ForPhysLib benchmark scores PKC worst of four designs at longhand authoring — but that the cost buys checking and nothing else: the kinded authoring computes exactly the bare-carrier value, and the curated-operator form (KindMul/KindDiv, the OperatorTable) elaborates to the same term as the longhand form (hmul_eq_mul, one rfl that transports every certificate). So m * (ω * ω) * (x * x) is character-identical to bare reals, and what remains of the cost is the per-model operator-table setup — a price the requirement makes measurable rather than deniable. This is the write once correctly, go fast automatically slogan stated as an obligation: correctness lives in the types and is paid at compile time, and the number that runs is the one a hand-written kernel would compute.

R25 — A kinded definition renders back as typeset mathematics. The reading-side twin of R21's writing-side claim. A definition annotated @[pkc_math] is lifted from its own elaborated term into a presentation language (MathTerm), normalized faithfully, and pretty-printed to a LaTeX equation in the declaration's docstring — with the kind bookkeeping suppressed and the notation (an object index as a subscript, a conventional symbol like \sigma^0) recovered rather than lost. The rendering is pinned with #guard_msgs, so it is a regression artifact, not a comment.