possibility_space_connected
plain-language theorem explainer
Every configuration in possibility space reaches the identity state (value 1) along a discrete path. Modal geometry researchers cite this to equip the space with star topology centered on the J-cost minimum. The proof supplies an explicit path function that holds the starting configuration at step zero and switches to identity_config at all later indices spaced by eight time units.
Claim. For any configuration $c$, there exists a sequence $p : ℕ → Config$ with $p(0) = c$ such that for every $n ∈ ℕ$ there is $m > n$ satisfying $p(m).value = 1$.
background
Config is the structure imported from Possibility that carries a real value and a time coordinate. The identity configuration is the canonical point at value 1, which ObserverForcing.identity identifies as the unique J-cost minimum. The local setting is the modal geometry layer built on top of J-cost and phi-ladder structures from PhiForcingDerived and DAlembert.LedgerFactorization.
proof idea
The proof is a direct term construction. It defines the path by cases: return the input $c$ at index 0 and otherwise apply identity_config to $c.time + 8·n$. Constructor splits the goal; the base equality is discharged by simp, while the tail clause is witnessed by $n+1$, with the strict inequality proved by omega and the value equality by simp on identity_config.
why it matters
The result supplies the connectivity axiom that realizes the star topology of possibility space with identity at the center, as stated in the declaration comment. It underpins sibling declarations such as possibility_curvature and modal_period. Within the Recognition framework the factor of eight in the path construction directly instantiates the eight-tick octave (T7) and the periodic return to the J-minimum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.