jlog_lt_jlog_of_one_lt
plain-language theorem explainer
The lemma shows that Jlog strictly increases for real arguments exceeding 1. Ledger-posting arguments in Recognition Science cite it to bound the cost of single-account updates that change the phi-vector by one unit. The term proof reduces the claim to the known strict monotonicity of Jlog on the non-negative reals after a trivial lower-bound check.
Claim. If $x > 1$, then $J(1) < J(x)$ where $J(t) := ((e^t + e^{-t})/2) - 1$.
background
The LedgerPostingAdjacency module models ledger states as pairs of debit and credit vectors whose difference is a phi-vector; a single post changes exactly one coordinate by one unit and therefore flips exactly one parity bit. Jlog is the log-domain cost function defined by Jlog(t) = cosh(t) - 1, which inherits its properties from the Recognition Composition Law and the J-cost on the positive reals. The upstream theorem Jlog_strictMonoOn_Ici0 states that Jlog is strictly increasing on the closed interval [0, ∞).
proof idea
The term proof obtains the strict-monotonicity theorem Jlog_strictMonoOn_Ici0, constructs the witness 0 ≤ x by transitivity from 0 ≤ 1 and 1 < x, and applies the monotonicity statement at the points 1 and x.
why it matters
The comparison is invoked by the downstream theorem postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 to certify that a monotone ledger transition whose Jlog cost is at most Jlog(1) is a valid PostingStep. This step closes the gap between ledger language and the one-bit parity adjacency result, which in turn feeds the eight-tick octave and D = 3 structure of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.