[Rafael-SOWNet]

forall n in ZZ+ : sum(f, k, a, n) = g is decided by induction from the least member of the set: the statement at that member, and the statement at n + 1 with the sum unfolded by one term and the sum to n replaced by g — the hypothesis — decided as an identity. Sullivan and Mackey's chapter 5 (Ex 5.2.5, §5.2.4 Try 1, §5.3.4 Try 6, Prob 5.7.1, 5.7.16, Thm 5.3.1's induction from any base).

Three things had to be read on the way, each a route in Quantifiers.Decide:

• A piecewise body. What a closed form comes as — sum(k, k, 1, n) is (n + n^2)/2 provided n >= 0 — and a quantifier did not read one, so forall n in ZZ+ : sum(k, k, 1, n) = n (n + 1)/2 stayed as written. The case whose condition holds at every member is the body; a case whose condition holds at none is passed over.
• An identity over atoms. The polynomial test read the names only, so -(1 - 2^(n + 1)) = 2^(n + 1) - 1 was not an identity. Whatever is not a sum, product, quotient or whole power is one indeterminate; a whole shift in an exponent is a factor (2^(n + 1) is 2 · 2^n, (-1)^(n - 1) is (-1)^n / (-1)), a whole multiple is a power (x^(2 n) is (x^n)^2), and a factorial of a shifted argument is the smaller one times the numbers between ((n + 2)! is (n + 2)(n + 1) n!). A difference of quotients is put over one denominator, and the identity is claimed where the denominator is not zero: decided over the set for the quantified name (n + 1 is never 0 on ZZ+), stated as a condition for a free parameter (sum(1/(a k (k + 1)), k, 1, n) = n/(a (n + 1)) is True provided not a = 0), and not claimed otherwise (forall x in RR : x/(x - 1) - 1/(x - 1) = 1 stays).
• The least member of ZZ+ /\ [2; +oo), so that induction starts there and Closed knows the set is not empty.

input	was	now
forall n in ZZ+ : sum(k, k, 1, n) = n (n + 1) / 2	as written	True
forall n in ZZ+ : sum(1 / (k (k + 1)), k, 1, n) = n / (n + 1)	as written	True, by induction
forall n in ZZ+ : sum(k k!, k, 1, n) = (n + 1)! - 1	as written	True
forall n in ZZ+ : sum((-1)^(k - 1) k^2, k, 1, n) = (-1)^(n - 1) n (n + 1) / 2	as written	True
forall n in ZZ+ : product((2 k - 1) / (2 k), k, 1, n) = (2 n)! / (4^n (n!)^2)	as written	True
forall n in ZZ+ : sum(k k!, k, 1, n) = (n + 1)!	as written	False, at n = 1
forall n in ZZ+ : n! >= 2^(n - 1)	as written	True
forall n in ZZ+ /\ [5; +oo) : 2^n > n^2 (Ex 5.3.2)	as written	True; from 4 it is False
forall n in ZZ+ /\ [7; +oo) : n! > 3^n, [12; +oo) : n! > 5^n (Prob 5.7.8–9), [8; +oo) : 3^n > n^4, [5; +oo) : 4^n > n^4 (Prob 5.7.2), [6; +oo) : n^3 < 3^(n - 1) (§5.3.4 Try 4)	as written	True
forall n in ZZ+ : 7^n + 7 < 7^(n + 1) (Prob 5.7.12)	as written	True; with base 2 it is False at 1
forall n in ZZ+ /\ [4; +oo) : n^2 - 2 n - 1 > 0	as written — no route read the cut set	True

Second commit — inequalities, which the first commit's body called v3-shaped and are not. The step of P(n) >= 0 is read off a multiple of the hypothesis: P(n + 1) = c P(n) + D for a c >= 0 (one, the base of an exponential, n + 1 beside a factorial) and a D >= 0 by a sign calculus over the shape — a positive base to any power, a factorial of a whole number, a polynomial in n decided over the set, sums and products of these, and a sum read per atom product with its collected coefficient ((n + 1) n! - 2 n! is (n - 1) n!). No hypothesis line is needed because the hypothesis enters as c P(n) and never as a rewrite. And the whole numbers from m are ZZ* shifted by m: a statement over ZZ+ /\ [4; +oo) is decided as one about 4 + t over ZZ*, which reaches every route (residues, solving, witness, both inductions) rather than one.

Only the shape with one sum or product alone on a side of an equation is read; a closed form with a case on a free parameter (the geometric sum at q = 1) is left as written, as the doc says, and so is an inequality whose step is not a multiple of the hypothesis plus something of known sign (2^n >= n^2 - 3 n + 3 is true and stays).

InductionTest (75 rows: proved, proved under a condition, refuted at a member, inequalities, left as written, identities over atoms); Syntax.md and BREAKING-CHANGES.md updated. Full suite 12342 passed; the allocation gate passes on all 19 gated benchmarks on each of the two commits (nothing here is on a benchmarked path).

Part of #1409.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

[Happypig375]

Don't just call that book "the reference" because we may have more references later.

[Rafael-SOWNet]

Done in f2dd604: Sullivan and Mackey named at every citation — the two comments of this PR, and the earlier ones in Quantifiers.cs, MatchedRules.cs, ResidueClasses.cs, Entity.Discrete.Classes.cs, Evaluation.Discrete.Classes.cs, five test summaries and five BREAKING-CHANGES entries, so that "the reference" no longer names it anywhere in the repository. The PR body used it too; edited.

[Happypig375]

Is the original link saved anywhere in a reference list of this repository as credits?

[Rafael-SOWNet]

It was not — the link lived only in #1409's body. Now it is: Sources/AngouriMath/Docs/References.md (ce2594b) is the reference list, with Sullivan and Mackey's book and its CMU link first, and the other works the code cites by name — Bronstein, von zur Gathen and Gerhard, Gruntz, Timofeev, Rubi and its test problems, Wester, DLMF, MathWorld, mathlib4, SymPy — each with what it is used for. AGENTS.md's Where things are written down table points at it, and the citation rule says to add a work there when it is first cited.