`bounceRadius`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.QuantumGravityFromRS on GitHub at line 35.

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

  32theorem qgApproachCount : Fintype.card QGApproach = 5 := by decide
  33
  34/-- Bounce radius at rung N: r_min(N) = φ^(N/2). -/
  35noncomputable def bounceRadius (N : ℕ) : ℝ := phi ^ N
  36
  37theorem bounceRadius_pos (N : ℕ) : 0 < bounceRadius N := pow_pos phi_pos N
  38
  39/-- Bounce increases with rung. -/
  40theorem bounceRadius_mono (N : ℕ) : bounceRadius N < bounceRadius (N + 1) := by
  41  unfold bounceRadius
  42  have hpos := pow_pos phi_pos N
  43  rw [pow_succ]
  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

papers checked against this theorem

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