[isPANN]

The growth domain previously returned unknown for polynomial exponents and variable bases. It now represents these forms in log space using exact rational coefficients and symbolic bases: examples include 2^(n*m), 2^sqrt(n), k^n, and n^n. This also includes the signed-logarithm and Stirling corrections from #1221.

Comparisons use exact rational powers and certified rational bounds for e. An overlapping interval or exhausted arithmetic budget leaves the order unproved. There is no floating-point sign heuristic. For a supported single-monomial factorial argument, Stirling retains the square-root and exponential-decay factors, so factorial(n) is not treated as equivalent to n^n.

Re-review found cancellation and signed-bound cases that could incorrectly report O(1) or a false exact bound. These are corrected here:

• A logarithm needs a two-sided bound on its positive argument to bound its magnitude; an upper bound alone now produces UnprovedLogarithmBound.
• Nonlinear powers and products cannot combine signed widened bounds without a proved monotonicity condition. Widened bases cannot silently discard negative exponent terms.
• The large-power fallback uses absolute coefficients, preserving a valid bound for expressions such as exp((-n-1)^18).
• Nearly equal rational bases are compared exactly, preventing rounding from discarding the dominant summand.

These guards deliberately return unknown for some expressions previously accepted without a sound proof, including a third nested logarithm. Known growth bounds do not certify monotonicity of the source expression. Audit findings still require manual checks of tightness, substitution validity and reduction cost.

Validation on ef31e35b8, including current main and #1219:

• Independent semantic and policy review passed. Native before/after probes reproduced each reported counterexample and confirmed the corrected result.
• All 44 focused growth tests passed, including randomized upper/lower-bound, idempotence and dominance checks and their negative controls.
• The SymPy oracle contains 29 growth comparisons, exercised by the focused suite. The fixture and its generator are updated together.
• make check: 7,207 tests passed, none failed/ignored/filtered; formatting and all-target/all-feature Clippy passed.
• make paper passed. The integrated audit completed over 2,358 paths: 1,878 consistent, 18 candidate improvements across seven variants, 360 incomparable, 85 unsupported-growth, 17 uncomposable and zero missing-complexity paths. Unsupported growth fell from 1,676 on current main to 85.
• All nine GitHub checks passed on this exact commit. Patch coverage is 97.30270%; project coverage is 97.19%. Both exceed the configured 95% thresholds.

The final PR changes only the growth implementation, its unit tests, and the symbolic-expression fixture plus generator. No dependency or model-construction changes are included.

[codecov]

Codecov Report

❌ Patch coverage is 97.30270% with 27 lines in your changes missing coverage. Please review.
✅ Project coverage is 97.19%. Comparing base (888d714) to head (ef31e35).

Files with missing lines	Patch %	Lines
src/growth.rs	96.31%	24 Missing ⚠️
src/unit_tests/growth.rs	99.14%	3 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #1220      +/-   ##
==========================================
+ Coverage   97.18%   97.19%   +0.01%     
==========================================
  Files        1146     1146              
  Lines      151076   151558     +482     
==========================================
+ Hits       146819   147308     +489     
+ Misses       4257     4250       -7     

☔ 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.

[GiggleLiu]

Agentic Review Report

PASS. Re-review of final commit ef31e35b897b0624efc9be10196fb0c00644509f, including current main and #1219. The original logarithmic-cancellation blockers and the additional soundness failures found during re-review are fixed. This supersedes my earlier request for changes.

Structural and semantic review

The four-file scope is limited to the growth implementation, unit tests, and SymPy fixture plus generator. #1221 is included. Independent read-only review found no remaining material correctness issue.

Native before/after probes reproduced these failures and confirmed the fixes:

• log(n*(n+1)-n^2-n+exp(-n))^2 is exactly n^2, but previously returned O(log(n)^2). The related cancellation sum incorrectly claimed an exact linear bound. Both now return typed unknown results because the positive logarithm argument lacks a proved lower bound.
• Squaring or multiplying widened signed exponent bounds could turn increasing expressions into O(1). Nonlinear signed combinations are now rejected unless their required monotonicity is proved.
• exp((-n-1)^18) previously became O(1). Absolute coefficients now give a valid upper bound beyond the exact expansion cap.
• A negative exponent of a widened base could also become O(1). The implementation no longer discards those negative terms.
• For A=(2^53+1)/2^53 and B=(2^53+2)/2^53, exact arithmetic proves A^3>B, but floating-point logarithms previously reversed that order and pruned the dominant summand. Rational arithmetic and certified intervals for e now determine signs; unresolved intervals remain unknown.

These corrections deliberately trade some precision for sound bounds. Supported exact logarithms and factorial/Stirling cases remain covered. The two changed existing expectations follow the new proved contract: a third nested logarithm is unknown, while a rational base above the certified interval for e has a provable order.

Quality and feature validation

• Independent quality and GitHub policy review: PASS. No unrelated changes, generated build exports, dependencies or debug leftovers.
• All 44 focused growth tests passed in 4.06 seconds, including randomized soundness/idempotence/dominance checks, negative controls and 29 SymPy oracle comparisons.
• make check: 7,207 tests passed, zero failed/ignored/filtered; formatting and all-target/all-feature Clippy passed.
• make paper passed.
• The actual audit completed over 2,358 paths: 1,878 consistent, 18 candidate improvements across seven variants, 360 incomparable, 85 unsupported-growth, 17 uncomposable and zero missing-complexity paths. Candidates still require manual mathematical review.
• The PR description now reflects certified comparison, retained Stirling factors, conservative unknown results and final validation.

All nine GitHub checks passed on this exact commit. Patch coverage is 97.30270% and project coverage is 97.19%, both exceeding the configured 95% thresholds. Rechecked discussion comments, reviews, inline comments, linked discussion, CI and Codecov; no outstanding finding remains in this PR.