identity_in_ball
plain-language theorem explainer
The lemma shows that the identity configuration lies inside any possibility ball centered at c whose radius strictly exceeds the modal distance to the identity at c's time. Modal geometry researchers use it to establish star-shaped connectivity of possibility space around the J-cost minimum. The proof is a direct term-mode instantiation of the witness time coordinate followed by simplification against the ball membership predicate.
Claim. Let $c$ be a configuration and $r$ a real number satisfying $r > d(c, i_{c.t})$, where $d$ is the modal distance and $i_t$ denotes the identity configuration (value 1) at tick $t$. Then there exists $t' : ℕ$ such that $i_{t'} ∈ B_r(c)$, where $B_r(c) = {y | d(c,y) ≤ r}$.
background
In the ModalGeometry module, configurations are triples (value : ℝ, pos : 0 < value, time : ℕ). The identity configuration at tick t is the unique point with value 1, which realizes the global J-cost minimum. Modal distance between two configurations is the J-transition cost divided by a reference scale τ₀; it is nonnegative, symmetric, and satisfies the triangle inequality by upstream results. The possibility ball B_r(c) is the closed set of all configurations lying at modal distance at most r from c.
proof idea
Term-mode proof. Instantiate the existential witness with c.time. Simplify the set-membership predicate using the definition of PossibilityBall. Discharge the resulting inequality modal_distance c (identity_config c.time) ≤ r by applying le_of_lt to the hypothesis.
why it matters
The result supplies the concrete witness needed for the star topology of possibility space, with identity at the center. It directly implements the connectivity claim stated in the module comment and aligns with the Recognition forcing chain's placement of the identity event at the J-cost minimum. The lemma is a prerequisite for any later connectedness or path-connectedness statements in the modal setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.