t1_cost_barrier
plain-language theorem explainer
The T1 cost barrier states that for any finite real bound C the defect functional exceeds C throughout some right neighborhood of zero. Unified RH ledger constructions cite it to rule out boundary-approaching scalar proxies. The argument is a direct one-line application of the nothing_cannot_exist theorem from the Law of Existence.
Claim. For every real number $C$ there exists $ε>0$ such that $0<x<ε$ implies $C<defect(x)$.
background
In the Unified RH module the T1 cost barrier supplies the divergence property that separates physically realizable ledgers from boundary-approaching configurations. The defect functional is defined by defect x := J x, where J is the Recognition cost from the Law of Existence; defect vanishes at unity and diverges as its argument approaches the non-existence boundary from above. The module replaces a global bounded-cost ledger with three components: CostDivergent sensors, EulerTraceAdmissible carriers, and PhysicallyRealizableLedger instances whose scalar proxies remain uniformly bounded away from zero.
proof idea
The proof is a one-line wrapper that applies the nothing_cannot_exist theorem directly to the supplied cost bound C.
why it matters
This result supplies the T1 barrier used by physicallyRealizableLedger_not_boundaryApproaching to conclude that no realizable ledger can approach the boundary x=0. It also appears in the unified_rh_cert_of_bridge definition and in realizedDefectCollapseScalar_defect_unbounded. Within the Recognition framework it instantiates the T1 scalar cost barrier from the Law of Existence, closing the realizability chain that prevents cost-divergent Euler carriers from being uniformly bounded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.