rh_frontier_inventory
plain-language theorem explainer
The rh_frontier_inventory declaration records the frozen April 2026 classification of active, alternate, and deprecated routes to the Riemann hypothesis inside the analytic trace module. A researcher auditing the Recognition Science unification would cite it to confirm that both the ontology bridge via EulerBoundaryBridgeAssumption and the analytic bridge via HonestPhaseCostBridge are RH-equivalent. Its proof is the one-line term trivial that simply asserts the inventory state.
Claim. The classification of open obligations toward an unconditional Riemann hypothesis, distinguishing the ontology route through the Euler boundary bridge assumption from the pure analytic route through the honest phase cost bridge, holds.
background
The Analytic Trace module assembles axiom-free carrier infrastructure for the Riemann hypothesis after eliminating prior axioms such as zeroWindingOfHolNonvanishing. It defines the HonestPhaseCostBridge structure requiring that any honest zeta phase family realizes bounded annular cost, which then forces zero defect charge via the general defect-cost theorem. The ZeroFreeCriterion packages log-derivative bounds on the strip, carrier nonvanishing, and the existence of honest phase families for nonzero-charge sensors. The module doc states that two routes exist: the preferred ontology route in UnifiedRH using EulerBoundaryBridgeAssumption and the pure analytic route targeting ZeroFreeCriterion from honest phase data. Upstream results include unified_rh, which shows no nonzero-charge sensor is compatible with the Euler carrier under the ontological exclusion principle, and direct_rh_from_honestPhaseCostBridge, which derives the zero-charge conclusion from any honest-phase bounded-cost bridge.
proof idea
The proof is a one-line term application of trivial that asserts the truth of the inventory classification without invoking lemmas or tactics.
why it matters
This declaration freezes the current frontier inventory, directing attention to the active bridges HonestPhaseCostBridge and EulerBoundaryBridgeAssumption as the RH-equivalent targets that close the analytic and ontology routes respectively. It feeds the parent results unified_rh and direct_rh_from_honestPhaseCostBridge while marking the deprecated path through defect_annular_cost_bounded. In the Recognition Science framework it touches the T5 J-uniqueness and T6 phi fixed-point steps by keeping the analytic trace consistent with the forcing chain, though it leaves open the discharge of the remaining bridge hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.