MATH.20:4.3 - Establish the bound over its claimed domain
Prove the inequality or inclusion for every admitted case to which the result will apply. A feasible witness establishes one attainable value. A claim about all candidates needs a relation covering all of them, as the edge inequalities in :5.1 cover every path.
Track the assumptions used. For a relaxed feasible set, establish the original set’s inclusion in it and keep the objective unchanged on original candidates. For a norm estimate, specify the norm and the operator property that supports it. For a probabilistic inequality, retain its distributional conditions and probability claim.
Use a known comparison theorem when it settles this question. If it does not, MATH.19 can construct the missing intermediate inequality and MATH.6 can test a suspected overclaim with a separating case.
Where the comparison cannot be established, return the condition that is missing or the counterexample. A trial value may remain useful for exploration without being used as the unproved bound.