`analytic_rh`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.AnalyticTrace
domain: NumberTheory
line: 304 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.AnalyticTrace on GitHub at line 304.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 301⚠ DEPRECATED: depends on `defect_annular_cost_bounded`.
 302For the preferred route, see `UnifiedRH.unified_rh` (ontology) or
 303`direct_rh_from_zero_free_criterion` (analytic). -/
 304theorem analytic_rh (sensor : DefectSensor) (hm : sensor.charge ≠ 0)
 305    (hbounded : DeprecatedDefectAnnularCostBounded sensor hm) :
 306    False :=
 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. -/
 317theorem direct_rh_from_zero_free_criterion (zfc : ZeroFreeCriterion) :
 318    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=
 319  rh_from_zero_free_criterion zfc
 320
 321/-! ### §6. Canonical frontier inventory -/
 322
 323/-- **Architecture summary (April 2026, inventory frozen):**
 324
 325### Classification of open obligations
 326
 327**ACTIVE** (on critical path to unconditional RH):
 328
 329| Item | Kind | Module | Route |
 330|------|------|--------|-------|
 331| `EulerBoundaryBridgeAssumption` | explicit hypothesis | `UnifiedRH` | Ontology (preferred) |
 332| `HonestPhaseCostBridge` | structure | `AnalyticTrace` | Analytic |
 333| `charge_zero_of_honest_phase` | field in `ZeroFreeCriterion` | `AnalyticTrace` | Analytic |
 334

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.