ontological_exclusion_of_realizable
plain-language theorem explainer
Any physically realizable ledger equipped with a divergence-to-boundary bridge cannot be cost-divergent once its Euler trace is admissible. Researchers closing the bounded-cost argument for Euler carriers in the Recognition Science unification cite this result. The term proof introduces the two hypotheses, builds a boundary-approaching witness from the divergence map, and applies the realizable-ledger contradiction.
Claim. Let $S$ be a defect sensor carrying a physically realizable ledger (scalar proxy $x_N>0$ with uniformly bounded T1 defect) and a divergence witness (admissible Euler trace plus cost divergence implies boundary approach). If the Euler trace on $S$ is admissible, then the annular cost on $S$ is not divergent.
background
PhysicallyRealizableLedger attaches to a sensor a scalar proxy state $x_N>0$ whose T1 defect stays uniformly bounded along the realized trajectory. DivergenceWitnessesBoundary supplies the map sending an admissible Euler trace and cost divergence to boundary approach. EulerTraceAdmissible requires a compatible regular carrier that is nonvanishing with bounded logarithmic derivative for all $σ>1/2$. CostDivergent asserts that annular cost grows without bound under uniform nonzero-charge sampling at large refinement depth.
proof idea
The term-mode proof introduces the admissibility and divergence hypotheses, constructs a BoundaryApproaching witness via the toBoundary method of DivergenceWitnessesBoundary, and concludes by exact application of physicallyRealizableLedger_not_boundaryApproaching.
why it matters
This supplies the core exclusion step for the parent theorem ontological_exclusion, which in turn feeds no_cost_divergent_sensor_of_boundary_transport. It closes the replacement of the former ontological exclusion axiom inside the T1-bounded realizability architecture of the Unified RH module. The argument rests on Euler instantiation data together with the external boundary bridge hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.