ofRat_obsEq_iff

In the DeltaReal module, a real is presented as a nested protocol of rational intervals whose widths shrink at least as $1/(n+1)$. Observational equality means the approximating intervals overlap at every precision $n$. The central faithfulness theorem states that this relation holds exactly when the two protocols have the same real value.

The constant rational protocol at $q$ returns the degenerate interval $[q,q]$ at every precision; its value is the cast of $q$ into $\mathbb{R}$. The present statement specialises faithfulness to that embedding: two such constant protocols are observationally equal precisely when the underlying rationals coincide.

Rewrite observational equality via the central faithfulness lemma (observational equality iff equal values). Replace each side's value by the simplification that the value of the constant rational protocol is the rational itself (cast to $\mathbb{R}$). The resulting biconditional $q=r\leftrightarrow q=r$ is reflexivity after a modular cast from $\mathbb{Q}$ to $\mathbb{R}$.

This pins down that the rational embedding into protocols is injective at the observational level, so distinct rationals remain distinguishable under the protocol calculus. It sits immediately after the value simplification for constant protocols and before the native arithmetic section (addition of protocols at refined precision). No downstream consumers are recorded yet; the lemma is infrastructure for any later argument that treats rational constants as faithful points inside the recognition real line. In the broader foundation layer it supports the claim that the protocol presentation does not collapse distinct rationals before the J-cost and forcing chain are applied.