zeroDefect_eq_cosh_sub_one
plain-language theorem explainer
This theorem supplies the closed-form expression equating the zero-location defect at a complex point to the hyperbolic cosine of its deviation minus one. Analysts working on zeta-zero distributions in the Recognition Science framework cite it to connect location costs directly to the J-function. The proof is a one-line simplification that unfolds the log-coordinate definition of J after invoking the base equality relating defect to that function.
Claim. Let ρ be a complex number and let δ = 2(Re ρ − 1/2) be its zero deviation. The zero-location defect at ρ then satisfies defect(ρ) = cosh(δ) − 1.
background
The module sets up the Recognition Science dictionary mapping zeta-zero location to zero-defect cost. Zero deviation is twice the real part of ρ minus one-half; zero defect is the defect applied to the exponential of that deviation. This forces the critical line Re ρ = 1/2 to be exactly the zero-defect locus. Upstream, J_log is defined on the real line by J_log(t) = cosh(t) − 1, the convex bowl centered at the origin that realizes the J-cost in logarithmic coordinates.
proof idea
The proof is a one-line wrapper. It invokes the prior equality that identifies zero defect with J in log coordinates, then applies the definition J_log(t) = cosh(t) − 1 via the simpa tactic to obtain the hyperbolic closed form.
why it matters
The result supplies the hyperbolic closed form required by the doubling recurrence on zero defects in the ZeroDoublingLaw module. It directly instantiates the J-uniqueness step (T5) of the forcing chain, where J(x) = cosh(log x) − 1, and thereby closes the dictionary between zero locations and defect costs. The equality feeds the self-composition law that converts the functional equation into a recurrence on the defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.