zetaDefectSensor
plain-language theorem explainer
Constructs a sensor object for a hypothetical zero of the Riemann zeta function whose real part lies strictly between one half and one, carrying the given multiplicity as charge. Analysts studying conditional forms of the Riemann hypothesis within the Recognition Science cost framework cite this when translating analytic data into defect carriers. The definition is a direct record constructor populating the charge, real-part, and strip-membership fields.
Claim. For a real number $σ$ satisfying $1/2 < σ < 1$, a witness $h$ to that inequality, and an integer $m$, the map produces the defect sensor whose charge equals $m$, whose real part equals $σ$, and whose strip membership is witnessed by $h$.
background
In the Recognition Science framework the Euler product for the Riemann zeta function instantiates the abstract carrier and sensor objects from the annular-cost layer. A defect sensor records a potential cost defect at a real part inside the critical strip together with an integer charge counting multiplicity. The module shows how the concrete Euler product supplies carriers that satisfy the regular-carrier interface required by the cost-covering bridge, with convergence of the Hilbert-Schmidt norm and nonvanishing on Re(s) > 1/2 established upstream.
proof idea
Direct structure constructor that populates the three fields of the sensor record from the supplied real part, strip hypothesis, and multiplicity.
why it matters
Supplies the sensor object required by the zero-induced proxy-physicalization bridge and by the decomposition argument that rules out strip zeros. It thereby connects the concrete Euler-product carrier to the RS Physical Thesis and to the conditional Riemann-hypothesis statement. The construction is invoked in the proofs that any strip zero would induce a nonphysical sensor of nonzero charge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.