Repository navigation
Collects means never larger, and Common declares sixteen more growths - #1195
Merged
Merged
Conversation
#746 tier 2's next item is a declared growth for the rules still at Unknown, because the growth ceiling protects only an inverse pair whose directions are declared. A census of the 152 over the corpus, then Common's 22 read in terms of hole sizes, found that thirteen of them are one shape: a hole matched twice and written once beside one new node -- a + a = 2 * a, a * a = a ^ 2, a + a * b = a * (1 + b), (v - a) * (v + a) = v ^ 2 - a ^ 2 and their relatives. Every one is 1 - |a|: exactly as large at a leaf and smaller everywhere else. That is the commonest collecting shape there is, and the contract could not say it: Collects was "always fewer" and Rearranges "always the same", so the family sat at Unknown as a finding, and the guide listed it among the shapes that look declarable and are not. Nothing consumed the strict reading. RulesUpTo(Rearranges) wants "never grows", the selector-cost proxy test asks for a majority, and the only check that read Collects as strict was the corpus test's own. So the contract is refined rather than the family left out: Collects promises never larger and smaller for some input; Rearranges the same size for every input; Expands larger for every input. The ninety-seven existing declarations -- "exactly -2", "at most -4" -- stay true, the corpus contradicts Collects only on a firing that grew, and the enum, the guide and the corpus test say so in the same words. Under it Common declares sixteen: the thirteen above as Collects, each with its count in the comment; the sign-times-absolute-value cancellation as Collects, since it is -1 - 2|a| outright; and the reciprocal-factor pair as exactly Rearranges and exactly Expands, because IsWholeReciprocal is `entity is Rational(...)` and admits the literal only -- the guide said it also took a written 1 / c and was wrong. The six that stay Unknown say why beside the rule: five attach a condition sized by their own operands, and a + a / b = a * (1 + 1 / b) is 3 - |a|, two nodes larger at a leaf, which the corpus had never fired. Six shapes join the corpus so that every newly declared rule fires on it at least once. Two pins moved and are re-recorded rather than loosened. The safe ceiling now moves two of the five ordinary inputs, not one: (x + 1) * (x - 1) goes to x ^ 2 - 1 ^ 2, and stops there because no safe rule folds a numeric power. And the narrow ceiling brings the difference of squares together, which a test asserted only the widest could -- renamed to what it shows now. The census is 111 collect, 46 rearrange, 31 expand, 136 unjudged; the safe ceiling admits 157 of 324. The relatives in Power and Factorization -- a ^ n * a, a / b / b and theirs -- are next, each on its own count. Part of #746. Full suite 9579 passed, 0 failed -- one of them a throwaway census probe, not committed. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
Measured on a build of master (72676b0) and of this branch, with one throwaway probe run on each. Transformation.CanonicalizationOverGraph(budget), public and at the safe ceiling by default, now collects what the rules collect: (x + y) * (x - y) was (-y + x) * (x + y) and is -y ^ 2 + x ^ 2, the tree x ^ 2 - y ^ 2 reaches; x + x was left as written and is 2 * x; x + x * y is (1 + y) * x. Entity.Canonicalize() runs the rule pass rather than the graph and is unchanged on every input probed. The growth of sixteen rules of RewriteRules.Common moves from Unknown, and what Collects promises moves from "fewer for every input" to "never more, fewer for some". Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
Rafael-SOWNet
added a commit
that referenced
this pull request
Sep 7, 2026
) * Power and Factorization declare the rest of the collecting family #1195 made Collects mean never larger and smaller for some input, and declared the thirteen rules of Common that are a hole matched twice and written once beside one new node. The guide named the relatives in Power and Factorization as next, and this declares them, each on its own count. Power declares nine. Eight are the family -- a ^ n * a, a / a ^ n, a ^ n / a, a ^ n * (a * rest), (c / a) ^ d * a, a / b / b, a / b ^ n / b and a / b / b ^ n -- and every one is 1 - |a| for the repeated hole: a base or a divisor matched twice and written once, against the one node the 1 in the new exponent or the exponent itself costs. The ninth, (c / a) ^ d * a ^ e = c ^ d * a ^ (e - d), was named a relative and is not one: the exponents fold to a leaf and the quotient goes, so it is -1 - |a| outright. Three more stay Unknown and say why beside the rule -- the logarithm of its own base attaches the node's domain condition, and the two radical rules compute through a helper whose answer is a whole times a root or a whole alone. Factorization declares its four: k + k*q, k + k, k - k*q and k*q - k, each 1 - |k|. Seven shapes join the corpus so that each newly declared rule fires on it at least once -- a power beside its own base on either side of a product or a quotient, and a divisor repeated, which the arithmetic grammar builds only with a power of a leaf. No pin moved this time: the safe ceiling still moves two of the five ordinary inputs. The census is 124 collect, 46 rearrange, 31 expand, 123 unjudged; the safe ceiling admits 170 of 324. Part of #746. Full suite 9579 passed, 0 failed -- one of them a throwaway census probe, not committed. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura * Record the answers the thirteen declarations change Measured on a build of master (4b105e6) and of this branch, with one throwaway probe run on each. Over Transformation.CanonicalizationOverGraph(budget), (2 / x) ^ 3 * x was left as (2 * 1 / x) ^ 3 * x and is 8 * x ^ (-2); (2 / x) ^ 3 * x ^ 2 is 8 * 1 / x. The other Power shapes are unchanged for a measured reason -- x ^ 2 * x reaches x ^ (2 + 1) over the graph, no smaller at a leaf, and no safe rule folds the exponent, so the input is kept -- and Factorization's four have Common twins declared in #1195, so a + a * b was already (1 + b) * a. Entity.Canonicalize() is unchanged on every input probed. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura --------- Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
Rafael-SOWNet
added a commit
that referenced
this pull request
Sep 7, 2026
#1195 and #1196 declared the collecting family and left the rest at Unknown, and the guide says a new Unknown should be a finding written beside the rule. This writes the finding beside every one that did not have it: Boolean's five and two of Trigonometric's attach a truth value or a value with a condition whose size nothing bounds; sin a cos a is 2 - |a|, one larger at a leaf, and so the collecting half of the runaway pair was never "never larger"; the six factorial rules answer the product between two offsets, which collects when they are one apart and expands when they are five; the long division, the gcd cancellation, the perfect square, the two rationalisations and the interval paraphrase compute through a helper, and the count each comment gives says where the size comes from -- the perfect square is 5 - |cross term|, the conjugate is seven nodes more as written and measured -2 and +2 on the corpus because the helper folds the denominator it builds, and a bounded interval is 1 + |x| more where a half-line is two fewer. Thirty-one rules sit at Unknown outside the three families the guide settles as families -- the comparison set, Sort and CommonDenominator -- and every one of them carries its reason now. Nothing declared changes: comments and one sentence in the guide. Part of #746. Full suite 9578 passed, 0 failed. Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
This was referenced Sep 7, 2026
Merged
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
#746 tier 2's next item is a declared growth for the rules still at
Unknown— #1194 showed thegrowth ceiling protects only an inverse pair whose directions are declared, so every
Unknownisa pair it cannot see. This is the first set,
Common, and the contract change it needed.What the census found
A probe over the corpus split the 152
Unknownrules into 55 never fired, 28 mixed, 27/21/21looking like
Rearranges/Collects/Expands— and a corpus can only refute, soCommon's 22were then read in hole sizes. Thirteen are one shape: a hole matched twice and written once
beside one new node —
a + a = 2a,a·a = a²,a + a·b = a(1 + b),(v − a)(v + a) = v² − a²and their relatives. Every one is
1 − |a|: exactly as large at a leaf, smaller everywhere else.That is the commonest collecting shape there is, and the contract could not say it:
Collectswas"always fewer",
Rearranges"always the same", so the family sat atUnknownas a finding andWritingARule.mdlisted it among the shapes that look declarable and are not.The decision
Collectsnow promises never larger, and smaller for some input.Rearrangesis the same sizefor every input;
Expandslarger for every input. Nothing consumed the strict reading:RulesUpTo(Rearranges)wants "never grows", the selector-cost test asks for a majority, and the onlycheck that read
Collectsstrictly was the corpus test's own. The 97 existing declarations("exactly −2", "at most −4") stay true; the corpus contradicts
Collectsonly on a firing thatgrew. The enum doc, the guide and the test say it in the same words.
What
CommondeclaresCollectsa-sign-times-a-thing-over-its-own-absolute-value-cancelsCollectsa-reciprocal-rational-factor-is-a-divisionRearrangesIsWholeReciprocalisentity is Rational(...), literal only; the guide said it also took a written1 / c, and was wronga-negated-reciprocal-rational-factor-is-a-negated-divisionExpandsSix stay
Unknownand say why beside the rule: five attach a condition sized by their ownoperands, and
a + a / b = a(1 + 1/b)is3 − |a|— two nodes larger at a leaf, a shape thecorpus had never fired. Six shapes join the corpus so every newly declared rule fires on it.
Pins that moved
Re-recorded, not loosened:
(x + 1)(x − 1) → x² − 1², and stopsthere because no safe rule folds a numeric power;
could, renamed to what it shows now.
Census: 111 collect, 46 rearrange, 31 expand, 136 unjudged; the safe ceiling admits 157 of
324.
Changed answers
Measured on a build of master (
72676b0c) and of this branch, and recorded inBREAKING-CHANGES.md.Transformation.CanonicalizationOverGraph(budget)— public, safe ceiling bydefault — now collects what the sixteen rules collect:
(x + y) * (x - y)was(-y + x) * (x + y)and is
-y ^ 2 + x ^ 2, the treex ^ 2 - y ^ 2reaches;x + xwas left as written and is2 * x;x + x * yis(1 + y) * x.Entity.Canonicalize()runs the rule pass, not the graph,and is unchanged on every input probed. Next: the relatives in
PowerandFactorization(aⁿ·a,a/b/b), each on its own count.Part of #746.
Checks
Full suite 9579 passed, 0 failed, 14 skipped — one of the 9579 a throwaway census probe, not committed. The Transformations area (822) was run twice more on its own.
🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura