theorem
proved
direct_rh_from_zero_free_criterion
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.AnalyticTrace on GitHub at line 317.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
bridge -
or -
has -
carrier -
carrier -
of -
phase -
forces -
cost -
cost -
of -
from -
of -
of -
admissible -
divergence -
total -
analytic_rh -
HonestPhaseCostBridge -
HonestPhaseCostBridge_iff_rh -
rh_chain_summary_legacy -
rh_from_zero_free_criterion -
VectorCChargeZeroBridge -
ZeroFreeCriterion -
rh_from_single_axiom -
and -
CompositionClosureHypothesis -
WitnessedDefectSensor -
ZetaPhaseFamilyData -
total -
phase -
EBBA_iff_rh -
EulerBoundaryBridgeAssumption -
convergent
used by
formal source
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
335Both active bridges are RH-equivalent:
336- `EBBA_iff_rh` : `EulerBoundaryBridgeAssumption ↔ (∀ sensor, sensor.charge ≠ 0 → False)`
337- `HonestPhaseCostBridge_iff_rh` : `HonestPhaseCostBridge ↔ (∀ sensor, sensor.charge = 0)`
338
339**ALTERNATE** (valid but not primary):
340
341| Item | Kind | Module | Note |
342|------|------|--------|------|
343| `VectorCChargeZeroBridge` | structure | `AnalyticTrace` | Requires extra input (`VectorCSymmetryOnlyNoGo`) |
344| `CompositionClosureHypothesis` | structure | `CompositionDivergence` | Separate conditional certificate |
345
346**DEPRECATED** (inconsistent or routed through inconsistent axiom):
347