J_zero_iff_one
plain-language theorem explainer
For positive real x the cost J vanishes precisely when x equals 1. Modal actualization arguments and cost-monotonicity lemmas cite the equivalence to isolate the identity configuration. The forward direction unfolds J, applies linear arithmetic to obtain x + x^{-1} = 2, reduces to the quadratic identity via field simplification, and closes with nlinarith on (x-1)^2; the converse rewrites and invokes the normalization lemma J_at_one.
Claim. For all real $x > 0$, the cost function $J(x) := (1/2)(x + x^{-1}) - 1$ satisfies $J(x) = 0$ if and only if $x = 1$.
background
J is the fundamental cost on positive reals, defined by $J(x) = (1/2)(x + x^{-1}) - 1$. It is the unique function satisfying d'Alembert's functional equation together with normalization at the multiplicative identity and calibration to the self-similar fixed point (T5). The present module Modal.Possibility assembles modal operators over configuration spaces whose transition costs are measured by J. Upstream, J_at_one records the normalization statement J(1) = 0, which is proved by direct substitution in several sibling modules.
proof idea
Constructor splits the biconditional. Forward direction: unfold J, obtain x + x^{-1} = 2 by linarith from the hypothesis, multiply through to reach x^2 + 1 = 2x by field_simp, then apply nlinarith to the non-negative square (x-1)^2. Backward direction: rewrite the hypothesis and discharge by exact J_at_one.
why it matters
The lemma supplies the zero set of J and is invoked directly by J_pos_of_ne_one (which separates the identity from all other positive ratios) and by possibility_actualization_adjoint_monotonic (which transfers cost-monotonic properties across the possibility and actualization adjunction). It therefore anchors the modal layer of the Recognition framework to the T5 uniqueness property of J and to the normalization step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.