Function checkBoundsAgainst

src/compute-engine/assume.ts:1070–1111

* Check a candidate bound against the existing bounds for the same subject * (design §4.3 — bounds-level consistency only, per subject). * * Returns `'tautology'` if the new bound is already implied, * `'contradiction'` if it is incompatible, `undefined` otherwise (store it).

(
  existing: IntervalBounds,
  candidate: IntervalBounds
)

  cause?: Expression
): AssumeResult {
  if (!hasDef(ce, symbol)) {
    ce.declare(symbol, type);
    recordDeclaredByAssumption(ce, symbol, cause);
    return 'ok';
  }

  // Shadow a parent-scope declaration in the current scope so the
  // assumption is reverted when the scope is popped. The shadow's creation
  // is recorded here — the write below then only appends when it actually
  // changes the shadow's type (append-on-change), so the creation entry is
  // the shadow's one guaranteed provenance record.
  if (!ce.context?.lexicalScope?.bindings.has(symbol)) {
    ce.declare(symbol, type);
    recordDeclaredByAssumption(ce, symbol, cause);
  }

  const def = ce.lookupDefinition(symbol);
  if (isValueDef(def)) {
    // An explicitly declared, known type is *narrowed* to the meet of the
    // declared type and the assumed type. It is a contradiction only when
    // that meet is empty. The old check (`!isSubtype(assumed, declared)`)
    // misfired whenever the assumed type was not a *subtype* of the declared
    // one even though they overlapped, e.g. `assume(q ∈ ℤ)` on a
    // `finite_number`-declared `q` (`integer ⊄ finite_number` only because
    // `integer` admits ±∞ — the meet is the satisfiable `finite_integer`).
    if (
      def.value.type &&
      !def.value.type.isUnknown &&
      !def.value.inferredType
    ) {
      const meet = reduceType({
        kind: 'intersection',
        types: [type, def.value.type.type],
      });
      if (isEmptyType(meet)) return 'contradiction';
      const previousMeet = def.value.type;
      def.value.type = new BoxedType(meet, ce._typeResolver);
      def.value.inferredType = false;
      recordAssumedType(ce, def.value, cause, previousMeet);
      return 'ok';
    }
    const previous = def.value.type;
    def.value.type = new BoxedType(type, ce._typeResolver);
    // The type was explicitly asserted: it is no longer an inferred type
    // (so a subsequent bare-symbol inequality won't widen it to 'real')