zeroDeviation_eq_zero_iff_on_critical_line
plain-language theorem explainer
The zero deviation of a complex point vanishes exactly when its real part equals one half. Analysts studying the location of zeta zeros in the Recognition Science setting cite this equivalence to connect deviation cost to the defect functional. The proof reduces directly to the explicit formula for the deviation by unfolding definitions and applying linear arithmetic in both directions.
Claim. For a complex number $ρ$, $2( Re(ρ) - 1/2 ) = 0$ if and only if $ Re(ρ) = 1/2 $.
background
The module establishes the RS dictionary mapping zeta-zero location to zero-defect cost. Zero deviation is the scaled offset $2(Re ρ − 1/2)$ from the critical line, chosen to align with the argument of the defect functional. OnCriticalLine holds when the real part is exactly 1/2. The defect itself is the J-cost applied to a positive real, with J satisfying the composition law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. The critical line is defined as the zero-defect locus because zero defect equals defect of exp(zero deviation). This equivalence is the base case for propagating zero cost under doubling and composition.
proof idea
Unfold the definitions of zero deviation and the critical-line predicate to obtain the arithmetic statement $2*(re ρ − 1/2) = 0$. Split the biconditional via constructor, then resolve each direction with linarith.
why it matters
This equivalence feeds zeroDefect_zero_iff_on_critical_line and zero_composition_diverges, which use it to show that off-line points generate positive and unbounded defect under iteration. It supplies the elementary step in the zero-location cost dictionary, linking directly to the J-uniqueness property and the requirement that only critical-line points achieve zero cost. Downstream results such as zeroCompositionLaw_forces_eta_zero invoke it to force minimizers onto the line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.