DefectSensor
plain-language theorem explainer
DefectSensor records a hypothetical zero of ζ(s) inside the critical strip by its multiplicity m (as charge) and real part σ, together with the strip condition 1/2 < σ < 1. Number theorists pursuing the Riemann Hypothesis through the Recognition Science cost-covering route cite this structure to represent the defect that would need to be covered by the carrier budget. The definition is a plain record type with three fields and carries no proof obligations.
Claim. A defect sensor at a point ρ consists of an integer m (the multiplicity of the zero of ζ at ρ, or order of the pole of ζ^{-1}), a real number σ (the real part of ρ), and a witness that 1/2 < σ < 1.
background
In the Recognition Science cost-covering bridge the carrier trace is realized by the explicit function C(s) = ∏_p (1 - p^{-s})^2 exp(2 p^{-s}), which is holomorphic and non-vanishing for Re(s) > 1/2. A DefectSensor encodes a potential violation: if ζ has a zero at ρ with Re(ρ) = σ > 1/2 and multiplicity m, then ζ^{-1} has a pole of order m there, forcing the topological floor to diverge as m² log N. The module packages this after the unconditional annular bounds from AnnularCost.lean, replacing earlier axioms with concrete BudgetedCarrier witnesses. Upstream results include the cost function from MultiplicativeRecognizerL4 and ledger factorization from DAlembert, which calibrate the J-cost underlying the annular excess bounds.
proof idea
The declaration is a direct structure definition with no proof body. It simply packages the three fields charge, realPart, and in_strip as a record type.
why it matters
DefectSensor supplies the input type for the conditional theorems that derive the Riemann Hypothesis from cost covering, including charge_zero_of_covered and floorCovered_iff_charge_zero in AnalyticTrace. It closes the explicit carrier package layer described in the module documentation, where any nonzero charge forces the defect floor m² log N to exceed the O(R²) carrier budget. This structure supports the shift from legacy analytic routes to the unified RH via zero-free criteria.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.