J_exp_eq_cosh
The identity equates the cost functional applied to an exponential argument with the shifted hyperbolic cosine. Researchers deriving the recognition wavelength from ledger curvature cite this conversion between multiplicative ratios and additive costs. The tactic proof unfolds the cost definition, substitutes the exponential inverse via simplification, and rewrites with the standard cosh identity.
claimFor every real number $t$, $J(e^t) = cosh(t) - 1$, where the cost functional satisfies $J(x) = (x + x^{-1})/2 - 1$.
background
The module derives the recognition wavelength from equating bit cost to curvature cost in RS-native units. The cost functional is defined by $J(x) = (x + x^{-1})/2 - 1$ and satisfies the Recognition Composition Law. Upstream results establish that recognition event costs equal this J-cost and that multiplicative recognizers induce derived costs on positive ratios. The module doc states: 'From the unique cost functional J(x) = ½(x + x⁻¹) - 1, evaluated at the self-similar scale φ, we get J_bit = J(φ) = cosh(ln φ) - 1.'
proof idea
Unfold the definition of J to expose the average of the argument and its inverse. A simp tactic yields (exp t)^{-1} = exp(-t). The final rewrite invokes the equality that defines cosh t as (exp t + exp(-t))/2.
why it matters in Recognition Science
The downstream theorem J_bit_eq_cosh applies this result to obtain the bit cost as cosh(log phi) - 1. It closes the first step in the Conjecture C8 chain that equates bit cost to curvature cost and recovers the Planck ratio after face averaging. The identity instantiates J-uniqueness at the exponential scale within the eight-tick octave structure.
scope and limits
- Does not prove non-negativity of J for positive arguments.
- Does not connect to the phi-ladder or mass formulas.
- Does not derive curvature cost or the 1/π averaging factor.
- Does not address SI unit restoration from native units.
Lean usage
calc J phi = J (exp (log phi)) := by rw [h_exp_log] _ = cosh (log phi) - 1 := J_exp_eq_cosh (log phi)formal statement (Lean)
51theorem J_exp_eq_cosh (t : ℝ) : J (exp t) = cosh t - 1 := by
proof body
Tactic-mode proof.
52 unfold J
53 have h : (exp t)⁻¹ = exp (-t) := by simp [exp_neg]
54 rw [h, Real.cosh_eq]
55
56/-- **Bit Cost**: J_bit := J(φ) = cosh(ln φ) - 1.
57
58This is the fundamental cost of a single ledger bit transition,
59evaluated at the self-similar scale φ (golden ratio). -/