tiny_le_zero
plain-language theorem explainer
A nonnegative real that is at most 1/(n+1) for every natural n must be zero. This is the Archimedean squeeze used when nested rational intervals pin a unique real. Downstream uniqueness and faithfulness of protocol values cite it. The proof is a short contradiction: positivity yields n with 1/(n+1) strictly below a.
Claim. If $a \in \mathbb{R}$ satisfies $a \ge 0$ and $a \le 1/(n+1)$ for every natural number $n$, then $a = 0$.
background
In the DeltaReal layer, a real is presented by a protocol: nested rational intervals whose widths shrink at least like $1/(n+1)$. The denoted value is the supremum of the lower endpoints (equivalently, the unique real lying in every interval).
When two candidate reals both sit in every interval of a protocol, their absolute difference is bounded by the width. The same bound appears when comparing values of observationally equal protocols. Closing those arguments needs the elementary fact that a nonnegative real squeezed by all $1/(n+1)$ vanishes.
The local setting is constructive-style real arithmetic over Mathlib: positivity, reciprocal inequalities, and the existence of a natural larger than a given positive real.
proof idea
Argue by contradiction. From nonnegativity and $a \ne 0$ obtain $a > 0$. Choose a natural $n$ with $n > 1/a$ (hence $n+1 > 1/a$). Reciprocal inequalities (via div_lt_iff₀ on the positive quantities $a$ and $n+1$) flip the comparison to $1/(n+1) < a$. That contradicts the hypothesis $a \le 1/(n+1)$. The only remaining step is absurd against the universal bound.
why it matters
This lemma is the terminal squeeze for protocol uniqueness. value_unique applies it to show any real trapped in every interval equals the protocol value (sup of lowers). obsEq_iff_value then lifts the same bound on $|x.value - y.value|$ to prove observational equality iff equality of values, the faithfulness statement for the calculus.
In the broader Recognition stack, protocols are the certified real layer under analytic expressions and transformers. Faithful values keep later forcing and continuum constructions from identifying distinct observables. The argument is pure Archimedean analysis; it does not itself invoke J-cost, $\varphi$, or the T0–T8 chain, but it underwrites the real arithmetic those layers consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.