Free Ultrafilter Charge Countermodel

Abstract

A free ultrafilter gives full residual mass at every finite budget, although the common blind residual is empty.

Definition 1.1 (The two-sign full-powerset charge).

$$\begin{array}{r}X=\mathbb{N}\times \mathrm{Bool}\left(\right)\\ q:X\to \mathbb{N},T:X\to \mathrm{Bool}\left(\right)\\ \forall k:\mathbb{N},\forall i:\mathrm{Bool}\left(\right),q((k,i))=k\\ \forall k:\mathbb{N},\forall i:\mathrm{Bool}\left(\right),T((k,i))=i\\ \Gamma =\mathrm{setOf}\left(n:\mathbb{N},1\le n\right)\\ d:\mathbb{N}\to X\to \mathrm{Bool}\left(\right)\\ \forall n:\mathbb{N},\forall k:\mathbb{N},\forall i:\mathrm{Bool}\left(\right),d(n)((k,i))=\mathrm{ite}\left(k\le n,i,\mathrm{false}\left(\right)\right)\\ c:\mathbb{N}\to \mathbb{R}\\ \forall n:\mathbb{N},c(n)=1\\ e:\mathrm{Bool}\left(\right)\to \mathbb{N}\to X\times X\\ \forall b:\mathrm{Bool}\left(\right),\forall k:\mathbb{N},e(b)(k)=((k,b),(k,\mathrm{BoolNot}\left(b\right)))\\ E=\mathrm{defectRelation}\left(q,T\right)\\ U=\mathrm{hyperfilter}\left(\mathbb{N}\right)\\ \mu :\mathrm{Set}\left(\mathbb{N}\right)\to \mathrm{NNReal}\left(\right)\\ \forall C:\mathrm{Set}\left(\mathbb{N}\right),\mu (C)=\mathrm{toNNReal}\left(\mathrm{ultrafilterCharge}\left(U,C\right)\right)\\ \nu :\mathrm{AddContent}\left(\mathrm{NNReal}\left(\right),\mathrm{univ}\left(\right):\mathrm{Set}\left(\mathrm{Set}\left(X\times X\right)\right)\right)\\ \forall C:\mathrm{Set}\left(X\times X\right),\nu (C)=\frac{1}{2}\mu (\mathrm{preimage}\left(e(\mathrm{false}\left(\right)),C\right))+\frac{1}{2}\mu (\mathrm{preimage}\left(e(\mathrm{true}\left(\right)),C\right))\\ w:\mathrm{EscapeWeight}\left(X\times X\right)\\ \forall C:\mathrm{Set}\left(X\times X\right),\mathrm{mass}\left(w,C\right)=\mathrm{coeReal}\left(\nu (C)\right)\\ \forall S:\mathrm{Finset}\left(\Gamma \right),R(S)=\mathrm{defectRelation}\left(\mathrm{conceptJoin}\left(q,\mathrm{finiteSelectionSupplement}\left(\Gamma ,d,S\right)\right),T\right)\\ B=\mathrm{intersection}\left(E,\mathrm{jointKernel}\left(i:\Gamma \mapsto d(\mathrm{val}\left(i\right))\right)\right)\\ \forall n:\mathbb{N},F(n)=\mathrm{FinsetImage}\left(j\mapsto \mathrm{subtype}\left(j+1,\Gamma \right),\mathrm{FinsetRange}\left(n\right)\right)\\ \forall n:\mathbb{N},A(n)=R(F(n+1))\end{array}$$

Formalization. D5/S3/ConceptDynamics/EscapeSpectrum/FreeUltrafilterChargeCountermodel.edgeCharge (✓ std3).

Source. Repository-derived.

Acknowledgement. Patrick S. Mahon (2026). The ultrafilter charge on P(ℕ). URL: https://github.com/pmahon3/Resolvent_Framework/blob/d01936f728ba0eb67e9bb2c07b8d451c5de4b5f8/formalization/QuerySystem/QuerySystem/UltrafilterCharge.lean.

Commentary.

The state space is the natural numbers times Bool, with false and true representing the two signs. The base readout forgets the sign and the target reads it. Only positive cutoffs belong to the language. The charge is defined on every set of pairs; its restriction to P(E) is the source charge. The real weight is the coercion of this AddContent.

Theorem 1.2 (The scalar membership formula).

$$\forall C:\mathrm{Set}\left(\mathbb{N}\right),\mu (C)=\mathrm{ite}\left(C\in U,1,0\right)$$

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

Source. Repository-derived.

Acknowledgement. Patrick S. Mahon (2026). The ultrafilter charge on P(ℕ). URL: https://github.com/pmahon3/Resolvent_Framework/blob/d01936f728ba0eb67e9bb2c07b8d451c5de4b5f8/formalization/QuerySystem/QuerySystem/UltrafilterCharge.lean.

Commentary.

The ENNReal membership charge has only values zero and one. Its finite-valued conversion to NNReal therefore has the displayed formula. Disjoint additivity is inherited from the ultrafilter charge through toNNReal_add. The chosen ultrafilter is hyperfilter Nat.

Theorem 1.3 (Every finite selected residual contains a tail).

$$\forall S:\mathrm{Finset}\left(\Gamma \right),\forall b:\mathrm{Bool}\left(\right),\mathrm{preimage}\left(e(b),R(S)\right)=\mathrm{setOf}\left(k:\mathbb{N},\forall j:\Gamma ,(j\in S)\Rightarrow \mathrm{val}\left(j\right)<k\right)$$

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

Source. Repository-derived.

Acknowledgement. Patrick S. Mahon (2026). The ultrafilter charge on P(ℕ). URL: https://github.com/pmahon3/Resolvent_Framework/blob/d01936f728ba0eb67e9bb2c07b8d451c5de4b5f8/formalization/QuerySystem/QuerySystem/UltrafilterCharge.lean.

Commentary.

The canonical residual decomposition makes an edge survive precisely when its index exceeds every selected cutoff. The empty selection gives the whole natural-number preimage. For any finite selection, the tail above its largest cutoff belongs to the free ultrafilter; both signs consequently have scalar mass one.

Theorem 1.4 (All affordable masses equal one).

$$\forall L:\mathrm{NNReal}\left(\right),\mathrm{finiteBudgetMassValues}\left(\Gamma ,d,q,T,c,w,L\right)=\mathrm{singleton}\left(1\right)$$

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

Source. Repository-derived.

Acknowledgement. Patrick S. Mahon (2026). The ultrafilter charge on P(ℕ). URL: https://github.com/pmahon3/Resolvent_Framework/blob/d01936f728ba0eb67e9bb2c07b8d451c5de4b5f8/formalization/QuerySystem/QuerySystem/UltrafilterCharge.lean.

Commentary.

The cost of a finite selection is its cardinality as a real number. The empty selection has cost zero and is affordable at every NNReal budget, including zero. Thus the set whose infimum defines the canonical budget envelope is exactly the singleton one.

Theorem 1.5 (Finite escape persists without decreasing-chain continuity).

$$\begin{array}{r}(\mathrm{Countable}\left(\Gamma \right))\wedge \\ (\mathrm{Nonempty}\left(\Gamma \right))\wedge \\ (\mathrm{Injective}\left(i:\Gamma \mapsto d(\mathrm{val}\left(i\right))\right))\wedge \\ (\forall i:\mathbb{N},(i\in \Gamma )\Rightarrow 0<c(i))\wedge \\ (\forall S:\mathrm{Finset}\left(\Gamma \right),\mathrm{finiteSelectionCost}\left(\Gamma ,c,S\right)=\mathrm{coeReal}\left(\mathrm{card}\left(S\right)\right))\wedge \\ (E=\mathrm{range}\left(e(\mathrm{false}\left(\right))\right)\cup \mathrm{range}\left(e(\mathrm{true}\left(\right))\right))\wedge \\ (\mathrm{toFilter}\left(U\right)\le \mathrm{cofinite}\left(\mathbb{N}\right))\wedge \\ (\forall C:\mathrm{Set}\left(\mathbb{N}\right),(\mathrm{Finite}\left(C\right))\Rightarrow \neg (C\in U))\wedge \\ (\forall C:\mathrm{Set}\left(\mathbb{N}\right),\mu (C)=\mathrm{ite}\left(C\in U,1,0\right))\wedge \\ (\forall C:\mathrm{Set}\left(X\times X\right),\nu (C)=\frac{1}{2}\mu (\mathrm{preimage}\left(e(\mathrm{false}\left(\right)),C\right))+\frac{1}{2}\mu (\mathrm{preimage}\left(e(\mathrm{true}\left(\right)),C\right)))\wedge \\ (\forall C:\mathrm{Set}\left(X\times X\right),\nu (C)=\nu (\mathrm{intersection}\left(C,E\right)))\wedge \\ (\nu (\varnothing )=0)\wedge \\ (\mathrm{Monotone}\left(C:\mathrm{Set}\left(X\times X\right)\mapsto \nu (C)\right))\wedge \\ (\forall C:\mathrm{Set}\left(X\times X\right),0\le \mathrm{coeReal}\left(\nu (C)\right))\wedge \\ (\forall C:\mathrm{Set}\left(X\times X\right),\forall D:\mathrm{Set}\left(X\times X\right),(\mathrm{Disjoint}\left(C,D\right))\Rightarrow \nu (C\cup D)=\nu (C)+\nu (D))\wedge \\ (\nu (E)=1)\wedge \\ (B=\varnothing )\wedge \\ (\forall S:\mathrm{Finset}\left(\Gamma \right),\mathrm{finiteResidualMass}\left(\Gamma ,d,q,T,w,S\right)=1)\wedge \\ (\forall n:\mathbb{N},(1\le n)\Rightarrow R(F(n))=\mathrm{image}\left(e(\mathrm{false}\left(\right)),\mathrm{Ioi}\left(n\right)\right)\cup \mathrm{image}\left(e(\mathrm{true}\left(\right)),\mathrm{Ioi}\left(n\right)\right))\wedge \\ (\mathrm{Monotone}\left(F\right))\wedge \\ (\forall i:\Gamma ,\exists n:\mathbb{N},i\in F(n+1))\wedge \\ (\mathrm{Antitone}\left(A\right))\wedge \\ (\mathrm{iInter}\left(n:\mathbb{N},A(n)\right)=\varnothing )\wedge \\ (\neg \mathrm{Tendsto}\left(n:\mathbb{N}\mapsto \mathrm{coeReal}\left(\nu (A(n))\right),\mathrm{atTop}\left(\right),\mathrm{nhds}\left(\mathrm{coeReal}\left(\nu (\varnothing )\right)\right)\right))\wedge \\ \forall L:\mathrm{NNReal}\left(\right),\mathrm{finiteEscapeSpectrum}\left(\Gamma ,d,q,T,c,w,L\right)=1.\end{array}$$

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

Source. Repository-derived.

Acknowledgement. Patrick S. Mahon (2026). The ultrafilter charge on P(ℕ). URL: https://github.com/pmahon3/Resolvent_Framework/blob/d01936f728ba0eb67e9bb2c07b8d451c5de4b5f8/formalization/QuerySystem/QuerySystem/UltrafilterCharge.lean.

Commentary.

The positive cutoffs are distinct definitions and form a countable nonempty language with unit costs. Each actual residual edge is eventually separated, so the common blind residual is empty. The exhausting initial segments leave exactly the two tails shown. Their antitone residual chain has empty intersection but constant mass one, whereas the empty set has mass zero. Normalization by the baseline mass one makes every finite nonnegative budget’s canonical spectrum equal one. The standard classical hyperfilter construction supplies the free ultrafilter; no additional existence or continuity hypothesis is assumed.

References

• Truth anchor: D5/S3/ConceptDynamics/EscapeSpectrum/FreeUltrafilterChargeCountermodel.edgeCharge
• Truth anchor: D5/S3/ConceptDynamics/EscapeSpectrum/FreeUltrafilterChargeCountermodel.finite_budget_values_eq_singleton
• Truth anchor: D5/S3/ConceptDynamics/EscapeSpectrum/FreeUltrafilterChargeCountermodel.free_ultrafilter_charge_countermodel
• Truth anchor: D5/S3/ConceptDynamics/EscapeSpectrum/FreeUltrafilterChargeCountermodel.mu_formula
• Truth anchor: D5/S3/ConceptDynamics/EscapeSpectrum/FreeUltrafilterChargeCountermodel.residual_edge_preimage
• Dependency: D5/S3/ConceptDynamics/EscapeSpectrum/BlindResidualChargeDecomposition