cosh_no_real_zeros
plain-language theorem explainer
cosh(t) is bounded below by 1 for every real t, so the function has no real roots. Researchers modeling the J-cost in the Recognition Science ledger would invoke this when establishing strict positivity of J away from its fixed point at 1. The short term proof combines the known positivity of cosh, its quadratic lower bound, and non-negativity of squares via linarith.
Claim. For all real numbers $t$, $1 ≤ cosh(t)$.
background
The PrimeLedgerStructure module develops the correspondence between the d'Alembert functional equation and the zeta function via the J-cost. The J-cost is defined in the Cost module as J(x) = cosh(log x) - 1, making the inequality cosh(t) ≥ 1 equivalent to J(e^t) ≥ 0. Upstream, the quadratic lower bound theorem states that cosh x ≥ 1 + x²/2 for all real x, proved via Taylor series with non-negative terms.
proof idea
The term proof first invokes Real.cosh_pos t to obtain cosh t > 0, then applies Cost.cosh_quadratic_lower_bound t to get cosh t ≥ 1 + t²/2, and finally uses linarith together with sq_nonneg t to deduce the desired lower bound of 1.
why it matters
It is cited by j_positive_off_fixed_point to show J is strictly positive away from the fixed point. This supports the structural parallel between J-cost symmetry and the ζ functional equation in the module, advancing the d'Alembert zero structure theorem. Within the Recognition Science framework it underpins the ledger conservation arguments that predict the Riemann Hypothesis, leaving open the question of Euler product constraints on the completed zeta.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.