Item 118: Rational attainment and certificate completeness for the computed forced interval

*Re-filed 2026-10-21 by the rebuttal-and-end-to-end round from branch round/2026-09-16-seed-statics, where it was item 94; content unchanged; the branch round is landed under projects/normativity/seed/rounds/2026-09-16-seed-statics/.*

SeedStatics.forcedInterval_spec proves the computed endpoints valid and attained at real points, because FourierMotzkin states satisfaction over ℝ; attainment at a rational point — the fact that a rational system feasible over ℝ is feasible over ℚ — is not in the repository, so the rational predicate IsForcedInterval is not inhabited by the computed pair. Separately, BoundCert.sound gives soundness of endpoint certificates and nothing gives tightness (LP duality). Either transfer the elimination's completeness direction to ℚ or give the vertex argument, and prove that every valid bound is certified. This is the duality half of item 79's completeness.

Deliverable shape: IsForcedInterval S W st F φ lo hi inhabited by forcedInterval, and ∀ c, LowerBound … c → ∃ cert, −cert.value ≥ c (or the statement that fails, with its witness). Acceptance check: the Lean audits clean.

Context: STATICS.md §§2, 5 of the seed-statics round; FourierMotzkin.lean's header on why satisfaction lives in ℝ. Consumed by: item 79; any registration of forcedInterval_spec. A solution ships: the two theorems.