Add missing formal proof for epoch boundary transitions

[diorlab]

• It appears that the transition rules at epoch boundaries are not fully proven in the Isabelle/HOL model. We should add or complete the proof, and ensure alignment with the Haskell executable model.