theorem proved term proof

`etaBAt_pos`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  36theorem etaBAt_pos (N : ℕ) : 0 < etaBAt N := by

Term-mode proof.

  37  unfold etaBAt
  38  exact zpow_pos Constants.phi_pos _
  39
  40/-- GUT-scale initial value: η_B(0) = 1. -/

From the project-wide theorem graph. These declarations reference this one in their body.

baryogenesisTrajectoryCert in IndisputableMonolith.Cosmology.BaryogenesisTrajectory decl_use
etaBAt_adjacent_ratio in IndisputableMonolith.Cosmology.BaryogenesisTrajectory decl_use
etaBAt_strictly_decreasing in IndisputableMonolith.Cosmology.BaryogenesisTrajectory decl_use

Lean names referenced from this declaration's body.