boundaryTransportCert_iff_rh_core
plain-language theorem explainer
Boundary transport certificate is equivalent to the assertion that no defect sensor carries nonzero charge. Researchers completing the RH-from-RCL decomposition cite this to close the logical gap between realized defect collapse and the analytic core. The proof is a one-line wrapper that rewrites via the Euler boundary bridge equivalence and applies the EBBA-to-RH lemma.
Claim. A boundary transport certificate holds if and only if every defect sensor satisfies that nonzero charge implies falsehood (i.e., no defect sensor has nonzero charge).
background
The module treats boundary transport as the remaining physical bridge in the RH-from-RCL route. UnifiedRH already shows that nonzero-charge realized defect families produce a collapse scalar approaching zero; the open question is whether this collapse transports to the T1-bounded Euler realizability scalar. BoundaryTransportCert is the structure whose sole field is the EulerBoundaryBridgeAssumption, making the certificate exactly that bridge assumption. Upstream, boundaryTransportCert_iff_EBBA records the direct equivalence to EulerBoundaryBridgeAssumption, while EBBA_iff_rh from UnifiedRH identifies the same assumption with the no-nonzero-charge sensor condition.
proof idea
The proof rewrites the left-hand side using boundaryTransportCert_iff_EBBA to obtain the Euler boundary bridge assumption, then applies exact EBBA_iff_rh to reach the no-nonzero-charge sensor statement.
why it matters
This equivalence identifies the boundary transport certificate with the RH core already isolated in UnifiedRH, allowing the decomposition to record that the final obstruction is precisely this certificate. It is invoked directly in rh_from_rcl_completion_boundary and rh_from_rcl_logicPrime_completion_boundary to state that supplying BoundaryTransportCert yields the Riemann hypothesis. The result sits at the T1-bounded Euler realizability step after the recognition composition law and the eight-tick octave forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.