possibility_space_connected
plain-language theorem explainer
Every configuration in possibility space admits a discrete path to the identity state (value 1) that returns to identity at arbitrarily late times. Modal geometry work cites the result to equip the space with a star topology centered on identity. The proof supplies an explicit path function that returns the input at step zero and thereafter inserts the identity configuration at time offsets that are multiples of eight.
Claim. For every configuration $c$ there exists a sequence of configurations $(p_n)_{n=0}^∞$ such that $p_0=c$ and, for every $n$, there is an index $m>n$ with the value field of $p_m$ equal to 1.
background
Configurations belong to the Possibility.Config structure carrying a value field and a time coordinate. The identity configuration is the unique point whose value equals 1, the J-cost minimum defined by ObserverForcing.identity. The eight-tick increments in the path construction align with the eight-tick octave of the forcing chain (T7). The theorem is stated inside ModalGeometry after the import of Possibility and Actualization; it precedes the curvature definitions that quantify spread around identity.
proof idea
The term proof exhibits the path explicitly: the function returns the input configuration when the index is zero and otherwise calls identity_config at time c.time + 8*n. The initial-condition conjunct is discharged by simp. The universal quantifier is witnessed by choosing m = n+1; the strict inequality follows from omega and the value-equality from simp on identity_config.
why it matters
The declaration supplies the connectivity property required for the star topology of possibility space. It anchors identity as the J-cost minimum and supplies the discrete-path infrastructure used by the sibling definitions of modal_distance and possibility_curvature in the same module. The explicit 8-step spacing directly instantiates the eight-tick octave (T7) of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.