Countable joint finite-block fusion

Abstract

A countable finite-block selector jointly preserves fixed reservoirs and one-sided cofinite inclusions.

The active predicate records delayed proper-stage domains. The displayed finite set consists of exactly the labels k active in block j. Every block has a finite active fibre, and every label is active from some stage onward. I and J are inherited stage sets; N is the literal fixed reservoir family, with both Bool colours retained. EventuallySubset uses the cofinite filter, so the conclusion is one-sided finite difference rather than symmetric difference.

Theorem 1.1 (Joint selector and countable limit sets).

$$\forall active\in Nat\to Nat\to Prop,\forall I\in Nat\to \mathrm{Set}\left(Nat\right),\forall J\in Nat\to Nat\to \mathrm{Set}\left(Nat\right),\forall N\in Nat\to Bool\to \mathrm{Set}\left(Nat\right),\left(\left(\forall j\in Nat,\mathrm{Finite}\left(\{k:Nat|\mathrm{active}\left(k,j\right)\}\right)\right)\wedge \left(\left(\forall k\in Nat,\exists j0\in Nat,\forall j\in Nat,\mathrm{Le}\left(j0,j\right)\Rightarrow \mathrm{active}\left(k,j\right)\right)\wedge \left(\left(\forall k\in Nat,\forall j\in Nat,\mathrm{active}\left(k,j\right)\Rightarrow \mathrm{Subset}\left(J\left(k,j\right),I\left(j\right)\right)\right)\wedge \left(\left(\forall h\in Nat,\forall j\in Nat,\mathrm{Le}\left(h,j\right)\Rightarrow \mathrm{EventuallySubset}\left(cofinite,I\left(j\right),I\left(h\right)\right)\right)\wedge \left(\left(\forall k\in Nat,\forall h\in Nat,\forall j\in Nat,\left(\mathrm{active}\left(k,h\right)\wedge \left(\mathrm{active}\left(k,j\right)\wedge \mathrm{Le}\left(h,j\right)\right)\right)\Rightarrow \mathrm{EventuallySubset}\left(cofinite,J\left(k,j\right),J\left(k,h\right)\right)\right)\wedge \left(\forall k\in Nat,\forall j\in Nat,\forall e\in Bool,\mathrm{active}\left(k,j\right)\Rightarrow \mathrm{Infinite}\left(\mathrm{inter}\left(J\left(k,j\right),N\left(k,e\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\exists v\in Nat\to Nat\to Bool\to Nat,\exists Ilim\in \mathrm{Set}\left(Nat\right),\exists Jlim\in Nat\to \mathrm{Set}\left(Nat\right),\left(\forall j\in Nat,\forall k\in Nat,\forall e\in Bool,\mathrm{active}\left(k,j\right)\Rightarrow \left(\mathrm{Lt}\left(j,v\left(j,k,e\right)\right)\wedge \left(\mathrm{Member}\left(v\left(j,k,e\right),J\left(k,j\right)\right)\wedge \left(\mathrm{Member}\left(v\left(j,k,e\right),N\left(k,e\right)\right)\wedge \left(\left(\forall h\in Nat,\mathrm{Le}\left(h,j\right)\Rightarrow \mathrm{Member}\left(v\left(j,k,e\right),I\left(h\right)\right)\right)\wedge \left(\forall h\in Nat,\mathrm{Le}\left(h,j\right)\Rightarrow \left(\mathrm{active}\left(k,h\right)\Rightarrow \mathrm{Member}\left(v\left(j,k,e\right),J\left(k,h\right)\right)\right)\right)\right)\right)\right)\right)\right)\wedge \left(\left(\forall k\in Nat,\forall n\in Nat,\mathrm{Member}\left(n,\mathrm{Jlim}\left(k\right)\right)\iff \left(\exists j\in Nat,\exists e\in Bool,\mathrm{active}\left(k,j\right)\wedge n=v\left(j,k,e\right)\right)\right)\wedge \left(Ilim=\mathrm{iUnion}\left(Jlim\right)\wedge \left(\left(\forall k\in Nat,\forall e\in Bool,\mathrm{Infinite}\left(\mathrm{inter}\left(\mathrm{Jlim}\left(k\right),N\left(k,e\right)\right)\right)\right)\wedge \left(\left(\forall h\in Nat,\mathrm{EventuallySubset}\left(cofinite,Ilim,I\left(h\right)\right)\right)\wedge \left(\forall k\in Nat,\forall h\in Nat,\mathrm{active}\left(k,h\right)\Rightarrow \mathrm{EventuallySubset}\left(cofinite,\mathrm{Jlim}\left(k\right),J\left(k,h\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

For each active triple (j,k,e), the proof removes the finitely many earlier I and same-label J exceptions from the infinite pool J(k,j) intersect N(k,e), and also imposes j<n. Classical choice selects one witness. Inactive triples are not inserted into Jlim.

The lower bound j<v(j,k,e) makes every fixed Jlim(k) intersect N(k,e) infinitely often once k is eventually active. Values from blocks before a fixed h form a finite set because each block has finitely many active labels and two colours; all later values satisfy the earlier I and J constraints. This proves the stated one-sided cofinite inclusions.

The proper-limit manuscript application supplies active(k,j) from a cofinal sequence of proper stages, with N unchanged. The selector applies only at proper countable limits; no final-stage I, J or N bookkeeping is part of this target. This result does not supply the ordinal adapter, successor residual initialization, analytic F or G clauses, lift existence, or transfinite CH recursion. The final inverse-limit model and its analytic endpoints remain outside this supplier, as do the full Talagrand K_r/V_n construction and a solution of Problem 8.2.

References

• Truth anchor: D5/S3/Topology/InverseLimit/CountableJointFusion.exists_countable_joint_finite_block_fusion