J_bit_eq_cosh
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 in Recognition Science
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 φ.
scope and limits
- Does not prove J_bit > 0.
- Does not derive the curvature term J_curv or the extremum condition.
- Does not restore physical units or introduce the factor 1/π.
- Does not compute the numerical ratio λ_rec / ℓ_P.
Lean usage
rw [J_bit_eq_cosh]formal statement (Lean)
63theorem J_bit_eq_cosh : J_bit_val = cosh (log phi) - 1 := by
proof body
Tactic-mode proof.
64 unfold J_bit_val
65 have hphi : phi > 0 := phi_pos
66 have h_exp_log : exp (log phi) = phi := exp_log hphi
67 calc J phi = J (exp (log phi)) := by rw [h_exp_log]
68 _ = cosh (log phi) - 1 := J_exp_eq_cosh (log phi)
69
70/-- J_bit > 0 since φ > 1 implies cosh(ln φ) > 1. -/