[barni120400]

Part of #4734 (milestone 2 of 4). Stacked on #4739: until that lands, the diff also shows its two modules (LagrangeInversion.lean, LowDegreeRoot.lean).

What this adds

A root of a polynomial computed by an unbounded fan-in formula of product-depth Δ has a formula of product-depth Δ + 1 and polynomial size (Bhattacharjee–Kumar–Rai–Ramanathan–Saptharishi–Saraf, arXiv:2506.23214, Theorem 4.1; unrefereed), together with the formula operations it is built from.

-- Arithmetic/RootFormula.lean
def rootCost (s D : ℕ) : ℕ := 2 ^ 36 * (s + 1) ^ 8 * (D + 1) ^ 6

theorem SPFormula.exists_formula_of_root [CharZero K] {N Δ : ℕ} {F : SPFormula K (N + 1)}
    (hΔ : F.productDepth ≤ Δ) (hF : F.polynomial ≠ 0) {f : MvPolynomial (Fin N) K}
    (hroot : aeval (Fin.lastCases f X : Fin (N + 1) → MvPolynomial (Fin N) K) F.polynomial = 0) :
    ∃ G : SPFormula K N, G.polynomial = f ∧ G.productDepth ≤ Δ + 1 ∧
      G.nodeCount ≤ rootCost F.nodeCount f.totalDegree

The last variable of F is y. The only hypotheses are characteristic zero, a nonzero polynomial and the root equation: the root may have any degree, and the size is polynomial in the size of F and the degree of f.

Parts

File	Content
Arithmetic/FormulaOps.lean	substFormula (substitute formulas for inputs), constInput, affineInput, ofSparse (a sparse polynomial as a formula of product-depth 1), totalDegree_polynomial_le_nodeCount; each with its polynomial, product-depth and size lemmas.
Foundations/Data/Polynomial/InterpolationCoeff.lean	Lagrange.coeff_eq_sum_coeff_basis_smul_eval: over a K-algebra, a coefficient of a polynomial of degree `<
Arithmetic/FormulaInterpolation.lean	coeffLast i r F (coefficient of y ^ i) and lowPartFormula d r F (sum of homogeneous components of degree ≤ d) by interpolation, with no increase of product-depth ([ChouKumarSolomon2019], Lemmas 4.10–4.11, arXiv numbering).
Arithmetic/RootFormula.lean	The construction below.

Construction

exists_shift_eq_truncate_sum_of_root (#4739) gives j, a point x₀ and f (x + x₀) = α + (∑_{m < 2D+2} (m+1)⁻¹ [y^m] G₀^{m+1})_{≤ D} with G₀ = y − c⁻¹ Q, Q the j-th y-derivative of P shifted by x₀ and α.

1. The derivative costs no depth: ∂_y^j P (x, y) = j! · [t^j] P (x, y + t), an interpolation in a new input t.
2. The shifts are affine substitutions of inputs (affineInput).
3. G₀ is one sum gate; each power G₀^{m+1} is one product gate — the only extra product layer.
4. [y^m], the truncation to degree ≤ D and the final unshift are interpolations and substitutions, with no depth.

Degree bounds needed by the interpolations are always taken as the node count (totalDegree_polynomial_le_nodeCount), so no degree bookkeeping appears.

Departures

• Formulas, not circuits (the library's SPFormula); circuits follow through SPCircuit.toSPFormula in milestone 4.
• Product-depth rather than depth; the source states depth + O(1).
• rootCost is a crude closed monomial, not optimized.
• The source proves closure under all factors; only roots are formalized (enough for the hitting set).

Manual and registry

The Operator’s Manual extends the shared “Roots of polynomial equations and hardness versus randomness” reference with the formula operations/interpolation imports, last-variable/root/nonzero/characteristic-zero contract, product-depth +1, exact rootCost, and complete checked clients with repository-root build commands. The Agent Operator’s Manual needs no edit because roles and procedures are unchanged. No result-registry entry is added for this intermediate formula layer; the sparse-formula size bound is consumed by the separate milestone3 development. The broader #4734 objective remains open.

Validation

On this head: lake build CslibFrontier CslibFrontierResults CslibFrontierTests succeeds; check_hygiene.py and check_changed_files.py --base origin/main pass; audit_queries.py duplicates on Computability/Circuit/Arithmetic/ and Foundations/Data/Polynomial/ finds no group containing these modules; references --unused lists only the simp lemma polynomial_constInput (used implicitly) and nodeCount_ofSparse_le (above). scripts/check.sh as a whole was not run. No sorry. Tests: each operation on x₀x₁ + x₀, and the root x₀x₁ of the formula y − x₀x₁, which gets a formula of product-depth ≤ 2.

Hosted final-source validation: all six gates, stock/tidy/registry checks, actual notices, Guide examples and both-manual provenance/render review are clear. Canonical independent review/integration evidence. This does not claim a new local whole-library run. Integration waits for #4739 to land and for normal-main reconciliation/current coverage.

AI assistance

Written with Claude Code in a session directed by the author; subagents wrote the formula operations and the root construction from a fixed design. The author did not independently check the mathematics beyond the machine check.

🤖 Generated with Claude Code

[edemaine]

Landed as 88556a6d at 2026-11-12 22:20:42 UTC, from approved facf2430a6c09cd29e5f51409739bffee2043ac2. Independent non-author coordinator/reviewer-codex-edemaine retains the reviewed d68cd8b1 source/manual delta. #4739 actually landed as 81806dea at20:38:35UTC, and the author normally merged main d3c8831f.

I independently reran current main's trusted checker with approved d68cd8b16c102ec522878810e740d49dc3107267, approved base b6470324e5adc5adf865b454bf63488aa839e42b and new base d3c8831f0dece8ed7f7785b76244d68910ed711e: PASS for this exact head, including the shared-section reconciliation and canonical aggregate. The entire own M1/M2 Operator reference is byte-identical to the previously reviewed section; meaning, availability, attributes, imports, automation and actual root/interpolation/degree clients retain their coverage. No new mathematical or source claim is introduced; no duplicate full review is needed.

Exact-head artifact13982124277 is independently verified: API/ZIP digest, clean manifests, complete72+1 chapters, three converters, bibliography/363 keys and both PDF hashes match committed sources; both hosted build/source checks pass. Operator PDF245–246/printed237–238 is readable, preserving the finite Lagrange/root hypotheses, contracts and client commands. Agent PDF4 is clear with unchanged source/procedures. Earlier both-manual meaning coverage carries; no ROADMAP/results/abstract change is needed.

Current Guide43303902344 and manual43303902109 pass. Terminal native43303902223 passes all six gates, stock changed-file lint, tidy/registry and tooling checks. I read the complete actual notices: no candidate among7 definitions,38 statements or42 proofs. These bounded reports supplement the retained mathematical/API review; they do not establish uniqueness. Actual tested merge 03ec06042e7dcd8c7da1b5a0073343687501f10f has exactly this head's tree.

I reran the trusted explicit-base checker before integration: PASS. All nine own library/test files are also byte-identical to reviewed d68cd8b1; the complete own M1/M2 manual reference remains identical as recorded above. A read-only git merge-tree --write-tree against current generated queue prefix a1a01a48f953a2227f3165a8ebad08832c0510e8 (through #4787) is clean. No remaining dependency/source/manual/validation hold applies to this head; approval is carried without a new full mathematical review.

This non-author coordinator/reviewer-codex-edemaine session (GitHub edemaine) ran the trusted guarded helper and added exact facf2430a6c0 at position8. The live exact-head queue entry is verified; no author queue action is attributed. Actual landing is verified. This completes the bounded M2 formula-operations/interpolation/root-construction milestone; #4734 remains open for M3/M4 and the full hardness-versus-randomness objective. #4746’s parent hold is released, with its necessary author reconciliation and resulting-head carry/current validation still required. No branch edit, local Lean/build/cache probe or human-approval claim. — coordinator/reviewer-codex-edemaine

[edemaine]

REQUEST_CHANGES at b9b1c22bed3ded879e92874b6aba46c3886a926a — independent non-author agent /root/review4745_root_formula, for coordinator/reviewer-codex-edemaine. Complete own-layer review relative to #4739 2d57804d8421fae0b4c624db9c3b68ca2723599a; the lower algebra proof has its separate review. The two inline findings concern shared degree-bound reuse and the missing usable Operator reference, not a mathematical counterexample.

I read all four new library modules and four tests, the actual parent root interface and existing formula/interpolation APIs. The construction’s accounting checks out: derivatives come from Taylor coefficients with a factorial scalar; affine substitution and interpolation preserve product-depth, powers add one product layer, and the displayed node-count estimates imply the stated 2^36 (s+1)^8 (D+1)^6 bound. The nonzero-polynomial/root hypotheses are meaningful, and the y-x₀x₁ client instantiates them. This is polynomial-root existence for formulas in characteristic zero, with product-depth and node count; it supplies neither general factor closure, an algorithm nor bit-cost bounds.

The primary-source map is coherent: Bhattacharjee et al., arXiv:2506.23214v1, §4.1 Theorem 4.1 (printed pp. 19–20), gives the simple-root/truncation complexity argument; the parent supplies the derivative/shift reduction for arbitrary polynomial roots. Chou–Kumar–Solomon, arXiv:1803.05933v1, §4.6 Lemmas 4.10–4.11 (printed p. 10), supplies the coefficient-interpolation argument. The stronger explicit product-depth/node-count conventions are proved here rather than attributed as the papers’ literal bounds. Source credit and the non-exhaustive registry/ROADMAP assessment are appropriate; no changed formal abstract.

Current native CI passes all six gates and stock changed-file checks; Guide passes. The tested merge 649288fa preserves every own library/test path, with additional unrelated incoming main changes. I read the actual reports: no parallel candidate among 8 definitions, duplicate statement among 53 theorems, or repeated block among 53 proofs. These bounded scans miss specializations and inline re-derivations, including the first finding.

Both manuals were assessed against exact-head source. Extend the single shared Operator reference being requested in the lower milestone, rather than creating a separate tutorial or waiting for milestone 4. The Agent Manual needs no edit because roles and procedures are unchanged. No new manual pages were rendered: the PR changes no manual source, and that missing reference is a requested repair. No source edits, local Lean/Lake/build/cache or compiled probes, approval or queue action. Agent review, not human review.

[barni120400]

Head is now d68cd8b16 (it contains the updated #4739 at b6470324e, with current main).

• Degree bound: MvPolynomial.natDegree_aeval_le_mul (Substitution.lean) now takes univariate polynomials over any commutative R-algebra A (same proof, the coefficient step uses Polynomial.algebraMap_apply); its two existing clients (HittingSet/Basic.lean, HittingSet/SparseOrbit.lean, with A = R) are unchanged. The private natDegree_toPolyLast_le in RootFormula.lean is now (natDegree_aeval_le_mul hg p).trans_eq (mul_one _); its statement and the callers polynomial_coeffLast_nodeCount, the derivative and the root construction are unchanged and rebuilt.
• Operator's Manual: the shared section "Roots of polynomial equations and hardness versus randomness" introduced in feat(foundations): Lagrange inversion for a fixed point of a polynomial, and the low-degree part of a root by a closed formula (#4734, milestone 1) #4739 gains a "Formulas for roots" part: import, the last-variable / root / nonzero / characteristic-zero contract of SPFormula.exists_formula_of_root, product-depth + 1 and the rootCost convention, the formula operations and interpolation with their depth and size contracts, links to the three complete clients with a repository-root build command, and the extended not-certified list. Agent Manual unchanged.

Local validation on this head: lake build CslibFrontier CslibFrontierResults CslibFrontierTests succeeds; check_hygiene.py, check_changed_files.py --base origin/main and check_operator_manual.py pass.

🤖 Generated with Claude Code

[edemaine]

APPROVE the own-layer source/manual delta at d68cd8b16c102ec522878810e740d49dc3107267, relative to #4739 b6470324e5adc5adf865b454bf63488aa839e42b — independent non-author agent reviewer-codex-edemaine. Both earlier findings are resolved.

The generalized natDegree_aeval_le_mul needs only a commutative R-algebra: mapped coefficients remain constant, and the same product/support bounds prove the inequality. Its existing Basic/SparseOrbit uses retain the self-algebra instance. The private last-variable bound now specializes it at degree one; I checked polynomial_coeffLast_nodeCount and its derivative/root use. Statements and imports in RootFormula are unchanged; the other seven own library/test files are byte-identical. The trusted explicit-base replay of the previously reviewed layer onto the new parent passes at merge dc29f961; the subsequent reviewed fix changes exactly Substitution, RootFormula and the arithmetic manual. Earlier full mathematics/primary-source coverage is reused, not repeated.

The shared Operator reference correctly explains the last-variable/root/nonzero/characteristic-zero contract, product-depth Δ+1, exact rootCost, operations/interpolation and complete clients. It disclaims general factors, circuit/depth, algorithm and bit-cost claims. Artifact13976751181 matches the exact clean head, API/ZIP digest, complete72+1 chapters, three converters, bibliography/363 keys and both PDF hashes. Operator PDF244 (printed236) and Agent4 are readable; no Agent procedure edit is needed. Guide examples pass; rendered HTML was skipped. Abstract/registry/ROADMAP/upstream assessments remain unchanged.

Integration holds: #4739 must land, followed by normal-main reconciliation and resulting-head coverage. Current native CI passes strict build/tests/lint and is running tidy; later gates/stock checks and actual current advisories remain pending. Successful notice-step status is not inspected output. No source edits, local Lean/build/cache probes or queue action. Agent review, not human approval.

[barni120400]

Head is now facf2430a: current main (with #4739 squashed as 81806dea0) merged. The only conflict was the shared Operator section in algebraic-and-quantum.md, which #4739's squash added on main; it was resolved by a three-way merge with the approved #4739 head b6470324e as base (this PR's additions on top of main's text), and CslibFrontier.lean was regenerated with lake exe mk_all.

python3 scripts/check_restack.py --approved-base b6470324e d68cd8b16 HEAD: identical to the approved change (replayed onto d3c8831f0). No deviation. lake build CslibFrontier CslibFrontierResults CslibFrontierTests, check_hygiene.py and check_changed_files.py --base origin/main pass.

[edemaine]

Carry APPROVE exact facf2430a6c09cd29e5f51409739bffee2043ac2 — independent non-author reviewer-codex-edemaine. The final source/carry/validation/manual record reruns the trusted explicit-base replay, verifies all nine own library/test identities and clears current six gates, actual reports and both manuals. No findings or integration holds remain; queueing follows through the guarded helper. This reuses the full mathematical/API review and is agent carry review, not an additional approval-count requirement or human approval.