Rovelli and NRS³, chapter by chapter

Carlo Rovelli's Reality Is Not What It Seems (Spanish edition: La realidad no es lo que parece, Tusquets, ISBN 978-84-9066-194-9) describes loop quantum gravity. Each chapter is set against the Lean modules of nava-robertson-schrodinger and the mosaic repositories. The summaries of the book are paraphrases; every module named is compiled Lean, and what is only declared is marked as such.

Relations: coincides — the same statement reached by another route; analogous — the same shape, different objects; departs — the canon says otherwise; declared bridge — a physical identification stated as a hypothesis in Lean and shown satisfiable, not derived; no counterpart — nothing in the canon. The canon is the git repositories; nothing here is cited from older trees.