J_transition
plain-language theorem explainer
The transition cost between positive real configurations x and y equals the absolute logarithm of their ratio times the average of their J costs. Modal geometry and actualization proofs cite this definition when constructing path actions and possibility metrics. It is introduced by a direct algebraic formula that scales the log-ratio by the mean J value.
Claim. For positive reals $x>0$ and $y>0$, the transition cost is $|ln(y/x)| · (J(x) + J(y))/2$, where $J(z) = ½(z + z^{-1}) - 1$.
background
In the Modal.Possibility module, configurations are positive reals carrying the J-cost. The J function is the unique cost satisfying d'Alembert's relation plus normalization and calibration, given explicitly by $J(x) = ½(x + x^{-1}) - 1$. This transition cost extends the single-state J to pairs and supplies the elementary increment for accumulated actions.
proof idea
Direct definition. It evaluates the absolute value of the natural log of the ratio y/x and multiplies the result by the arithmetic mean of J(x) and J(y).
why it matters
This definition supplies the elementary transition cost used to construct PathAction in Modal.Actualization and modal_distance in ModalGeometry. It realizes the action functional for direct steps in the Recognition framework, resting on J-uniqueness from the forcing chain T5 and enabling cost accumulation along paths that feed the Born rule and modal topology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.