functionalReflection_re
plain-language theorem explainer
The theorem states that the real part of the functional reflection of any complex number ρ equals one minus the real part of ρ. Researchers tracking zeta-zero locations against defect costs in the Recognition Science dictionary would cite this identity to confirm symmetry around the critical line. The proof is a direct simplification from the definition of functionalReflection.
Claim. For any complex number $ρ$, the real part of its reflection across the line Re$(s)=1/2$ satisfies Re$(1-ρ)=1-$Re$(ρ)$.
background
This module formalizes the RS dictionary between zeta-zero location and zero-defect cost. zeroDeviation ρ is defined as 2(Re ρ - 1/2) and zeroDefect ρ applies the defect function to exp of that deviation, so the critical line Re ρ = 1/2 is exactly the zero-defect locus. The upstream definition functionalReflection ρ := 1 - ρ implements reflection across Re(s) = 1/2.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of functionalReflection, which expands directly to the real-part identity.
why it matters
This result confirms the reflection symmetry required by the zero-location cost formalism. It supports the module's mapping of zeroDeviation and zeroDefect under reflection, consistent with the critical-line locus in the Recognition Science framework. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.