Neighborhood ideal and common color support
Abstract
Convergent maximal families have large value neighborhoods and a common threshold color support.
Information audit is unfinished: the exact source scope and compiled Reg attempt do not establish validated raw source reconstruction. The concrete missing evidence for this theorem is tracked in https://github.com/the-omega-institute/trureturing/issues/16293. This does not add a mathematical assumption or claim a complete adaptive-refinement counterexample.
InFiniteUnionIdeal(M,E) means that E is contained in the union of finitely many actual M(x), together with a finite set. ColorSupport(M,u,D) contains the r for which every neighborhood V of r has u-preimage(V) intersected with D outside this ideal. LowerThird is {n : natValue(n) ≤ 1/3}; UpperTwoThirds is {n : natValue(n) < 2/3}. All inequalities concern the real coercion of the unit-interval value. nhds, preimage, inter and compl denote literal Lean neighborhoods and set operations.
Theorem 1.1 (Actual maximal family with large value neighborhoods).
Proof. Machine-checked in Lean as D5/S3/Topology/AlmostDisjoint/NeighborhoodIdeal.exists_mad_with_no_small_neighborhood (✓ std3). ∎
Source. Repository-derived.
Commentary.
The existing branch-labeled convergent maximal family is retained in full. Every value fiber has continuum many branch labels, so a label can be chosen outside any given finite family. Its infinite member has only finitely many points outside the value neighborhood and only finitely many intersections with the proposed cover members. A finite cover plus a finite exceptional set would make that member finite, a contradiction.
Theorem 1.2 (Exact thresholds force a common color support).
Proof. Machine-checked in Lean as D5/S3/Topology/AlmostDisjoint/NeighborhoodIdeal.threshold_common_color_support (✓ std3). ∎
Source. Repository-derived.
Commentary.
The generated ideal is closed under taking subsets and finite unions. Each color support is closed: a small neighborhood at r contains an open smaller neighborhood witnessing smallness at every point in it. The two supports cover the interval, since two small colored neighborhoods would make their intersection a small uncolored neighborhood.
The lower threshold excludes zero from the complement-color support, and the upper threshold excludes one from the D-color support. Connectedness of unitInterval therefore gives a point in both closed supports. The partitioner diagonal, uncountability and continuum size of both limit-color fibers, separator elimination, compact counterexample, and Ref classification remain unproved.