eulerScalarProxy_not_boundaryApproaching
plain-language theorem explainer
The theorem shows that the Euler scalar proxy attached to a defect sensor cannot approach the T1 boundary. A physicist working on bounded realizability would cite it to confirm that the Euler carrier's bounded scale stays stable without external forcing. The proof is a direct one-line wrapper that instantiates the Euler-specific PhysicallyRealizableLedger and applies the general non-approach lemma for realizable ledgers.
Claim. Let $s$ be a defect sensor. If $s$ carries a physically realizable ledger via the Euler carrier, then the scalar proxy state of $s$ does not approach the T1 boundary: $¬$ BoundaryApproaching$(s)$.
background
The Unified RH module replaces earlier total-cost axioms with a three-component architecture: CostDivergent sensors force unbounded annular cost, EulerTraceAdmissible carriers are convergent with bounded logarithmic derivative, and PhysicallyRealizableLedger attaches a scalar proxy state $x_N > 0$ whose T1 defect remains uniformly bounded. The class PhysicallyRealizableLedger requires an admissible Euler trace plus the scalarStatePos and scalarDefectBounded predicates. Upstream results include IntegrationGap.A (the active edge count per tick, satisfying the $φ$-power balance at $D=3$) and cost definitions from MultiplicativeRecognizerL4 and ObserverForcing that ground J-cost. The module proof chain runs from euler_trace_admissible through PhysicallyRealizableLedger to the T1 prohibition on boundary approach.
proof idea
Assume BoundaryApproaching sensor. Instantiate PhysicallyRealizableLedger sensor via euler_physically_realizable sensor. Apply the upstream lemma physicallyRealizableLedger_not_boundaryApproaching sensor to obtain the contradiction. The entire proof is a one-line wrapper around that general realizable-ledger result.
why it matters
This step confirms the Euler proxy cannot collapse toward the T1 boundary on its own, making explicit the need for a separate bridge theorem under cost divergence. It occupies the position in the module chain immediately after PhysicallyRealizableLedger sensor and before any DivergenceWitnessesBoundary hypothesis. In the Recognition Science setting it reinforces T1-bounded realizability, consistent with the eight-tick octave and the Euler instantiation data that fix the carrier scale. No downstream uses are recorded yet; the result closes one potential collapse path for the scalar proxy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.