#4859 limit2: finite-nonzero ÷ ind returns und instead of ind

[David Scherfgen]

Spotted by Claude:

limit(cos(1/x)/(sin(x)+2), x, inf);   /* actual: und;  expected: ind */

Cause:

((eq d1 '$ind)
 (cond ((and (infinityp n1) (eq ($sign dn) '$pos)) (return n1))
       ((and (infinityp n1) (eq ($sign dn) '$neg)) (return (simpinf (m* -1 n1))))
       ((and (zerop1 n1) (or (eq ($sign dn) '$pos) (eq ($sign dn) '$neg))) (return 0))
       (t (return '$und))))          ; <- finite nonzero n1 falls here

When the numerator limit n1 is a finite nonzero constant and the denominator limit d1 is ind (bounded oscillation), the catch-all returns und unconditionally. But a finite constant divided by a bounded, provably nonzero oscillating quantity is itself bounded, i.e. ind. The sibling ind/ind clause just above (line 945) already does exactly the right guard.

[David Scherfgen]

Comment by Claude:

Follow-up — before "fixing" this, note that the obvious one-liner is not safe.

The tempting fix is to just mirror the ind/ind clause above it:

(t (return (if (eq t (mnqp dn 0)) '$ind '$und)))   ; DON'T just do this

That last clause is a catch-all reached by three structurally different
situations, and ind is correct for only one of them.

At that clause we know d1 (post-ridofab) is $ind, and n1 (post-ridofab)
is neither $und (already consumed by the ((or (eq d1 '$und) ...)) clause) nor
$ind (the ind/ind case is consumed above, and ridofab never manufactures
$ind). So n1 is one of { finite value, an infinity, exact 0 }, and the
sub-cond dispatches on which:

1. n1 finite nonzero → always falls through to the catch-all (the earlier arms
   gate on infinityp/zerop1 of n1). Correct: finite / bounded-nonzero =
   ind. ✓ This is the reported case.
2. n1 an infinity ($inf/$minf/$infinity) → falls through only when
   ($sign dn) is neither $pos nor $neg (otherwise the infinityp arms
   fire). Correct: ∞ / bounded-nonzero = infinity, not ind.
3. n1 exact 0 → falls through only when ($sign dn) is neither $pos nor
   $neg (otherwise the zerop1 arm fires). Correct: 0 / bounded-nonzero =
   0, not ind.
   The unconditional (if (eq t (mnqp dn 0)) '$ind '$und) returns ind for all
   three, so it turns cases 2 and 3 into wrong answers — and worse than the
   current und, which is at least a vague "can't say" rather than a definite
   (wrong) "bounded".

Cases 2 and 3 are reachable with a complex denominator: then ($sign dn) is
$complex (neither pos nor neg) while mnqp(dn,0)=t. (For a real continuous
dn, provably-nonzero forces a constant sign by IVT, so the pos/neg arms catch
it before the catch-all.) Untested, but the routing looks like:

• case 2: limit(x/(sin(x)+%i), x, inf) — should be infinity; naive fix gives ind

• case 3: limit(sin(1/x)/(sin(x)+%i), x, inf) — should be 0; naive fix gives ind
  Two more subtleties worth recording:

• Keep the (eq t (mnqp dn 0)) form; do not shorten to (if (mnqp dn 0) ...).
  mnqp is three-valued: t = proven ≠ 0, nil = proven = 0, otherwise a
  $notequal/$unknown noun that is truthy in Lisp. A bare if would treat
  "can't decide" as "nonzero" and wrongly return ind.

• mnqp(dn,0)=t proves dn ≠ 0 but not that dn is bounded away from 0. A
  dn with limit ind can be provably nonzero yet have infimum 0 — e.g.
  exp(-x)+1+cos(x) (provably > 0, limit 1+cos(x) = ind, but → 0 where
  cos(x) = -1). Then even finite/dn is unbounded and the honest answer is
  und/infinity, not ind. This heuristic gap already exists in the ind/ind
  clause, so it is pre-existing, but note that "provably nonzero ⇒ ind" is not
  airtight even for case 1.
  Safe minimal fix — restrict ind to the case it is valid for, leave 2 and 3 as
  they are today (no regression), which still resolves the reported
  cos(1/x)/(sin(x)+2) case:

(t (return (if (and (eq t (mnqp dn 0))
                    (not (infinityp n1))
                    (not (zerop1 n1)))
               '$ind
               '$und)))

Optional — case 2 can be sharpened safely (a bounded-nonzero denominator cannot
stop an infinite numerator from diverging), while case 3 should stay und (0/dn
is only 0 when dn is bounded away from 0, which mnqp does not establish):

(t (return (cond ((not (eq t (mnqp dn 0))) '$und)
                 ((infinityp n1) '$infinity)   ; ∞ / bounded-nonzero -> infinity
                 ((zerop1 n1)    '$und)         ; 0 / bounded-nonzero not reliably 0
                 (t              '$ind))))

(The same bounded-away-from-zero caveat applies to the ind/ind clause if anyone
decides to harden that too.)