Function assumeElement

src/compute-engine/assume.ts:751–801

(proposition: Expression)

              // We already know symbol > lowerVal (or >=)
              if (isStrict) {
                // Assuming symbol > k: tautology if existing lower bound implies this
                // If lowerVal > k, then symbol > lowerVal > k, so symbol > k (tautology)
                // If lowerVal == k and bound is strict, then symbol > lowerVal = k (tautology)
                if (lowerVal > k) return 'tautology';
                if (bounds.lowerStrict && lowerVal >= k) return 'tautology';
              } else {
                // Assuming symbol >= k: tautology if lowerVal >= k (with strict bound) or lowerVal > k
                if (lowerVal > k) return 'tautology';
                if (bounds.lowerStrict && lowerVal >= k) return 'tautology';
                if (!bounds.lowerStrict && lowerVal >= k) return 'tautology';
              }
            }
          }

          if (bounds.upper !== undefined) {
            const upperVal = isNumber(bounds.upper)
              ? bounds.upper.numericValue
              : undefined;
            if (typeof upperVal === 'number' && isFinite(upperVal)) {
              // We know symbol < upperVal (or <=), now checking symbol > k
              if (isStrict) {
                // Contradiction if upperVal <= k
                if (upperVal < k) return 'contradiction';
                if (bounds.upperStrict && upperVal <= k) return 'contradiction';
                if (!bounds.upperStrict && upperVal <= k)
                  return 'contradiction';
              } else {
                // symbol >= k: contradiction if upperVal < k
                if (upperVal < k) return 'contradiction';
                if (bounds.upperStrict && upperVal <= k) return 'contradiction';
              }
            }
          }
        } else {
          // effectiveOp is 'less' or 'lessEqual'
          // We're asserting symbol < k or symbol <= k
          const isStrict = effectiveOp === 'less';

          if (bounds.upper !== undefined) {
            const upperVal = isNumber(bounds.upper)
              ? bounds.upper.numericValue
              : undefined;
            if (typeof upperVal === 'number' && isFinite(upperVal)) {
              // We already know symbol < upperVal (or <=)
              if (isStrict) {
                // Assuming symbol < k: tautology if existing upper bound implies this
                if (upperVal < k) return 'tautology';
                if (bounds.upperStrict && upperVal <= k) return 'tautology';
              } else {
                // symbol <= k: tautology if upperVal <= k
                if (upperVal < k) return 'tautology';
                if (upperVal <= k) return 'tautology';
              }
            }