zeroDefect_zero_iff_on_critical_line
plain-language theorem explainer
The equivalence asserts that the zero-location defect of a complex number ρ vanishes precisely when Re(ρ) equals 1/2. Number theorists mapping zeta zeros onto the Recognition Science defect functional would cite this result when translating the critical-line condition into cost language. The proof is a short term-mode reduction that rewrites the defect via its J-log form and chains the J-log zero equivalence with the sibling deviation equivalence.
Claim. For any complex number ρ, the zero-location defect vanishes if and only if Re(ρ) = 1/2, where the defect is obtained by applying the J-functional to exp(2(Re(ρ) − 1/2)).
background
The module defines zeroDeviation ρ := 2(Re ρ − 1/2) and zeroDefect ρ := defect(exp(zeroDeviation ρ)), with defect(x) := J(x). OnCriticalLine ρ is the predicate Re(ρ) = 1/2. The upstream lemma J_log_eq_zero_iff states that J_log t = 0 if and only if t = 0, proved by the identity cosh t = 1 ⇔ t = 0. The sibling zeroDeviation_eq_zero_iff_on_critical_line supplies the remaining link between vanishing deviation and the critical-line predicate.
proof idea
The term proof first rewrites zeroDefect ρ via zeroDefect_eq_J_log. It then applies constructor. The forward direction reduces zeroDefect = 0 to zeroDeviation = 0 by J_log_eq_zero_iff, then invokes zeroDeviation_eq_zero_iff_on_critical_line. The reverse direction runs the same two equivalences in the opposite order.
why it matters
The result is invoked by zeroCompositionWitness_forces_zero_defect to conclude that any ZeroCompositionWitness forces zero defect, and by current_vectorC_attempt_data to package the iff together with non-negativity of the doubled defect. It completes the RS dictionary that identifies the critical line with the zero-cost locus, directly supporting the T5–T6 forcing steps that place the self-similar fixed point on Re(s) = 1/2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.