@@ -394,6 +394,127 @@ function assumeInequality(proposition: BoxedExpression): AssumeResult {
394394 const unknowns = result . unknowns ;
395395 if ( unknowns . length === 0 ) return 'not-a-predicate' ;
396396
397+ // Check if the new inequality is implied by or contradicts existing bounds
398+ // (for single-symbol inequalities)
399+ if ( unknowns . length === 1 ) {
400+ const symbol = unknowns [ 0 ] ;
401+ const bounds = getInequalityBoundsFromAssumptions ( ce , symbol ) ;
402+
403+ // The normalized form is Less(p, 0) or LessEqual(p, 0) where p = lhs - rhs
404+ // For a simple symbol case like "x > k", this becomes Less(-x + k, 0) meaning k - x < 0, i.e., x > k
405+ // For "x < k", this becomes Less(x - k, 0) meaning x - k < 0, i.e., x < k
406+
407+ // Check if this is a simple "symbol > value" or "symbol < value" case
408+ const originalOp = proposition . operator ;
409+ const isSymbolOnLeft = proposition . op1 . symbol === symbol ;
410+ const otherSide = isSymbolOnLeft ? proposition . op2 : proposition . op1 ;
411+
412+ // Only do bounds checking for simple comparisons like "x > k" where k is numeric
413+ if ( otherSide . numericValue !== null ) {
414+ const k = otherSide . numericValue ;
415+
416+ if ( typeof k === 'number' && isFinite ( k ) ) {
417+ // Determine the EFFECTIVE relationship based on operator and symbol position
418+ // Less(a, b) means a < b:
419+ // - if a is symbol: symbol < b, effective is "less"
420+ // - if b is symbol: a < symbol, so symbol > a, effective is "greater"
421+ // Greater(a, b) means a > b:
422+ // - if a is symbol: symbol > b, effective is "greater"
423+ // - if b is symbol: a > symbol, so symbol < a, effective is "less"
424+ let effectiveOp : 'greater' | 'greaterEqual' | 'less' | 'lessEqual' ;
425+ if ( originalOp === 'Greater' ) {
426+ effectiveOp = isSymbolOnLeft ? 'greater' : 'less' ;
427+ } else if ( originalOp === 'GreaterEqual' ) {
428+ effectiveOp = isSymbolOnLeft ? 'greaterEqual' : 'lessEqual' ;
429+ } else if ( originalOp === 'Less' ) {
430+ effectiveOp = isSymbolOnLeft ? 'less' : 'greater' ;
431+ } else {
432+ // LessEqual
433+ effectiveOp = isSymbolOnLeft ? 'lessEqual' : 'greaterEqual' ;
434+ }
435+
436+ // Check for tautologies and contradictions based on existing bounds
437+ if ( effectiveOp === 'greater' || effectiveOp === 'greaterEqual' ) {
438+ // We're asserting symbol > k or symbol >= k
439+ const isStrict = effectiveOp === 'greater' ;
440+
441+ if ( bounds . lowerBound !== undefined ) {
442+ const lowerVal = bounds . lowerBound . numericValue ;
443+ if ( typeof lowerVal === 'number' && isFinite ( lowerVal ) ) {
444+ // We already know symbol > lowerVal (or >=)
445+ if ( isStrict ) {
446+ // Assuming symbol > k: tautology if existing lower bound implies this
447+ // If lowerVal > k, then symbol > lowerVal > k, so symbol > k (tautology)
448+ // If lowerVal == k and bound is strict, then symbol > lowerVal = k (tautology)
449+ if ( lowerVal > k ) return 'tautology' ;
450+ if ( bounds . lowerStrict && lowerVal >= k ) return 'tautology' ;
451+ } else {
452+ // Assuming symbol >= k: tautology if lowerVal >= k (with strict bound) or lowerVal > k
453+ if ( lowerVal > k ) return 'tautology' ;
454+ if ( bounds . lowerStrict && lowerVal >= k ) return 'tautology' ;
455+ if ( ! bounds . lowerStrict && lowerVal >= k ) return 'tautology' ;
456+ }
457+ }
458+ }
459+
460+ if ( bounds . upperBound !== undefined ) {
461+ const upperVal = bounds . upperBound . numericValue ;
462+ if ( typeof upperVal === 'number' && isFinite ( upperVal ) ) {
463+ // We know symbol < upperVal (or <=), now checking symbol > k
464+ if ( isStrict ) {
465+ // Contradiction if upperVal <= k
466+ if ( upperVal < k ) return 'contradiction' ;
467+ if ( bounds . upperStrict && upperVal <= k ) return 'contradiction' ;
468+ if ( ! bounds . upperStrict && upperVal <= k ) return 'contradiction' ;
469+ } else {
470+ // symbol >= k: contradiction if upperVal < k
471+ if ( upperVal < k ) return 'contradiction' ;
472+ if ( bounds . upperStrict && upperVal <= k ) return 'contradiction' ;
473+ }
474+ }
475+ }
476+ } else {
477+ // effectiveOp is 'less' or 'lessEqual'
478+ // We're asserting symbol < k or symbol <= k
479+ const isStrict = effectiveOp === 'less' ;
480+
481+ if ( bounds . upperBound !== undefined ) {
482+ const upperVal = bounds . upperBound . numericValue ;
483+ if ( typeof upperVal === 'number' && isFinite ( upperVal ) ) {
484+ // We already know symbol < upperVal (or <=)
485+ if ( isStrict ) {
486+ // Assuming symbol < k: tautology if existing upper bound implies this
487+ if ( upperVal < k ) return 'tautology' ;
488+ if ( bounds . upperStrict && upperVal <= k ) return 'tautology' ;
489+ } else {
490+ // symbol <= k: tautology if upperVal <= k
491+ if ( upperVal < k ) return 'tautology' ;
492+ if ( upperVal <= k ) return 'tautology' ;
493+ }
494+ }
495+ }
496+
497+ if ( bounds . lowerBound !== undefined ) {
498+ const lowerVal = bounds . lowerBound . numericValue ;
499+ if ( typeof lowerVal === 'number' && isFinite ( lowerVal ) ) {
500+ // We know symbol > lowerVal (or >=), now checking symbol < k
501+ if ( isStrict ) {
502+ // Contradiction if lowerVal >= k
503+ if ( lowerVal > k ) return 'contradiction' ;
504+ if ( bounds . lowerStrict && lowerVal >= k ) return 'contradiction' ;
505+ if ( ! bounds . lowerStrict && lowerVal >= k ) return 'contradiction' ;
506+ } else {
507+ // symbol <= k: contradiction if lowerVal > k
508+ if ( lowerVal > k ) return 'contradiction' ;
509+ if ( bounds . lowerStrict && lowerVal > k ) return 'contradiction' ;
510+ }
511+ }
512+ }
513+ }
514+ }
515+ }
516+ }
517+
397518 // Case 3: single unknown - ensure the symbol has type 'real'
398519 // (inequalities imply the symbol is a real number)
399520 if ( unknowns . length === 1 ) {
0 commit comments