euler_boundary_bridge
plain-language theorem explainer
The definition supplies the boundary transport witness for any defect sensor once the remaining ontology bridge assumption is granted. Researchers establishing the ontological exclusion principle cite it to link cost divergence to scalar proxy approach at the T1 boundary. The construction is a direct one-line wrapper around the divergence witness lemma.
Claim. Given the remaining ontology bridge assumption (collapse of the realized defect family transports to boundary approach for the Euler realizability proxy) and a defect sensor, the definition yields that the sensor satisfies: admissible Euler trace plus cost divergence implies the scalar proxy approaches the T1 boundary.
background
The Unified RH module organizes realizability into three layers: CostDivergent (nonzero charge forces unbounded annular cost), EulerTraceAdmissible (convergent carrier with bounded logarithmic derivative), and PhysicallyRealizableLedger (uniformly bounded T1 defect for the Euler carrier). DivergenceWitnessesBoundary is the class asserting that any such ledger, if cost-divergent, must drive its scalar proxy toward the T1 boundary x=0. This replaces the former ontological exclusion axiom with a structured transport statement. The upstream EulerBoundaryBridgeAssumption isolates the remaining hypothesis that converts realized-defect collapse into proxy boundary approach.
proof idea
One-line wrapper that applies the euler_divergence_witnesses_boundary construction to the supplied bridge assumption and sensor.
why it matters
It supplies the instance required by the ontological exclusion theorem, which states that Euler admissibility plus boundary transport forbid cost divergence. This closes the chain from Euler instantiation data through the T1-bounded realizability architecture to the prohibition of divergent sensors, replacing the prior axiom. The definition is invoked directly in the certificate form of boundary transport and in the no-cost-divergent-sensor result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.