OnCriticalLine
plain-language theorem explainer
The predicate identifies those complex numbers whose real part equals exactly one half. Researchers formalizing the Riemann hypothesis inside the Recognition Science framework cite this predicate when they encode the claim that every nontrivial zeta zero satisfies the critical-line condition. The definition is a direct one-line abbreviation of the real-part equality.
Claim. A complex number $ρ$ lies on the critical line when its real part satisfies $Re(ρ) = 1/2$.
background
The module encodes the dictionary between zeta-zero location and zero-defect cost. Zero deviation of a point $ρ$ is defined by zeroDeviation $ρ = 2 (Re ρ - 1/2)$, after which zeroDefect $ρ$ is obtained by applying the defect map to the exponential of that deviation. Consequently the locus where real part equals one half is exactly the zero-defect locus.
proof idea
The declaration is a direct definition that sets the predicate equal to the real-part condition.
why it matters
The predicate is invoked inside the Composition Closure Hypothesis, which bounds iterated defects for any off-line zero, and inside the theorem that derives the Riemann hypothesis from that hypothesis by exhibiting divergence under the Recognition Composition Law. It also appears in the Vector C bridge that discharges the analytic target charge_zero_of_honest_phase and in the symmetry-only no-go result for the completed xi surface. The definition supplies the precise vanishing locus required by T5 J-uniqueness and the RCL self-composition step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.