pith. machine review for the scientific record. sign in
def definition def or abbrev

baryogenesisTrajectoryCert

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  94def baryogenesisTrajectoryCert : BaryogenesisTrajectoryCert where
  95  eta_pos := etaBAt_pos

proof body

Definition body.

  96  initial_unity := etaBAt_zero
  97  one_step_ratio := etaBAt_succ_ratio
  98  strictly_decreasing := etaBAt_strictly_decreasing
  99  adjacent_ratio_eq_inv_phi := etaBAt_adjacent_ratio
 100  present_value := etaBAt_44
 101
 102end
 103end BaryogenesisTrajectory
 104end Cosmology
 105end IndisputableMonolith

depends on (7)

Lean names referenced from this declaration's body.