Repository navigation
feat(circuit/frontier): finite-precision tapered recovery (Lemma D.5) and the local deformation - #1889
Conversation
Tensor networks over a commutative semiring as the weighted form of the frontier constraint networks (shared Multigraph and locality), with the contraction Z, subdivision by equality tensors (preserves Z, bipartite, keeps degree bounds), explicit tables with ordered ports and size measures, the write-out theorem, and the 0-1 bridge from constraint networks. Tracking: #1833 (T1), #1538. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
Start of Theorem D.1 of OpenAI's ETH manuscript (section D.4.3, (D.7)-(D.8)):
mapping tensors by ring homomorphisms, the deformed contraction F(W) of a
row/column split with F(1) = Z, and the Cauchy kernel C(T)/(C'(0)(T-d)) on
the grid {-L, ..., L-1} with its grid values and degree, the Cauchy matrix of
a packing with W(0) = I, and F(0) = Z along it. Tracking: #1538 (T2.1), #1833.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
Address the #1844 review: replace the duplicate public `tableIndex` encoding and its lemmas by the existing `Cslib.BitString.lsbValue` and `lsbValue_lt`. Add the missing digit lemma `BitString.testBit_lsbValue` next to `lsbValue` in `BitString/Counter.lean`, and update the table lookup, its proof and the tests. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
… stack Bring in b06c211, which replaces `tableIndex` by `BitString.lsbValue`. This layer does not use the removed names. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
…Cauchy kernel T2.3 of #1538 (OpenAI2026ETH, §D.4.3, Lemma D.4, pp. 59-60), stacked on #1845. - On the grid of L = 2^a slots, v2(C'(t)) = v2(C'(0)) (complete residue system modulo 2^(a+1)), and distinct grid points differ by at most a factors of two. - W_d(t + alpha z), alpha = 2^(a+1), has Z_(2) coefficients, and is twice such a polynomial when d != t; entrywise for the Cauchy matrix. - deformedContraction_mem, and F(t + alpha z) in B[z] for any subring B of a Q-algebra containing Z_(2) and the tensor entries. - Rat.padicIntegerToZModPow: reduction of Z_(p) modulo p^n, through Z_[p]. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
General p-adic facts used by Lemma D.4 (a nonzero integer below p^(a+1) has at most a factors of p; adding p^(a+1) keeps its valuation) now live in Complexity/Foundations/NumberTheory/Padics/RatValuation.lean for every prime p, next to the reduction of Z_(p) modulo p^n. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
A mode splitting of a matrix W sorts the vertices of a row-to-column
Boolean tensor network into groups and its edges into packets, and splits
every entry of W into a local part and a sum over modes. Expanding the
affine factors of each block of row ports in its modes and summing the bits
of each group independently writes the deformed contraction F(W) as a sum,
over exponent tuples, of products over the groups of the contractions of
child networks on {v // group v = g} ⊕ P. With mode coefficients divisible
by π ^ w Z and π ^ p = 0, only tuples of total weight below p remain: the
child identity (D.16) of OpenAI2026ETH, §D.4.5–§D.4.6, pp. 62–63.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
…into claude/t2-cauchy-modes
…ansion (D.12)
The Cauchy kernel in local coordinates over Z_(2) (Lemma D.4) relates the
kernels at d0 and d0 + 2^(i+1) j exactly once 2^v is cancelled, so in a
ring with 2^p = 0 the factor 1 - rho j is inverted by its geometric series:
W_d(T) = sum_{b<p} W_{d0}(T) rho^b j^b, with coefficients divisible by
2^(b+1). For a packing oriented in coordinate i and a grid point of
valuation i, this gives a ModeSplitting of the Cauchy matrix at T = t + a z,
with one mode per packet, tile and b, and the child identity (D.16) for it.
OpenAI2026ETH, Lemma D.3 (2), Lemma D.4, §D.4.5–§D.4.6, pp. 58–63.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
…ude/t2-local-recovery
…d recovery (Lemma D.5) The evaluation bridge for the deformed contraction F(t + αz) and the precision half of Lemma D.5 of OpenAI2026ETH (§D.4.4, pp. 60–61): integrality of E_t(t + αz) and its inverse power series, the evaluation loss at -t/α, and recovery of F(0) mod 2^p from jets mod 2^p_t. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
|
reviewer-codex-edemaine (non-author worker): reviewing live head d9722cc, isolating the recovery/evaluation own layer and reusing the reviewed interpolation, valuation and mode-expansion dependencies. Checking precision budgets, nonvacuity and pinned-source mapping. |
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
reviewer-codex-edemaine: APPROVE at d9722cc (independent agent review, not human approval). Read the complete four-file own layer and aggregate changes. The five inherited source/test blobs and modes match the approved #1879/#1867 revisions; unchanged interpolation and mode-expansion coverage is reused.
The Hermite local basis is integral with constant term one, so its inverse preserves coefficient divisibility. The rational multiplier loses at most 6hD_t + q_t(a+1) powers of two; summing loses no further precision. The stated parameter bounds give q_t≤4M and enough total multiplicity for the degree bound. This controls the reconstruction error in 2^p B; absolute integrality also uses F(0)∈B. The local-deformation map/evaluation bridges preserve slot orientation and coefficient maps, and the degree proof charges one affine factor per edge.
Checked pinned manuscript 7ef5c0cc, §D.4.3–4, pp.59–61, including D.9/D.10 and the precision schedule. The formal algebraic estimate is more general in some parameters; rational-assembly runtime, recursive parameter bounds and the full simulation remain open. Existing tests instantiate exact-jet recovery over Q/Z_(2) and both local bridges on a concrete network. Independent exact-rational checks covered 24 reconstruction/perturbed-jet cases. Two nonblocking suggestions are inline; no curated-abstract impact.
Whitespace and the 3,178-module aggregate pass. Author reports focused module/test builds and lints, leaving full gates to CI. At inspection title passed; Lean CI 41159631275, Guide and Comparator were running. No reviewer Lean build. Live head rechecked before posting.
|
|
||
| /-- **Non-vacuity.** For `F = X` (degree `1 = M (2 L - 1)` with `M = 1`, `L = 1`), `u = 1` and | ||
| `h = 3`, exact jets recover `F(0)` modulo every `2 ^ p`. -/ | ||
| theorem exists_taperedRecovery_X (p : ℕ) : |
There was a problem hiding this comment.
Nonblocking regression suggestion: the current instance uses exact jets. A nonzero-error case within the source's parameter range is a=u=M=1, h=3, p=2, F=X: perturb only the z² coefficient at t=1 by 2^66. Its contribution is delta/128 = 2^59 (E_1(0)=1/8 and -t/alpha=-1/4), still correct modulo 4. This would exercise the new precision mechanism directly.
| namespace TensorNetwork | ||
|
|
||
| /-- Mapping the tensors twice is mapping them by the composition. -/ | ||
| theorem map_map {R S T U : Type*} [CommSemiring R] [CommSemiring S] [CommSemiring T] |
There was a problem hiding this comment.
Nonblocking API-placement suggestion: this general map composition law belongs beside TensorNetwork.map in Deformation.lean, or can be private if only proof plumbing is intended. A generic client should not need CauchyModes merely to compose maps.
|
|
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
|
|
|
Carry-forward record ( |
Toward #1538 (Theorem D.1, ℓ = 1) for #1833.
worker-claude-e6cf7b0d-t2-recursion-2, Claude Code, Opus.Stacked on #1879 (which includes #1876 and #1867), merged into current
main. The new files are the four listed below; everything else in the diff belongs to those PRs.Change
This finishes Lemma D.5 of [OpenAI2026ETH] and adds the bridge between
F(t + αz)and its values at interpolation points. Locators were checked in the pinned PDF (openai/math@7ef5c0cc).TensorNetwork/TaperedRecovery.lean: the precision half of Lemma D.5 (§D.4.4, pp. 60–61). Setting:Kis aℚ-algebra andB ⊆ Ka subring containingℤ_(2). The manuscript's case isK = ℚ[U]/(f)andB = O.recoveryNodes aare the nonzero grid points andtaperMult u h t = h·max(0, u − v₂ t)are the multiplicities.taperedRecoveryis the right side of (D.9) for given jets.eval_zero_eq_taperedRecovery: (D.9) itself, specialised from feat(Polynomial): Hermite interpolation with node-varying multiplicities #1854.hermiteBasis_comp_eq_map:E_t(t + αz)is the image of aℤ_(2)polynomial with constant term 1. So its inverse power series is integral (the source's "forming the quotient loses no precision").exists_taperedRecovery_eq_add: suppose the jetsG tagree withF(t + αz)mod2^p_tbelowz^q_t, withp + 6hD_t + q_t(a+1) ≤ p_t. Then the recovered value isF(0) + 2^p bwithb ∈ B. The6hD_tterm is (D.10) from feat(Polynomial): two-adic bound for tapered Hermite basis values (D.10) #1860. Theq_t(a+1)term is the evaluation loss at−t/α.exists_taperedRecovery_eq_add_of_params: the manuscript's parameters,p_t = p + 8hD_t + 8M(a+1)anddeg F ≤ M(2L−1), with3M ≤ hu ≤ 3M + u(true forh = ⌈3M/u⌉). This usestaperMult_le(q_t ≤ 4M) andle_sum_taperMult(∑ q_t ≥ Lhu > M(2L−1)).TensorNetwork/LocalDeformation.lean: the evaluation bridge (§D.4.3–§D.4.5, pp. 59–62).localDeformationisF(t + αz)as a polynomial over any ringBthat receivesℤ_(2). It is the deformed contraction alongcauchyLocalMatrix, the matrix of feat(circuit/frontier): modes of the Cauchy matrix and the geometric expansion (D.12) #1879'slocalKernels.map_localDeformation: in aℚ-algebra it maps toF(T)composed witht + αz. HereF(T)is feat(circuit/frontier): deformed contraction and the Cauchy kernel #1845's deformed contraction along the Cauchy matrix, whose value at 0 is the contraction.eval₂_localDeformation: under anyπ : B → R', its value atζis the deformed contraction along feat(circuit/frontier): modes of the Cauchy matrix and the geometric expansion (D.12) #1879'scauchyValueMatrix (π ∘ κ) ζ. This is what the child identity (D.16) expands.natDegree_deformedContraction_leand its corollaries give the degree boundM(2L − 1)from p. 59.Limits
This is mathematics only. The source's algorithmic claims for Lemma D.5 (polynomial-time rational assembly) are not formalised here; they belong to T2.9. The recursion, its parameters (D.4)–(D.6), (D.11) and (D.15) come in follow-up PRs.
Existing notions considered
hermiteBasisandhermiteQuotient(feat(Polynomial): Hermite interpolation with node-varying multiplicities #1854) and the D.10 bound (feat(Polynomial): two-adic bound for tapered Hermite basis values (D.10) #1860): reused.localKernel,kernelValueandcauchyValueMatrix(feat(circuit/frontier): modes of the Cauchy matrix and the geometric expansion (D.12) #1879), anddeformedContraction_map(feat(circuit/frontier): deformed contraction and the Cauchy kernel #1845): reused.x = y + 2^p * bwithb ∈ B, which needs no new notion. Mathlib'sSModEqwould need aB-module structure onKand would not simplify the statements.No abstract is affected.
Validation
ComplexityTests/.../TensorNetworkTaperedRecovery.leanand.../TensorNetworkLocalDeformation.lean.K = ℚandB = ℤ_(2).runLinteron both modules,lint-style,check_hygiene.pyandmk_all. On this branchcheck.sh --quickfalls back to the full gates because oflakefile.tomllibrary options, so the full run is left to CI.AI assistance
Written by Claude Code (Opus) as a worker of
coordinator-claude-e6cf7b0d. It needs outside-fleet review.🤖 Generated with Claude Code
https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG