ontological_exclusion
plain-language theorem explainer
The ontological exclusion principle states that for a defect sensor with an admissible Euler trace, the boundary transport bridge forces the annular cost to remain non-divergent. Researchers deriving the unified Riemann hypothesis from Recognition Science would cite this to exclude nonzero charges from the Euler carrier. The proof is a term-mode wrapper that instantiates the physically realizable ledger and divergence witness instances, then applies the core realizable-ledger exclusion lemma.
Claim. Let $B$ be the Euler boundary bridge assumption and let $s$ be a defect sensor. If the Euler trace is admissible at $s$, then the annular cost of $s$ does not diverge.
background
The Unified RH module replaces an earlier total-cost axiom with a three-component architecture. CostDivergent sensor means that for every real bound $B$ there exists a mesh refinement $N$ such that the annular cost exceeds $B$ whenever every ring winding equals the sensor charge. EulerTraceAdmissible sensor requires a regular carrier whose radius matches the sensor real part minus one-half, nonvanishing on the right half-plane, and bounded logarithmic derivative. PhysicallyRealizableLedger sensor carries a scalar proxy whose T1 defect remains uniformly bounded for the Euler carrier instance. EulerBoundaryBridgeAssumption is the remaining external hypothesis that collapse of the realized defect family transports to boundary approach for the bounded realizability proxy.
proof idea
The proof is a term-mode wrapper. It first lets in the PhysicallyRealizableLedger instance via euler_physically_realizable sensor. It then lets in the DivergenceWitnessesBoundary instance via euler_boundary_bridge bridge sensor. It concludes by exact application of the lemma ontological_exclusion_of_realizable sensor.
why it matters
This theorem replaces the former ontological axiom and is invoked directly by unified_rh to conclude that no nonzero-charge sensor is compatible with the Euler carrier. It closes the T1-bounded realizability step in the Recognition Science chain, ensuring that admissible traces cannot approach the T1 boundary where costs would diverge. The remaining external hypothesis is EulerBoundaryBridgeAssumption; downstream argument_principle_sampling relies on the exclusion to maintain consistency with the phi-ladder and eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.