9. Correspondence and audit
The eight chapters before this one follow the paper's results in the paper's order. This chapter is organized by the formalization instead. It lists, for every numbered result of Zheng (2026), the node that documents it and the state of the mapping; collects the vocabulary that the paper and the Lean development do not share; summarizes every registered deviation in one place; states what the kernel check covers and what stands outside it; and records, for each of the development's 139 modules, which node accounts for it.