`self_composition_cosh`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.XiJBridge
domain: NumberTheory
line: 170 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.XiJBridge on GitHub at line 170.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

formal source

 167
 168    This follows from the cosh double-angle formula cosh(2t) = 2cosh²(t)−1,
 169    which is itself a consequence of the RCL in log-coordinates. -/
 170theorem self_composition_cosh (η : ℝ) :
 171    Real.cosh (2 * (2 * η)) - 1 =
 172    2 * (Real.cosh (2 * η) - 1) ^ 2 + 4 * (Real.cosh (2 * η) - 1) := by
 173  have hd := Real.cosh_two_mul (2 * η)
 174  have hs := Real.cosh_sq (2 * η)
 175  set c := Real.cosh (2 * η) with hc_def
 176  set s := Real.sinh (2 * η) with hs_def
 177  have lhs : Real.cosh (2 * (2 * η)) - 1 = 2 * c ^ 2 - 2 := by linarith
 178  have rhs : 2 * (c - 1) ^ 2 + 4 * (c - 1) = 2 * c ^ 2 - 2 := by ring
 179  linarith
 180
 181end
 182
 183end NumberTheory
 184end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.