criticalReflection_re
plain-language theorem explainer
The declaration shows that the real part of the critical reflection of any complex number ρ equals 1 minus the real part of ρ. Researchers mapping zeta-zero positions to zero-defect costs in the Recognition Science dictionary would cite this when confirming the real-part symmetry under reflection. The proof is a one-line simplification that unfolds the definition of critical reflection.
Claim. For any complex number ρ, the real part of the reflection of ρ across the line Re(s) = 1/2 satisfies Re(1 - conj(ρ)) = 1 - Re(ρ).
background
The Zero Location Cost module formalizes the RS dictionary between zeta-zero location and zero-defect cost: zeroDeviation ρ equals 2(Re ρ - 1/2) and zeroDefect ρ equals defect(exp(zeroDeviation ρ)). The critical line Re ρ = 1/2 is therefore exactly the zero-defect locus. The upstream definition states that criticalReflection ρ is given by 1 - conj ρ, implementing reflection across Re(s) = 1/2 composed with conjugation.
proof idea
The proof is a one-line wrapper that applies simp to the definition of criticalReflection, which directly computes the real part as 1 minus the real part of ρ.
why it matters
This identity anchors the real-part behavior under reflection and thereby supports the module's claim that the critical line coincides with the zero-defect locus. It fills a basic step in the Recognition Science dictionary between zero locations and the defect functional, consistent with the forcing chain landmarks T5 through T8. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.