qgApproachCount

formal source

  29  | canonicalQG | spinFoam | causalSets | CDT | loopQG
  30  deriving DecidableEq, Repr, BEq, Fintype
  31
  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