cosh_at_zero
The theorem confirms that cosh evaluates to 1 at argument zero, fixing the unique real minimum of the J-cost at the multiplicative identity. Number theorists examining the Recognition Science ledger model cite it when checking zero loci under the d'Alembert equation. The proof is a direct one-line simplification that invokes the standard library identity for cosh at zero.
claim$G(0) = 1$ where $G(t) = F(e^t)$ reparametrizes the cost function $F$ in log coordinates, confirming the minimum of $G(t) = cosh(t) - 1$ at the ledger balance point $t = 0$ (i.e., $x = 1$).
background
The module treats natural numbers as transactions on a discrete multiplicative ledger, with primes as the irreducible entries whose unique factorization supplies the balance sheet. The J-cost appears via the reparametrization $G(t) = F(exp t)$ from Cost.FunctionalEquation, specialized to $G(t) = cosh(t) - 1$ whose zero at $t = 0$ marks the RS balance point. Upstream, Constants.G supplies the RS-native gravitational constant while ObserverForcing.cost and MultiplicativeRecognizerL4.cost identify the cost of any recognition event with this J-cost.
proof idea
The proof is a one-line term-mode wrapper that applies the simp tactic to the library fact Real.cosh_zero.
why it matters in Recognition Science
This result belongs to the proved d'Alembert zero-structure block in PrimeLedgerStructure, which supplies the structural parallel between J-cost symmetry and the zeta functional equation. It anchors the T5 J-uniqueness step of the forcing chain and the eight-tick octave before the module turns to the open question of whether the Euler product imposes d'Alembert-type constraints on the completed zeta function.
scope and limits
- Does not prove uniqueness of the zero outside the real line.
- Does not derive any statement about prime factorization or irreducibility.
- Does not close the open gap between the Euler product and d'Alembert constraints on zeta.
formal statement (Lean)
81theorem cosh_at_zero : Real.cosh 0 = 1 := by
proof body
Term-mode proof.
82 simp [Real.cosh_zero]
83
84/-- The J-cost G(t) = cosh(t) - 1 has its unique real zero at t = 0.
85 In log coordinates, t = 0 means x = e⁰ = 1: the RS balance point. -/