Skip to content

A logarithm of a perfect power takes the exponent out, so related logarithms collect - #1217

Merged
Rafael-SOWNet merged 1 commit into
masterfrom
log-perfect-power
Sep 8, 2026
Merged

Rafael-SOWNet merged 1 commit into
masterfrom
log-perfect-power

Conversation

@Rafael-SOWNet

Copy link
Copy Markdown
Member

Part of #1212 — the first of the small items in my comment there: question I.5's presentation.

What changes

ln(4/3) + ln(16/9) / 2 was left as written; it is 2 ln(4/3), which the metric then prefers as the single literal ln(16/9). The rule that reads log(a, b^n) as n log(a, b) could not see a rational literal that is a power without saying so.

A new rule in Power, in both spellings: a logarithm of a positive rational literal that is a perfect power is offered as the exponent times the logarithm of the root — ln(16/9) as 2 ln(4/3), ln(64) as 6 ln(2), ln(1/8) as 3 ln(1/2). The largest exponent that fits is read exactly, on numerators and denominators within 64 bits (TreeAnalyzer.TryPerfectPower). A positive root only: -8 is (-2)^3, but ln(-8) is ln 8 + iπ where 3 ln(-2) is 3 ln 2 + 3iπ, so a negative root is refused rather than assumed. Sound, Expands (+2 nodes), so it is offered to the metric and never taken on its own.

input was is
integral((2x^2+x+1)/(x^3+x^2+x+1), x, 3/4, 4/3) — question I.5 ln(4/3) + ln(16/9) / 2 ln(16/9)
ln(4/3) + ln(16/9) / 2 ln(4/3) + ln(16/9) / 2 2 * ln(4/3)
ln(8) - 3 ln(2), log(3, 81) / 4 0, 1 the same
ln(16/9), ln(64) alone the literal the literal — the longer form loses

Checks

LogarithmOfAPerfectPowerTest: five perfect powers read, five non-powers refused (including -8, 1, 0), the sheet's integral, three collections, two literals left alone. The rule census moves by one (WritingARule.md, the guide tests, ReversibleRuleTest, the Saturation remark). Full suite in two chunks: 9,715 passed, 0 failed (Calculus 1,355, the rest 8,360).

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

…arithms collect

ln(4/3) + ln(16/9) / 2 was left as written; it is 2 ln(4/3), which the
metric then prefers as the single literal ln(16/9). The rule that reads
log(a, b^n) as n log(a, b) could not see a rational literal that is a
power without saying so, and 16/9 is (4/3)^2.

A logarithm of a positive rational literal that is a perfect power is
offered as the exponent times the logarithm of the root -- the largest
exponent that fits, read exactly on numerators and denominators that fit
64 bits. A positive root only: -8 is (-2)^3, but ln(-8) is ln 8 + i pi
where 3 ln(-2) is 3 ln 2 + 3 i pi, so nothing is assumed by refusing it.
The form is longer on its own and the metric keeps the literal; it is
what lets two logarithms of related literals collect. Both spellings of
the rule, Sound and Expands; the census moves by one.

Question I.5 of #1212's presentation: the integral answers ln(16/9).
BREAKING-CHANGES.md has the rows, measured on both builds.

Part of #1212.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
@Rafael-SOWNet
Rafael-SOWNet merged commit 27ed5b5 into master Sep 8, 2026
31 checks passed
@Rafael-SOWNet
Rafael-SOWNet deleted the log-perfect-power branch September 8, 2026 12:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant