Lean 4 formalisation of the two examples in 'Uniform sheafy Tate rings that are not stably uniform' (Birkbeck-Torzewski), kernel-certified with leanprover/comparator