zeroDefect
plain-language theorem explainer
The Recognition Science defect attached to the zero-location deviation of a complex number ρ is obtained by applying the defect functional to the exponential of twice the real-part offset from one half. Number theorists working on the Recognition framework formulation of the Riemann hypothesis cite this when measuring costs of off-critical zeros. It is realized as a direct composition of the defect with the exponential of the deviation.
Claim. Let $d = 2 (Re ρ - 1/2)$. The zero-location defect is $defect(exp(d))$, where $defect$ coincides with the J-cost on the positive reals.
background
The Zero Location Cost module establishes the dictionary between zeta-zero location and zero-defect cost in Recognition Science. The deviation of ρ from the critical line is twice the real-part offset from 1/2, and the defect is obtained by exponentiating that deviation and applying the J functional. The critical line is thereby the zero-defect locus.
proof idea
The definition is a one-line wrapper that applies the defect function to the exponential of the deviation of ρ.
why it matters
This definition supplies the cost measure that populates zeroDefectSet and enters the RSPhysicalThesisDataLogic structure for logic-aware decompositions. It implements the module claim that the critical line is the zero-defect locus, linking to J-uniqueness in the forcing chain. Downstream results use it to extract pairing invariants under reflection and conjugation from the completed xi surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.