pith. machine review for the scientific record. sign in
structure definition def or abbrev high

ZeroFreeCriterion

show as:
view Lean formalization →

ZeroFreeCriterion packages the four analytic conditions required to derive the Riemann Hypothesis from honest phase data on the zeta reciprocal in the pure analytic route. Researchers targeting an axiom-free RH derivation in Recognition Science would cite it as the central target structure replacing the deprecated annular cost bound. The definition assembles positive logarithmic derivative bounds on the carrier, nonvanishing of the carrier value, existence of zeta phase families for nonzero charges, and the forcing of charge zero from such data

claimA structure asserting that for all real parts $σ > 1/2$ the carrier logarithmic derivative bound is positive, the carrier value is nonzero, every witnessed defect sensor with nonzero charge admits a matching zeta phase family data, and conversely the existence of such a phase family for a sensor implies its charge vanishes.

background

In the Analytic Trace module the pure analytic route to RH is assembled axiom-free by packaging carrier estimates and phase data from the Euler product. The carrier value is the exponential of the log series $C(σ) = ∏_p (1−p^{−σ})^2 exp(2p^{−σ})$, while the carrier derivative bound is the explicit sum $2∑_p (log p) p^{-2σ}/(1−p^{-σ})$ for $σ > 1/2$. WitnessedDefectSensor records a point $ρ$ in the critical strip together with its integer charge and the meromorphic order witness from the reciprocal zeta function at that point.

proof idea

ZeroFreeCriterion is a structure definition that collects four fields. The first two fields are supplied directly by the proved lemmas carrierDerivBound_pos and carrier_nonvanishing. The honest phase family field is discharged by honest_argument_principle_phase_family using the genuine zetaDerivedPhaseFamily construction. The charge zero implication remains the narrowed target to be discharged by a subsequent cost or vector bridge.

why it matters in Recognition Science

This structure is the central target for the pure analytic route to RH and feeds directly into direct_rh_from_zero_free_criterion together with the honest-phase charge-zero bridges. It replaces the deprecated defect_annular_cost_bounded marker and closes the analytic trace infrastructure by linking meromorphic order data to charge vanishing. The remaining open step is upgrading the sampled family to bounded total cost or floor coverage.

scope and limits

formal statement (Lean)

 114structure ZeroFreeCriterion where
 115  logDeriv_bounded_on_strip :
 116    ∀ σ, 1/2 < σ → 0 < carrierDerivBound σ
 117  carrier_nonvanishing_on_strip :
 118    ∀ σ, 1/2 < σ → carrierValue σ ≠ 0
 119  honest_phase_family :
 120    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 →
 121      ∃ zfd : ZetaPhaseFamilyData,
 122        zfd.sensor = sensor.toDefectSensor ∧
 123          zfd.phaseFamily.sensor = sensor.toDefectSensor
 124  charge_zero_of_honest_phase :
 125    ∀ (sensor : WitnessedDefectSensor),
 126      (∃ zfd : ZetaPhaseFamilyData,
 127        zfd.sensor = sensor.toDefectSensor ∧
 128          zfd.phaseFamily.sensor = sensor.toDefectSensor) →
 129        sensor.charge = 0
 130
 131/-- A `ZeroFreeCriterion` gives the RH directly. -/

used by (20)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.