EulerBoundaryBridgeAssumption
plain-language theorem explainer
EulerBoundaryBridgeAssumption defines the remaining ontology bridge hypothesis linking realized defect collapse to boundary approach for the Euler realizability proxy. Researchers closing the analytic route to the Riemann hypothesis cite it as the interface that supplies both the honest phase cost bridge and the zero-free criterion. The declaration is introduced as a direct Prop definition that quantifies over DefectSensor, instantiates the Euler-specific PhysicallyRealizableLedger, and asserts CollapseBoundaryTransport.
Claim. For every defect sensor $s$, given the physically realizable ledger instance $euler_physically_realizable(s)$ for the Euler carrier, collapse boundary transport holds for $s$.
background
The Unified RH module replaces the former inconsistent bounded annular cost claim with a three-component T1-bounded realizability architecture. CostDivergent is proved unconditionally from annular coercivity for any nonzero-charge sensor. EulerTraceAdmissible establishes that the Euler carrier is convergent, nonvanishing, and has bounded logarithmic derivative at every hypothetical sensor location. PhysicallyRealizableLedger then carries a scalar proxy state whose T1 defect stays uniformly bounded for the Euler carrier instance. Boundary transport (DivergenceWitnessesBoundary) remains the external hypothesis: if a realizable Euler ledger were cost-divergent, its scalar proxy would be forced toward the T1 boundary $x=0$.
proof idea
This is a definition, not a proved theorem. It directly encodes the universal quantification over DefectSensor, inserts the Euler-specific PhysicallyRealizableLedger instance via letI, and asserts the CollapseBoundaryTransport property with no further reduction or lemmas.
why it matters
The definition supplies the ontology bridge that feeds zeroFreeCriterion_of_EBBA, honestPhaseCostBridge_of_EBBA, and direct_rh_from_EBBA_via_analytic, thereby closing all active routes to the Riemann hypothesis simultaneously. It corresponds to the final external hypothesis in the T1-bounded realizability chain of the Recognition framework before deriving the contradiction for nonzero-charge sensors. Downstream results quote it to obtain the honest argument principle phase family and the full zero-free criterion without invoking the deprecated defect_annular_cost_bounded route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.