traceZ_cosh
plain-language theorem explainer
Under the real embedding of ℤ[φ], the discrete ladder trace at integer n equals 2 cosh(n log φ). Anyone citing the T5 display bridge or the classical cosh form of recognition cost on the φ-ladder needs this identity. The proof rewrites the trace as φⁿ + φ⁻ⁿ, converts integer powers to exponentials, and matches the definition of cosh.
Claim. For every integer $n$, the real evaluation of the discrete ladder trace at $n$ equals $2\cosh(n\log\varphi)$, where $\varphi=(1+\sqrt{5})/2$ is the classical golden ratio forced by T6.
background
The module GoldenIntReal is the sigma1 display boundary: DeltaSpine.GoldenInt derives T6 (φ as unique positive golden root) inside ℤ[φ] with only propext and Quot.sound; this file evaluates that structure into ℝ once. The map toReal sends $a+b\varphi_{\mathbb{Z}}$ to $a+b\varphi_{\mathbb{R}}$ and is a ring embedding, with toReal phi = PhiForcing.φ.
Upstream, CostUniqueness defines the discrete ladder trace so that the doubled cost is Jdouble n = traceZ n - 2, and documents Jdouble n = φⁿ + φ⁻ⁿ − 2 = 2·J(φⁿ) for the canonical cost $J(x)=(x+x^{-1})/2-1$. Thus the trace itself is the integer-ladder avatar of $φⁿ+φ⁻ⁿ$. The classical recognition cost Jcost is the same formula on positive reals.
The local point of the cosh display is that the d'Alembert functional equation already proved at sigma0 is exactly the addition law of cosh; this theorem makes that identification numerical under evaluation.
proof idea
Tactic proof, not a wrapper. First prove the auxiliary identity $φ^m=\exp(m\logφ)$ for all $m\in\mathbb{Z}$ by rewriting integer powers through Real.rpow_intCast and Real.rpow_def_of_pos (using positivity of φ). Next push casts to get $(-n)\logφ=-(n\logφ)$. Rewrite the goal with the evaluation lemma for the discrete trace (so the left side becomes $φ^n+φ^{-n}$), apply the exponential form of both powers, insert the sign identity, expand via Real.cosh_eq, and finish by ring.
why it matters
This is one of the two conjuncts of t5_bridge, the T5 display bridge and module capstone: under evaluation, the sigma0-forced cost ladder is exactly classical J-cost on the φ-ladder together with its cosh form. Downstream doc-comment: everything with mathematical content (existence, uniqueness, composition law) was proved at sigma0 in CostUniqueness; t5_bridge is pure translation, and this theorem supplies the cosh half.
In the forcing chain, T5 is J-uniqueness with $J(x)=(x+x^{-1})/2-1$, also written $\cosh(\log x)-1$. The identity here is the ladder-level witness of that cosh presentation: $2\cosh(n\logφ)=φ^n+φ^{-n}$. It also ties the discrete RCL at sigma0 to the addition formula for cosh, so the continuum display of the recognition composition law sits on standard hyperbolic trigonometry rather than a private surrogate.
No open scaffold: the claim is fully proved. It closes the display side of the T5 story once jdouble_eq_jcost is paired with it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.