EBBA_iff_rh
plain-language theorem explainer
The theorem establishes logical equivalence between the EulerBoundaryBridgeAssumption and the prohibition of nonzero-charge defect sensors. Researchers deriving the Riemann Hypothesis from T1-bounded realizability in Recognition Science would cite this result. The proof is a term-mode pairing of the forward direction unified_rh with the converse EBBA_of_rh.
Claim. The Euler boundary bridge assumption (collapse of the realized defect family transports to boundary approach for the Euler realizability proxy) holds if and only if every defect sensor satisfies charge = 0.
background
The Unified RH module replaces direct bounding of total annular cost with a three-component architecture: CostDivergent (nonzero charge forces unbounded annular cost, proved from annular coercivity), EulerTraceAdmissible (Euler carrier is convergent and nonvanishing), and PhysicallyRealizableLedger (Euler carrier instance with bounded T1 defect). EulerBoundaryBridgeAssumption is the remaining ontology bridge: for any defect sensor equipped with the Euler physically realizable ledger, CollapseBoundaryTransport must hold. This setting draws on the Physical structure (positivity of c, ħ, G) and bridge definitions from fluids and constants modules. The module's proof chain runs from euler_trace_admissible through PhysicallyRealizableLedger to the T1 boundary prohibition.
proof idea
The proof is a one-line term wrapper that applies the two directions unified_rh and EBBA_of_rh to construct the biconditional.
why it matters
This result identifies the Riemann Hypothesis with the no-nonzero-charge sensor statement inside the T1-bounded realizability architecture, closing the ontological route of §11. It supplies the core equivalence used by direct_rh_from_zero_free_criterion (which derives RH from a zero-free criterion packaging bounded log-derivative and carrier nonvanishing) and boundaryTransportCert_iff_rh_core (which equates boundary transport certification to the same statement). The declaration touches the open question of realizing the analytic zero-free criterion without invoking the cost framework contradiction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.