Function assumeElementOfSet

src/compute-engine/assume.ts:818–936

* Assume `symbol ∈ setExpr`, decomposing structured sets into independent * stored facts plus type refinements ("shallow saturation", design §3.2): * * | Set shape | Action | * |---|---| * | primitive number set (ℂ, ℝ, ℤ…) | type refinement (historical behavior) | * | `Range(a, b)` | `integer`

(
  ce: ComputeEngine,
  symbol: string,
  setExpr: Expression
)

      if (r === 'ok') sawOk = true;
    }
    return sawOk ? 'ok' : 'tautology';
  }

  let op = '';
  let lhs: Expression;
  let rhs: Expression;
  if (proposition.operator === 'Less') {
    lhs = proposition.op1;
    rhs = proposition.op2;
    op = '<';
  } else if (proposition.operator === 'LessEqual') {
    lhs = proposition.op1;
    rhs = proposition.op2;
    op = '<=';
  } else if (proposition.operator === 'Greater') {
    lhs = proposition.op2;
    rhs = proposition.op1;
    op = '<';
  } else if (proposition.operator === 'GreaterEqual') {
    lhs = proposition.op2;
    rhs = proposition.op1;
    op = '<=';
  }
  if (!op) return 'internal-error';
  // The proposition is boxed `{ form: 'raw' }` (engine-assumptions.ts), so its
  // operands are non-canonical. Arithmetic (`.sub()`, and the `.neg()` it calls)
  // must run on canonical operands — otherwise a canonical `Negate` ends up
  // wrapping a non-canonical symbol, tripping the `isCanonical` assert in
  // `BoxedSymbol.toNumericValue` once the difference is numerically compared.
  const p = lhs!.canonical.sub(rhs!.canonical);

  // Case 2
  const result = ce.expr([op === '<' ? 'Less' : 'LessEqual', p, 0]).evaluate();

  if (isSymbol(result, 'True')) return 'tautology';
  if (isSymbol(result, 'False')) return 'contradiction';

  const unknowns = result.unknowns;
  if (unknowns.length === 0) return 'not-a-predicate';

  //
  // Part-subject inequalities (design §4.2), e.g. `Re(s) > 1` normalized to
  // `Less(1 - Real(s), 0)`: the normalized lhs is ±Part(x) plus an optional
  // numeric constant, where Part ∈ {Real, Imaginary, Abs, Argument}.
  //
  const normalizedLhs = isFunction(result) ? result.op1 : undefined;
  const partSubject =
    normalizedLhs !== undefined ? partBoundSubject(normalizedLhs) : undefined;
  if (partSubject !== undefined) {
    const newBounds = boundsFromNormalizedInequality(result, partSubject);

    // Bounds-level tautology/contradiction check against existing bounds on
    // the *same* subject (design §4.3; cross-subject consistency is out of
    // scope).
    if (newBounds !== undefined) {
      const existing = boundsForCurrentDefinition(ce, partSubject);
      const status = checkBoundsAgainst(existing, newBounds);
      if (status !== undefined) return status;