zetaDefectSensor
The zetaDefectSensor definition constructs a DefectSensor record for any hypothetical Riemann zeta zero whose real part lies strictly inside (1/2,1), assigning the supplied multiplicity as charge. Researchers linking the Riemann Hypothesis to Recognition Science cost structures cite it when they need a concrete charged sensor from a strip zero. The definition is realized by a direct record constructor that copies the real-part input, the strip-bounds hypothesis, and the multiplicity into the three sensor fields.
claimLet $1/2 < σ < 1$ and let $m ∈ ℤ$. The defect sensor associated with a hypothetical zero of the Riemann zeta function at real part $σ$ and multiplicity $m$ is the structure whose charge equals $m$, whose real part equals $σ$, and whose in-strip predicate is witnessed by the given bounds on $σ$.
background
This definition sits inside the EulerInstantiation module, whose purpose is to show that the Euler product for ζ(s) supplies a concrete model of the abstract carrier/sensor framework developed in AnnularCost and CostCoveringBridge. The module first builds the prime-sum operators PrimeSum and HilbertSchmidtNorm, proves their convergence for real part >1/2, constructs the holomorphic non-vanishing carrier C(s) = det₂²(I−A(s)), and verifies that C satisfies both the EulerCarrier and RegularCarrier interfaces. The DefectSensor type is the basic data structure that encodes a hypothetical zero as a charged defect inside this cost-covering layer; its three fields (charge, realPart, in_strip) are exactly what the downstream proxy-physicalization and ontological-dichotomy arguments consume.
proof idea
The declaration is a plain structure constructor. It directly populates the DefectSensor record by setting charge to the multiplicity argument, realPart to the realPart argument, and in_strip to the supplied h_strip hypothesis. No lemmas, tactics, or reductions are applied beyond the record builder itself.
why it matters in Recognition Science
zetaDefectSensor supplies the concrete sensor object required by every zero-induced argument in the module. It is invoked inside zeta_zero_gives_charged_sensor to produce a nonzero-charge sensor, inside the definition of ZeroInducedProxyPhysicalizationBridge, and inside the decomposition theorems that derive the RS Physical Thesis from the absence of strip zeros. By furnishing this sensor the definition closes the instantiation chain from Euler product through bounded logarithmic derivative to the cost-covering axiom, thereby supporting the conditional Riemann Hypothesis obtained via the ontological dichotomy of Recognition Science.
scope and limits
- Does not assert existence of any zeta zero inside the strip.
- Does not bound or compute the multiplicity of any zero.
- Applies only when the real part lies strictly between 1/2 and 1.
- Does not address zeros on the critical line or with real part ≤1/2 or ≥1.
formal statement (Lean)
876def zetaDefectSensor (realPart : ℝ) (h_strip : 1/2 < realPart ∧ realPart < 1)
877 (multiplicity : ℤ) : DefectSensor where
878 charge := multiplicity
proof body
Definition body.
879 realPart := realPart
880 in_strip := h_strip
881
882/-- The sensor/carrier compatibility: the carrier is regular in
883 a neighborhood of any hypothetical zero.
884 Specifically: if Re(ρ) = σ₀ > 1/2, then D(ρ, σ₀ − 1/2) ⊂ {Re(s) > 1/2}
885 and the carrier is holomorphic nonvanishing on this disk. -/
used by (11)
-
zeta_zero_gives_charged_sensor -
rsPhysicalThesis_of_ZeroInducedProxyPhysicalizationBridge -
zeroInducedBridge_iff_no_strip_zeros -
ZeroInducedProxyPhysicalizationBridge -
unit_sensor_not_physical_cert -
no_strip_zeros_of_decomposed_data -
RSPhysicalThesis -
strip_zero_gives_nonphysical_sensor -
unit_sensor_not_physical -
zetaDefectSensor_charge_ne_zero -
zetaDefectSensor_charge_one