criticalReflection
plain-language theorem explainer
The critical reflection map sends a complex number ρ to 1 minus its conjugate. Researchers analyzing zeta zero locations under the Recognition Science zero-defect dictionary cite this map to derive pairing invariants and defect preservation. It is introduced as a direct algebraic definition with no lemmas or reductions required.
Claim. The critical reflection of a complex number $ρ$ is the value $1 - ¯ρ$. This operation reflects across the line Re$(s) = 1/2$ and composes with conjugation.
background
The Zero Location Cost module formalizes the dictionary between zeta-zero location and zero-defect cost via zeroDeviation ρ = 2 (Re ρ - 1/2) and zeroDefect ρ = defect (exp (zeroDeviation ρ)). Here defect is the functional from the Law of Existence that equals J for positive arguments, and the critical line Re ρ = 1/2 is exactly the zero-defect locus. Upstream structures include the J-cost calibration from PhiForcingDerived and the defect definition that vanishes at unity.
proof idea
This is a direct definition that assigns to ρ the explicit value 1 minus the complex conjugate of ρ. No lemmas are invoked and no tactics are applied; the body is the algebraic expression implementing the stated reflection.
why it matters
This map supplies the symmetry operation used in zero_pairing_under_critical_reflection and functionalEquation_gives_pairing_invariants to show that zeros of the completed xi surface are stable under reflection and conjugation while preserving zero deviation up to sign. It thereby supports the claim that the critical line coincides with the zero-defect locus in the Recognition Science dictionary. The definition closes the algebraic step needed for downstream invariance results without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.