`echoDelay`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.QuantumGravityFromRS
domain: Physics
line: 47 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.QuantumGravityFromRS on GitHub at line 47.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  44  linarith [mul_lt_mul_of_pos_left one_lt_phi hpos]
  45
  46/-- Echo delay = 2r_min × log φ: positive (structural). -/
  47noncomputable def echoDelay (N : ℕ) : ℝ := 2 * bounceRadius N * Real.log phi
  48
  49theorem echoDelay_pos (N : ℕ) : 0 < echoDelay N := by
  50  unfold echoDelay
  51  apply mul_pos (mul_pos (by norm_num) (bounceRadius_pos N))
  52  exact Real.log_pos one_lt_phi
  53
  54structure QuantumGravityCert where
  55  five_approaches : Fintype.card QGApproach = 5
  56  bounce_pos : ∀ N, 0 < bounceRadius N
  57  bounce_mono : ∀ N, bounceRadius N < bounceRadius (N + 1)
  58  echo_pos : ∀ N, 0 < echoDelay N
  59
  60noncomputable def quantumGravityCert : QuantumGravityCert where
  61  five_approaches := qgApproachCount
  62  bounce_pos := bounceRadius_pos
  63  bounce_mono := bounceRadius_mono
  64  echo_pos := echoDelay_pos
  65
  66end IndisputableMonolith.Physics.QuantumGravityFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.