unified_rh
plain-language theorem explainer
The theorem shows that the Euler boundary bridge assumption forces a contradiction for any defect sensor with nonzero charge via the ontological exclusion principle. Researchers closing the Recognition Science derivation of the Riemann Hypothesis cite this as the ontology-based closure. The proof is a one-line term application of ontological_exclusion to the admissible Euler trace and the proved cost divergence for nonzero charge.
Claim. Assuming the Euler boundary bridge hypothesis, for every defect sensor $s$ with nonzero charge a contradiction follows.
background
The module replaces the inconsistent bounded annular cost claim with a three-component architecture. CostDivergent shows nonzero charge forces unbounded annular cost from annular coercivity. EulerTraceAdmissible establishes that the Euler carrier is convergent, nonvanishing, and has bounded logarithmic derivative at every sensor. PhysicallyRealizableLedger carries a T1-bounded scalar proxy state for the Euler carrier instance. The EulerBoundaryBridgeAssumption is the remaining hypothesis that realized defect family collapse transports to boundary approach for the realizability proxy. This combines with the proved fact that T1 forbids boundary approach for realizable ledgers. Upstream results include the defect functional from LawOfExistence, which equals J for positive arguments, and the logical integers from IntegersFromLogic.
proof idea
The proof is a one-line term wrapper that applies ontological_exclusion to the supplied bridge, the sensor, the proved euler_trace_admissible sensor, and the proved nonzero_charge_cost_divergent sensor hm.
why it matters
This theorem supplies the ontology closure for the Riemann Hypothesis, feeding directly into honestPhaseCostBridge_of_EBBA and rh_frontier_inventory. It completes the chain from T1-bounded realizability through the Euler carrier to exclusion of nonzero charge sensors. It fills the step from the Law of Existence defect functional and Euler instantiation data. The framework landmarks include the T1 defect bound and the eight-tick octave structure. It leaves open discharge of the external bridge hypothesis for an unconditional result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.