module
module
IndisputableMonolith.Holography.HorizonClockRate
show as:
view Lean formalization →
used by (1)
depends on (3)
declarations in this module (11)
-
structure
NearHorizonRindlerForm -
def
euclideanAngle -
theorem
euclideanAngle_rate -
theorem
euclideanAngle_deriv_eq -
structure
ClockRateBundle -
theorem
clockRateBundle_of_rindler -
def
HyperbolicMismatchClass -
theorem
period_is_b2_output_not_b3_input -
theorem
turnRatio_unity_at_b2_period -
theorem
clockRateBundle_silent_on_period -
theorem
legacy_horizonRate_is_separate