Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite marginals and ordered split geometry

Abstract

Fixed finite signed marginals and exact clopen traces in ordered closed splits.

K is a compact Borel space. L is a Hausdorff Borel space and p is continuous. The measures are arbitrary real SignedMeasure values. A candidate and its reference have the same signed base projection and the same total variation mass as that base measure. The base variation vanishes outside the given clopen support. Each fixed Boolean coordinate eventually becomes constant on the whole base fibres in that support.

Theorem 1.1 (Uniform fixed finite signed marginals).

Proof. Machine-checked in Lean as D5/S3/Topology/Measures/SignedSplitSuccessorSupport.eventually_uniform_finite_marginal (✓ std3). ∎

Source. Repository-derived.

Commentary.

For the finite coordinate map, each clopen atom has the same signed mass for every admissible lift. The signed reference limit gives convergence on these finitely many atoms. Summing their absolute differences computes the total variation mass of the finite signed difference and makes the estimate uniform over all lifts.

Exact mass preservation for p separately identifies the pushed positive variations. Applying whole-fibre constancy to their clopen tests proves equality of the positive finite marginals. No preservation of variation by the finite-coordinate map is asserted: it can identify opposite signed atoms. The finite coordinate type may be empty and the filter is arbitrary.

Theorem 1.2 (Auxiliary index in the prescribed infinite reservoir).

Proof. Machine-checked in Lean as D5/S3/Topology/Measures/SignedSplitSuccessorSupport.exists_auxiliary_index (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix the finite Boolean coordinate family before choosing the next index. The reservoir S is any infinite subset of the natural numbers, such as one of the inherited fixed parity pools. Reference signed convergence and whole-fibre coordinate constancy hold along atTop intersect principal(S). The pulled-back row supports are pairwise disjoint, and v is any finite positive measure on K.

Their v masses form a summable sequence and tend to zero. The uniform fixed-marginal estimate, all finitely many coordinate conditions, this small-mass tail and the lower index bound hold together eventually in S. Infinitude supplies a member beyond the resulting finite threshold. The chosen index retains the original reservoir; it satisfies both signed and positive marginal conclusions without changing a parity set.

Theorem 1.3 (Target index for all fixed finite exclusions).

Proof. Machine-checked in Lean as D5/S3/Topology/Measures/SignedSplitSuccessorSupport.exists_target_index (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix a finite family of clopen sets A(j). The positive variation evaluations of the reference lifts converge on these fixed sets to v(A(j)), each strictly below its prescribed bound b(j). Whole-fibre constancy for membership in every A(j) holds eventually in the infinite reservoir S. Exact preservation of base variation transfers each reference evaluation to every signed lift in its norm-preserving class.

A finite intersection of the resulting eventual conditions and a lower index bound leaves an infinite tail in S. One target index therefore controls every exclusion simultaneously for every signed lift. The same selected index retains whole-fibre constancy of every exclusion. The family may be empty. The input is fixed-test convergence of positive variations; it assumes neither a moving-test estimate nor a signed weak-star limit for those variations.

Theorem 1.4 (Signed target piece after exclusion).

Proof. Machine-checked in Lean as D5/S3/Topology/Measures/SignedSplitSuccessorSupport.exists_signed_target_piece (✓ std3). ∎

Source. Repository-derived.

Commentary.

The target is an arbitrary real signed measure nu on a compact Hausdorff zero-dimensional Borel space L. Its Jordan parts are regular, its variation vanishes off the clopen V, and its positive mass is at least one half. The continuous p maps K to L. For every lift preserving signed projection and total variation mass, the clopen exclusion R has variation mass at most one sixteenth.

Positive-clopen approximation gives a clopen B inside V with nu(B) greater than one third. Put H=p inverse(B) minus R. For every such signed lift t, its mass on p inverse(B) is nu(B), while t on the removed intersection is at most its variation on R. Thus t(H) is greater than one third minus one sixteenth, namely thirteen forty-eighths, which is greater than one sixth. The selected H is shared by all lifts. The output retains the clopen B, its containment in V, and the literal equation H=p inverse(B) minus R.

Theorem 1.5 (Target after the finite earlier exclusions).

Proof. Machine-checked in Lean as D5/S3/Topology/Measures/SignedSplitSuccessorSupport.exists_target_after_finite_exclusion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite row set A and earlier columns j<q are fixed before the target index is selected. Distinct row codes give the budget (1/64)(1/2)^(code(r))(1/2)^j. The sum of all such budgets is at most one sixteenth, including when A or the earlier column set is empty.

The positive reference variation on each fixed clopen exclusion is strictly below its budget. Positive-variation convergence and whole-fibre constancy select one larger target index for which every signed norm-preserving lift obeys all those bounds. Finite subadditivity therefore bounds the variation of their whole union by one sixteenth. Positive clopen approximation then constructs the common H outside the union with signed mass greater than thirteen forty-eighths, hence greater than one sixth, for every lift. The literal base slice is retained, and the earlier exclusion tests prove whole-target-fibre constancy of H at this same selected index.

Definition 1.6 (Literal split carrier).

Formalization. D5/S3/Topology/Measures/SignedSplitSuccessorSupport.splitCarrier (✓ std3).

Source. Repository-derived.

Commentary.

The carrier is a literal subset of K times Bool. Points on the zero side lie over Y and points on the one side lie over Z.

Definition 1.7 (Finite even prefix).

Formalization. D5/S3/Topology/Measures/SignedSplitSuccessorSupport.evenPrefix (✓ std3).

Source. Repository-derived.

Commentary.

The union ranges over s in range(q+1), retaining H(s) exactly when s modulo two is zero. It is clopen when each H(s) is clopen.

Theorem 1.8 (Closed split from ordered exclusion).

Proof. Machine-checked in Lean as D5/S3/Topology/Measures/SignedSplitSuccessorSupport.exists_closed_split_of_ordered_exclusion (✓ std3). ∎

Source. Repository-derived.

Commentary.

For each row r and active column q, every later H(s) avoids the entire clopen support W(r,q). Consequently the union of all even H(s) and its finite even prefix have exactly the same trace on W(r,q). Closure preserves this trace because both the support and the finite prefix are clopen.

Define Z as the closure of the full even union and Y as the closure of its complement. These closed sets cover K. Their local traces are complementary, so their common boundary avoids each active support. The literal split is closed, its first projection is surjective, and its new Boolean coordinate on an active support is precisely membership in the finite prefix. Pairwise disjoint clopen target supports T(q), with H(q) contained in T(q), have exact traces H(q) on even q and the empty set on odd q, including q=0. Their boundaries are excluded as well. The row type can be finite, including a single row.

References