`echoDelay_pos`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.QuantumGravityFromRS on GitHub at line 49.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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.