Function checkInstance

scripts/fungrim/numeric-check.ts:128–223

Numerically check one substituted formula instance.

(expr: BoxedExpression)

  'Greater',
  'GreaterEqual',
  'NotEqual',
]);

/** Numerically check one substituted formula instance. */
function checkInstance(expr: BoxedExpression): {
  outcome: InstanceOutcome;
  detail?: string;
} {
  const op = expr.operator;
  const tol = isApproximateInstance(expr.json) ? APPROX_REL_TOL : REL_TOL;

  if (op === 'Equal' && isFunction(expr) && expr.ops.length >= 2) {
    const vals: (Complex | null)[] = expr.ops.map((o) => {
      try {
        return numericValue(o);
      } catch {
        return null;
      }
    });
    if (vals.some((v) => v === null))
      return { outcome: 'not-evaluable', detail: 'side not numeric' };
    if (vals.some((v) => !Number.isFinite(v!.re) || !Number.isFinite(v!.im)))
      return { outcome: 'Unknown', detail: 'non-finite side' };
    for (let i = 0; i + 1 < vals.length; i++) {
      if (!approxEqual(vals[i]!, vals[i + 1]!, tol)) {
        const fmt = (z: Complex) => `${z.re}${z.im ? `+${z.im}i` : ''}`;
        return {
          outcome: 'False',
          detail: `sides differ: ${vals.map((v) => fmt(v!)).join(' vs ')}`,
        };
      }
    }
    return { outcome: 'True' };
  }

  if (RELATIONS.has(op) && isFunction(expr) && expr.ops.length >= 2) {
    const vals: (Complex | null)[] = expr.ops.map((o) => {
      try {
        return numericValue(o);
      } catch {
        return null;
      }
    });
    if (vals.some((v) => v === null))
      return { outcome: 'not-evaluable', detail: 'side not numeric' };
    // Relations other than NotEqual require (numerically) real operands
    if (
      op !== 'NotEqual' &&
      vals.some((v) => Math.abs(v!.im) > REL_TOL * Math.max(absC(v!), 1))
    )
      return { outcome: 'Unknown', detail: 'complex operand in order relation' };
    // chain semantics: every consecutive pair must satisfy the relation
    for (let i = 0; i + 1 < vals.length; i++) {
      const a = vals[i]!;
      const b = vals[i + 1]!;
      const scale = Math.max(absC(a), absC(b), 1);
      const closeTo = approxEqual(a, b);
      let r: InstanceOutcome;