J_transition_self
The lemma establishes that the transition cost between a positive real configuration and itself is zero under the J-transition definition. Modal geometry constructions and change analyses in Recognition Science cite this to simplify self-loops and establish zero self-distance. The proof is a direct term-mode reduction that unfolds the transition formula and applies the logarithm property at unity.
claimFor every positive real number $x$, the transition cost $J(x,x)$ equals zero, where the transition cost is defined by $J(x,y) = |ln(y/x)| · (J(x) + J(y))/2$ and $J$ denotes the underlying recognition cost function.
background
J_transition measures the action cost of a direct move from configuration $x$ to $y$ as the absolute logarithmic ratio scaled by the average J-cost at the endpoints. The J-cost itself is the non-negative recognition cost function on positive reals, vanishing only at unity and satisfying the multiplicative composition law. This lemma appears in the Modal.Possibility module, which builds possibility spaces for configurations under the Law of Existence and supplies the basic distance properties needed for modal geometry.
proof idea
The proof is a one-line term wrapper. It unfolds the definition of J_transition, which produces |log(x/x)| times the average J-cost, then simplifies the ratio x/x to 1 via div_self and notes that log(1) is zero, collapsing the entire expression to zero.
why it matters in Recognition Science
The result feeds directly into modal_distance_self, which lifts the zero self-cost to configuration space, and into J_change_self, which isolates the stasis contribution when no transition occurs. It supplies the base case for modal distances in the Recognition framework, consistent with the self-similar fixed point at phi and the non-negativity of costs along the forcing chain. No open scaffolding remains at this step.
scope and limits
- Does not address transitions between distinct positive reals.
- Does not extend to non-positive configurations.
- Does not incorporate physical units or empirical constants.
- Does not treat multi-step or composite transitions.
Lean usage
lemma modal_distance_self (c : Config) : modal_distance c c = 0 := by unfold modal_distance; exact J_transition_self c.posformal statement (Lean)
130lemma J_transition_self {x : ℝ} (hx : 0 < x) : J_transition x x hx hx = 0 := by
proof body
Term-mode proof.
131 unfold J_transition
132 simp [div_self (ne_of_gt hx)]
133
134/-- Transition cost is symmetric. -/