Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Exact countable signed norm reflection

Abstract

One proper stage preserves the whole countable signed family’s total variation and Jordan masses and reflects the supplied clopens.

CountableStage is the actual subtype of ordinals strictly below omega-one. F is a Profinite diagram on its opposite category, with nonempty carriers, Borel measurable structures and surjective bonding maps. C is the actual limit cone with its Borel measurable structure. NonemptyBorelComponents abbreviates exactly these component hypotheses; BorelLimitCone includes the IsLimit witness and Borel structure of the cone point. In the formula mass is measure application, posPart and negPart are the actual Jordan parts, map is signed pushforward and measureMap is positive-measure pushforward. Profinite1 fixes universe one and CountableStageOpp is the opposite stage category. s is any natural-indexed family of actual finite real signed measures with regular total variation. I is any countable type, including the empty type, and W is any I-indexed clopen family.

Theorem 1.1 (One common proper stage with exact signed masses).

Proof. Machine-checked in Lean as D5/S3/Topology/InverseLimit/CountableSignedMeasureReflection.exists_common_stage (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Tomasz Kania and Jerzy Kakol (2026). Talagrand compacta, 2DCP, and pointwise quotients. URL: https://arxiv.org/abs/2607.06808v2.

Commentary.

There is beta at or above the prescribed base, still strictly below omega-one. Each W(i) is the full inverse image of a clopen V(i) under the actual beta projection. Nonemptiness and all pairwise disjointness relations are equivalent at the final and beta levels. For every later proper gamma with beta <= gamma and every n, the pushed signed measure has exactly the original total variation, positive Jordan and negative Jordan whole masses. These masses are in extended nonnegative real units, not a normalized replacement. Its variation measure equals the pushforward of the original variation. At beta, variation-nullity of the complement of V(i) is equivalent to original variation-nullity of the complement of W(i), for every n and i.

RegularSignedLift.regular_jordanParts_of_regular_totalVariation supplies regularity of both original Jordan parts. PositiveClopenMass.exists_isClopen_subset_lt_apply_of_lt_posPart gives A(n,k) with signed mass greater than the positive whole mass minus 1/(k+1), including zero positive mass. CountableClopenReflection.exists_common_stage reflects the disjoint union of the entire witness family and W at one beta. Signed evaluation on every witness is unchanged. Each evaluation is bounded by the pushed positive whole mass. Variation contraction and preservation of total signed mass imply the opposite upper bound on the pushed positive mass, using twice positive mass = variation mass + signed mass. Archimedean squeezing forces equality. Jordan subtraction then gives negative-mass equality and addition gives variation-mass equality. No regularity of the pushed Jordan parts is used in this squeeze, and no projection is assumed isometric.

For beta <= gamma, cone naturality identifies projection to beta with projection to gamma followed by its bonding map. Positive-mass contraction for the two maps sandwiches the mass at gamma between equal endpoint masses. NormPreservingLifts.totalVariation_map_of_mass upgrades equality of whole variation mass to equality of the variation measures. Evaluation of this equality on clopen complements proves the stated support-nullity equivalence.

Application to SignedBirthEnumeration.BornData uses I = Nat and a supplied disjoint nonempty clopen support family W. The reflected V is a SupportFamily by the two exact equivalences. If each original signed measure has variation whole mass one, positive Jordan whole mass at least one half and zero variation outside W(n), the pushed whole sequence has those same three properties. Continuous pushforward of the original regular finite variation is regular; the proved variation-measure identity and RegularSignedLift recover regular Jordan parts at beta. Hence this is legal whole BornData at that one beta. On a live CH path, exists_signed_enumeration chooses one label for this entire BornData value at the actual launch row; labels are not chosen separately for individual terms. No CH hypothesis is needed for reflection itself. This supplier neither constructs the transfinite compactum nor provides a full raw history, final collision or a solution to the CH signed Talagrand problem.

References