physicallyRealizableLedger_not_boundaryApproaching
plain-language theorem explainer
A physically realizable ledger, carrying a scalar proxy whose T1 defect remains uniformly bounded, cannot have that proxy driven arbitrarily close to zero. Researchers working on the unified RH architecture cite this result to close the T1 boundary exclusion step. The proof assumes boundary approach, extracts the uniform defect bound K from the ledger interface, invokes the T1 cost barrier to produce an N where defect exceeds K, and obtains the contradiction via not_lt_of_ge.
Claim. Let $s$ be a defect sensor equipped with a physically realizable ledger, so that its scalar proxy state $x_N > 0$ satisfies a uniform bound on the defect functional: there exists $K$ such that defect$(x_N) ≤ K$ for all $N$. Then $x_N$ cannot approach the T1 boundary: it is not the case that for every $ε > 0$ there exists $N$ with $x_N < ε$.
background
In the Unified RH module the architecture separates cost divergence, Euler trace admissibility, and the PhysicallyRealizableLedger interface. The latter attaches to a DefectSensor a scalar proxy state $x_N$ together with the guarantee that defect$(x_N)$ stays bounded by some fixed $K$; defect is the J-cost functional from LawOfExistence. BoundaryApproaching is the predicate that this proxy can be driven below any positive $ε$. The module imports K from Constants (defined as $ϕ^{1/2}$) and the canonical/extracted arithmetic objects, but the local argument relies only on the ledger interface and the sibling t1_cost_barrier lemma.
proof idea
Proof by contradiction. Assume BoundaryApproaching sensor. Obtain the uniform bound $K$ from PhysicallyRealizableLedger.scalarDefectBounded. Apply t1_cost_barrier K to produce $ε > 0$ such that any positive scalar state below $ε$ has defect strictly larger than $K$. The boundary assumption supplies an $N$ with scalarState $N < ε$; the barrier then yields $K <$ defect(scalarState $N$), contradicting the uniform bound via not_lt_of_ge.
why it matters
This supplies the proved half of the T1 boundary exclusion used directly by realizable_not_boundary_approaching and by bridge_contradiction_core to reach absurdity. It is invoked inside ontological_exclusion_of_realizable and obstruction_structural_asymmetry to separate the bounded realizability proxy from the collapse observable that approaches zero. The result closes the T1 step in the forcing chain for the Euler carrier while leaving the external DivergenceWitnessesBoundary bridge as the remaining hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.