zeroDeviation_criticalReflection
plain-language theorem explainer
Reflection of a complex number rho across the line Re(s) = 1/2 negates its zero-deviation measure. Number theorists studying zeta-zero locations in the Recognition Science setting cite this when proving symmetry of the attached defect. The argument is a direct term reduction that unfolds the two definitions and closes by linear arithmetic on the real parts.
Claim. For any complex number $rho$, let $delta(rho) = 2(Re rho - 1/2)$ be the zero deviation and let $rho^* = 1 - bar{rho}$ be the critical reflection. Then $delta(rho^*) = -delta(rho)$.
background
The module formalizes an RS dictionary that attaches a defect cost to the location of a complex number rho. zeroDeviation rho is defined as twice the signed distance of Re rho from 1/2, while zeroDefect rho applies the defect functional to exp of that deviation; the critical line Re rho = 1/2 is therefore the zero-defect locus. Upstream, defect is the J functional from LawOfExistence, and criticalReflection is the map rho |-> 1 - conj rho that sends each point to its mirror image across Re s = 1/2.
proof idea
The proof is a term-mode reduction. It unfolds zeroDeviation and criticalReflection, applies simp to normalize the resulting real-arithmetic expressions, and invokes linarith to obtain the equality.
why it matters
The result supplies the sign-reversal step required by the downstream theorem zeroDefect_invariant_under_reflection, which asserts that zeroDefect itself is unchanged under critical reflection. It thereby strengthens the module claim that the critical line is precisely the zero-defect locus in the Recognition Science dictionary between zeta zeros and the J-cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.