The development as a book

The Lean development, presented as a hyperlinked math book split into one section per Lean module. Each entry is a numbered Definition, Theorem or Lemma with the author’s own explanation, typeset in printed math (free variables are implicitly universally quantified). Every Proof cites the lemmas it rests on — click a citation to jump straight to that result (on its own section page), read it, and follow its proof deeper; symbols inside the formulas link to their definitions; and a source ↗ link opens the exact Lean line.

A hyperlinked math book in 49 sections (1000 numbered definitions, lemmas and theorems). Pick a section:

BornJoin  (3)

• QIQTH.BornJoin  3 entries (#1–3)

BornJoinGleason  (1)

• QIQTH.BornJoinGleason  1 entries (#4–4)

BranchLedger  (1)

• QIQTH.BranchLedger  1 entries (#5–5)

ChristoffelSmooth  (5)

• QIQTH.ChristoffelSmooth  5 entries (#6–10)

ClausiusFiniteWitness  (1)

• QIQTH.ClausiusFiniteWitness  1 entries (#11–11)

ClausiusToPernull  (1)

• QIQTH.ClausiusToPernull  1 entries (#12–12)

CoreNoCollapse  (2)

• QIQTH.CoreNoCollapse  2 entries (#13–14)

Curvature  (56)

• QIQTH.Curvature  56 entries (#15–70)

DifferentialAreaLaw  (3)

• QIQTH.DifferentialAreaLaw  3 entries (#71–73)

EffectGleason  (3)

• QIQTH.EffectGleason  3 entries (#74–76)

EinsteinEquationOfState  (6)

• QIQTH.EinsteinEquationOfState  6 entries (#77–82)

EinsteinFieldEquation  (11)

• QIQTH.EinsteinFieldEquation  11 entries (#83–93)

Fock  (334)

• QIQTH.Fock.BoostKMS  115 entries (#94–208)
• QIQTH.Fock.CyclicWitness  22 entries (#209–230)
• QIQTH.Fock.FreeFieldHFlux  5 entries (#231–235)
• QIQTH.Fock.Localization  34 entries (#236–269)
• QIQTH.Fock.OneParticle  16 entries (#270–285)
• QIQTH.Fock.OneParticleBW  34 entries (#286–319)
• QIQTH.Fock.SchwartzDecay  6 entries (#320–325)
• QIQTH.Fock.WedgeAnalyticity  58 entries (#326–383)
• QIQTH.Fock.WienerL2  44 entries (#384–427)

GaussianMode  (17)

• QIQTH.GaussianMode  17 entries (#428–444)

HregExplicitKG  (3)

• QIQTH.HregExplicitKG  3 entries (#445–447)

KGStressConservation  (21)

• QIQTH.KGStressConservation  21 entries (#448–468)

KMSCorrelation  (21)

• QIQTH.KMSCorrelation  21 entries (#469–489)

LocalizedMode  (1)

• QIQTH.LocalizedMode  1 entries (#490–490)

ModularRelativeEntropy  (43)

• QIQTH.ModularRelativeEntropy  43 entries (#491–533)

PPWaveMetric  (12)

• QIQTH.PPWaveMetric  12 entries (#534–545)

QiqtGrComplete  (1)

• QIQTH.QiqtGrComplete  1 entries (#546–546)

QiqtGrCovCong  (1)

• QIQTH.QiqtGrCovCong  1 entries (#547–547)

QiqtGrExplicitKG  (1)

• QIQTH.QiqtGrExplicitKG  1 entries (#548–548)

QiqtGrFreeField  (7)

• QIQTH.QiqtGrFreeField  7 entries (#549–555)

QiqtGrGaussian  (1)

• QIQTH.QiqtGrGaussian  1 entries (#556–556)

QiqtGrPPWave  (1)

• QIQTH.QiqtGrPPWave  1 entries (#557–557)

QiqtGrShowcase  (1)

• QIQTH.QiqtGrShowcase  1 entries (#558–558)

QiqtGrThermo  (1)

• QIQTH.QiqtGrThermo  1 entries (#559–559)

QiqtToGR  (4)

• QIQTH.QiqtToGR  4 entries (#560–563)

Raychaudhuri  (11)

• QIQTH.Raychaudhuri  11 entries (#564–574)

RaychaudhuriCongruence  (4)

• QIQTH.RaychaudhuriCongruence  4 entries (#575–578)

RecordContract  (3)

• QIQTH.RecordContract  3 entries (#579–581)

RelEntPositivity  (2)

• QIQTH.RelEntPositivity  2 entries (#582–583)

RicciSymm  (2)

• QIQTH.RicciSymm  2 entries (#584–585)

Spectral  (167)

• QIQTH.Spectral.PVM  84 entries (#586–669)
• QIQTH.Spectral.SpectralTheorem  83 entries (#670–752)

StandardSubspaceModular  (55)

• QIQTH.StandardSubspaceModular  55 entries (#753–807)

StandardSubspaceModularFlow  (171)

• QIQTH.StandardSubspaceModularFlow  171 entries (#808–978)

StripUniqueness  (14)

• QIQTH.StripUniqueness  14 entries (#979–992)

ValueSelection  (4)

• QIQTH.ValueSelection  4 entries (#993–996)

WedgeKMSToGR  (4)

• QIQTH.WedgeKMSToGR  4 entries (#997–1000)