Full Cubical Agda Formalisation of Coinductive ζ(2k)

We give a full Cubical Agda formalisation of the coinductive digit-stream witness for ζ(2k)/2, with a constructive Bernoulli library using only the generating-function recurrence and exact rationals. We prove the central contractibility theorem and provide a Lean 4 shadow using Mathlib.