J_bit_pos
plain-language theorem explainer
Positivity of the bit cost J_bit_val follows directly from φ > 1 forcing ln φ > 0 and therefore cosh(ln φ) > 1. Workers deriving the recognition wavelength λ_rec or proving stellar-assembly bounds invoke the result to guarantee that derived lengths remain positive. The short term-mode proof rewrites via J_bit_eq_cosh, applies one_lt_phi together with log_pos and Real.one_lt_cosh, then finishes with linarith.
Claim. $J(φ) > 0$ where $J(x) = ½(x + x^{-1}) - 1$ and $φ = (1 + √5)/2 > 1$ is the golden ratio, equivalently $cosh(ln φ) - 1 > 0$.
background
The PlanckScaleMatching module derives λ_rec ≈ 0.564 ℓ_P from the ledger-curvature extremum. J_bit_val is defined as J(φ) and satisfies the identity J_bit_val = cosh(log φ) - 1. The module documentation states: 'Bit Cost (J_bit): From the unique cost functional J(x) = ½(x + x⁻¹) - 1, evaluated at the self-similar scale φ, we get J_bit = J(φ) = cosh(ln φ) - 1.' Upstream results supply one_lt_phi (φ > 1) and J_bit_eq_cosh (the cosh form).
proof idea
The term proof rewrites the goal with J_bit_eq_cosh. It obtains phi > 1 from one_lt_phi, deduces log phi > 0 via log_pos, applies Real.one_lt_cosh to reach 1 < cosh(log phi), and closes with linarith.
why it matters
J_bit_pos supplies the positivity required by lambda_rec_from_Jbit_pos and by extremum_condition, which equates J_curv(lambda_rec_from_Jbit) to J_bit_val. It thereby supports planck_scale_matching_cert that certifies the full derivation λ_rec = ℓ_P / √π from Conjecture C8. The result closes the positivity link in the forcing chain from T6 (phi forced as self-similar fixed point) onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.