Registry · Theorem I.T49 tau-effective formalized

I.T49 — Countable Additivity

The stage-k counting measure is finitely additive: for disjoint subsets S, T of Z/M_k Z, μ_k(S ∪ T) = μ_k(S) + μ_k(T). Verified computationally at stage 3 for even/odd and B/C sector partitions.

Book I Part 18 Ch. 84

Dependency Graph

Depends on (2)

Depended on by (1)

Lean Formalization

Module: TauLib.BookI.Boundary.Measure

Symbol: additivity_even_odd_3