value_le_hi
plain-language theorem explainer
For any Delta-real protocol, its real value (supremum of lower endpoints) never exceeds the upper endpoint at precision n. Interval-arithmetic and certified-evaluation proofs cite this to keep the denoted real inside every approximating interval. The proof is a one-line application of the complete-lattice bound on the supremum, using cross-index lower-vs-upper comparison.
Claim. Let $x$ be a Delta-real protocol (a nested family of rational intervals with width at most $1/(n+1)$). Write $x.v$ for the supremum of its lower endpoints and $x^+(n)$ for the upper endpoint at precision $n$. Then for every $n\in\mathbb{N}$, $x.v \le x^+(n)$.
background
A Protocol (Delta-real) is a nested sequence of rational intervals whose width at stage $n$ is at most $1/(n+1)$. The intended real is the unique point common to every interval. Lower and upper endpoint sequences are monotone in opposite directions: lowers nondecreasing, uppers nonincreasing.
The real value of a protocol is defined as the supremum of the lower endpoints, $x.v := \sup_n x^-(n)$. The companion cross-comparison lemma states that any lower endpoint lies below any upper endpoint, regardless of index: $x^-(a) \le x^+(b)$ for all $a,b$. That fact is the only nontrivial input here.
The local setting is constructive real arithmetic for Recognition Science: quantities are carried as certified nested intervals rather than bare floats, so every derived real must be shown to sit inside each approximating interval before arithmetic laws (add, neg) and observational equality can be stated.
proof idea
Term-mode one-liner. The value is $\mathrm{iSup}, x^-$, so it suffices to show every lower endpoint is $\le x^+(n)$. Apply ciSup_le to the family $k \mapsto$ the cross-index inequality $x^-(k) \le x^+(n)$ supplied by lo_le_hi_cross. No further case splits or width estimates are needed.
why it matters
This is half of the sandwich that puts the denoted real inside every interval. Downstream, value_mem packages it with the dual lower bound as $x^-(n) \le x.v \le x^+(n)$; that membership is the workhorse for value_add and value_neg (uniqueness of the real in the sum/negation intervals) and for obsEq_iff_value, the faithfulness theorem that observational equality of protocols is exactly equality of values.
In the Recognition stack this sits under Primitive Recognition Calculus: certified analytic protocols and transformers evaluate expressions to Delta-reals, then read off .value. Without the upper bound, the supremum definition would not be known to land in the nested family, and the unique-real story (and thus measurement extraction) would fail. No forcing-chain landmark (T5–T8) is touched directly; the lemma is pure real-arithmetic scaffolding for later RS-native constants and observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.