Lower bound on validity check in spec?

[bwbush]

I'm confused about the following lines in the LL specification:

ouroboros-leios-formal-spec/formal-spec/Leios/Linear.lagda.md

Lines 132 to 133 in c7f8d61

	∙ slotNumber eb + 3 * Lhdr ≤ slot
	∙ slot ≡ slotNumber eb + validityCheckTime eb

Doesn't this imply 3 * Lhdr ≤ validityCheckTime eb? Wouldn't this be violated if the validity check occurs very quickly?

[WhatisRT]

Oh, you're right! This should be max (3 * Lhdr) (validityCheckTime eb) instead.

[bwbush]

Thanks. Please close this ticket when it is fixed.