Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Uncountable Singleton Cut Countermodel

Abstract

Uncountably many singleton cuts cover every defect edge, while each finite selection leaves Lebesgue charge one and escape spectrum one.

Let J be the actual closed unit interval in the real numbers, with its Lebesgue probability measure mu, and let X be J times Bool. The base readout reads the interval coordinate and the target reads the Boolean coordinate. Every t in J supplies the definition d_t(s,i), equal to i when s=t and false otherwise. All definitions have cost one.

The supported algebra contains exactly the subsets of E whose two interval sections are NullMeasurableSet for mu. This predicate is measurability for completed Lebesgue measure. Under the interval inclusion, it is equivalent to Lebesgue measurability of the real image, with the same measure on every interval set. The half-sum formula defines nu on every ambient set of pairs. Interval probability makes both section measures finite, so their toNNReal conversions preserve their values. The real weight w is the coercion of this same AddContent.

Theorem 1.1 (Every finite residual has mass one).

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/EscapeSpectrum/UncountableSingletonCutCountermodel.finite_residual_mass_eq_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite selection S from the full language, the actual Option-valued finiteSelectionSupplement leaves each directed edge precisely when its basepoint is absent from P(S). The finite image P(S) has Lebesgue measure zero. Both residual sections therefore have measure one, and their half-sum is one.

Theorem 1.2 (The full uncountable cover and all finite budget spectra).

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/EscapeSpectrum/UncountableSingletonCutCountermodel.uncountable_singleton_cut_countermodel (✓ std3). ∎

Source. Repository-derived.

Commentary.

The interval language is nonempty and uncountable. Evaluation at (t,true) distinguishes its definitions, so their range is uncountable as well. Each singleton cut contains exactly the two directed edges over its basepoint. Every edge is cut by its own definition; this proves the full cover pointwise and makes the common blind residual empty. The algebra is a ring with complements relative to E, and the subtype carrier correspondence is exact in both directions. The charge is supported on E, has total mass one, is globally monotone and nonnegative, and is additive for disjoint algebra members. Finite cut unions have mass zero; each residual and its difference from B belong to the algebra and satisfy the common blind decomposition. A finite selection costs its cardinality. The empty selection is affordable for every NNReal budget, including zero. The finite residual equality gives the affordable mass set {1}, hence canonical spectrum one at every budget. The positive baseline and global monotonicity identify its limit with the all-finite infimum one. The blind ratio is zero and differs strictly from that limit. The full uncountable cover is a pointwise identity; each budget continues to permit only finite selections.

References