Jlog_eq_zero_iff
plain-language theorem explainer
The lemma shows that the log-domain cost vanishes exactly when its real argument is zero. Researchers characterizing zero-cost states in log coordinates or multiplicative structures cite this equivalence. The term proof unfolds the definition of Jlog together with the unit property of Jcost and applies the standard exponential identity.
Claim. Let $J(t) := (t-1)^2/(2t)$ for $t>0$ and define the log-domain cost by $Jlog(t) := J(e^t)$. Then $Jlog(t)=0$ if and only if $t=0$.
background
The Cost.FlogEL module works in log-domain coordinates by composing the base cost with the exponential: Jlog(t) is defined as Jcost(Real.exp t). This converts the multiplicative zero of Jcost at unity into an additive zero at the origin. The upstream lemma Jcost_unit0 supplies the algebraic anchor Jcost(1)=0, while the definition of Jcost itself is the squared-ratio form (x-1)^2/(2x). The local setting treats log-domain costs as the natural bridge to averaging derivations and higher-dimensional extensions.
proof idea
The term proof is a one-line wrapper: simp unfolds Jlog and Jcost_unit0 to reduce the statement to exp t = 1 ↔ t = 0, which is discharged directly by the library fact Real.exp_eq_one_iff.
why it matters
The result supplies the zero-cost characterization in log coordinates that is invoked by JcostN_eq_zero_iff in Ndim.Core and by jcost_log_zero_unique in PrimeLedgerStructure. It also feeds Flog_eq_zero_iff_of_derivation, extending the same property to averaging derivations. Within the Recognition framework this pins the unique real zero of the J-cost at the balance point (unity in multiplicative coordinates, origin in log coordinates) and supports the transition from T5 J-uniqueness to higher-dimensional and number-theoretic applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.