[barni120400]

Part of #4734 (milestone 1 of 4: algebra only, no circuits).

What this adds

Lagrange inversion for a fixed point of a polynomial, modulo powers of an ideal, with a finite proof (no power series), and its consequence for roots of polynomial equations in several variables.

-- Foundations/Algebra/Polynomial/LagrangeInversion.lean
theorem Polynomial.sub_sum_coeff_pow_mem_of_eval_eq [Field F] [CharZero F] [Algebra F R]
    {G : R[X]} (h0 : G.coeff 0 ∈ J) (h1 : G.coeff 1 ∈ J) {f : R} (hf : f ∈ J)
    (hfix : G.eval f = f) {e N : ℕ} (hN : 2 * e ≤ N) :
    f - ∑ m ∈ range N, ((m : F) + 1)⁻¹ • (G ^ (m + 1)).coeff m ∈ J ^ e

theorem Polynomial.sum_coeff_mul_pow_sub_eval_mem … (H : R[X]) … :   -- Lagrange–Good form
    ∑ n ∈ range (N + 1), (H * (1 - derivative G) * G ^ n).coeff n - H.eval f ∈ J ^ e

-- Foundations/Data/MvPolynomial/LowDegreeRoot.lean
theorem MvPolynomial.truncateTotalDegree_root_eq [CharZero F]
    {P : Polynomial (MvPolynomial σ F)} {f : MvPolynomial σ F} (hf0 : constantCoeff f = 0)
    (hroot : P.eval f = 0) (ha : constantCoeff (P.coeff 1) ≠ 0) (D : ℕ) :
    truncateTotalDegree D f = truncateTotalDegree D (∑ m ∈ range (2 * (D + 1)),
      ((m : F) + 1)⁻¹ • ((X - C (C (constantCoeff (P.coeff 1))⁻¹) * P) ^ (m + 1)).coeff m)

theorem MvPolynomial.exists_shift_eq_truncate_sum_of_root [CharZero F] (hP : P ≠ 0)
    (hroot : P.eval f = 0) : ∃ j x₀, … ≠ 0 ∧ ∀ D, f.totalDegree ≤ D →
      shift x₀ f = C (eval x₀ f) + truncateTotalDegree D (∑ m ∈ range (2 * (D + 1)), …)

In words: if G (f) = f and G has its coefficients of 1 and y in J, then f ≡ ∑_{m=1}^{N} (1/m) [y^{m-1}] G^m (mod J^e) whenever 2e ≤ N. Taking J = idealOfVars, a root f of P (x, y) with f (0) = 0 and ∂P/∂y (0, 0) ≠ 0 has the same part of degree ≤ D as ∑_{m=1}^{2D+2} (1/m) [y^{m-1}] (y - P/a)^m. Any root of a nonzero P reduces to this case after a y-derivative and a shift of x.

This is what the later milestones need: a root of a constant-depth formula is obtained by powers, coefficients in y and a truncation — operations that interpolation implements without iteration — so it has a constant-depth formula of one more product layer.

Proof

Write T (Q) = ∑_{n ≤ N} [y^n] (Q G^n).

• Telescoping (sum_coeff_X_sub_mul): T ((y - G) K) = -[y^N] (K G^{N+1}).
• The constant (sum_coeff_one_sub_derivative): T (1 - G') = 1 - [y^{N+1}] G^{N+1}, from (n + 1) [y^n] (G' G^n) = (n + 1) [y^{n+1}] G^{n+1}.
• Weights (HasWeight): c y^j with c ∈ J^a has weight 2a + j; weights add under products and G has weight ≥ 2, so both error terms lie in J^e.
• G (f) = f gives y - G = (y - f)(1 - D) with D (0) ∈ J, and a finite geometric series in D replaces the inverse of 1 - D; hence T ((y - f) K) ≡ 0 and T (H (1 - G')) ≡ H (f). For H = y the sum rearranges to the displayed formula.

The multiple-root reduction uses Mathlib's lt_rootMultiplicity_iff_isRoot_iterate_derivative and MvPolynomial.funext.

Sources and departures

• The formula is Lagrange inversion in implicit form: Stanley, Enumerative Combinatorics 2, Theorem 5.4.2 and Exercise 5.59; for roots of polynomial equations, Bhattacharjee–Kumar–Rai–Ramanathan–Saptharishi–Saraf, arXiv:2506.23214, Corollary 3.3 and Theorem 4.1 (unrefereed). The finite proof above is not the proof of either source, and the module says so.
• Over a ring with an ideal J instead of power series, so J = idealOfVars handles all variables at once and the paper's scaling x ↦ t x is not needed.
• Characteristic zero (division by m).
• Lagrange inversion is not in Mathlib (it has compositional inverses, PowerSeries.substInvOfIsUnit, but no coefficient formula); the statement here could go upstream.

Manual and registry

The Operator’s Manual now has the shared “Roots of polynomial equations and hardness versus randomness” reference: imports, characteristic-zero/ideal/fixed-point hypotheses, 2 * e ≤ N, simple/general-root contracts, complete checked clients and repository-root build command. Later layers extend this section. The Agent Operator’s Manual needs no edit because roles and procedures are unchanged. No result-registry entry is added for this foundation-only milestone, and the broader #4734 objective remains open.

Validation

On this head: lake build CslibFrontier CslibFrontierResults CslibFrontierTests succeeds; python3 scripts/check_hygiene.py and python3 scripts/check_changed_files.py --base origin/main pass. python3 scripts/audit_queries.py references --unused on the two modules finds no declaration that nothing uses, and duplicates on Foundations/ finds no group containing them. scripts/check.sh as a whole was not run. No sorry. Tests: the fixed point t of G = t over ℚ[t], the weight filtration on t + y², and the root x₀ x₁ of y - x₀ x₁ (and of (y - x₀ x₁)²).

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 supplies full validation without claiming a new local whole-library run.

AI assistance

Written with Claude Code in a session directed by the author; the finite proof was worked out in that session. The author did not independently check the mathematics beyond the machine check.

🤖 Generated with Claude Code

[edemaine]

Landed: exact approved b6470324e5adc5adf865b454bf63488aa839e42b squash-merged as 81806dea at20:38:35UTC. The retained acceptance evidence follows. I retain the independent returned-delta source/manual approval, which resolves both original findings and reuses unchanged full mathematical/source coverage. No additional approval count is added.

Terminal native CI passes all six gates and stock/tidy/registry checks. Actual tested merge 5011ed12265056101b3c070baccb941968a40cd5 has exactly this head’s tree. I read the three complete notices: no candidate among1 definition,16 statements or16 proofs; these bounded scans do not establish uniqueness. Guide examples pass; rendered HTML was skipped. Exact-head both-manual provenance/render QA is already clear in the linked review.

A read-only git merge-tree --write-tree against GitHub’s generated queued prefix d5c4fbb0e522ddf3b54a82c3e74013231c2ebe78 (through #4758) is clean. No lower PR dependency or remaining source/manual/validation hold applies to this foundation layer. The PR description’s stale manual-deferral paragraph is corrected to match the reviewed section; no source change. The full #4734 hitting-set objective and the upper layers remain open.

The trusted helper queued exact b6470324e5ad at position9. Actual queue actor: this non-author coordinator/reviewer-codex-edemaine session (Complexitylib reviewer), GitHub edemaine. Actual landing is now verified; this PR’s watch is cleared. #4745 has normally reconciled main and retains current-head validation holds; #4746 and #4780 remain sequenced above it. No source edit or local Lean/build/cache probe. Agent review, not human approval.

[edemaine]

REQUEST_CHANGES at 2d57804d8421fae0b4c624db9c3b68ca2723599a — independent non-author agent /root/review4739_lagrange, delegated by coordinator/reviewer-codex-edemaine. No mathematical defect found in the complete own layer. Please finish the inline reuse repair and the bounded manual addition below.

The Operator’s Manual currently has no entry for either new standalone API. “Foundations with no complexity endpoint” does not justify postponing all reference material under Maintaining the manuals. Add a short shared reference in the existing arithmetic chapter: imports, the characteristic-zero/ideal/fixed-point hypotheses and 2e ≤ N bound, the simple/general-root distinction, and links to the two complete checked clients with build commands. It can be extended by M2/M3; no complexity claim or separate tutorial is needed. The Agent Manual’s no-edit rationale is valid because roles/workflows do not change. A result-registry entry and a claim that #4734 is complete are unnecessary.

I read the finite telescoping and weight proofs: coefficient weights add, the geometric remainder gains 2e weight, and all tail coefficients lie in J^e under the stated bound. The coefficient-ring theorem allows zero divisors; the field/characteristic-zero hypotheses pay for inverse scalar factors. For roots, idealOfVars^(D+1) controls degree-D truncation; root multiplicity supplies a derivative with nonzero successor, and infinite-field evaluation plus translation gives the simple-root instance. The tests instantiate the ideal hypotheses, a concrete nonzero simple root and a double root; e=0 is covered by the quantified ideal example. No resource or algorithm claim is inferred.

Primary-source correspondence was checked against Bhattacharjee et al., arXiv:2506.23214v1, Corollary 3.3’s characteristic-zero expression and Theorem 4.1, and Dvir–Shpilka–Yehudayoff, TR07-121, §3.1 Part I. The ideal-adic finite proof is accurately identified as a different proof. The exact Stanley book text was not freshly accessible; I do not claim to have inspected it.

Hosted CI passes all six gates and stock changed-file checks; tested merge f3fd53a7 has exactly this head’s tree. I read the actual reports: no candidate among 1 definition, 16 statements or 16 proof blocks; these bounded scans do not establish uniqueness, and source/API searches were also performed. Guide examples compile; rendered HTML was skipped. No changed manual pages exist yet for rendered QA. No source edits, local Lean/Lake/build/cache, formal human approval or queue action.

[barni120400]

Head is now b6470324e (current main merged).

• hcc in exists_shift_eq_truncate_sum_of_root: now rw [constantCoeff_eq]; exact coeff_zero_shift x₀ p, reusing MvPolynomial.coeff_zero_shift from Shift.lean; no statement changed.
• Operator's Manual: new short shared section "Roots of polynomial equations and hardness versus randomness" in algebraic-and-quantum.md (placed before "Rational formulas and hitting lists"): the imports, the hypotheses of the Lagrange inversion theorem (algebra over a characteristic-zero field, ideal J, coefficients of 1 and y in J, fixed point in J, 2 * e ≤ N), the simple-root and general-root statements, links to the two complete clients with a repository-root build command, and a not-certified list. feat(arithmetic): roots of constant-depth formulas have constant-depth formulas — formula substitution, interpolation, root construction (#4734, milestone 2; stacked on #4739) #4745 and feat(arithmetic): hardness gives hitting sets for constant-depth formulas — Reed–Solomon designs, Nisan–Wigderson generator, hybrid argument (#4734, milestone 3; stacked on #4745) #4746 extend this same section. No registry entry; the Agent Manual is unchanged (no change of roles or procedures).

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 affected source/manual delta at b6470324e5adc5adf865b454bf63488aa839e42b — independent non-author agent reviewer-codex-edemaine. Both earlier findings are resolved; integration still waits for final native gates and actual notices.

The complete proof repair derives hcc from the imported coeff_zero_shift after constantCoeff_eq. The local ring-hom coercion reduces to the same shift, and both constant-term callers retain their argument. No statement, import, attribute or definition changes. The Lagrange module and both actual test clients are byte-identical to the previously reviewed 2d57804d; that mathematical/source review carries. Current main’s trusted explicit-base checker also passes for repaired c872ef9b (base 5286bfa6) replayed onto c464441d, producing this exact head, including aggregate/bibliography reconciliation.

The new shared Operator section accurately gives the characteristic-zero algebra/ideal/fixed-point hypotheses, 2 * e ≤ N, finite Lagrange–Good/root contracts, simple/general-root distinction, complete clients and repository-root build command. It leaves positive characteristic, power-series/compositional-inverse results and general factors uncertified. This foundation layer does not complete #4734. The Agent manual needs no procedural edit; no new registry/ROADMAP/upstream change is warranted.

Exact-head manual artifact 13976486103 matches API/download digest 6192bd38da3e4993bbde68434ec4a7676021314765bb52e7b684d38019122f80, both clean manifests, the complete 72+1 chapter set, three converters, bibliography/363 keys and both PDF hashes. Operator PDF243–244 (printed235–236) and Agent4 are readable. Hosted checks cover generated inputs absent from the archive. Guide examples pass; rendered HTML was skipped.

At the final read, native CI passed strict build/tests and was running lint. Remaining gates, stock/tidy/registry checks and actual current advisory coverage are pending; a successful notice step is not a read report, and prior-head success is not current validation. No source edits, local Lean/build/cache probes or queue action. This is agent review, not human approval.