pith. machine review for the scientific record. sign in
def definition def or abbrev high

OnCriticalLine

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  25def OnCriticalLine (ρ : ℂ) : Prop :=

proof body

Definition body.

  26  ρ.re = 1 / 2
  27
  28/-- Reflection across the line `Re(s) = 1/2`. -/

used by (19)

From the project-wide theorem graph. These declarations reference this one in their body.