Function findFailingConjunct

src/compute-engine/rubi/rubi-utils.ts:561–585

(json: Json, ctx: Ctx)

/** Rubi SumSimplerAuxQ — recursion over (expanded) sum terms:
 * - v a sum: every term of v is rational or aux-simpler wrt u
 * - u a sum: some term of u is aux-simpler wrt v
 * - both terms: v ≠ 0, same non-numeric factors, and the numeric-factor
 *   ratio nf(u)/nf(v) < −1/2 (or = −1/2 with nf(u) < 0) */
function sumSimplerAuxQ(u: Expression, v: Expression): boolean {
  if (v.operator === 'Add' && v.ops)
    return v.ops.every((t) => isLiteralRational(t) || sumSimplerAuxQ(u, t));
  if (u.operator === 'Add' && u.ops)
    return u.ops.some((t) => sumSimplerAuxQ(t, v));
  if (v.isSame(0)) return false;
  const su = splitNumericFactor(u);
  const sv = splitNumericFactor(v);
  if (!su.rest.isSame(sv.rest)) return false;
  const q = su.coef / sv.coef;
  return q < -0.5 || (q === -0.5 && su.coef < 0);
}

// ---------------------------------------------------------------------------
// Predicates — FAIL-CLOSED (undecidable ⇒ false)
// ---------------------------------------------------------------------------

type PredFn = (args: Json[], ctx: Ctx) => boolean;

export function evalCondition(json: Json, ctx: Ctx): boolean {
  if (typeof json === 'string') {
    if (json === 'True') return true;
    if (json === 'False') return false;
    // SimplifyFlag and friends — not in steps mode
    return fail(`bare symbol condition '${json}'`);