theorem proved term proof

`rh_frontier_inventory`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 367theorem rh_frontier_inventory : True := trivial

proof body

Term-mode proof.

 368
 369/-- ⚠ DEPRECATED: routes through the inconsistent `defect_annular_cost_bounded`.
 370Use `unified_rh` (ontology) or `direct_rh_from_honestPhaseCostBridge` (analytic). -/

depends on (3)

Lean names referenced from this declaration's body.

or in IndisputableMonolith.Constants.EulerMascheroni decl_use
direct_rh_from_honestPhaseCostBridge in IndisputableMonolith.NumberTheory.AnalyticTrace decl_use
unified_rh in IndisputableMonolith.Unification.UnifiedRH decl_use