[isPANN]

Stacked on #1220.

What

Growth::relation() now says whether a computed Big-O form is tight:

• ParameterRelation::Exact: the expression is Θ(growth), so the growth is also a lower bound.
• ParameterRelation::UpperBound: some step widened the expression.
• None: the growth is unknown.

This reuses the ParameterRelation type that reduction overheads already use.

The rules for exactness:

• Variables and positive constants are exact.
• Products and constant powers are exact when their operands are.
• A sum is exact when all its summands are exact. It is also exact when every widened summand, including a subtracted one, is strictly dominated by an exact summand. So n - 1 and n^2 - n log n are exact, while n - m and n*m - n^2 are upper bounds.
• An exponential is exact when its exponent expands exactly and its base is bounded exactly. A single-monomial base with any coefficient, such as (2n)^n, now counts as exact.
• A logarithm is exact when its argument is exact and grows without bound. A ln ln v that was widened to ln v is not exact.
• factorial(x) of an exact single monomial now uses Stirling's formula, x! ≍ x^(x+1/2) e^(-x), and is exact. Before, it was bounded by x^x. Any other factorial argument still widens to x^x and is reported as an upper bound.

Why

The complexity consistency audit (#1219) can now report a violation as proven only when the registered side's growth is exact. With an upper-bound growth, "registered ≻ derived" might only show that our bound is loose. Stirling also makes factorial(n) strictly smaller than n^n, which the comparison could not separate before.

Visible change: factorial complexities now display as, for example, O(n^(0.5 + n) * exp(-1 * n)) instead of O(n^n).

Tests

• test_growth_relation: 15 exact cases, 13 upper-bound cases, and one unknown case.
• test_growth_factorial_stirling: equalities and strict orderings around n!.
• A new lower-bound property harness (8,000 random expressions) checks numerically that every growth reported exact satisfies growth ≤ C·e. Its negative control seeds a bug: an Add that returns the product of its summands and calls it exact. The harness catches it. The harness uses variable-only leaves, because constant leaves can keep an exact term hidden past the finite window it evaluates.
• SymPy oracle: four Stirling cases added (ratio_limit √(2π) and 2√π for the equivalences), and all of them agree.
• cargo test --workspace passes. Clippy reports only the existing normalized_n warning.

🤖 Generated with Claude Code

[isPANN]

Agentic Review Report

PR #1221: Growth::relation() (Exact / UpperBound), Stirling factorial, lower-bound property harness, SymPy oracle cases. Generic (non-model, non-rule) change to src/growth.rs. I reviewed it against feat/growth-polynomial-exponents.

Structural

• Scope is limited to src/growth.rs, src/unit_tests/growth.rs, the SymPy fixture, and its generator script. There are no generated exports and no unrelated edits.
• cargo test --lib growth passes 38/38.

Soundness probing (Exact must mean Θ, i.e. also a lower bound)

I probed about 40 expressions through Growth::from_expr in a scratch binary. Most paths hold up:

• Variables, positive constants, mul, and pow_const (including mixed antichains such as (n+m)^2).
• Exponentials with an exact base and exponent, for example (2n)^n, (n/2)^n and n^(m-1).
• Stirling on single monomials: factorial(n/2), factorial(sqrt(n)) and factorial(n*m).
• Logs of non-growing arguments, such as log(1 + exp(-n)), which are correctly UpperBound.
• Subtractions with equal-order cancellation, such as sqrt(n^2+1) - n, n*m - n*(m-1) and 2^n - 2^(n-1)*2, which are correctly UpperBound.
• Zero constants: n*log(1) is UpperBound.

The covers rule in add is the exception (see Critical below).

Quality

• The lower-bound harness never exercises the new covers rule or the constant-sign rule (see Important below).

Feature test

pred show FlowShopScheduling now prints Best Known Complexity: O(num_jobs^(0.5 + num_jobs) * exp(-1 * num_jobs)). This matches the PR description.

Findings

Critical

1. add's covers rule assumes the widened summand's growth bounds its magnitude. log of a decaying argument breaks that assumption (src/growth.rs:1145-1161 together with log_term at src/growth.rs:1241).

   • log_term drops negative-weight atoms. For log(exp(-n)) = -n the growth is therefore O(1). That is a valid signed upper bound but not a bound on |value|.

   • covers then treats the -n summand as o(n) and reports Exact.

   • Reproduced, all within the trust contract (the totals are nonnegative and monotone):

     Expression	True value	Reported
     n + log(exp(-n)) + 1	1	O(n), Exact
     n^2 + n*log(exp(-n))	0	O(n^2), Exact
     log(n) + log(exp(-log(n)))	0	O(log n), Exact
     n^(1/2) + log(exp(-(n^(1/2))))	0	O(n^0.5), Exact

   • The same root cause also breaks the plain upper bound once a power is applied. This predates the PR but is now additionally labelled Exact:

     Expression	True value	Reported
     log(exp(-n))^2	n^2	O(1)
     n + log(exp(-n))^2	n + n^2	O(n), Exact

   • Suggested root-cause fix: give log of a term that has a non-positive atom a magnitude bound. Emit the growth of every atom regardless of weight sign, or return Unknown when no positive atom dominates.

   • Alternatively, covers can require the low summand's growth to be a magnitude bound. For example, carry a "signed-only" flag that log_growth sets whenever log_is_exact fails, and have pow_const and covers reject it.

   • Add the four expressions in the first table to test_growth_relation as non-Exact.

Important

2. The lower-bound property harness cannot reach the new exactness logic (src/unit_tests/growth.rs:854 STABLE_VARIABLE_LEAVES, generator at :864).
   • Lower mode uses variable-only leaves with positive coefficients and only growing 2^x/exp(x). It never produces:
     • subtraction or negative constants (the covers path and exact_if(sign == Greater));
     • decaying exponentials;
     • logs of non-growing arguments;
     • factorials.
   • So every Exact sum it checks comes from both_exact, and finding 1 is invisible to it.
   • The negative control (an Add that returns a product) only shows that the harness catches gross errors.
   • Suggested fix: add a lower-mode generator branch that emits a - c*b with b structurally smaller than a, plus exp(-linear) and log(<decaying>) leaves. Add a negative control that drops covers' strict-dominance check, so it reports Exact whenever the high side is exact.

Minor

3. The doc comment overstates what covers licenses (src/growth.rs:1142-1144, "a widened summand, even a subtracted one, is then o of the exact part").

   • This holds only if the summand's growth bounds its absolute value. State that invariant explicitly, or enforce it as in finding 1.
   • Likewise, the module doc at lines 33-36 says "every known growth is an upper bound". It is a signed upper bound, and the distinction matters as soon as negative subterms are admitted.

4. The Stirling output is less readable in user-facing Big-O (pred show, docs): O(n^(0.5 + n) * exp(-1 * n)).

   • It is correct, but consider whether the display layer should keep the simpler upper form or a factorial(n) spelling.
   • Note also that test_every_registered_complexity_uses_the_shared_analysis now compares only terms_of, so a relation change on round-trip goes unchecked. That is acceptable, but it is worth a comment.

[isPANN]

Review follow-up (0b41f6b):

1. Critical: fixed at the root. log_term now gives every atom's growth whatever its sign, so growths bound magnitudes. log(exp(-n)) is O(n) and log(exp(-n))^2 is O(n^2). All four reported cases are now UpperBound. n^2 + log(exp(-n)) stays Exact because the negative part is dominated. These are pinned in test_growth_log_of_decaying_term_bounds_magnitude.
2. Important: partly addressed. The generator now builds v*v - v (this reaches the dominance rule in add) and log(exp(-linear)). A harness control for the undominated decaying-log case can't fail numerically: exp(-x) underflows f64 past x ≈ 745, and a linear gap fits inside the slack of 16 over the size window. So that case is covered by the targeted unit test above, and a code comment notes this.
3. Minor: fixed. The doc comments now say "magnitude upper bound".
4. Minor: test fixed, display left as is. The registered round-trip test now also asserts that an exact normal form stays exact. The Stirling display (n^(0.5 + n) * exp(-1 * n)) is left unchanged here. It is correct, and prettier rendering would be an Expr display change.

[GiggleLiu]

Agentic Review Report

PR #1221. Reviewed head 0b41f6beba60c06db704ecf4200017f789ab8b1f against own base 2dc824e3da8f2c8b12103106206a2eed25ef6f2a (feat/growth-polynomial-exponents). Read-only review; no tracked edits, pushes, PR comments or merges.

Verdict

HOLD. The existing follow-up fixes the originally reported negative-log example, but a new exactness counterexample still returns a false Θ bound at the reviewed head.

Structural

Reviewed the four-file own-base diff and full growth-transfer logic. Stirling is sound for the supported exact positive single-monomial factorial arguments. Exactness propagation through ordinary positive sums/products and exact exponential polynomial expansions is reasonable. The covers rule is sound only if every widened summand has a true magnitude bound; log_growth still violates that invariant when its argument's growth is inexact.

Quality

The revised tests cover direct log(exp(-n)) and subtraction of smaller terms, but not algebraically cancelling polynomial terms inside a logarithm. Numeric f64 sampling is particularly weak here because the positive residual can disappear through catastrophic cancellation before the exponential underflows. Use symbolic simplification/limits or targeted identities for this class, not larger random sample counts.

Feature test

An independent standalone Rust probe compiled the exact #1220 and #1221 growth sources side by side using the shared expression code. Output is in /tmp/problemreductions-pr-review-20261029/growth-probe.txt; source in /tmp/problemreductions-growth-probe. The existing regression log(exp(-n))^2 now correctly produces O(n^2), UpperBound. Stirling for factorial(n) produces O(n^(0.5+n)*exp(-n)), Exact. The two counterexamples below remain broken. git diff --check BASE...HEAD passed. No full exact-head library/CLI suite was independently rerun.

Findings

1. Critical: log_growth on a widened argument produces a false magnitude bound, then add upgrades it to Exact. src/growth.rs:1208-1213 and :1151-1159.

Let A(n)=n(n+1)−n²−n+exp(−n). Algebraically A(n)=exp(−n)>0 for all n. The production Expr does not expand the cancelling product, so Growth first widens A to O(n²). Applying log_growth yields O(log n), which is not a magnitude upper bound for log A=−n.

Actual independent outputs:

Input	True value	Reported at 0b41f6b
log(n*(n+1) - n^2 - n + exp(-n))^2	n²	O(log(n)^2), UpperBound
n + log(n*(n+1) - n^2 - n + exp(-n)) + 1	1	O(n), Exact

Both complete expressions meet the stated nonnegative/nondecreasing trust contract. This is not merely a loose bound or unsupported domain. The second result falsely promises a lower bound and can make downstream comparisons assert a strict separation that does not exist.

Fix the operation at its source: a magnitude upper bound for A alone is insufficient to bound |log A|. Carry a proved positive lower bound/away-from-zero property, use appropriate exact symbolic reduction, or return Unknown where neither is available. Do not let covers consume a signed-only or otherwise uncertified logarithmic estimate. Add these identities as targeted regression tests. Merely marking the logarithm UpperBound is insufficient because the first result is not an upper bound at all.

GitHub PR policy audit

GATE: PASS. This is the harm-signals gate only; it does not override the correctness verdict above.

• harm.secrets (security.no-secrets): OK. No obvious credential/private-key/token addition detected in the own-base diff.
• harm.dangerous-files (git.harm-signals): OK. No conflict markers, unexplained archives or local scratch/config artifacts detected.
• harm.generated-artifacts (code.generated-artifacts): OK. No blacklisted generated graph/schema/example exports or build targets added. Test oracle fixtures are intentional test inputs; small browser contracts/fonts are intentional source assets.
• harm.cache (code.generated-cache): OK. No cache directories added.
• harm.debug-leftovers (code.debug-leftovers): OK. No debugger, breakpoint or temporary debug print addition detected. Browser performance marks are deliberate verification instrumentation.
• pr.description-quality (github.pr-description-quality): OK. Purpose, changes, validation and limitations are described.
• pr.traceable (github.prs-traceable): OK. The PR states its purpose and own stack context.

Policy evidence: own-base name/status, numstat and patch inspection; added-line secret/conflict/debug scan; git diff --check; gh-axi pr view 1221 --full --comments --reviews. No claim of exhaustive secret scanning. The parent reviewer owns the final head/base recheck before any merge.