OAI/MathematicalPhysics/Boltzmann/Branching/CommonHistoryCore.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

All bounded histories in a short late-box window use one characteristic core

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.characteristicHistoryCore_shift line 14
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedFlightCone_mem_commonCore line 28