J_transition_symm
plain-language theorem explainer
Symmetry of transition costs between positive real configurations holds in the modal possibility space. Researchers working on modal geometry cite this when establishing that distances in configuration space are symmetric. The proof proceeds by unfolding the definition of J_transition and applying properties of the logarithm to equate the absolute values of the log ratios.
Claim. For all positive real numbers $x, y$, $J_{transition}(x,y) = J_{transition}(y,x)$, where $J_{transition}(x,y) := |ln(y/x)| · (J(x) + J(y))/2$.
background
In the Modal.Possibility module, configurations are positive reals equipped with the J-cost function from Recognition Science. The transition cost is defined as the absolute log-ratio of the configurations multiplied by the average J-cost of the endpoints. This setup models the action for direct transitions in possibility space. Upstream results include the definition of J from the foundation and constants like tick and octave that set the scale for recognition cycles. The J function satisfies the Recognition Composition Law.
proof idea
The proof unfolds the definition of J_transition. It then applies congr to reduce to showing equality of the log absolute value and the averaged J terms. For the log part, it uses Real.log_div twice to establish that log(y/x) = -log(x/y), followed by abs_neg. The averaged term is handled by ring.
why it matters
This lemma supports the modal_distance_symm result in ModalGeometry, which establishes symmetry of distances in configuration space. It fills the symmetry requirement for the possibility topology in the Recognition framework, aligning with the eight-tick octave structure where costs are paid symmetrically. No open questions are directly touched here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.