a divides b: divisibility as a statement node by Rafael-SOWNet · Pull Request #1220 · ASC-Community/AngouriMath

Rafael-SOWNet · 2026-09-08T15:16:13Z

Part of #1212 — the first of the nodes agreed there, on the spelling settled in this comment: a | b was found to be a or b already, so the keyword is divides.

What it is

Dividesf(Divisor, Dividend), a statement beside membership — a divides b is the statement that b is a whole multiple of a.

Grammar: divides at the level of in, so the operands are arithmetic and the result is a statement: 2 divides x + 4 is 2 divides (x + 4), 2 divides x and x > 0 is (2 divides x) and (x > 0), not a divides b is not (a divides b). Left-folded and not associative, like in. The parser is regenerated from the grammar with the checked-in ANTLR jar and post-processed as the workflow does.
Printers: the same words back out, so it round-trips; a \mid b in LaTeX; sympy.Eq(sympy.Mod(b, a), 0) in the SymPy export, since SymPy has no divisibility statement and Eq keeps it a statement where == would force a bool.
Code: Entity.Divides(dividend) and MathS.NumberTheory.Divides(divisor, dividend).
Evaluation: decided for integers — 3 divides 12 is True, 0 divides b exactly when b is 0. NaN over a number that is not an integer (3 divides 5/2, i divides 4), the way an inequality is over a non-real number; the intrinsic condition is both operands in ZZ. A symbolic statement is carried.
No simplification rules yet. 1 divides x and x divides x hold for integer x and not for every x; a rule with an assumption is a rule to write under the simplification contract with its soundness stated, not something to slip into the evaluation. They come with the card node's PR or on their own.
Threaded through everything a node has to be in: substitution, sort keys, JSON serialisation, the buildable-node table (WritingARule.md's census moves from 44 to 45), the inverter (declined the way membership is — the solutions are a set), the public-API record (24 new lines).

The cost

divides is a keyword, so a variable of that name no longer parses. Measured on 27ed5b53: "divides" was the variable, "2 divides" was 2 * divides, and "3 divides 12" was 3 * divides ^ 12. All three are a parse error, or the statement, now. In BREAKING-CHANGES.md as a Loud row and a section, with the table measured on both builds.

Not in this PR

CSharpMath's LaTeX reader does not know \mid as a binary relation yet; that is a PR on the other repository, and abs's (| |) is untouched here. card/# is next.

Checks

DividesTest: twelve decided statements, four NaN cases, the symbolic carry, six parse-and-print round trips, three precedence shapes, LaTeX, the two code spellings, SymPy, JSON. The reflection-driven node tests (every node survives every pipeline, buildable at its arity, serialisation, the limit terminating on every node, the public surface) all pass with the new node. Full suite in two chunks: 8397 and 1387 pass.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

Divisibility had no spelling: b mod a = 0 states it for integers, but nothing prints as, parses as, or is a divisibility statement. Dividesf is one, a statement beside membership: `a divides b` in the grammar at the level of `in` (the operands are arithmetic, the result a statement), the same words back out, `a \mid b` in LaTeX, and `sympy.Eq(sympy.Mod(b, a), 0)` in the SymPy export. Entity.Divides and MathS.NumberTheory.Divides build it in code. It is decided for integers -- 0 divides b exactly when b is 0 -- and is NaN over a number that is not an integer, the way an inequality is over a non-real number; a symbolic statement is carried. No simplification rules yet: `1 divides x` and `x divides x` are true for integer x and not for every x, and a rule with an assumption is a rule to write under the contract, not to slip into the evaluation. `divides` is a keyword now, so a variable of that name no longer parses; BREAKING-CHANGES.md has the row, measured on both builds. The parser is regenerated from the grammar, the public-API record has the node's surface, and the buildable-node census in WritingARule.md moves to 45. The first of the nodes agreed on #1212: `#`/`card` next, then the extrema over a set, the distributions, and sequences. Part of #1212. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

A set had no count: a finite set knows its Count in code, and nothing in the language asks for it. Cardf is a function of a set -- card(S) in the grammar beside phi and abs, the same words back out, \operatorname{card}(S) in LaTeX (not |S|, which reads back as a modulus), len(S) in the SymPy export, MathS.Sets.Card in code. Counted where the count is known: a finite set whose elements are numbers, since {x, 1} has two elements unless x is 1 and a set with a symbol in it is not counted until its elements are distinct; and an interval with numeric ends that is one point or none. Left as written for a proper interval and for RR, ZZ and the rest -- an infinite set has a cardinality this library has no number for, and answering +oo would say that [0; 1] and ZZ have the same size -- and for a set builder, which is not enumerated. The expansion that maps a function into a finite set's elements is switched off for this one: card({1, 2}) is a count of the set, not a set of counts. `card(` is a token now, so `card(x)` no longer reads as the product of a variable and a parenthesis; BREAKING-CHANGES.md has the row, measured on both builds. The parser is regenerated from the grammar, the public-API record has the node's surface, and the buildable-node census in WritingARule.md moves to 45. The second of the nodes agreed on #1212, after `divides` (#1220). Part of #1212. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

An expression had no way to name its largest value over a set. max and min took two values; max(f(t), t in S) parsed as the two-value max of f(t) and the membership statement t in S, a category error that stayed unevaluated, and argmax and argmin were not functions at all. Maximumf, Minimumf, Argmaxf, Argminf read the second argument as `variable in set` and bind the variable over the expression and the set. Spelt max(f, t in S), min, argmax, argmin; printed \max_{t in S} f and \operatorname{argmax}_{t in S} f; the two-value max(a, b) is untouched, and a second argument that is not `variable in set` stays the two-value form. The value is answered (ExtremumOverSet) over a finite set of numbers, by evaluating at each and comparing, and over a closed interval with numeric ends for an expression whose extrema are all stationary -- sums, products, whole non-negative powers, sines, cosines, exponentials with a positive base -- by comparing the closed endpoints with the derivative's zeros inside, a periodic family enumerated where it lands. Two guards, because a wrong maximum is worse than none: the smoothness check, so every interior extremum is a zero of the derivative; and the best candidate checked against the expression sampled along the interval, since the solver's list of zeros is not guaranteed complete -- a sample that beats it leaves the question as written. An open endpoint is not a candidate, so max(x, x in [0; 1)) has no maximum; a symbolic set or end, a pole, a kink, and a set with a symbol in it are left as written. argmax and argmin return the set of points. The stationary points are read by Vars, not FreeVariables, so the constants pi, e and i in a root the solver wrote are not miscounted as parameters of a periodic family. Question I.6 of #1212 -- max(sin(t)^3 cos(t), t in [0; pi/2]) is 3 sqrt(3) / 16. BREAKING-CHANGES.md has the rows, measured on both builds. The fourth of the nodes agreed on #1212, after divides (#1220) and card (#1221). Part of #1212. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

A set had no count: a finite set knows its Count in code, and nothing in the language asked for it. Cardf is a function of a set, spelt canonically as the prefix # -- #S, #{ 1, 2, 3 }, #(A \/ B) -- with card( ) accepted on input. # binds as tightly as a function call, so #S + 1 is (#S) + 1 and a set expression takes parentheses. Printed #S, \#S in LaTeX (not |S|, whose bars read back as a modulus), len(S) in the SymPy export, MathS.Sets.Card in code. Counted where the count is known: a finite set whose elements are numbers, since {x, 1} has two elements unless x is 1; and an interval with numeric ends that is one point or none. Left as written for a proper interval and for RR, ZZ and the rest -- an infinite set has a cardinality this library has no number for, and +oo would say [0; 1] and ZZ have the same size -- and for a set builder. The one-argument expansion into a finite set element-wise is off: #{1, 2} is a count of the set, not a set of counts. # and card( ) are grammar now, so card(x) no longer reads as a product and # is no longer free; a bare card is still a variable. The parser is regenerated, and the buildable-node census in WritingARule.md moves to 45. # was chosen as canonical on the review of #1221. The second of the nodes agreed on #1212, after divides (#1220). Part of #1212. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

A set had no count: a finite set knows its Count in code, and nothing in the language asked for it. Cardf is a function of a set, spelt canonically as the prefix # -- #S, #{ 1, 2, 3 }, #(A \/ B) -- with card( ) accepted on input. # binds as tightly as a function call, so \#S in LaTeX (not |S|, whose bars read back as a modulus), len(S) in the SymPy export, MathS.Sets.Card in code. Counted where the count is known: a finite set whose elements are numbers, since {x, 1} has two elements unless x is 1; and an interval with numeric ends that is one point or none. Left as written for a proper interval and for RR, ZZ and the rest -- an infinite set has a cardinality this library has no number for, and +oo would say [0; 1] and ZZ have the same size -- and for a set builder. The one-argument expansion into a finite set element-wise is off: #{1, 2} is a count of the set, not a set of counts. and # is no longer free; a bare card is still a variable. The parser is regenerated, and the buildable-node census in WritingARule.md moves to 45. # was chosen as canonical on the review of #1221. The second of the nodes agreed on #1212, after divides (#1220). Part of #1212. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

An expression had no way to name its largest value over a set. max and min took two values; max(f(t), t in S) parsed as the two-value max of f(t) and the membership statement t in S, a category error that stayed unevaluated, and argmax and argmin were not functions at all. Maximumf, Minimumf, Argmaxf, Argminf read the second argument as `variable in set` and bind the variable over the expression and the set. Spelt max(f, t in S), min, argmax, argmin; printed \max_{t in S} f and \operatorname{argmax}_{t in S} f; the two-value max(a, b) is untouched, and a second argument that is not `variable in set` stays the two-value form. The value is answered (ExtremumOverSet) over a finite set of numbers, by evaluating at each and comparing, and over a closed interval with numeric ends for an expression whose extrema are all stationary -- sums, products, whole non-negative powers, sines, cosines, exponentials with a positive base -- by comparing the closed endpoints with the derivative's zeros inside, a periodic family enumerated where it lands. Two guards, because a wrong maximum is worse than none: the smoothness check, so every interior extremum is a zero of the derivative; and the best candidate checked against the expression sampled along the interval, since the solver's list of zeros is not guaranteed complete -- a sample that beats it leaves the question as written. An open endpoint is not a candidate, so max(x, x in [0; 1)) has no maximum; a symbolic set or end, a pole, a kink, and a set with a symbol in it are left as written. argmax and argmin return the set of points. The stationary points are read by Vars, not FreeVariables, so the constants pi, e and i in a root the solver wrote are not miscounted as parameters of a periodic family. Question I.6 of #1212 -- max(sin(t)^3 cos(t), t in [0; pi/2]) is 3 sqrt(3) / 16. BREAKING-CHANGES.md has the rows, measured on both builds. The fourth of the nodes agreed on #1212, after divides (#1220) and card (#1221). Part of #1212. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

A set had no count: a finite set knows its Count in code, and nothing in the language asked for it. Cardf is a function of a set, spelt canonically as the prefix # -- #S, #{ 1, 2, 3 }, #(A \/ B) -- with card( ) accepted on input. # binds as tightly as a function call, so \#S in LaTeX (not |S|, whose bars read back as a modulus), len(S) in the SymPy export, MathS.Sets.Card in code. Counted where the count is known: a finite set whose elements are numbers, since {x, 1} has two elements unless x is 1; and an interval with numeric ends that is one point or none. Left as written for a proper interval and for RR, ZZ and the rest -- an infinite set has a cardinality this library has no number for, and +oo would say [0; 1] and ZZ have the same size -- and for a set builder. The one-argument expansion into a finite set element-wise is off: #{1, 2} is a count of the set, not a set of counts. and # is no longer free; a bare card is still a variable. The parser is regenerated, and the buildable-node census in WritingARule.md moves to 45. # was chosen as canonical on the review of #1221. The second of the nodes agreed on #1212, after divides (#1220). Part of #1212. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

An expression had no way to name its largest value over a set. max and min took two values; max(f(t), t in S) parsed as the two-value max of f(t) and the membership statement t in S, a category error that stayed unevaluated, and argmax and argmin were not functions at all. Maximumf, Minimumf, Argmaxf, Argminf read the second argument as `variable in set` and bind the variable over the expression and the set. Spelt max(f, t in S), min, argmax, argmin; printed \max_{t in S} f and \operatorname{argmax}_{t in S} f; the two-value max(a, b) is untouched, and a second argument that is not `variable in set` stays the two-value form. The value is answered (ExtremumOverSet) over a finite set of numbers, by evaluating at each and comparing, and over a closed interval with numeric ends for an expression whose extrema are all stationary -- sums, products, whole non-negative powers, sines, cosines, exponentials with a positive base -- by comparing the closed endpoints with the derivative's zeros inside, a periodic family enumerated where it lands. Two guards, because a wrong maximum is worse than none: the smoothness check, so every interior extremum is a zero of the derivative; and the best candidate checked against the expression sampled along the interval, since the solver's list of zeros is not guaranteed complete -- a sample that beats it leaves the question as written. An open endpoint is not a candidate, so max(x, x in [0; 1)) has no maximum; a symbolic set or end, a pole, a kink, and a set with a symbol in it are left as written. argmax and argmin return the set of points. The stationary points are read by Vars, not FreeVariables, so the constants pi, e and i in a root the solver wrote are not miscounted as parameters of a periodic family. Question I.6 of #1212 -- max(sin(t)^3 cos(t), t in [0; pi/2]) is 3 sqrt(3) / 16. BREAKING-CHANGES.md has the rows, measured on both builds. The fourth of the nodes agreed on #1212, after divides (#1220) and card (#1221). Part of #1212. Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

A set had no count: a finite set knows its Count in code, and nothing in the language asked for it. Cardf is a function of a set, spelt canonically as the prefix # -- #S, #{ 1, 2, 3 }, #(A \/ B) -- with card( ) accepted on input. # binds as tightly as a function call, so \#S in LaTeX (not |S|, whose bars read back as a modulus), len(S) in the SymPy export, MathS.Sets.Card in code. Counted where the count is known: a finite set whose elements are numbers, since {x, 1} has two elements unless x is 1; and an interval with numeric ends that is one point or none. Left as written for a proper interval and for RR, ZZ and the rest -- an infinite set has a cardinality this library has no number for, and +oo would say [0; 1] and ZZ have the same size -- and for a set builder. The one-argument expansion into a finite set element-wise is off: #{1, 2} is a count of the set, not a set of counts. and # is no longer free; a bare card is still a variable. The parser is regenerated, and the buildable-node census in WritingARule.md moves to 45. # was chosen as canonical on the review of #1221. The second of the nodes agreed on #1212, after divides (#1220). Part of #1212. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

A set had no count: a finite set knows its Count in code, and nothing in the language asked for it. Cardf is a function of a set, spelt canonically as the prefix # -- #S, #{ 1, 2, 3 }, #(A \/ B) -- with card( ) accepted on input. # binds as tightly as a function call, so \#S in LaTeX (not |S|, whose bars read back as a modulus), len(S) in the SymPy export, MathS.Sets.Card in code. Counted where the count is known: a finite set whose elements are numbers, since {x, 1} has two elements unless x is 1; and an interval with numeric ends that is one point or none. Left as written for a proper interval and for RR, ZZ and the rest -- an infinite set has a cardinality this library has no number for, and +oo would say [0; 1] and ZZ have the same size -- and for a set builder. The one-argument expansion into a finite set element-wise is off: #{1, 2} is a count of the set, not a set of counts. and # is no longer free; a bare card is still a variable. The parser is regenerated, and the buildable-node census in WritingARule.md moves to 45. # was chosen as canonical on the review of #1221. The second of the nodes agreed on #1212, after divides (#1220). Part of #1212. Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

`|` was the one spelling in the grammar that already means something else in mathematics than we read it as: it is divides (a | b), "such that" ({x | P(x)}), "given" (P(A | B)), and the delimiter in |x|. None of those is disjunction, which is written with a vee. So input written by a mathematician was read as an or and answered as one. a | b is now the statement that b is a whole multiple of a -- the same node a divides b has built since #1220, at the same precedence. Defined over the integers and NaN over anything else, the way an inequality is over a non-real number. 0 | 0 is True; 0 | b is otherwise False. This is a silent change: an expression that used | still parses and answers something else. I proposed a two-release migration through a parse error to avoid that; Happypig375's decision on #1212 was to make the change directly, since semantic versioning admits it, and to put the entry early in the breakages list. Both done. "2 | 6" was 2 or 6 is 2 divides 6, True "x > 0 | x < -1" was a disjunction is regrouped, since divisibility binds tighter than > "A | B" on booleans was A or B is NaN or is unaffected and always was the primary spelling -- it is what the library prints, so a round-tripped expression never held a | to begin with. Replacing | with or restores the old reading exactly, everywhere. That is why the cost is small: 7 of 8,525 tests referenced the old reading, five of them boolean-solver inputs written A | B and two written to record this spelling as at risk. The grammar is regenerated and post-processed; the parser is internal again, checked rather than assumed. All five suites green: UnitTests 8514 and 1500, FSharpWrapperUnitTests 134, InteractiveWrapperUnitTests 18, TerminalUnitTests 41. #1212 Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

Rafael-SOWNet mentioned this pull request Sep 8, 2026

card(S): the number of elements of a set, spelt #S #1221

Merged

Rafael-SOWNet force-pushed the divides branch from 4a21932 to adaacd8 Compare September 8, 2026 15:30

Rafael-SOWNet mentioned this pull request Sep 8, 2026

The extremum of an expression over a set, as a binder #1222

Merged

Rafael-SOWNet merged commit f253fa1 into master Sep 8, 2026
34 of 35 checks passed

Rafael-SOWNet deleted the divides branch September 8, 2026 16:15

This was referenced Sep 9, 2026

Math Club orientation week questions #1212

Open

Pending breakages: changes agreed or arguable that cannot ship before a major version #1019

Open

| is divisibility, and was disjunction #1241

Merged

Navigation Menu

Repository navigation

a divides b: divisibility as a statement node - #1220

a divides b: divisibility as a statement node#1220
Rafael-SOWNet merged 1 commit into
masterfrom
divides

Rafael-SOWNet commented Sep 8, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

Rafael-SOWNet commented Sep 8, 2026

What it is

The cost

Not in this PR

Checks

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant