sensor_carrier_compatible
The theorem shows that any DefectSensor at a hypothetical zero with real part σ₀ > 1/2 admits a RegularCarrier of radius exactly σ₀ − 1/2 that remains inside Re(s) > 1/2 and is holomorphic nonvanishing on the disk. Researchers closing the Euler-product instantiation of the RS cost-covering framework would cite it to confirm carrier compatibility before invoking the conditional RH axiom. The proof is a direct exact construction that invokes the Euler regular carrier builder and checks radius positivity by linear arithmetic on the strip-membersip
claimLet σ₀ > 1/2 be the real part of a hypothetical zero ρ. There exists a regular carrier whose radius equals σ₀ − 1/2 and is strictly positive, so that the disk D(ρ, σ₀ − 1/2) lies inside {Re(s) > 1/2} with the carrier holomorphic and nonvanishing throughout the disk.
background
The Euler Product Instantiation module realizes the abstract RS carrier/sensor framework of AnnularCost and CostCoveringBridge by means of the zeta-function Euler product. A DefectSensor encodes the location of a hypothetical zero together with its membership in the half-plane Re(s) > 1/2. A RegularCarrier is a holomorphic nonvanishing function defined on a disk that covers the annular region between the critical line and the sensor’s real part.
proof idea
The proof is a one-line exact tactic. It constructs the carrier by applying eulerRegularCarrier to the sensor’s real part and its strip-membership hypothesis, then verifies the radius equality and the strict positivity 0 < radius by rewriting the inequality and discharging it with linarith on the strip fact.
why it matters in Recognition Science
This result supplies the carrier_compatible field of the EulerTraceAdmissible structure in UnifiedRH, which in turn completes the Euler instantiation certificate that licenses the cost-covering axiom and yields conditional RH. It therefore closes the concrete-to-abstract bridge in the chain primes → Hilbert–Schmidt operator → det₂ convergence → holomorphic nonvanishing carrier → cost-covering applicability.
scope and limits
- Does not prove existence of any zero with real part > 1/2.
- Does not apply when the sensor real part is ≤ 1/2.
- Does not supply explicit numerical bounds on the logarithmic derivative.
- Does not address convergence of the Euler product on or to the left of the critical line.
Lean usage
theorem use_in_unified (sensor : DefectSensor) : EulerTraceAdmissible sensor := by exact euler_trace_admissible sensorformal statement (Lean)
886theorem sensor_carrier_compatible (sensor : DefectSensor) :
887 ∃ (carrier : RegularCarrier),
888 carrier.radius = sensor.realPart - 1/2 ∧
889 0 < carrier.radius := by
proof body
Tactic-mode proof.
890 exact ⟨eulerRegularCarrier sensor.realPart sensor.in_strip.1,
891 euler_regular_carrier_covers_strip sensor.realPart sensor.in_strip.1,
892 by
893 change 0 < sensor.realPart - 1 / 2
894 linarith [sensor.in_strip.1]⟩
895
896/-! ### §9. The full instantiation certificate -/
897
898/-- **Euler Instantiation Certificate.**
899 Packages the complete chain:
900 Euler product → carrier convergent → nonvanishing → derivative bounded
901 → abstract interface satisfied → cost-covering applicable. -/