Infinite Historical Fibers
Abstract
Infinite Historical Fibers.
Theorem 1.1 (Isolated inactive extensions).
Lean statement: D5/S3/ConceptDynamics/Spacetime/InactiveArchiveFibers.infinite_fibre
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Spacetime/InactiveArchiveFibers.infinite_fibre (✓ std3). ∎
Source. Repository-derived.
Commentary.
In every finite dimension, any rich history has an injective family of extensions indexed by the natural numbers. The extension at index k adds exactly k isolated inactive events. An inclusion preserves every old event name, attribute and causal relation, and maps the current region and selected subset exactly onto those of the extension. Selected and background charges are unchanged. Distinct indices give different archive cardinalities, excluding historical isomorphisms. The construction also applies to empty archives and empty selections.