zeroDeviation
plain-language theorem explainer
zeroDeviation maps a complex number ρ to twice its real-part offset from 1/2, supplying the signed input scale for the RS defect functional. Researchers in the Recognition Science program cite this map when converting zeta-zero locations into J-cost budgets for composition-closure arguments. The definition is a direct algebraic scaling of Re(ρ) - 1/2 with no further computation.
Claim. For a complex number ρ, the zero deviation is defined by $2( Re(ρ) - 1/2 )$.
background
The Zero Location Cost module establishes the dictionary between zeta-zero locations and defect costs. The defect functional, drawn from LawOfExistence, equals J(x) for positive x, where J is the cost function (x + x^{-1})/2 - 1. Upstream structures supply J-cost convexity from PhiForcingDerived and the discrete tier context from SpectralEmergence and NucleosynthesisTiers.
proof idea
This is a definition that directly computes twice the real-part deviation from 1/2. It serves as a one-line wrapper that applies the scaling to prepare the input for the defect functional.
why it matters
This definition supplies the coordinate change used by downstream results such as functionalEquation_gives_pairing_invariants in CompletedXiSymmetry, which records that zeroDeviation of the functional reflection is the negation. It also feeds CompositionDivergence's composition_violates_budget, where iterated defects from nonzero deviation exceed any bound, supporting the Riemann Hypothesis via the Composition Closure Hypothesis. It aligns with the T5 J-uniqueness and the critical line as the zero-defect locus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.