Jlog_eq_zero_iff
plain-language theorem explainer
The log-domain cost vanishes if and only if its argument is zero. Researchers characterizing equilibrium states in the Recognition Science framework cite this equivalence when working in exponential coordinates. The tactic proof rewrites via the squared algebraic form of the cost and reduces the equation using the injectivity of the exponential map after clearing the denominator.
Claim. Let $J(t) := J_ {cost}(e^t)$. Then $J(t) = 0$ if and only if $t = 0$.
background
The Cost module defines the J-cost as $J(x) = (x + x^{-1})/2 - 1$ for positive $x$, equivalently expressed as the squared ratio $J(x) = (x-1)^2/(2x)$. Jlog is the composition of this cost with the exponential map, yielding $Jlog(t) = J(exp t)$. The local setting develops algebraic identities and zero properties of the cost before extensions to averaging derivations and vector-valued versions. The upstream squared-form lemma supplies the explicit quotient used in the argument, while the zero-value lemma handles one direction of the equivalence.
proof idea
The tactic proof opens with constructor to split the biconditional. The forward direction substitutes the squared expression from the Jcost squared lemma, invokes div_eq_zero_iff on the resulting quotient, solves the numerator equation with nlinarith and linarith to reach exp t = 1, then applies the exponential one-to-one lemma. The reverse direction invokes the pre-established zero lemma for Jlog directly.
why it matters
This equivalence supplies the zero characterization for the log-domain cost and is invoked by the Flog zero lemma in the FlogEL submodule as well as the N-dimensional cost theorem. It also appears in the prime-ledger unique-zero result, which identifies the balance point at unity. In the framework it confirms the unique minimum of the J-cost at the self-similar fixed point, aligning with the J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.