From 020354c74b45fec13266164f9347c9aa906cdba4 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Tue, 27 Oct 2026 21:20:30 +0000 Subject: [PATCH] The power reduction of a squared cosine is proved, as the squared sine's is sin(x)^2 - (1 - cos(2x))/2 simplified to 0 and cos(x)^2 - (1 + cos(2x))/2 did not. Its candidates reach -1/2 + cos(x)^2 / 2 + sin(x)^2 / 2, which is 0, and stopped there: a rational coefficient is written as a divisor, so k sin(x)^2 + k cos(x)^2 = k (#2175) does not see cos(x)^2 / 2, and the two squares are not siblings for the switch's rules either. squared-sine-and-cosine-over-one-divisor-sum-to-its-reciprocal gathers sin(x)^2 / d and cos(x)^2 / d of one argument and one divisor and writes 1 / d: Sound, since both sides are defined exactly where d is not 0, two-sided, Collects, and with no backwards reading, as it forgets the angle. Two different divisors are left alone. The census moves by one in WritingARule.md, Saturation's remark and the tests that pin them. On 2.6.0 and on this branch, Simplify: cos(x)^2 - (1 + cos(2*x))/2 unchanged -> 0 Chain against master 856b3cb6b: verdicts identical, 0 moves; performance gate passed on all 19; unit suite 17,169 passed, 0 failed. RuleCheck passes, Confluence and CanonCheck match their baselines, SimpSweep 10,463/10,463. Part of https://github.com/asc-community/AngouriMath/issues/2142 Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura --- BREAKING-CHANGES.md | 12 ++++++ .../Transformations/Matching/MatchedRules.cs | 26 +++++++++++ .../Core/Transformations/Saturation.cs | 4 +- .../Docs/Contributing/WritingARule.md | 16 +++---- .../UnitTests/Common/PowerReductionTest.cs | 43 +++++++++++++++++++ .../Transformations/ReversibleRuleTest.cs | 7 +-- .../Transformations/RuleAuthoringGuideTest.cs | 13 +++--- .../Core/Transformations/RuleMetadataTest.cs | 4 +- .../Transformations/StepAsASentenceTest.cs | 2 +- 9 files changed, 105 insertions(+), 22 deletions(-) create mode 100644 Sources/Tests/UnitTests/Common/PowerReductionTest.cs diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index a838613d5..5d1080d35 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -231,6 +231,18 @@ is `null`. A row with symbols in it is tried at one value of them, and where it | `MathS.Equations("ln(x) + ln(y)", "x - y").Solve("x", "y")` | `[[-1, -1], [1, 1]]` | `[[1, 1]]`: `ln(-1) + ln(-1)` is `2 pi i` | | `MathS.Equations("sqrt(y) - x", "y - a").Solve("x", "y")` | `[[sqrt(a), (sqrt(a)) ^ 2], [-sqrt(a), (-sqrt(a)) ^ 2]]` | `null`: the second row is a solution only at `a = 0` | +### The power reduction of a squared cosine is proved, as the squared sine's is + +**Silent: an identity reaches its value.** `cos(x)^2 = (1 + cos(2x))/2` was not proved while +`sin(x)^2 = (1 - cos(2x))/2` was: the difference reached `-1/2 + cos(x)^2 / 2 + sin(x)^2 / 2`, where the squares +carry their coefficient as a divisor, and no rule found a squared sine and cosine over one divisor among other terms. +`sin(x)^2 / d + cos(x)^2 / d = 1 / d` is now found wherever the two sit in a sum +([#2142](https://github.com/asc-community/AngouriMath/issues/2142)). + +| Input | Was (2.6.0) | Now | +|---|---|---| +| `"cos(x)^2 - (1 + cos(2*x))/2".Simplify()` | `cos(x) ^ 2 - (1 + cos(2 * x)) / 2` | `0` | + ### `conj`, `arg` and `det` are refused by name **Not silent: these now throw `UnrecognizedFunctionParseException` where they parsed.** A name the parser does not diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs index 5eaf6b069..f6821fe78 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs @@ -372,6 +372,32 @@ internal static class MatchedRules Soundness.Sound, description: "k sin(x)^2 + k cos(x)^2 = k"), + // ... + sin(x)^2 / d + ... + cos(x)^2 / d + ... -> 1 / d + (everything else) + // A rational coefficient is written as a divisor, cos(x)^2 / 2 and not 1/2 cos(x)^2, + // so the rule above does not see it. The power reduction cos(x)^2 = (1 + cos(2x))/2 + // reached -1/2 + cos(x)^2 / 2 + sin(x)^2 / 2 and stopped, while its sine twin was 0. + // Sound: both sides are defined exactly where d is not 0. + // https://github.com/asc-community/AngouriMath/issues/2142 + new MatchedRule( + "squared-sine-and-cosine-over-one-divisor-sum-to-its-reciprocal", + MatchPattern.Gathered( + "rest", + MatchPattern.Node( + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Any("x")), + MatchPattern.Exact(Integer.Create(2))), + MatchPattern.Any("d")), + MatchPattern.Node( + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Any("x")), + MatchPattern.Exact(Integer.Create(2))), + MatchPattern.Any("d"))), + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Exact(Integer.Create(1)), MatchPattern.Any("d")), + MatchPattern.Any("rest")), + Soundness.Sound, + description: "sin(x)^2 / d + cos(x)^2 / d = 1 / d"), + // ... + 1 + ... + tan(x)^2 + ... -> sec(x)^2 + (everything else), and the same with // the cotangent. The identity divided through by cos^2 and by sin^2 is also in // TrigonometricRules, but for two siblings only, so the sort decided again: secant diff --git a/Sources/AngouriMath/Core/Transformations/Saturation.cs b/Sources/AngouriMath/Core/Transformations/Saturation.cs index 19042aa38..efd6b52be 100644 --- a/Sources/AngouriMath/Core/Transformations/Saturation.cs +++ b/Sources/AngouriMath/Core/Transformations/Saturation.cs @@ -43,8 +43,8 @@ internal static class Saturation /// one, and that is a measurement rather than a preference. It reads like the value a /// ceiling should refuse — it means the rule's growth was not judged, because its /// replacement is code rather than a written pattern, so admitting it accepts a rewrite - /// nobody measured. But it is where the rules are: of the 340 rules in - /// , 129 collect, 49 rearrange, 36 expand and 126 are + /// nobody measured. But it is where the rules are: of the 341 rules in + /// , 130 collect, 49 rearrange, 36 expand and 126 are /// unjudged. A ceiling that refuses the fourth value still refuses 37% of the library, /// and what is left could not do much when this was written — over six expression pairs /// equal only through a larger intermediate form, the diff --git a/Sources/AngouriMath/Docs/Contributing/WritingARule.md b/Sources/AngouriMath/Docs/Contributing/WritingARule.md index 87701090d..1d7001430 100644 --- a/Sources/AngouriMath/Docs/Contributing/WritingARule.md +++ b/Sources/AngouriMath/Docs/Contributing/WritingARule.md @@ -18,7 +18,7 @@ effect". This is how to supply those seven things. ## Where a rule goes `Core/Transformations/Matching/MatchedRules.cs`, as a value in a `MatchedRuleSet`. **33** sets and -**340** rules live there today. +**341** rules live there today. The `switch` statements in `Functions/Simplification/Patterns` are the older form. **All thirty registered sets now run as data and describe what they run**; none executes its `switch` any more. @@ -64,7 +64,7 @@ in a name and putting the identity in brackets after it: 2. Tangent is sine over cosine (tan(a) = sin(a) / cos(a)), so tan(x) becomes sin(x) / cos(x). ``` -So the name has to be a clause that survives being read that way. **All 311 distinct rule names are, +So the name has to be a clause that survives being read that way. **All 312 distinct rule names are, and `StepAsASentenceTest` holds them to it** — a name with a capital, a bracket or an underscore fails that test rather than degrading the prose quietly. @@ -91,7 +91,7 @@ debugged for an afternoon. | `Left.ToString()` | `Divf(var a, Divf(var b, var c))` — how the matcher spells it | Write the identity with `=`, not `->`: it is an equality, and the arrow belongs to the direction the -rule happens to be applied in. **337** rules carry one today; a new rule should. +rule happens to be applied in. **338** rules carry one today; a new rule should. ## The pattern language @@ -123,14 +123,14 @@ matches and silently builds nothing. `BuildableNodeTypesTest` is the list. ## Replacement: a pattern, or code -**41** of the 340 rules have a pattern on both sides. The rest build their answer in code, and both +**42** of the 341 rules have a pattern on both sides. The rest build their answer in code, and both are legitimate — but the choice costs two things, so make it deliberately. A pattern replacement gets: -- **a direction.** `MatchedRule.Reversed` is the rule read the other way, and **36** of the 41 - two-sided rules have one. The other five forget something: `sin²+cos² = 1` and - `k sin² + k cos² = k` forget the angle, +- **a direction.** `MatchedRule.Reversed` is the rule read the other way, and **36** of the 42 + two-sided rules have one. The other six forget something: `sin²+cos² = 1`, + `k sin² + k cos² = k` and `sin²/d + cos²/d = 1/d` forget the angle, `{ x : x in S } = S` forgets the name the set builder bound, and `c ^ log(c, a) = a` and `c ^ (k * log(c, a)) = a ^ k` for a constant `c` forget which constant, so none has anything to read back. @@ -227,7 +227,7 @@ limit, against nothing for handing the node over. | `SoundUnderAssumptions` | holds given something the rule does not check | | `Heuristic` | usually right | -**189** of the 340 rules are `Sound` and **151** are conditional. Every one of the thirty registered +**190** of the 341 rules are `Sound` and **151** are conditional. Every one of the thirty registered *sets* declares `SoundUnderAssumptions`, because a set's tier is the **minimum** over its rules — so the set grain says nothing and the rule grain says everything. A derivation reports the rule's tier (`RewriteStep.Soundness`), which is why getting it right matters beyond the label. diff --git a/Sources/Tests/UnitTests/Common/PowerReductionTest.cs b/Sources/Tests/UnitTests/Common/PowerReductionTest.cs new file mode 100644 index 000000000..0caee85af --- /dev/null +++ b/Sources/Tests/UnitTests/Common/PowerReductionTest.cs @@ -0,0 +1,43 @@ +// +// Copyright (c) 2019-2026 Angouri. +// AngouriMath is licensed under MIT. +// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md. +// Website: https://am.angouri.org. +// + +using AngouriMath; +using AngouriMath.Extensions; +using Xunit; +using static AngouriMath.Entity.Number; + +namespace AngouriMath.Tests.Common +{ + /// + /// cos(x)^2 = (1 + cos(2x))/2 was not proved while its sine twin was: the difference + /// reached -1/2 + cos(x)^2 / 2 + sin(x)^2 / 2, and a squared sine and cosine over one + /// divisor was found by no rule. + /// #2142 + /// + [Trait("Area", "Common")] + public sealed class PowerReductionTest + { + [Theory] + [InlineData("cos(x)^2 - (1 + cos(2*x))/2", "0")] + [InlineData("sin(x)^2 - (1 - cos(2*x))/2", "0")] + [InlineData("sin(x)^2/3 + cos(x)^2/3", "1/3")] + [InlineData("a + sin(t)^2/b + cos(t)^2/b", "a + 1/b")] + public void TheIdentityHolds(string input, string expected) + { + // a + 1/b less itself is 0 provided b is not 0, and the condition is not what is compared. + var difference = (input.Simplify() - expected.ToEntity()).Simplify(); + while (difference is AngouriMath.Entity.Providedf(var inner, _)) + difference = inner; + Assert.Equal(Integer.Zero, difference); + } + + /// Two different divisors are not the identity. + [Fact] + public void DifferentDivisorsAreLeft() + => Assert.Contains("sin", "sin(x)^2/2 + cos(x)^2/3".Simplify().Stringize()); + } +} diff --git a/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs b/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs index dbe63ddc1..00b1d01bb 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs @@ -370,6 +370,7 @@ public void EveryDataRuleIsClassifiedAsWritten() "one-less-a-squared-sine-is-a-squared-cosine: ReplacementIsCode", "sine-of-a-whole-multiple-of-an-angle: ReplacementIsCode", "squared-sine-and-cosine-of-one-argument-sum-to-one: ReplacementDropsHoles", + "squared-sine-and-cosine-over-one-divisor-sum-to-its-reciprocal: ReplacementDropsHoles", "squared-sine-and-cosine-with-one-coefficient-sum-to-it: ReplacementDropsHoles", "the-arctangent-of-one-over-root-three: ReplacementIsCode", "the-arctangent-of-root-three: ReplacementIsCode", @@ -437,13 +438,13 @@ public void AReversedRuleSaysWhatAnExpressionCameFrom() [Fact] public void ARuleThatForgetsAHoleHasNoBackwardsReading() { - // Both Pythagorean rules of the set, with a coefficient and without, drop the - // argument. The set's other two, 1 + tan^2 = sec^2 and its cotangent twin, keep it, + // The three Pythagorean rules of the set, with a coefficient, a divisor or neither, + // drop the argument. The set's other two, 1 + tan^2 = sec^2 and its cotangent twin, keep it, // and they are the only ones its reversal holds. var pythagoras = MatchedRules.PythagoreanIdentity.Rules .Where(rule => rule.Name.StartsWith("squared-sine-and-cosine", StringComparison.Ordinal)) .ToList(); - Assert.Equal(2, pythagoras.Count); + Assert.Equal(3, pythagoras.Count); foreach (var rule in pythagoras) { Assert.Equal(RuleReversal.ReplacementDropsHoles, rule.Reversal); diff --git a/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs index 878affbea..f04226356 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs @@ -43,7 +43,7 @@ private static void Stated(int stated, int measured, string claim) public void WhereARuleGoes() { Stated(33, MatchedRules.All.Count, "the number of rule sets written as data"); - Stated(340, MatchedRules.All.Sum(set => set.Rules.Count), "the number of rules written as data"); + Stated(341, MatchedRules.All.Sum(set => set.Rules.Count), "the number of rules written as data"); Stated(30, RewriteRules.All.Count, "the number of registered sets"); // Two families register under one name and run a data set under another -- // CommonDenominator over MatchedRules.CommonDenominator(level), CanonicalOrder over @@ -64,7 +64,7 @@ public void TheNameIsASentence() { var names = MatchedRules.All.SelectMany(set => set.Rules) .Select(rule => rule.Name).Distinct(StringComparer.Ordinal).ToList(); - Stated(311, names.Count, "the number of distinct rule names"); + Stated(312, names.Count, "the number of distinct rule names"); var words = names.Select(name => name.Split('-').Length).ToList(); Stated(4, words.Min(), "the shortest rule name in words"); @@ -73,7 +73,7 @@ public void TheNameIsASentence() [Fact] public void TheIdentityIsNotTheName() - => Stated(337, + => Stated(338, MatchedRules.All.SelectMany(set => set.Rules).Count(rule => rule.Description is not null), "how many rules carry an identity"); @@ -85,7 +85,7 @@ public void ThePatternLanguage() public void ReplacementAPatternOrCode() { var rules = MatchedRules.All.SelectMany(set => set.Rules).ToList(); - Stated(41, rules.Count(rule => rule.Right is not null), + Stated(42, rules.Count(rule => rule.Right is not null), "how many rules have a pattern on both sides"); Stated(36, rules.Count(rule => rule.Reversed is not null), "how many two-sided rules have a direction"); @@ -97,7 +97,7 @@ public void ReplacementAPatternOrCode() // rearrange, 9 expand and 270 unjudged", measured before the growth declarations // went in. The argument survived; the arithmetic did not. A number a remark reasons // from belongs somewhere that fails when it moves. - Stated(129, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Collects), + Stated(130, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Collects), "how many rules are declared Collects"); Stated(49, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Rearranges), "how many rules are declared Rearranges"); @@ -121,6 +121,7 @@ public void ReplacementAPatternOrCode() "a-constant-raised-to-a-logarithm-of-itself-is-the-antilogarithm", "a-constant-raised-to-a-multiple-of-a-logarithm-of-itself-is-a-power-of-the-antilogarithm", "squared-sine-and-cosine-of-one-argument-sum-to-one", + "squared-sine-and-cosine-over-one-divisor-sum-to-its-reciprocal", "squared-sine-and-cosine-with-one-coefficient-sum-to-it", }, oneWay); @@ -133,7 +134,7 @@ public void ReplacementAPatternOrCode() public void SoundnessIsPerRule() { var rules = MatchedRules.All.SelectMany(set => set.Rules).ToList(); - Stated(189, rules.Count(rule => rule.Soundness is Soundness.Sound), + Stated(190, rules.Count(rule => rule.Soundness is Soundness.Sound), "how many rules are Sound"); Stated(151, rules.Count(rule => rule.Soundness is Soundness.SoundUnderAssumptions), "how many rules are SoundUnderAssumptions"); diff --git a/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs index e8e7f9267..b6f6cd8a3 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs @@ -88,8 +88,8 @@ public void AddressableGrowthIsTheRulesOwnAnswer() public void SoundnessIsFinerPerRuleThanPerSet() { var rules = MatchedRules.All.SelectMany(set => set.Rules).ToList(); - Assert.Equal(340, rules.Count); - Assert.Equal(189,rules.Count(rule => rule.Soundness is Soundness.Sound)); + Assert.Equal(341, rules.Count); + Assert.Equal(190,rules.Count(rule => rule.Soundness is Soundness.Sound)); Assert.Equal(151, rules.Count(rule => rule.Soundness is Soundness.SoundUnderAssumptions)); // And every set still reports the weakest of them, which is what makes the set grain diff --git a/Sources/Tests/UnitTests/Core/Transformations/StepAsASentenceTest.cs b/Sources/Tests/UnitTests/Core/Transformations/StepAsASentenceTest.cs index e71c6ef15..1b04223cc 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/StepAsASentenceTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/StepAsASentenceTest.cs @@ -59,7 +59,7 @@ public void EveryRuleWrittenAsDataIsNamedInProse() { var names = MatchedRules.All.SelectMany(set => set.Rules).Select(rule => rule.Name) .Distinct(StringComparer.Ordinal).ToList(); - Assert.Equal(311, names.Count); + Assert.Equal(312, names.Count); Assert.All(names, name => Assert.True(Explanation.IsProse(name), $"'{name}' is a rule name that does not read as a phrase in English"));