[isPANN]

Summary

The growth domain (src/growth.rs) now supports two shapes that used to fall back to O(?): polynomial exponents and variable bases.

Each growth term is now stored in log space as exp(Σ weight · atom).

• An atom is either a monomial ∏ v^p (ln v)^l, or ln ln v.
• A weight is an exact combination Σ c_b · ln b of symbolic bases. Bases are never rounded through a floating-point logarithm.

Under this scheme, n^2 is the atom ln n with weight 2, 2^(n·m) is the atom n·m with weight ln 2, and k^n is the atom n·ln k with weight 1.

Shape	Before	After
2^(n*m), 2^sqrt(n), 2^(log(n)^2), 2^((n+m)^2)	O(?)	exact
k^n, n^n, num_groups^(2*num_groups)	O(?)	exact
(k+1)^n	O(?)	O(2^n * k^n). The base B = Σ c_i μ_i is bounded by C·M, so B^E ≤ C^E · M^E.
factorial(x)	O(?)	O(x^x) (upper bound)
2^(n-m), 0.5^n	O(?) (decaying)	exact, so 2^n · 2^(-n) cancels to O(1)
2^(2^n), (2^n)^m	O(?)	O(?)

Comparison: to compare two terms, take the log-space difference and determine the sign of each atom's weight. The sign is decided exactly when all summands share a sign, otherwise by a floating-point estimate with a 1e-9 relative margin, and otherwise by exact rational powers. One term dominates when every atom that might be negative is strictly dominated by a positive atom (componentwise in (power, log power)).

Exactness: exponents expand exactly into polynomials over v and ln v. Fractional powers of sums and logs of sums are widened to upper bounds, which are tracked with an exactness flag and only ever combined monotonically.

GrowthFailure variants are renamed to match what can still fail: UnsupportedExponent, UnsupportedVariableBase, UnsupportedFactorial and DecayingWidenedExponent. No code outside growth.rs matched on the old variants.

Verification

• Unit and property tests: the unit tests are rewritten for the new representation, and cases that used to be unknown or unproved are now positive assertions. The randomized generator now also produces nonlinear exponents, variable bases and factorials. Upper-bound soundness, idempotence and dominance soundness all hold, and the negative control still catches its seeded bug.
• SymPy fixture: 11 new growth cases, bringing the total to 25, all agreeing with SymPy 1.14.0. Regenerate with uv run --project scripts python scripts/generate_symbolic_expr_fixture.py.
• One-off SymPy cross-check: I took every comparison the audit tool in Add complexity consistency audit; fix NonTautology, MinimumWeightDecoding and MaxCut<One> complexities #1219 makes, substituted all variables with a single n, and checked against SymPy limits.
  • 914 of 921 Growth results are confirmed upper bounds of their source. There were 0 violations; the other 7 timed out in SymPy on degree-5 to degree-7 exponents.
  • All 710 decided verdicts (674 dominates, 7 dominated, 29 equal) match SymPy.
  • The 153 incomparable verdicts can't be checked against a single-variable limit, as expected.
• Effect on the audit: with this change, the audit's unknown-growth paths fall from 1,409 to 14 and comparable paths rise from about 420 to 1,583. Once both PRs are merged, Add complexity consistency audit; fix NonTautology, MinimumWeightDecoding and MaxCut<One> complexities #1219's audit numbers will be out of date; I'll rerun the audit in a follow-up.
• Gates: cargo test --workspace, fmt and clippy all pass. The only clippy warning is the existing normalized_n warning on main.

Known limitation

A widened shape compares by its bound. For example, factorial(n) compares as equal to n^n even though n! is smaller. Subtraction already worked this way (n - m widens to n + m), so audit findings still need a manual check.

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 96.90608% with 28 lines in your changes missing coverage. Please review.
✅ Project coverage is 97.19%. Comparing base (a10ee83) to head (7348b7e).

Files with missing lines	Patch %	Lines
src/growth.rs	96.02%	25 Missing ⚠️
src/unit_tests/growth.rs	98.91%	3 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #1220      +/-   ##
==========================================
+ Coverage   97.18%   97.19%   +0.01%     
==========================================
  Files        1146     1146              
  Lines      151076   151464     +388     
==========================================
+ Hits       146819   147213     +394     
+ Misses       4257     4251       -6     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[isPANN]

Retargeted onto feat/binary-ilp-to-sat (#1218) so this stacks on the branch that introduces poly_compare / polynomial and the exact/upper-bound certificate vocabulary. Merged that branch in (no rebase); the diff here is again only the four growth files. cargo test --workspace, fmt, and clippy pass on the combined tree.

[GiggleLiu]

Agentic Review Report

PR #1220. Reviewed head 2dc824e3da8f2c8b12103106206a2eed25ef6f2a against own base 0daa9a8265aefe40983beeba0464f8feea8c3316 (feat/binary-ilp-to-sat). Read-only review; no tracked edits, pushes, PR comments or merges.

Verdict

HOLD. The new support for decaying exponentials produces invalid magnitude upper bounds under logarithms. #1221 repairs the simplest case, but an additional cancellation case remains broken even in #1221.

Structural

Reviewed all growth-transfer/comparison implementation changes, revised tests and fixture generator changes against the exact base. New polynomial exponents and symbolic base coefficients preserve substantially more information than the former domain. The distinction between a signed logarithmic upper bound and an upper bound on magnitude is nevertheless not preserved.

Quality

The numerical property tests mostly probe positive growing expressions. A test that drops negative logarithmic terms can pass those checks despite failing on nonnegative monotone totals. The oracle fixtures test positive univariate asymptotics but not a logarithm of a decaying term squared.

Feature test

Compiled and executed a standalone Rust probe using the exact PR growth.rs, the shared expression implementation, and the actual dependency versions, with one build job and debug/incremental output disabled. This avoids a second full library build. Source is in /tmp/problemreductions-growth-probe; output is /tmp/problemreductions-pr-review-20261029/growth-probe.txt. This is an independent counterexample run, not a full exact-head unit suite. git diff --check BASE...HEAD passed.

Findings

1. Critical: dropping negative atoms from a logarithm makes the output cease to be an upper bound. src/growth.rs:1144-1146. Growth::from_expr(Expr::parse("log(exp(-n))^2")) returns O(1) although the expression is exactly n², nonnegative and nondecreasing for n≥2. log(exp(-n)) is −n, whose magnitude cannot be dropped before applying a square. Preserve a magnitude bound or return Unknown for the unsupported operation. The concrete #1221 follow-up fixes this case, so #1220 must not land independently.
2. Critical remaining in the combined stack: log(n*(n+1)-n^2-n+exp(-n))^2 is also exactly n² but returns O(log(n)^2) both here and at #1221. An upper bound on a positive argument gives no bound on the magnitude of its logarithm near zero. This needs a lower bound on the argument or an Unknown result, not just the negative-atom adjustment. Full details and the false Exact consequence are in the #1221 report.

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 1220 --full --comments --reviews. No claim of exhaustive secret scanning. The parent reviewer owns the final head/base recheck before any merge.