jcost_log_zero_unique
plain-language theorem explainer
The result states that the J-cost of e^t vanishes precisely when t equals zero, identifying the unique real balance point in logarithmic coordinates. Ledger modelers analyzing multiplicative decompositions and prime irreducibility cite this to anchor transaction balance. The proof reduces the statement to the corresponding zero property of the auxiliary Jlog function by a single rewrite followed by direct application of an existing lemma.
Claim. Let $G(x)$ denote the J-cost function on positive reals. Then $G(e^t) = 0$ if and only if $t = 0$, for every real number $t$. Equivalently, the function $G(t) := Jcost(e^t)$ has its sole real root at the origin.
background
In the Recognition Science ledger, every natural number represents a multiplicative transaction. The J-cost function quantifies deviation from balance, with the explicit form $G(x) = (x + x^{-1})/2 - 1$ for $x > 0$, equivalently written as $cosh(log x) - 1$. The auxiliary function Jlog is defined by composition: Jlog(t) := Jcost(e^t). The module situates this within the discrete multiplicative ledger where primes are the irreducible transactions and unique factorization supplies the balance sheet. The upstream lemma Jlog_eq_zero_iff already records that Jlog(t) = 0 precisely when t = 0.
proof idea
The term-mode proof performs a single definitional rewrite that replaces Cost.Jcost (Real.exp t) by Cost.Jlog t, then invokes the lemma Jlog_eq_zero_iff t to obtain the biconditional.
why it matters
The declaration fixes the unique zero of J-cost at the multiplicative identity in log coordinates, supplying the balance point required for the ledger analysis of irreducible transactions. It supports the module's treatment of d'Alembert symmetry and the structural parallel to the zeta functional equation. Within the forcing chain it instantiates the J-uniqueness step (T5) that precedes the self-similar fixed point and the eight-tick octave. No downstream uses are recorded yet; the result remains available for later closure of the Riemann-hypothesis hypothesis in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.