neg_contains_neg
plain-language theorem explainer
neg_contains_neg establishes that containment is preserved under negation for closed intervals with rational endpoints. Numerics code bounding transcendental functions or phi-ladder quantities would cite it when sign flips appear in interval propagations. The term-mode proof constructs the two containment inequalities directly after unfolding the negated bounds and applying order reversal.
Claim. If $x$ lies in the closed interval $I=[a,b]$ with $a,b$ rational and $a≤b$, then $-x$ lies in $-I$, where containment means $a≤x≤b$.
background
The module supplies verified interval arithmetic that uses rational endpoints to produce exact bounds on real computations. Interval is the structure carrying lo and hi as rationals together with the proof lo≤hi. The predicate contains asserts that a real number x satisfies lo≤x≤hi for the given interval.
proof idea
The term proof opens the contains goal with constructor, then simplifies the definitions of the negated lower and upper bounds via neg_lo and neg_hi (which insert Rat.cast_neg). Each resulting inequality is discharged by applying neg_le_neg to the corresponding half of the hypothesis hx.
why it matters
The lemma supplies a basic closure property for the interval arithmetic layer that supports numerical checks throughout Recognition Science. It feeds verified bound propagation for quantities such as J-cost minima and phi-tier masses, consistent with the eight-tick octave and D=3 spatial structure. No direct downstream uses are recorded, leaving it as foundational scaffolding for later numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.