Jlog_pos_iff
plain-language theorem explainer
The equivalence establishes that Jlog vanishes only at the origin for real arguments. Cost analysts in Recognition Science cite it when proving strict positivity for ledger transitions or forcing-chain steps. The short proof rewrites via the cosh identity and invokes the two directions of one_lt_cosh together with sub_pos.
Claim. $0 < Jlog(t) ↔ t ≠ 0$ for $t ∈ ℝ$, where $Jlog(t) := cosh(t) - 1$.
background
Jlog is the log-domain cost function defined by composing Jcost with the exponential map, or explicitly as ((exp t + exp(-t))/2) - 1. The sibling lemma Jlog_eq_cosh_sub_one records the identity Jlog(t) = cosh(t) - 1 that follows from the standard definition of hyperbolic cosine. The module Cost.Jlog supplies the basic algebraic and sign properties of this function inside the Recognition Science cost layer, where it appears in monotonicity arguments and ledger posting rules.
proof idea
The term proof first rewrites the goal with Jlog_eq_cosh_sub_one, converting the claim into 0 < cosh(t) - 1. It then splits the biconditional with constructor. The forward direction extracts 1 < cosh(t) from the hypothesis via sub_pos and feeds it to one_lt_cosh. The reverse direction applies one_lt_cosh directly to the nonzero assumption and recovers the strict inequality via sub_pos.
why it matters
The lemma is invoked by Jlog_eq_zero_iff in the same module to obtain the zero-equivalence and by the postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 theorem in LedgerPostingAdjacency to certify distinct ledger states under a cost bound. It supplies the strict-positivity ingredient required by the Recognition framework's cost analysis, consistent with the J-uniqueness and eight-tick octave steps that rely on nonzero defects to enforce distinct configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.