TY  - RPRT
TI  - Retro-synthetic Riemannian geometry in Rocq I : Taylor series of a metric
AU  - Gabriella Clemente
AU  - Hugo Herbelin
AU  - Carlos Simpson
PY  - 2026
UR  - https://arxiv.org/abs/2609.20127
ID  - 2609.20127
ER  -