What each chapter in this arc rests on, and what is still unchecked
This arc was written under one rule: a statement that compiles, or reads well, is not thereby established. The ledger below says for each chapter what was read, what was only taken on someone's authority, and what is still open.
Kaluza, “On the Unification Problem in Physics” (English translation, arXiv:1803.08616). Ravndal, “Oskar Klein and the fifth dimension” (arXiv:1309.4113).
van Dongen, “Einstein and the Kaluza-Klein particle” (arXiv:gr-qc/0009087): the sections on Kaluza, Klein, Einstein 1938–43 and the monopole soliton. Overduin and Wesson, “Kaluza-Klein gravity” (arXiv:hep-th/9805018): the section on eleven-dimensional supergravity and strings. Witten (arXiv:hep-th/9503124): the abstract only. Liu et al. (arXiv:2208.07794): the abstract only. Grabowska and Grabowski (arXiv:2207.04484): read earlier for the Kaluza–Klein remark.
Literature check on the contact condition (delegated web search, abstracts and excerpts only, then spot-checked by me against the arXiv abstracts of Hamilton and Goto): Hamilton, arXiv:1001.1953; Ding and Geiges, arXiv:1107.4948; Goto, arXiv:2310.17925; Eager, Gary and Roberts, arXiv:1011.5231; Dahl, arXiv:0811.2002. The Ding–Geiges, Eager–Gary–Roberts and Dahl entries rest on the search agent's report and were not independently opened.
The New Scientist article on the 37-dimension experiment (the site is blocked in this workflow). Nothing in the arc is drawn from it.
The contact condition η∧(dη)² = κ² dy∧F∧F, the constant-field example, and the Darboux identification of J¹(ℝ²,ℝ). Now known to be a standard Boothby–Wang fact in new dress. One symbolic check of R(5) = −κ²B²/2. None of these is formalized in Lean.
The Lerman, Boyer–Galicki and Geiges books and papers beyond the abstracts and excerpts read so far; the original Einstein–Bergmann paper (paywalled); Klein's original 1926 paper, to see which charge normalisation he used; Book 4 Chapter 6's construction (the Galilean example and Theorem T1 are now marked as flawed in place); a native-speaker review of the Portuguese edition, which is a machine-assisted draft.