boundaryTransportCert_iff_EBBA
plain-language theorem explainer
Boundary transport certificates are equivalent to the Euler boundary bridge assumption. Researchers deriving the Riemann hypothesis from recognition composition laws cite this to connect realized defect collapse scalars to T1-bounded Euler ledger boundaries. The proof is a direct constructor that extracts the bridge field forward and repacks the assumption backward.
Claim. A boundary transport certificate holds if and only if the Euler boundary bridge assumption is satisfied.
background
The Boundary Transport module isolates the remaining physical bridge in the RH-from-RCL route. UnifiedRH already shows that nonzero-charge realized defect families possess a concrete collapse scalar approaching zero; the open content is whether this scalar transports to the T1-bounded Euler realizability scalar. BoundaryTransportCert is the structure whose sole field is precisely that Euler boundary bridge assumption.
proof idea
The term proof applies the constructor tactic to split the biconditional. Forward direction extracts the bridge field from the certificate structure. Reverse direction wraps the assumption into the certificate constructor.
why it matters
This equivalence is the direct parent of boundaryTransportCert_iff_rh_core, which rewrites to the no-nonzero-charge sensor statement identified as the RH core. It supplies the named certificate for the boundary transport step that links defect collapse to Euler ledger boundaries in the T1-exclusion setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.