sensor_realPart_pos

formal source

  32/-! ## Prime Euler events -/
  33
  34/-- The strip real part of a defect sensor is positive. -/
  35theorem sensor_realPart_pos (sensor : DefectSensor) : 0 < sensor.realPart := by
  36  linarith [sensor.in_strip.1]
  37
  38/-- The basic arithmetic recognition event contributed by a prime Euler factor.
  39
  40Its ratio is the positive real quantity `p^{-σ}`. -/
  41noncomputable def primeEulerEvent (σ : ℝ) (hσ : 0 < σ) (p : Nat.Primes) :
  42    LedgerForcing.RecognitionEvent where
  43  source := 0
  44  target := p
  45  ratio := (p : ℝ) ^ (-σ)
  46  ratio_pos := eigenvalue_pos hσ p
  47
  48@[simp] theorem primeEulerEvent_ratio (σ : ℝ) (hσ : 0 < σ) (p : Nat.Primes) :
  49    (primeEulerEvent σ hσ p).ratio = (p : ℝ) ^ (-σ) := rfl
  50
  51@[simp] theorem primeEulerEvent_target (σ : ℝ) (hσ : 0 < σ) (p : Nat.Primes) :
  52    (primeEulerEvent σ hσ p).target = p := rfl
  53
  54/-- The prime Euler event is genuinely nontrivial: its ratio is strictly below `1`. -/
  55theorem primeEulerEvent_ratio_lt_one {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
  56    (primeEulerEvent σ hσ p).ratio < 1 := by
  57  simpa [primeEulerEvent] using eigenvalue_lt_one hσ p
  58
  59/-- Hence the prime Euler event does not have ratio `1`. -/
  60theorem primeEulerEvent_ratio_ne_one {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
  61    (primeEulerEvent σ hσ p).ratio ≠ 1 := by
  62  exact (primeEulerEvent_ratio_lt_one hσ p).ne
  63
  64/-- The reciprocal Euler event has ratio `p^σ`. -/
  65theorem reciprocal_primeEulerEvent_ratio {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :