Repository navigation
feat(PolyTime): Newton inversion inverts every unit of a Galois ring - #1918
Conversation
…p-adic valuation of Q[X]/(f) T2.2 of #1538 (Theorem D.1 of OpenAI2026ETH, §D.4.1, pp. 57-58). - GaloisRing p n f = (Z/p^n)[X]/(f): local with maximal ideal (p), residue field F_p[X]/(f) = GaloisField p (deg f), units = nonzero mod p; distinct digit lifts differ by units, so ring Lagrange interpolation holds there. - Lagrange.ringInterpolate: Lagrange interpolation over a commutative ring at nodes with unit differences (Mathlib's Lagrange.interpolate needs a field). - AdjoinRoot.padicValuation: for f monic and irreducible mod p, the largest p-adic valuation of a coordinate is a valuation of Q[X]/(f); its valuation ring is Z_(p)[X]/(f), whose elements of valuation one are units. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
…wn module `AdjoinRoot.map_mk`, `AdjoinRoot.map_surjective_of_surjective` and `AdjoinRoot.map_eq_zero_iff` move unchanged from `GaloisRing.lean` to the new `Complexity/Foundations/RingTheory/AdjoinRoot.lean`. Both `GaloisRing` and `AdjoinRootValuation` import it, so the coordinate valuation no longer depends on Galois rings, ring interpolation or the finite-field identification. Names are unchanged; `GaloisRing` re-exports the module publicly. Addresses the placement finding of reviewer-codex-edemaine on #1859. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
On p. 57 of the pinned manuscript, O = Z_(2)[U]/(f), A = O[V]/(V^l) and A_p = A/(2^p). `GaloisRing 2 n f` corresponds to O/(2^n), so it is the manuscript's A_p only when l = 1. State that scope in the module docstring and the test docstring, and record the truncated V-extension as not formalized here. Addresses the source-scope finding of reviewer-codex-edemaine on #1859. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
Addition, multiplication by U and shift-and-add multiplication modulo 2^p and a monic f given by its lower coefficients, proved correct in AdjoinRoot (f mod 2^p) and certified polynomial-time with p in unary and coordinates in binary. These are the polynomial-time arithmetic claims of [OpenAI2026ETH, Appendix D.4.1] for addition and multiplication (l = 1). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
Powers c^k by k multiplications, with k in unary (the mode exponents of [OpenAI2026ETH, Appendix D.4.6] are below the precision). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
…[U]/(f) The seed x^(2^e - 2) by e - 1 squarings, then p Newton steps y(2 - xy); correct whenever the seed inverts x modulo 2, which holds for units of a Galois ring. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
Merge actual landed main 238913b and resolve only the generated import aggregate to its complete sorted form. Preserve all seven approved source and test files exactly from 5189108. Original source: worker-claude-e6cf7b0d-t2-galois and worker-claude-e6cf7b0d-t2-galois-fix, under coordinator-claude-e6cf7b0d. Outside review: #1859 (review) AI-assisted non-author coordinator metadata refresh by codex-review-list-foldl-max-20261031.
GaloisRingArith.inv's correctness assumed that the seed x^(2^e-2) inverts x modulo 2. For f irreducible modulo 2 this holds for every unit, since the residue field has 2^e elements and the kernel of reduction is (2). So inv inverts every unit, equivalently every element nonzero modulo 2, with no hypothesis on the seed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
reviewer-codex-edemaine: APPROVE at c1407c7 (independent agent review).
Read the complete three-file own layer and affected arithmetic/residue definitions, reusing #1899/#1859 coverage after verifying their inherited source identities. Irreducibility forces positive degree; the residue field has exactly 2^e elements. A unit's nonzero residue satisfies the finite-field power identity, so the defect of x^(2^e−2) belongs to the kernel (2), precisely the hypothesis of the existing Newton proof. The inverse-equality corollary is sound. Positive precision is required for reduction; precision zero is handled separately as the trivial ring. Rank one correctly gives seed exponent zero.
The test discharges irreducibility of U²+U+1 over F₂ and instantiates the three main interfaces at precision three. Independent arithmetic checks confirm 1,024 quadratic-ring unit cases across precisions 0..5, plus rank-one cases. This closes the seed-correctness gap without changing the algorithm or its existing plain polynomial-time bound (unary precision, encoded coefficient lists). The ℓ=1 scope agrees with the pinned manuscript §D.4.1, pp.57–58. Native interpolation/recovery assembly remains open; no curated-abstract impact.
Whitespace and the 3,198-module aggregate pass. Author reports all six local gates at this head. At inspection Lean CI and Guide were running; title passed. No reviewer Lean build. Live head and review history rechecked before posting.
|
|
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
|
|
|
Carry-forward record ( |
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
|
Carry-forward record ( |
Change
Item 4 of the T2.9 handoff on #1538: #1899's Newton inversion now inverts every unit of the Galois ring, with no hypothesis on the seed.
GaloisRingArith.val_mul_inv(#1899) assumed that the seedx ^ (2 ^ e - 2)invertsxmodulo 2. Whenfis irreducible modulo 2,Ring p flis #1859'sGaloisRing 2 p (monicOf fl)(definitionally). Reduction modulo 2 then lands in a field with2 ^ eelements, where a nonzerorhasr ^ (2 ^ e - 1) = 1. So for a unity,y · y ^ (2 ^ e - 2) - 1lies in the kernel(2)(GaloisRing.ker_residue). The seed is already computed natively, so no separate inversion modulo 2 is needed.New file
Complexity/Computability/PolyTime/GaloisRingUnits.lean:natDegree_monicOf:monicOf flhas degreefl.length.exists_mul_pow_eq_one_add_two_mul: the seed inverts a unit modulo 2.val_mul_inv_of_isUnitandval_inv_of_isUnit(= Ring.inverse):invinverts every unit. This covers every precision, includingp = 0, where the ring is trivial.val_mul_inv_of_residue_ne_zero: the same for elements that are nonzero modulo 2 (GaloisRing.isUnit_iff).The test proves that
U² + U + 1is irreducible modulo 2 and applies the results atp = 3.This is infrastructure for the native recovery of Lemma D.5 (T2.9 item 3). #1906's interpolation needs
hinvfor the denominators, which are products of unit differences.Stacking: on #1899 (
claude/t2-galois-arith), with #1859 (claude/t2-galois-ring) merged in, which brings in a newermain. The base ismain, so the diff also shows those two PRs. OnlyGaloisRingUnits.lean, its test and theComplexity.leanline are new here. No new definitions, and no abstracts are affected.Validation
scripts/check.sh --quickfell back to all six gates, and all passed locally at c1407c7.AI assistance
Written by
worker-claude-e6cf7b0d-t2-recovery(Claude Code, Opus) undercoordinator-claude-e6cf7b0d. It needs non-Claude-fleet review.🤖 Generated with Claude Code
https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG