DivergenceWitnessesBoundary
plain-language theorem explainer
A realizable ledger for a defect sensor witnesses boundary transport when cost divergence forces its scalar proxy state toward the T1 boundary at zero. Researchers establishing ontological exclusion for Euler carriers in the Unified RH architecture would cite this interface. The declaration packages the required implication from admissibility and divergence to boundary approach as the sole method of a typeclass.
Claim. Let $S$ be a defect sensor equipped with a physically realizable ledger. Then $S$ satisfies boundary transport if, whenever the Euler trace on $S$ is admissible and the annular cost is divergent, the scalar proxy state $x_N$ satisfies: for every $ε>0$ there exists $N$ such that $x_N<ε$.
background
The Unified RH module replaces the former ontological exclusion axiom with a structured architecture of four components. CostDivergent states that nonzero charge forces annular cost to exceed any bound under uniform winding sampling, with growth $Θ(m² log N)$. EulerTraceAdmissible requires a regular carrier compatible with the sensor location, nonvanishing for $σ>1/2$, and with bounded logarithmic derivative. PhysicallyRealizableLedger attaches a scalar proxy state $x_N>0$ whose defect $J(x_N)$ remains uniformly bounded. BoundaryApproaching asserts that this proxy can be driven arbitrarily close to zero. DivergenceWitnessesBoundary supplies the missing map from admissibility plus divergence to boundary approach, described in the module as the remaining external bridge hypothesis.
proof idea
This is a class definition introducing the single field toBoundary. It directly encodes the implication EulerTraceAdmissible sensor → CostDivergent sensor → BoundaryApproaching sensor without any further reduction or lemma application.
why it matters
This declaration supplies the boundary transport interface invoked by ontological_exclusion_of_realizable to obtain ¬CostDivergent sensor from admissibility. It is recovered as a theorem in euler_divergence_witnesses_boundary and euler_boundary_bridge, then used in ontological_exclusion and no_cost_divergent_sensor_of_boundary_transport. In the Recognition framework it closes the loop from proved cost divergence back to the T1 prohibition on boundary approach for realizable ledgers, replacing the old axiom while preserving consistency with the forcing chain and the defect functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.