pith. machine review for the scientific record. sign in
theorem proved term proof

direct_rh_from_zero_free_criterion

show as:
view Lean formalization →

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)

 317theorem direct_rh_from_zero_free_criterion (zfc : ZeroFreeCriterion) :
 318    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=

proof body

Term-mode proof.

 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
 348| Item | Kind | Module |
 349|------|------|--------|
 350| `defect_annular_cost_bounded` | `axiom` | `EulerInstantiation` |
 351| `analytic_rh` | theorem | `AnalyticTrace` |
 352| `rh_chain_summary_legacy` | theorem | `AnalyticTrace` |
 353| `rh_from_single_axiom` | theorem | `ArgumentPrincipleProved` |
 354
 355### Ontology route (preferred, single bridge hypothesis)
 3561. Every sensor has admissible Euler trace. **Proved.**
 3572. Nonzero charge forces cost divergence. **Proved.**
 3583. Collapse-to-proxy transport bridge. **`EulerBoundaryBridgeAssumption` (RH-equivalent).**
 3594. No nonzero-charge sensor exists. **Proved from 1+2+3.**
 360
 361### Pure analytic route
 3621. Euler carrier convergent, nonvanishing, bounded log-derivative. **Proved.**
 3632. Floor coverage ↔ charge = 0. **Proved.**
 3643. Honest witnessed ζ⁻¹ phase data → `ZetaPhaseFamilyData`. **Proved.**
 3654. Honest phase data gives perturbation control and exact zero excess. **Proved.**
 3665. Bounded total cost → charge = 0. **`HonestPhaseCostBridge` (RH-equivalent).** -/

used by (1)

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

depends on (35)

Lean names referenced from this declaration's body.

… and 5 more