defectIterate_zero_eq_J_log
plain-language theorem explainer
The zero-level defect for real deviation t equals the logarithmic J-cost. Analysts of the zeta zero composition law cite this base case to initialize the defect cascade under the Recognition Composition Law. The proof is a direct simplification that unfolds the iteration definition together with the log form of J.
Claim. For any real number $t$, the zero-level defect satisfies $d_0(t) = 2^{-1}(e^t + e^{-t}) - 1$.
background
The module develops the composition law for zeta zeros induced by the Recognition Composition Law on the J functional equation. For a zero with real deviation parameter t, the initial defect is the level-zero term of the iteration sequence. Upstream, J_log is defined by J(e^t) = cosh(t) - 1; the doc-comment states: 'J in log coordinates: J(eᵗ) = cosh(t) - 1. This is a convex bowl centered at t = 0.'
proof idea
The proof is a one-line term-mode simplification that rewrites using the definitions of defectIterate at iteration count zero and J_log from the DiscretenessForcing foundation.
why it matters
This supplies the base case for the defect iteration sequence in the zero composition law. It is invoked directly by defectIterate_zero_eq_zeroDefect to equate the iterated defect to zeroDefect and by defectIterate_zero_pos to obtain strict positivity for t ≠ 0. The step connects J-uniqueness (T5) to the exponential amplification of defects for off-critical zeros, consistent with the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.