defectIterate_zero_pos
plain-language theorem explainer
The theorem establishes strict positivity of the base defect d₀ for any nonzero real deviation t from the critical line. Researchers analyzing the forced divergence of off-critical zeta zeros under the Recognition Composition Law would cite this as the initial step of the amplification cascade. The proof reduces the claim directly to the known positivity of the J-log function through a single equality rewrite.
Claim. For every real number $t ≠ 0$, the zero-iteration defect satisfies $0 < d_0(t)$, where $d_0(t) = J(e^{2t})$ and $J(x) = (x + x^{-1})/2 - 1$.
background
The module develops the composition law for zeta zero defects induced by the Recognition Composition Law. Given a nontrivial zero with real deviation η from the critical line, the base defect is defined as d₀ = J(e^{2η}) = cosh(2η) - 1. The RCL applied to the pair (e^{2η}, e^{-2η}) produces the recurrence d_{n+1} = 2 d_n (d_n + 2), with iteration d_n = cosh(2^{n+1} η) - 1. The upstream theorem J_log_pos states that J_log is strictly positive for t ≠ 0, and the equality defectIterate_zero_eq_J_log identifies the base defect with this J-log value.
proof idea
The term proof rewrites defectIterate t 0 via the equality defectIterate_zero_eq_J_log, then applies the upstream theorem J_log_pos directly to the hypothesis t ≠ 0.
why it matters
This supplies the base positivity required by the monotonicity theorem defectIterate_mono and the unboundedness theorem defectIterate_unbounded in the same module. The latter shows that any off-critical zero generates a divergent defect cascade, obstructing finite carrier budgets. It instantiates the framework's T5 J-uniqueness and the RCL forcing of exponential growth away from the critical line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.