RetractiveReservoir
Abstract
Classical arbitrary-set retractive attachment supplier; original Efimov KPI 0.
The pinned Scribe projection corpus does not contain these new declarations. Each node therefore uses the supported no-formula presentation and records its native projection gap; the exact Lean signature and full ambient parameters are reproduced below. The validated scoped report separately contains the complete kernel statement-v1 ASTs. The scientific source and independent ordinary review are identified in the cited Library note; neither source-level review nor this exposition substitutes for kernel checking.
Universes u v w are arbitrary and all parameters and hypotheses are displayed in the Lean signature below. Space, core and limitMap are the literal constructions documented in RetractiveAttachment and CompactRangePersistence. SmallCategory J and IsCofilteredOrEmpty J impose no cofinality bound; a nonempty ordinal inverse prefix is one instance. The stagewise hypotheses concern actual compact Hausdorff component spaces, natural continuous attachment maps and one actual common core thread. The conclusion uses the actual final coherent-thread spaces and the literal attachment topology.
Theorem 1.1 (Direct consumed reservoir obstruction in the final actual carrier).
Lean statement: D5/S3/Topology/InverseLimit/RetractiveReservoir.persistent_reservoir_sequence
Proof. Machine-checked in Lean as D5/S3/Topology/InverseLimit/RetractiveReservoir.persistent_reservoir_sequence (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Supplied independent mathematical source and reviewer (2026). Evolving continuous attachments and persistent compact range reservoirs. URL: https://github.com/the-omega-institute/trureturing.
Commentary.
Exact Lean signature, under the ambient parameters stated above: theorem persistent_reservoir_sequence {J : Type u} [SmallCategory J] [IsCofilteredOrEmpty J] {I : Type w} (G : J ⥤ TopCat.{max u v}) (F : I → J ⥤ TopCat.{max u v}) (t : ∀ i, F i ⟶ G) [∀ i j, CompactSpace ((F i).obj j)] [∀ i j, T2Space ((F i).obj j)] [∀ j, T2Space (G.obj j)] (b : (TopCat.limitCone G).pt) (R : Set I) (hR : R.Infinite) (hb : ∀ i ∈ R, ∀ j, b.val j ∈ range ((t i).app j)) : (∀ i ∈ R, b ∈ range (limitMap (F i) G (t i))) ∧ ∃ x : ℕ → Space (fun i => limitMap (F i) G (t i)), Injective x ∧ Tendsto x atTop (𝓝 (core (fun i => limitMap (F i) G (t i)) b)) ∧ ∀ n, x n ≠ core (fun i => limitMap (F i) G (t i)) b
The core is the actual TopCat.limitCone G thread space; component i is the actual TopCat.limitCone (F i) thread space; its attachment is the actual continuous coordinatewise limitMap of the supplied natural transformation. A fixed infinite set R of indices and one actual core thread b are given. Proper-stage actual range membership for every index in R is the only range premise. CompactRangePersistence proves final membership for every such index. The attachment theorem then constructs an actual injective natural sequence converging to the literal final core point, with that point outside all terms. This directly consumes both suppliers. No final-range premise is assumed, and the proof makes no irreducibility assertion about any prefix or successor. In the reviewed example the prefix is reducible and only its specified final successor is irreducible. No sequence-free core is constructed; original ZFC Efimov remains unsolved and all supplier/helper credit is original KPI 0.