J_bit_eq_cosh
plain-language theorem explainer
J_bit_val equals cosh(log φ) - 1, supplying the hyperbolic expression for the bit cost at the golden ratio scale. Derivations of the recognition wavelength λ_rec from the extremum J_bit = J_curv(λ) cite this form. The proof unfolds the definition of J_bit_val, substitutes φ via exp(log φ), and applies the exponential identity theorem for J.
Claim. $J_ {bit} := J(φ)$ satisfies $J_{bit} = cosh(ln φ) - 1$, where φ denotes the golden ratio and J is the cost functional.
background
The module derives λ_rec ≈ 0.564 ℓ_P from the ledger-curvature extremum argument. Bit cost is defined as J_bit := J(φ) with J(x) = ½(x + x^{-1}) - 1 evaluated at the self-similar scale φ. The theorem supplies the equivalent cosh(ln φ) - 1 expression. It rests on the upstream result J(exp t) = cosh t - 1, quoted as the log-transformed version of the cost functional.
proof idea
Unfolds J_bit_val to J phi. Establishes phi > 0 via phi_pos, applies exp_log to rewrite the argument as exp(log phi), then invokes J_exp_eq_cosh at t = log phi to reach the cosh form.
why it matters
This equivalence completes the bit cost step in the Planck-scale matching chain for Conjecture C8. It is invoked by the subsequent positivity result J_bit_pos. The form aligns with J-uniqueness (T5) in the forcing chain, confirming the hyperbolic representation at φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.