defectIterate_nonneg
plain-language theorem explainer
Nonnegativity of the iterated defect d_n(t) = cosh(2^n t) - 1 holds for every real t and natural number n. Workers on the zeta-zero composition law cite it to justify the base case before proving amplification steps. The proof is a direct term-mode reduction that unfolds the definition and invokes cosh(x) ≥ 1 via linarith.
Claim. Let $d_n(t) := cosh(2^n t) - 1$. Then $d_n(t) ≥ 0$ for all real $t$ and all natural numbers $n$.
background
The module develops the composition law for zeta zero defects induced by the Recognition Composition Law satisfied by J. The iterated defect is defined by defectIterate t n := Real.cosh ((2 : ℝ) ^ n * t) - 1. For a nontrivial zero with deviation η = Re(ρ) - 1/2 one sets t = 2η, so that d_n records the n-th self-composition under the RCL, yielding d_n = cosh(2^{n+1} η) - 1.
proof idea
The proof is a one-line term-mode wrapper. It simplifies with the definition of defectIterate to reduce the goal to 0 ≤ cosh(2^n t) - 1, then applies linarith to the standard inequality Real.one_le_cosh.
why it matters
The result is invoked by defectIterate_four_mul_le to obtain d_{n+1} ≥ 4 d_n. That amplification step feeds the exponential lower bound and the divergence claim for off-critical zeros. It supplies the nonnegativity foundation required by the RCL self-composition cascade.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.