No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
304theorem analytic_rh (sensor : DefectSensor) (hm : sensor.charge ≠ 0)
305 (hbounded : DeprecatedDefectAnnularCostBounded sensor hm) :
306 False :=
proof body
Term-mode proof.
307 rh_from_complex_analysis_axioms sensor hm hbounded
308
309/-! ### §5. Direct RH from zero-free criterion (analytic route target) -/
310
311/-- **Direct RH from a zero-free criterion.**
312
313The honest analytic route targets a `ZeroFreeCriterion` (§4 above) which
314packages bounded log-derivative + carrier nonvanishing + honest phase-family
315data for witnessed zeros. Once realized, this gives RH without the cost
316framework contradiction. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (12)
Lean names referenced from this declaration's body.
-
carrier
in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice
decl_use
-
carrier
in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity
decl_use
-
phase
in IndisputableMonolith.Foundation.EightTick
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
ZeroFreeCriterion
in IndisputableMonolith.NumberTheory.AnalyticTrace
decl_use
-
DefectSensor
in IndisputableMonolith.NumberTheory.CostCoveringBridge
decl_use
-
DeprecatedDefectAnnularCostBounded
in IndisputableMonolith.NumberTheory.EulerInstantiation
decl_use
-
rh_from_complex_analysis_axioms
in IndisputableMonolith.NumberTheory.EulerInstantiation
decl_use
-
phase
in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge
decl_use