Clopen disjointization
Abstract
Nonmetric finite-history clopen selection and paired-sign signed normalization.
K is an arbitrary compact Hausdorff zero-dimensional Borel space. Regularity is required for the actual input probabilities or total variations; it is not inferred for arbitrary Borel measures. The construction uses classical choice, a free ultrafilter and positive RMK. It makes no effective or choice-free claim.
Theorem 1.1 (Disjoint clopens retaining probability mass).
Proof. Machine-checked in Lean as D5/S3/Topology/Measures/ClopenDisjointization.exists_clopen_disjointization (✓ std3). ∎
Source. Repository-derived.
Commentary.
Compactness of ProbabilityMeasure K gives a free-ultrafilter cluster nu. Positive RMK represents integration against nu by a regular lambda. RMK finiteness on compact sets gives finiteness on K before evaluating one to prove lambda(K)=1. The representing identity tests every fixed clopen indicator; it does not identify nu and lambda on all Borel sets.
Countable additivity makes lambda(E_n) summable and hence convergent to zero. The recursive state contains the next allowed index and the actual preceding clopen union P, with lambda.real(P)<eta/8. Set delta=(eta/8-lambda.real(P))/2. Intersect the ultrafilter-large fixed-P test mu_n(P)<eta/4, the eventual bound lambda(E_n)<delta, and the increasing-index tail. Regularity of the selected input supplies a compact core inside E_n minus P with mass greater than 1-eta/2. Outer regularity of lambda and the zero-dimensional clopen sandwich give a clopen W containing that core, avoiding all of P and of lambda mass below delta. The new union remains below eta/8, so ordinary recursion yields increasing indices and actual pairwise disjoint nonempty clopens. No countable filter intersection, moving-Borel convergence, metrizability or sequential compactness is used.
Theorem 1.2 (Total-variation normalization and one paired common sign).
Proof. Machine-checked in Lean as D5/S3/Topology/Measures/ClopenDisjointization.exists_signed_clopen_disjointization (✓ std3). ∎
Source. Repository-derived.
Commentary.
Apply the positive construction to the actual regular total variations. For q=totalVariation(v)(W)>0, define t=q inverse times the restriction of v to W. The variation/restriction and variation/scalar interfaces are required: signed mass v(W), which may vanish by cancellation, is not the normalization factor. Regularity survives measurable restriction and finite positive rescaling. The normalized measure has total variation one and zero total variation on the complement of W.
Restrict t-v separately to W and its complement. Their variations have masses (q inverse minus one)q and 1-q. Additivity of the variation measure gives the exact error 2(1-q), including q=1. An infinite pigeonhole argument selects one sign and a further increasing subsequence with positive Jordan mass at least one half. The same sign multiplies BOTH the approximant and the corresponding original, preserving the exact error. A fixed positive approximation bound supplies no weak-star convergence of t; the theorem asserts none.
The ordinary selection argument is classical background, not a novelty claim. The source-level suppliers are the pinned Mathlib Prokhorov forward compactness theorem, positive RealRMK, finite-measure summability, regularity, the clopen sandwich, and the signed/Jordan variation interfaces. Library/Topology/kania2026talagrand.md records the application boundary and the local kernel-checked supplier provenance. Neither local theorem proves KPR, the signed A-G recursion, final capture, the Grothendieck C(T) endpoint or exclusion in the whole signed dual unit ball. Information audit remains unfinished for both theorem targets: the source equivalence and actual-positive bridges are present, while Contract.Registration, whole-family variation, sensitivity, observational dependence, enrolled readout binding and complete raw sourceSelection evidence are absent. The target-specific unfinished registration is tracked at https://github.com/the-omega-institute/trureturing/issues/20708; the broader source-reconstruction context is https://github.com/the-omega-institute/trureturing/issues/16293. No registration retry is performed here, and neither theorem has a declared_validated registration.