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

zeroDefect

show as:
view Lean formalization →

The zero-location defect attaches the Recognition Science defect functional to the exponential of a complex number ρ's deviation from the critical line. Number theorists decomposing zeta-zero data into RS-physical thesis components cite this definition when tracking defect costs along the completed-ξ surface. It is a direct one-line composition of defect with the exponential of zeroDeviation.

claimFor a complex number $ρ$, define the zero-location defect as $defect(exp(2(Re ρ - 1/2)))$, where $defect(x) = J(x)$ for positive real $x$ and $J$ denotes the Recognition Science cost function satisfying $J(e^t) = cosh(t) - 1$.

background

The module ZeroLocationCost formalizes the dictionary between zeta-zero location and RS defect cost. It introduces zeroDeviation ρ = 2(Re ρ - 1/2) and sets zeroDefect ρ = defect(exp(zeroDeviation ρ)). The critical line Re ρ = 1/2 is thereby the exact zero-defect locus. Upstream, defect(x) equals J(x) for positive x with defect at unity equal to zero, while J_log(t) = cosh(t) - 1 supplies the log-coordinate form of the cost bowl centered at t = 0.

proof idea

This is a one-line wrapper that applies the defect functional to the exponential of zeroDeviation ρ.

why it matters in Recognition Science

The definition supplies the zero-defect measure required by zeroDefectSet on the completed-ξ surface and by RSPhysicalThesisDataLogic in the logic-aware RH decomposition. It realizes the claim that the critical line is the zero-defect locus, linking directly to the Recognition Science forcing chain through J-uniqueness and the eight-tick octave. It feeds the functional-equation invariants and the boundary-transport certificates used in LogicRH_From_RCL.

scope and limits

formal statement (Lean)

  42def zeroDefect (ρ : ℂ) : ℝ :=

proof body

Definition body.

  43  Foundation.LawOfExistence.defect (Real.exp (zeroDeviation ρ))
  44
  45/-- The zero-location defect is exactly `J_log` evaluated on the deviation. -/

used by (20)

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

depends on (8)

Lean names referenced from this declaration's body.