feat(circuit/frontier): direct summation over networks with described tensors by SamuelSchlesinger · Pull Request #1914 · cslib-community/complexitylib

SamuelSchlesinger · 2026-10-31T03:21:17Z

Change

This is infrastructure for #1538 (T2.9): the leaf step for implicit networks. Draft only because it is stacked on #1896, and the branch is #1896 with main merged in. Until #1896 lands, review only TensorNetwork/DescribedContraction.lean and its test.

The leaves of the recursion in Theorem D.1 are summed directly (§D.4.7, p. 64). Their packet tensors cannot be tables, though: a packet vertex with up to 2L ports would have 2^(2L) entries. Entries are therefore computed from descriptions (§D.4.6, p. 63). #1862's directContraction handles explicit tables only, and this PR handles descriptors.

DescribedNetwork T. Each vertex has ports and a descriptor t : T, and its entry at bits bs is eval t bs for an evaluator eval. contraction_ofExplicit shows that explicit networks are the case where the descriptors are tables and eval is table lookup.
Direct summation as a StackRecursion instance (sumScheme). Three kinds of node:
- the sum, whose children are the 2^m assignments;
- an assignment, whose children are the vertex entries, multiplied modulo 2^P;
- an entry, which is a leaf evaluated by the evaluator.
Each step is polynomial-time; only the evaluator is not. eval_sumRoot: the derivation has 2^m(k+1)+1 nodes and two levels, with a size invariant.
Scheme.Loop.counted, a generic lemma: a call whose children are indexed by a counter has a loop derivation. It lives in this file, in namespace Cslib.GenericRAM.StackRecursion.Scheme. It can move into StackRecursion.lean after feat(GenericRAM/Native): depth-first stack recursion with native bounds #1896.
contractionCertificate eval ev. One native machine computes d.contraction eval % 2^P on every input (P, d), from any native certificate ev of the evaluator (run_sumScheme).
contractionCertificate_le. Suppose the evaluator takes time ≤ E and space ≤ ES, and outputs ≤ Ev bits, on the bits of each vertex. Then the time is ≤ (2^m(k+1)+1)·(K(n+Ev+1)^K + 2E) and the space ≤ K(n+Ev+1)^K + ES, with one constant K.

This is the real leaf the T2.9 instance needs. Its T will be T2.7's descriptor of retained and packet tensors, and ev the exp(O(L log s)) entry evaluation of §D.4.6.

Existing notions considered.

ExplicitTensorNetwork and feat(circuit/frontier): direct-summation contraction modulo 2^P #1862's directContraction handle tables only. Generalizing them would change merged clients (feat(circuit/frontier): direct-summation contraction modulo 2^P #1862, feat(machines): explicit Boolean block-counting networks (#1833 H3) #1877), so this PR adds a described layer with a bridge (contraction_ofExplicit).
BooleanFold needs a polynomial body. A non-polynomial evaluator fits the stack recursion's leaf step instead, which needed no new loop combinator.

Validation

Local scripts/check.sh --quick passes (it fell back to all six gates). check_hygiene.py passes.
ComplexityTests/DescribedContraction.lean:
- on a one-edge network, with tables as descriptors, runs the machine to 31 mod 16, and checks the partial state one step earlier;
- checks correctness for any evaluator and the explicit-network bridge;
- certifies table lookup polynomial-time;
- builds the contraction certificate and applies contractionCertificate_le.

AI assistance

Written by worker-claude-e6cf7b0d-t2-native (Claude Code, Opus 5.5) under coordinator-claude-e6cf7b0d. Needs non-Claude-fleet review.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

A generic recursion scheme (leaf test, leaf step, start/next/absorb/finish) run by an explicit stack machine. Derivations `Eval I x y n h` (n nodes, h stack levels) are evaluated in 2n - 1 steps through states with at most h open frames. One native certificate runs the machine for a natively computed fuel; its time is (fuel + 1) times a polynomial in (h+1)(F+1) plus the leaf time, and its space a polynomial plus the leaf space. Also the node count of a recursion tree and its 2^O(n/sqrt(log n)) bound (Foundations/Data/Nat/RecursionTree.lean), for the call count of [OpenAI2026ETH, Appendix D.4.7]. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

…n docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

…mial time The fuel of the stack recursion on the scale of ContractionAlgorithm, computed in binary from n in unary. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

…rsion

… tensors Networks whose tensors are given by descriptors and an evaluator, and their direct summation as a stack recursion: one native machine for the contraction modulo 2^P from any native certificate of the evaluator, with time (2^m (k+1) + 1) (poly + 2E) and space poly + ES. This is the leaf step of [OpenAI2026ETH, Appendix D.4.7] with implicit packet tensors. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

SamuelSchlesinger · 2026-10-31T03:27:51Z

coordinator-claude-e6cf7b0d: requesting an outside-fleet review of 792613291bce8b9d183ff5b14b4ccb2664042655 from reviewer-codex-edemaine, Codex /root or reviewer-crei-opus. This is #1538 T2.9 groundwork, the native runtime for Theorem D.1 (prerequisite of #1833). Implicit-network leaf: DescribedNetwork with direct summation as a StackRecursion instance (draft; review only its own files until #1896 lands).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

SamuelSchlesinger · 2026-10-31T04:18:45Z

integrator-claude-e6cf7b0d-a (integration delegate of coordinator-claude-e6cf7b0d, at Samuel's request): merging main into this branch now that #1896 has landed, so the diff is only this PR's own files. It stays a draft and is not queued.

SamuelSchlesinger · 2026-10-31T05:16:14Z

coordinator-claude-e6cf7b0d: superseded by #1928, which contains this PR's files and generalizes the leaf to A_p values. This PR will be closed once #1928 lands. Please don't queue it separately.

SamuelSchlesinger · 2026-10-31T06:45:00Z

coordinator-claude-e6cf7b0d: closing as superseded by #1928, which has merged. #1928 contains this PR's files, generalized to A_p values, and reviewer-codex-edemaine's review of #1928 covered this layer in full. The branch is left in place.

…operations, with A_p coefficient lists (cslib-community#1928) * feat(GenericRAM/Native): depth-first stack recursion with native bounds A generic recursion scheme (leaf test, leaf step, start/next/absorb/finish) run by an explicit stack machine. Derivations `Eval I x y n h` (n nodes, h stack levels) are evaluated in 2n - 1 steps through states with at most h open frames. One native certificate runs the machine for a natively computed fuel; its time is (fuel + 1) times a polynomial in (h+1)(F+1) plus the leaf time, and its space a polynomial plus the leaf space. Also the node count of a recursion tree and its 2^O(n/sqrt(log n)) bound (Foundations/Data/Nat/RecursionTree.lean), for the call count of [OpenAI2026ETH, Appendix D.4.7]. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): arithmetic in (Z/2^p)[U]/(f) on coefficient lists 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 * doc(GenericRAM/Native): qualify the module path in the stack recursion docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime/Nat): the clock 2^(K n / sqrt(floor(log2 n))) in polynomial time The fuel of the stack recursion on the scale of ContractionAlgorithm, computed in binary from n in unary. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): unit and powers in (Z/2^p)[U]/(f) 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 * feat(PolyTime): negation, subtraction and Newton inversion in (Z/2^p)[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 * feat(circuit/frontier): direct summation over networks with described tensors Networks whose tensors are given by descriptors and an evaluator, and their direct summation as a stack recursion: one native machine for the contraction modulo 2^P from any native certificate of the evaluator, with time (2^m (k+1) + 1) (poly + 2E) and space poly + ES. This is the leaf step of [OpenAI2026ETH, Appendix D.4.7] with implicit packet tensors. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): direct summation over described networks with ring operations on values Generalize the leaf of cslib-community#1914 from natural numbers modulo 2^P to any ring operations on values (SumOps), with their reduced values, homomorphisms and polynomial-time certificates. The scheme computes the fold of the operations (sumValue); a homomorphism takes it to the contraction of the mapped entries. Instances: natural numbers modulo 2^P (SumOps.mod, the previous behaviour, with sumValue_mod and modContractionCertificate) and coefficient lists of (Z/2^p)[U]/(f) with GaloisRingArith (SumOps.galois, val_sumValue_galois). The resource theorem takes a bound Rv on reduced values. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): share the port/descriptor record between explicit and described networks `DescribedNetwork T` moves to `TensorNetwork/Explicit.lean` with `equivProd`, `wordBits`, `contraction` and `map_contraction`, and `ExplicitTensorNetwork R` becomes the abbreviation `DescribedNetwork (List R)`: an explicit network is a described network whose descriptors are tables. `DescribedNetwork.ofExplicit` is removed (it is the identity), and `contraction_ofExplicit` becomes `DescribedNetwork.contraction_entry`, for any commutative semiring. `DirectContraction` uses the shared `DescribedNetwork.equivProd` in place of its own copy. Addresses reviewer-codex-edemaine's request on cslib-community#1928. Written by worker-claude-e6cf7b0d-eval-fixer, taking over from worker-claude-e6cf7b0d-t2-evaluator. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(circuit/frontier): name IsRowsFirstBipartite explicitly on an anonymous explicit network An anonymous constructor ascribed ExplicitTensorNetwork ℕ elaborates at the shared record DescribedNetwork (List ℕ), so field notation no longer finds the explicit-network namespace. 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>

…n polynomial space (Theorem D.1, T2.9) (cslib-community#1937) * feat(circuit/frontier): Boolean tensor networks and their contraction 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: cslib-community#1833 (T1), cslib-community#1538. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): deformed contraction and the Cauchy kernel 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: cslib-community#1538 (T2.1), cslib-community#1833. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): index explicit tables by BitString.lsbValue Address the cslib-community#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 * feat(circuit/frontier): Lemma D.4, integral local coordinates of the Cauchy kernel T2.3 of cslib-community#1538 (OpenAI2026ETH, §D.4.3, Lemma D.4, pp. 59-60), stacked on cslib-community#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 * refactor(foundations): move integer valuation bounds to RatValuation 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 * feat(circuit/frontier): mode expansion and the child identity (D.16) 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 * feat(circuit/frontier): modes of the Cauchy matrix, the geometric expansion (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 * feat(GenericRAM/Native): depth-first stack recursion with native bounds A generic recursion scheme (leaf test, leaf step, start/next/absorb/finish) run by an explicit stack machine. Derivations `Eval I x y n h` (n nodes, h stack levels) are evaluated in 2n - 1 steps through states with at most h open frames. One native certificate runs the machine for a natively computed fuel; its time is (fuel + 1) times a polynomial in (h+1)(F+1) plus the leaf time, and its space a polynomial plus the leaf space. Also the node count of a recursion tree and its 2^O(n/sqrt(log n)) bound (Foundations/Data/Nat/RecursionTree.lean), for the call count of [OpenAI2026ETH, Appendix D.4.7]. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): arithmetic in (Z/2^p)[U]/(f) on coefficient lists 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 * doc(GenericRAM/Native): qualify the module path in the stack recursion docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime/Nat): the clock 2^(K n / sqrt(floor(log2 n))) in polynomial time The fuel of the stack recursion on the scale of ContractionAlgorithm, computed in binary from n in unary. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): unit and powers in (Z/2^p)[U]/(f) 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 * feat(PolyTime): negation, subtraction and Newton inversion in (Z/2^p)[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 * feat(circuit/frontier): direct summation over networks with described tensors Networks whose tensors are given by descriptors and an evaluator, and their direct summation as a stack recursion: one native machine for the contraction modulo 2^P from any native certificate of the evaluator, with time (2^m (k+1) + 1) (poly + 2E) and space poly + ES. This is the leaf step of [OpenAI2026ETH, Appendix D.4.7] with implicit packet tensors. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): explicit packet entries of the child networks (Theorem D.1, T2.9 item 1) The child networks of an active call keep their packet tensors implicit (§D.4.6 of OpenAI2026ETH). This adds the explicit evaluation formula on the packet data and proves that it is the entry of the child network of `cauchyModeSplitting`: * `listCoeff`: coefficient extraction along a list of factors, equal to the sum over all choices (`sum_eq_listCoeff`) and to `blockCoeff` for any mode splitting and any order of the rows (`blockCoeff_eq_listCoeff`); * `packetEntry` and its terms, with `packetTensor_cauchyModeSplitting` and `child_tensor_inr_cauchyModeSplitting`; * `map_packetEntry`: the formula commutes with ring homomorphisms when 2 is nilpotent, so an evaluation in A_p transfers to the recursion's quotients; * the field lemmas of `cauchyModeSplitting` beyond side/group/packet. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the local Cauchy kernel as a product of units (Lemma D.4 evaluation) `kernelValue_eq_prod`: with t - q = 2^v_q u_q, u_q odd, W_d(t + αζ) is κ(kernelUnit a) times ∏_{q ≠ d, t} (u_q + 2^(a+1-v_q) ζ), times 2^(a+1-v_d) ζ when d ≠ t, where kernelUnit a is the inverse of the odd part of C'(0). The powers of two cancel exactly by `sum_padicValInt_sub_eq`, so kernel values need only ring operations and inverses of odd integers, as the source evaluates them (p. 60). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): direct summation over described networks with ring operations on values Generalize the leaf of cslib-community#1914 from natural numbers modulo 2^P to any ring operations on values (SumOps), with their reduced values, homomorphisms and polynomial-time certificates. The scheme computes the fold of the operations (sumValue); a homomorphism takes it to the contraction of the mapped entries. Instances: natural numbers modulo 2^P (SumOps.mod, the previous behaviour, with sumValue_mod and modContractionCertificate) and coefficient lists of (Z/2^p)[U]/(f) with GaloisRingArith (SumOps.galois, val_sumValue_galois). The resource theorem takes a bound Rv on reduced values. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): evaluate packet entries on coefficient lists of A_p Native evaluation of the packet entries of the child networks (Theorem D.1, section D.4.6) on GaloisRingArith coefficient lists: kernel values by the product formula of Lemma D.4's evaluation, cross ratios by Newton inversion of an element that is one modulo two, local forms, mode coefficients and values, row terms, and coefficient extraction along a list of modes. val_packetEntryList proves the value in A_p is packetEntry at the reduction of Z_(2); map_val_packetEntryList transports it along any ring map, using that ring maps from Z_(2) are unique when 2 is nilpotent (padicInteger_ringHom_ext). The 2-adic valuation is computed by halving (twoVal), so the functions reduce; tests check tiny packets by decide. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): packet modes by dense index y0 * nb + b Read the exponents of the packet modes at dense indices, matching a dense beta-slice in the packet descriptor, so coefficient extraction runs over a list of indices with a dense exponent list. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): coefficient extraction as a stack recursion Packet entries expand at most L affine row factors and keep the coefficient of a mode monomial (section D.4.6). CoeffScheme gives this as a StackRecursion scheme on GaloisRingArith coefficient lists: a node with rows has m + 1 children (the local term and each mode, lowering its exponent in a dense list), a node without rows is a leaf. val_value proves the value is listCoeff along the modes; eval_value gives the derivation with at most (m + 2)^L nodes and L open calls. From polynomial-time data the components are polynomial-time, and valueCertificate_le bounds one native machine by time K (m + 2)^L Z^K and space K Z^K. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): take the number of slots L as a parameter of kernel values Kernel values iterate over the 2^(a+1) grid points, so a native certificate needs the number of slots L = 2^a in unary. The native functions now take L, and the correctness theorems assume L = 2^a. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(circuit/frontier): mode terms vanish when a packet has no exponents With nb = 0 the exponent k % nb is k itself; guard it so that the exponent of a mode term is always below nb. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging main Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging the base Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): share the port/descriptor record between explicit and described networks `DescribedNetwork T` moves to `TensorNetwork/Explicit.lean` with `equivProd`, `wordBits`, `contraction` and `map_contraction`, and `ExplicitTensorNetwork R` becomes the abbreviation `DescribedNetwork (List R)`: an explicit network is a described network whose descriptors are tables. `DescribedNetwork.ofExplicit` is removed (it is the identity), and `contraction_ofExplicit` becomes `DescribedNetwork.contraction_entry`, for any commutative semiring. `DirectContraction` uses the shared `DescribedNetwork.equivProd` in place of its own copy. Addresses reviewer-codex-edemaine's request on cslib-community#1928. Written by worker-claude-e6cf7b0d-eval-fixer, taking over from worker-claude-e6cf7b0d-t2-evaluator. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(circuit/frontier): name IsRowsFirstBipartite explicitly on an anonymous explicit network An anonymous constructor ascribed ExplicitTensorNetwork ℕ elaborates at the shared record DescribedNetwork (List ℕ), so field notation no longer finds the explicit-network namespace. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): number packet modes with Mathlib's finProdFinEquiv Replace `NativePacket.modeIndex` (with `modeIndex_div`, `modeIndex_mod` and `modeIndex_apply`) by `finProdFinEquiv.toEmbedding.trans Fin.valEmbedding`, which numbers the mode `(y₀, b)` as `b + nb y₀`, the same number. `val_packetEntryList` and `map_val_packetEntryList` now read the exponents at `finProdFinEquiv Z`. Addresses reviewer-codex-edemaine's request on cslib-community#1932. Written by worker-claude-e6cf7b0d-eval-fixer, taking over from worker-claude-e6cf7b0d-t2-evaluator. 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>

…og s)) and polynomial space (Theorem D.1, T2.9) (cslib-community#1944) * feat(circuit/frontier): Boolean tensor networks and their contraction 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: cslib-community#1833 (T1), cslib-community#1538. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): deformed contraction and the Cauchy kernel 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: cslib-community#1538 (T2.1), cslib-community#1833. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): index explicit tables by BitString.lsbValue Address the cslib-community#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 * feat(circuit/frontier): Lemma D.4, integral local coordinates of the Cauchy kernel T2.3 of cslib-community#1538 (OpenAI2026ETH, §D.4.3, Lemma D.4, pp. 59-60), stacked on cslib-community#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 * refactor(foundations): move integer valuation bounds to RatValuation 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 * feat(circuit/frontier): mode expansion and the child identity (D.16) 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 * feat(circuit/frontier): modes of the Cauchy matrix, the geometric expansion (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 * feat(GenericRAM/Native): depth-first stack recursion with native bounds A generic recursion scheme (leaf test, leaf step, start/next/absorb/finish) run by an explicit stack machine. Derivations `Eval I x y n h` (n nodes, h stack levels) are evaluated in 2n - 1 steps through states with at most h open frames. One native certificate runs the machine for a natively computed fuel; its time is (fuel + 1) times a polynomial in (h+1)(F+1) plus the leaf time, and its space a polynomial plus the leaf space. Also the node count of a recursion tree and its 2^O(n/sqrt(log n)) bound (Foundations/Data/Nat/RecursionTree.lean), for the call count of [OpenAI2026ETH, Appendix D.4.7]. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): arithmetic in (Z/2^p)[U]/(f) on coefficient lists 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 * doc(GenericRAM/Native): qualify the module path in the stack recursion docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime/Nat): the clock 2^(K n / sqrt(floor(log2 n))) in polynomial time The fuel of the stack recursion on the scale of ContractionAlgorithm, computed in binary from n in unary. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): unit and powers in (Z/2^p)[U]/(f) 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 * feat(PolyTime): negation, subtraction and Newton inversion in (Z/2^p)[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 * feat(circuit/frontier): direct summation over networks with described tensors Networks whose tensors are given by descriptors and an evaluator, and their direct summation as a stack recursion: one native machine for the contraction modulo 2^P from any native certificate of the evaluator, with time (2^m (k+1) + 1) (poly + 2E) and space poly + ES. This is the leaf step of [OpenAI2026ETH, Appendix D.4.7] with implicit packet tensors. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): explicit packet entries of the child networks (Theorem D.1, T2.9 item 1) The child networks of an active call keep their packet tensors implicit (§D.4.6 of OpenAI2026ETH). This adds the explicit evaluation formula on the packet data and proves that it is the entry of the child network of `cauchyModeSplitting`: * `listCoeff`: coefficient extraction along a list of factors, equal to the sum over all choices (`sum_eq_listCoeff`) and to `blockCoeff` for any mode splitting and any order of the rows (`blockCoeff_eq_listCoeff`); * `packetEntry` and its terms, with `packetTensor_cauchyModeSplitting` and `child_tensor_inr_cauchyModeSplitting`; * `map_packetEntry`: the formula commutes with ring homomorphisms when 2 is nilpotent, so an evaluation in A_p transfers to the recursion's quotients; * the field lemmas of `cauchyModeSplitting` beyond side/group/packet. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the local Cauchy kernel as a product of units (Lemma D.4 evaluation) `kernelValue_eq_prod`: with t - q = 2^v_q u_q, u_q odd, W_d(t + αζ) is κ(kernelUnit a) times ∏_{q ≠ d, t} (u_q + 2^(a+1-v_q) ζ), times 2^(a+1-v_d) ζ when d ≠ t, where kernelUnit a is the inverse of the odd part of C'(0). The powers of two cancel exactly by `sum_padicValInt_sub_eq`, so kernel values need only ring operations and inverses of odd integers, as the source evaluates them (p. 60). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): direct summation over described networks with ring operations on values Generalize the leaf of cslib-community#1914 from natural numbers modulo 2^P to any ring operations on values (SumOps), with their reduced values, homomorphisms and polynomial-time certificates. The scheme computes the fold of the operations (sumValue); a homomorphism takes it to the contraction of the mapped entries. Instances: natural numbers modulo 2^P (SumOps.mod, the previous behaviour, with sumValue_mod and modContractionCertificate) and coefficient lists of (Z/2^p)[U]/(f) with GaloisRingArith (SumOps.galois, val_sumValue_galois). The resource theorem takes a bound Rv on reduced values. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): evaluate packet entries on coefficient lists of A_p Native evaluation of the packet entries of the child networks (Theorem D.1, section D.4.6) on GaloisRingArith coefficient lists: kernel values by the product formula of Lemma D.4's evaluation, cross ratios by Newton inversion of an element that is one modulo two, local forms, mode coefficients and values, row terms, and coefficient extraction along a list of modes. val_packetEntryList proves the value in A_p is packetEntry at the reduction of Z_(2); map_val_packetEntryList transports it along any ring map, using that ring maps from Z_(2) are unique when 2 is nilpotent (padicInteger_ringHom_ext). The 2-adic valuation is computed by halving (twoVal), so the functions reduce; tests check tiny packets by decide. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): packet modes by dense index y0 * nb + b Read the exponents of the packet modes at dense indices, matching a dense beta-slice in the packet descriptor, so coefficient extraction runs over a list of indices with a dense exponent list. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): coefficient extraction as a stack recursion Packet entries expand at most L affine row factors and keep the coefficient of a mode monomial (section D.4.6). CoeffScheme gives this as a StackRecursion scheme on GaloisRingArith coefficient lists: a node with rows has m + 1 children (the local term and each mode, lowering its exponent in a dense list), a node without rows is a leaf. val_value proves the value is listCoeff along the modes; eval_value gives the derivation with at most (m + 2)^L nodes and L open calls. From polynomial-time data the components are polynomial-time, and valueCertificate_le bounds one native machine by time K (m + 2)^L Z^K and space K Z^K. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): take the number of slots L as a parameter of kernel values Kernel values iterate over the 2^(a+1) grid points, so a native certificate needs the number of slots L = 2^a in unary. The native functions now take L, and the correctness theorems assume L = 2^a. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(circuit/frontier): mode terms vanish when a packet has no exponents With nb = 0 the exponent k % nb is k itself; guard it so that the exponent of a mode term is always below nb. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native packet evaluator in time exp(O(L log s)) and polynomial space Row terms of packet entries are polynomial-time: kernel values, cross ratios, local forms, mode coefficients and values, with the counts in unary and the integers in binary sign-magnitude form; the 2-adic valuation needs at most size |n| halvings. A packet context gives coefficient extraction for a packet as polynomial-time CoeffScheme data. packetEntryNative multiplies the stack recursion's value by the source mode powers; val_packetEntryNative_eq proves it is packetEntry in A_p, and entryCertificate_le bounds one native machine by time K (m + 2)^L Z^K and space K Z^K. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): descriptors of packet vertices and their native evaluator PacketDesc is a packet context, the ports (isRow, slot) in port order and the dense exponents. packetVertexEntry reads the row and column ports from the bits; vertexCertificate is its native machine, the evaluator of the described-network direct summation at coefficient lists, with val_packetVertexEntry and the bounds vertexCertificate_le. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging main Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging the base Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): share the port/descriptor record between explicit and described networks `DescribedNetwork T` moves to `TensorNetwork/Explicit.lean` with `equivProd`, `wordBits`, `contraction` and `map_contraction`, and `ExplicitTensorNetwork R` becomes the abbreviation `DescribedNetwork (List R)`: an explicit network is a described network whose descriptors are tables. `DescribedNetwork.ofExplicit` is removed (it is the identity), and `contraction_ofExplicit` becomes `DescribedNetwork.contraction_entry`, for any commutative semiring. `DirectContraction` uses the shared `DescribedNetwork.equivProd` in place of its own copy. Addresses reviewer-codex-edemaine's request on cslib-community#1928. Written by worker-claude-e6cf7b0d-eval-fixer, taking over from worker-claude-e6cf7b0d-t2-evaluator. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(circuit/frontier): name IsRowsFirstBipartite explicitly on an anonymous explicit network An anonymous constructor ascribed ExplicitTensorNetwork ℕ elaborates at the shared record DescribedNetwork (List ℕ), so field notation no longer finds the explicit-network namespace. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): number packet modes with Mathlib's finProdFinEquiv Replace `NativePacket.modeIndex` (with `modeIndex_div`, `modeIndex_mod` and `modeIndex_apply`) by `finProdFinEquiv.toEmbedding.trans Fin.valEmbedding`, which numbers the mode `(y₀, b)` as `b + nb y₀`, the same number. `val_packetEntryList` and `map_val_packetEntryList` now read the exponents at `finProdFinEquiv Z`. Addresses reviewer-codex-edemaine's request on cslib-community#1932. Written by worker-claude-e6cf7b0d-eval-fixer, taking over from worker-claude-e6cf7b0d-t2-evaluator. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): read packet exponents at finProdFinEquiv in the native evaluator Follows cslib-community#1932's switch from `modeIndex` to Mathlib's `finProdFinEquiv`: the statements of `val_packetEntryNative_eq`, `map_val_packetEntryNative` and `val_packetVertexEntry` read the dense exponents at `finProdFinEquiv Z` (the same number as `Z.1 * nb + Z.2`). 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>

…child networks (Theorem D.1, T2.9) (cslib-community#1952) * feat(circuit/frontier): Boolean tensor networks and their contraction 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: cslib-community#1833 (T1), cslib-community#1538. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): deformed contraction and the Cauchy kernel 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: cslib-community#1538 (T2.1), cslib-community#1833. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): index explicit tables by BitString.lsbValue Address the cslib-community#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 * feat(circuit/frontier): Lemma D.4, integral local coordinates of the Cauchy kernel T2.3 of cslib-community#1538 (OpenAI2026ETH, §D.4.3, Lemma D.4, pp. 59-60), stacked on cslib-community#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 * refactor(foundations): move integer valuation bounds to RatValuation 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 * feat(circuit/frontier): mode expansion and the child identity (D.16) 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 * feat(circuit/frontier): modes of the Cauchy matrix, the geometric expansion (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 * feat(GenericRAM/Native): depth-first stack recursion with native bounds A generic recursion scheme (leaf test, leaf step, start/next/absorb/finish) run by an explicit stack machine. Derivations `Eval I x y n h` (n nodes, h stack levels) are evaluated in 2n - 1 steps through states with at most h open frames. One native certificate runs the machine for a natively computed fuel; its time is (fuel + 1) times a polynomial in (h+1)(F+1) plus the leaf time, and its space a polynomial plus the leaf space. Also the node count of a recursion tree and its 2^O(n/sqrt(log n)) bound (Foundations/Data/Nat/RecursionTree.lean), for the call count of [OpenAI2026ETH, Appendix D.4.7]. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): arithmetic in (Z/2^p)[U]/(f) on coefficient lists 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 * doc(GenericRAM/Native): qualify the module path in the stack recursion docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime/Nat): the clock 2^(K n / sqrt(floor(log2 n))) in polynomial time The fuel of the stack recursion on the scale of ContractionAlgorithm, computed in binary from n in unary. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): unit and powers in (Z/2^p)[U]/(f) 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 * feat(PolyTime): negation, subtraction and Newton inversion in (Z/2^p)[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 * feat(circuit/frontier): direct summation over networks with described tensors Networks whose tensors are given by descriptors and an evaluator, and their direct summation as a stack recursion: one native machine for the contraction modulo 2^P from any native certificate of the evaluator, with time (2^m (k+1) + 1) (poly + 2E) and space poly + ES. This is the leaf step of [OpenAI2026ETH, Appendix D.4.7] with implicit packet tensors. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): explicit packet entries of the child networks (Theorem D.1, T2.9 item 1) The child networks of an active call keep their packet tensors implicit (§D.4.6 of OpenAI2026ETH). This adds the explicit evaluation formula on the packet data and proves that it is the entry of the child network of `cauchyModeSplitting`: * `listCoeff`: coefficient extraction along a list of factors, equal to the sum over all choices (`sum_eq_listCoeff`) and to `blockCoeff` for any mode splitting and any order of the rows (`blockCoeff_eq_listCoeff`); * `packetEntry` and its terms, with `packetTensor_cauchyModeSplitting` and `child_tensor_inr_cauchyModeSplitting`; * `map_packetEntry`: the formula commutes with ring homomorphisms when 2 is nilpotent, so an evaluation in A_p transfers to the recursion's quotients; * the field lemmas of `cauchyModeSplitting` beyond side/group/packet. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the local Cauchy kernel as a product of units (Lemma D.4 evaluation) `kernelValue_eq_prod`: with t - q = 2^v_q u_q, u_q odd, W_d(t + αζ) is κ(kernelUnit a) times ∏_{q ≠ d, t} (u_q + 2^(a+1-v_q) ζ), times 2^(a+1-v_d) ζ when d ≠ t, where kernelUnit a is the inverse of the odd part of C'(0). The powers of two cancel exactly by `sum_padicValInt_sub_eq`, so kernel values need only ring operations and inverses of odd integers, as the source evaluates them (p. 60). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): direct summation over described networks with ring operations on values Generalize the leaf of cslib-community#1914 from natural numbers modulo 2^P to any ring operations on values (SumOps), with their reduced values, homomorphisms and polynomial-time certificates. The scheme computes the fold of the operations (sumValue); a homomorphism takes it to the contraction of the mapped entries. Instances: natural numbers modulo 2^P (SumOps.mod, the previous behaviour, with sumValue_mod and modContractionCertificate) and coefficient lists of (Z/2^p)[U]/(f) with GaloisRingArith (SumOps.galois, val_sumValue_galois). The resource theorem takes a bound Rv on reduced values. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): evaluate packet entries on coefficient lists of A_p Native evaluation of the packet entries of the child networks (Theorem D.1, section D.4.6) on GaloisRingArith coefficient lists: kernel values by the product formula of Lemma D.4's evaluation, cross ratios by Newton inversion of an element that is one modulo two, local forms, mode coefficients and values, row terms, and coefficient extraction along a list of modes. val_packetEntryList proves the value in A_p is packetEntry at the reduction of Z_(2); map_val_packetEntryList transports it along any ring map, using that ring maps from Z_(2) are unique when 2 is nilpotent (padicInteger_ringHom_ext). The 2-adic valuation is computed by halving (twoVal), so the functions reduce; tests check tiny packets by decide. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): packet modes by dense index y0 * nb + b Read the exponents of the packet modes at dense indices, matching a dense beta-slice in the packet descriptor, so coefficient extraction runs over a list of indices with a dense exponent list. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): coefficient extraction as a stack recursion Packet entries expand at most L affine row factors and keep the coefficient of a mode monomial (section D.4.6). CoeffScheme gives this as a StackRecursion scheme on GaloisRingArith coefficient lists: a node with rows has m + 1 children (the local term and each mode, lowering its exponent in a dense list), a node without rows is a leaf. val_value proves the value is listCoeff along the modes; eval_value gives the derivation with at most (m + 2)^L nodes and L open calls. From polynomial-time data the components are polynomial-time, and valueCertificate_le bounds one native machine by time K (m + 2)^L Z^K and space K Z^K. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): take the number of slots L as a parameter of kernel values Kernel values iterate over the 2^(a+1) grid points, so a native certificate needs the number of slots L = 2^a in unary. The native functions now take L, and the correctness theorems assume L = 2^a. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(circuit/frontier): mode terms vanish when a packet has no exponents With nb = 0 the exponent k % nb is k itself; guard it so that the exponent of a mode term is always below nb. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native packet evaluator in time exp(O(L log s)) and polynomial space Row terms of packet entries are polynomial-time: kernel values, cross ratios, local forms, mode coefficients and values, with the counts in unary and the integers in binary sign-magnitude form; the 2-adic valuation needs at most size |n| halvings. A packet context gives coefficient extraction for a packet as polynomial-time CoeffScheme data. packetEntryNative multiplies the stack recursion's value by the source mode powers; val_packetEntryNative_eq proves it is packetEntry in A_p, and entryCertificate_le bounds one native machine by time K (m + 2)^L Z^K and space K Z^K. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): descriptors of packet vertices and their native evaluator PacketDesc is a packet context, the ports (isRow, slot) in port order and the dense exponents. packetVertexEntry reads the row and column ports from the bits; vertexCertificate is its native machine, the evaluator of the described-network direct summation at coefficient lists, with val_packetVertexEntry and the bounds vertexCertificate_le. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging main Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging the base Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): vertex descriptors and the entries of native child networks (Theorem D.1, T2.9) VertexDesc (a table or a packet descriptor) with one native evaluator and its resource bound; a described network with port lists has the contraction of the network it describes; retained vertices keep their tensors; the packet vertices of a Cauchy child have the child's entries for ports in any order with tags computed from the same port list; reductionLift maps the Galois ring back into O / 2^n with reductionLift ∘ reduction = mk. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): share the port/descriptor record between explicit and described networks `DescribedNetwork T` moves to `TensorNetwork/Explicit.lean` with `equivProd`, `wordBits`, `contraction` and `map_contraction`, and `ExplicitTensorNetwork R` becomes the abbreviation `DescribedNetwork (List R)`: an explicit network is a described network whose descriptors are tables. `DescribedNetwork.ofExplicit` is removed (it is the identity), and `contraction_ofExplicit` becomes `DescribedNetwork.contraction_entry`, for any commutative semiring. `DirectContraction` uses the shared `DescribedNetwork.equivProd` in place of its own copy. Addresses reviewer-codex-edemaine's request on cslib-community#1928. Written by worker-claude-e6cf7b0d-eval-fixer, taking over from worker-claude-e6cf7b0d-t2-evaluator. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(circuit/frontier): name IsRowsFirstBipartite explicitly on an anonymous explicit network An anonymous constructor ascribed ExplicitTensorNetwork ℕ elaborates at the shared record DescribedNetwork (List ℕ), so field notation no longer finds the explicit-network namespace. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): number packet modes with Mathlib's finProdFinEquiv Replace `NativePacket.modeIndex` (with `modeIndex_div`, `modeIndex_mod` and `modeIndex_apply`) by `finProdFinEquiv.toEmbedding.trans Fin.valEmbedding`, which numbers the mode `(y₀, b)` as `b + nb y₀`, the same number. `val_packetEntryList` and `map_val_packetEntryList` now read the exponents at `finProdFinEquiv Z`. Addresses reviewer-codex-edemaine's request on cslib-community#1932. Written by worker-claude-e6cf7b0d-eval-fixer, taking over from worker-claude-e6cf7b0d-t2-evaluator. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): read packet exponents at finProdFinEquiv in the native evaluator Follows cslib-community#1932's switch from `modeIndex` to Mathlib's `finProdFinEquiv`: the statements of `val_packetEntryNative_eq`, `map_val_packetEntryNative` and `val_packetVertexEntry` read the dense exponents at `finProdFinEquiv Z` (the same number as `Z.1 * nb + Z.2`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): read packet exponents at finProdFinEquiv for vertex descriptors Follows cslib-community#1932's switch from `modeIndex` to Mathlib's `finProdFinEquiv`: `map_val_entry_inr` and the dense-exponent hypothesis of `map_val_entry_child_inr` read the exponents at `finProdFinEquiv Z` (the same number as `Z.1 * nb + Z.2`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging the base 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>

…ne, reduced to the resource analysis (Theorem D.1, T2.9) (cslib-community#1970) * feat(circuit/frontier): Boolean tensor networks and their contraction 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: cslib-community#1833 (T1), cslib-community#1538. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): deformed contraction and the Cauchy kernel 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: cslib-community#1538 (T2.1), cslib-community#1833. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): index explicit tables by BitString.lsbValue Address the cslib-community#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 * feat(foundations): Galois rings, ring Lagrange interpolation and the p-adic valuation of Q[X]/(f) T2.2 of cslib-community#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 * feat(circuit/frontier): Lemma D.4, integral local coordinates of the Cauchy kernel T2.3 of cslib-community#1538 (OpenAI2026ETH, §D.4.3, Lemma D.4, pp. 59-60), stacked on cslib-community#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 * refactor(foundations): move integer valuation bounds to RatValuation 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 * feat(circuit/frontier): mode expansion and the child identity (D.16) 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 * feat(circuit/frontier): modes of the Cauchy matrix, the geometric expansion (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 * feat(circuit/frontier): local deformation and finite-precision tapered 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 * refactor(foundations): move AdjoinRoot coefficient reduction to its own 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 cslib-community#1859. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(foundations): scope GaloisRing to the manuscript's base ring O/(2^n) 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 cslib-community#1859. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): correctness of one active call, packing bridge and child sizes One active call of the contraction recursion of OpenAI2026ETH (§D.4.4–§D.4.7, pp. 60–64): interpolation of values congruent to F(t + αζ) mod 2^p_t followed by tapered recovery gives the contraction mod 2^p. Also the Lemma D.3 (2) orientation bridge for PacketPacking.Packing, the child degree and edge bounds of §D.4.6, and field lemmas for cauchyModeSplitting. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test: make the tapered recovery test module public Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(GenericRAM/Native): depth-first stack recursion with native bounds A generic recursion scheme (leaf test, leaf step, start/next/absorb/finish) run by an explicit stack machine. Derivations `Eval I x y n h` (n nodes, h stack levels) are evaluated in 2n - 1 steps through states with at most h open frames. One native certificate runs the machine for a natively computed fuel; its time is (fuel + 1) times a polynomial in (h+1)(F+1) plus the leaf time, and its space a polynomial plus the leaf space. Also the node count of a recursion tree and its 2^O(n/sqrt(log n)) bound (Foundations/Data/Nat/RecursionTree.lean), for the call count of [OpenAI2026ETH, Appendix D.4.7]. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: merge main and regenerate Complexity.lean Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): arithmetic in (Z/2^p)[U]/(f) on coefficient lists 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 * doc(GenericRAM/Native): qualify the module path in the stack recursion docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime/Nat): the clock 2^(K n / sqrt(floor(log2 n))) in polynomial time The fuel of the stack recursion on the scale of ContractionAlgorithm, computed in binary from n in unary. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): unit and powers in (Z/2^p)[U]/(f) 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 * feat(PolyTime): negation, subtraction and Newton inversion in (Z/2^p)[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 * refactor(circuit/frontier): packingGroup takes the edge ends directly packingGroup and its lemmas now take a packing of arbitrary edge ends src/tgt instead of a network, so the orientation hypothesis of cauchyModeSplitting can be supplied for N.map f. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): renaming and lifting tensor networks TensorNetwork.reindex transports a network along bijections of its vertices and edges and keeps its contraction; TensorNetwork.mapFun maps the entries by a function, and reducing a lift along a ring homomorphism recovers the network. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(foundations): digit lifts in Z_(p)[X]/(f) have unit differences The O-side counterpart of GaloisRing.isUnit_digitLift_sub: the binary-coordinate lifts of [OpenAI2026ETH] (§D.4.1, p. 58) in the valuation ring of AdjoinRoot.padicValuation differ by units. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the contraction recursion and its correctness (T2.7) contractRec evaluates a network by active calls (callValue: packing, mode splitting at each active node, children through a contraction oracle, interpolation and tapered recovery), with direct summation at leaves, inactive calls and children that are not smaller. It is well founded on the number of edges, and exists_contractRec_eq_add proves it returns the contraction modulo 2^p for every schedule, given interpolation points with unit differences. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(foundations): count tuples of bounded weight by the partition generating function The number of tuples beta : iota -> N of total weight sum w_i beta_i < p, with at most m coordinates of each positive weight, is at most exp(theta p + m pi^2/(6 theta)) for every theta > 0, hence at most 2^(4 floor(sqrt(m p)) + 4). This is the mode count (D.15) of the Boolean tensor contraction theorem of [OpenAI2026ETH] (cslib-community#1538). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): children of an active call have at most M/16 edges under (D.6) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): polynomials over (Z/2^p)[U]/(f) and Lagrange interpolation Addition, scaling, multiplication by z - v and Horner evaluation of coefficient-list polynomials, and Lagrange interpolation with Newton inverses of the denominators, proved to take the given values and certified polynomial-time with the precision in unary. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): unfolding lemmas for an active call and a leaf of the recursion Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): parameter schedule of the contraction recursion, (D.11) and (D.15) The schedule (D.4)-(D.6) of the Boolean tensor contraction recursion of [OpenAI2026ETH] on the floor-log / Nat.sqrt scale of cslib-community#1865, with the certificate exists_activeBounds: for large s every active call satisfies the packing conditions (D.6), the precision bound (D.11) p_t u <= 34 M D_t, polynomial precisions and depth <= log s - 2. The mode count (D.15) card_modeBudget_le bounds the mode tuples by 2^e_d, and the e_d sum to O(s / sqrt(log s)) (cslib-community#1538). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): fields of the active-node splitting; expose oracle correctness Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): mode count at a certified active call ActiveBounds.card_modeBudget_le supplies the hypotheses of card_modeBudget_le from the certificate, and ActiveBounds.two_le. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the contraction recursion has 2^O(s/sqrt(log s)) calls Compose ContractionSchedule.sum_branchExponent_le with Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): run the recursion with the parameter schedule of cslib-community#1908 The recursion now uses ContractionSchedule.nodePrecision for p_t, carries a degree bound in CallParams and guards active calls by CallParams.Guard (admissible parameters, rows to columns, at most Δ ports per vertex end). Children lifted by finLift keep this guard (rowsToColumnsLE_finLift_child). ScheduledRecursion.lean defines the schedule of call parameters (leaf iff M ≤ leafSize s, a = slotBits, u = taper, h = ⌈3M/u⌉, Δ = degreeBound) and, at an active call with ActiveBounds, the per-call facts a runtime certificate needs: the call is callValue, its children have at most M/16 edges and precisions within the schedule, and the mode count (D.15). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): direct summation over networks with described tensors Networks whose tensors are given by descriptors and an evaluator, and their direct summation as a stack recursion: one native machine for the contraction modulo 2^P from any native certificate of the evaluator, with time (2^m (k+1) + 1) (poly + 2E) and space poly + ES. This is the leaf step of [OpenAI2026ETH, Appendix D.4.7] with implicit packet tensors. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): Newton inversion inverts every unit of a Galois ring 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 * wip: native recovery definitions and constants Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): explicit packet entries of the child networks (Theorem D.1, T2.9 item 1) The child networks of an active call keep their packet tensors implicit (§D.4.6 of OpenAI2026ETH). This adds the explicit evaluation formula on the packet data and proves that it is the entry of the child network of `cauchyModeSplitting`: * `listCoeff`: coefficient extraction along a list of factors, equal to the sum over all choices (`sum_eq_listCoeff`) and to `blockCoeff` for any mode splitting and any order of the rows (`blockCoeff_eq_listCoeff`); * `packetEntry` and its terms, with `packetTensor_cauchyModeSplitting` and `child_tensor_inr_cauchyModeSplitting`; * `map_packetEntry`: the formula commutes with ring homomorphisms when 2 is nilpotent, so an evaluation in A_p transfers to the recursion's quotients; * the field lemmas of `cauchyModeSplitting` beyond side/group/packet. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: reciprocal and multiplier correctness Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): native tapered recovery components (Lemma D.5) Native recovery in A_(p+Δ) on coefficient lists: interpolation, the truncated reciprocal of E_t(t + αz) as a product of geometric series, the multipliers 2^Δ E_t(0)(-t/α)^j as 2-adic integers, and cancellation of 2^Δ. Proved: the slope constants, the reciprocal and the multipliers against any ring map from Z_(2), and the precision estimate that the multipliers annihilate 2^p_t. Supporting coordinates, precision changes and truncated products over A_p. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the local Cauchy kernel as a product of units (Lemma D.4 evaluation) `kernelValue_eq_prod`: with t - q = 2^v_q u_q, u_q odd, W_d(t + αζ) is κ(kernelUnit a) times ∏_{q ≠ d, t} (u_q + 2^(a+1-v_q) ζ), times 2^(a+1-v_d) ζ when d ≠ t, where kernelUnit a is the inverse of the odd part of C'(0). The powers of two cancel exactly by `sum_padicValInt_sub_eq`, so kernel values need only ring operations and inverses of odd integers, as the source evaluates them (p. 60). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): native recovery computes recoverFromValues mod 2^p Bridge cslib-community#1906's native interpolation to `Lagrange.ringInterpolate` through a ring map `π : B →+* A_N` (`exists_pval_interp_eq_add`), show that the reciprocal series inverts `E_t(t + α z)` so the Hermite quotient of a polynomial over `B` is integral (`hermiteQuotient_map_subtype`), and assemble: `2 ^ Δ * recoverFromValues` is a sum over `B` (`two_pow_mul_recoverFromValues`), and when the recovered value lies in `B`, `val p (recover …) = reduce (π R)` (`val_recover`, `val_recover_of_eq_add`). Adds the unfolding lemmas `taperedRecovery_def` and `recoverFromValues_def`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): direct summation over described networks with ring operations on values Generalize the leaf of cslib-community#1914 from natural numbers modulo 2^P to any ring operations on values (SumOps), with their reduced values, homomorphisms and polynomial-time certificates. The scheme computes the fold of the operations (sumValue); a homomorphism takes it to the contraction of the mapped entries. Instances: natural numbers modulo 2^P (SumOps.mod, the previous behaviour, with sumValue_mod and modContractionCertificate) and coefficient lists of (Z/2^p)[U]/(f) with GaloisRingArith (SumOps.galois, val_sumValue_galois). The resource theorem takes a bound Rv on reduced values. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): native recovery is polynomial-time Certify `NativeRecovery.recover` in polynomial time, with the precision, the shift, the parameters and `2 ^ a` in unary (`computableInPolyTime_recover`), through certificates for each loop: the capped 2-adic valuation, the multiplicities, the other node indices, the slope constants, the geometric series, the reciprocal, the multipliers and the node contributions; and for `tmul`, `cauchyCoeff` and `shiftDown` in `GaloisRingSeries`. `twoVal` now counts the `i < b` with `2 ^ (i + 1) ∣ d` (a filter, so its certificate is a filtered range), with the same `twoVal_eq`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): evaluate packet entries on coefficient lists of A_p Native evaluation of the packet entries of the child networks (Theorem D.1, section D.4.6) on GaloisRingArith coefficient lists: kernel values by the product formula of Lemma D.4's evaluation, cross ratios by Newton inversion of an element that is one modulo two, local forms, mode coefficients and values, row terms, and coefficient extraction along a list of modes. val_packetEntryList proves the value in A_p is packetEntry at the reduction of Z_(2); map_val_packetEntryList transports it along any ring map, using that ring maps from Z_(2) are unique when 2 is nilpotent (padicInteger_ringHom_ext). The 2-adic valuation is computed by halving (twoVal), so the functions reduce; tests check tiny packets by decide. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(circuit/frontier): terminal rewrites in twoVal_eq Replace the two non-terminal `simp` calls flagged by source hygiene with explicit rewrites. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): packet modes by dense index y0 * nb + b Read the exponents of the packet modes at dense indices, matching a dense beta-slice in the packet descriptor, so coefficient extraction runs over a list of indices with a dense exponent list. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the value table of native recovery `NativeRecovery.storeValue` appends a value to the row of a node index in the table that `recover` reads: the accumulator update of a recursive call once the value at an interpolation point is complete. Storing a sequence of values gives each node index its values in order (`getD_foldl_storeValue`), in polynomial time (`computableInPolyTime_storeValue`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): the kernel of reduction A_N → A_n is 2^n A_N `exists_eq_add_of_reduce_eq`: elements of `(ℤ/2^N)[U]/(f)` with equal reductions to precision `n` differ by `2 ^ n` times an element; so a native value computed at precision `p_t` lifts to `A_(p+Δ)` in the form that `NativeRecovery.val_recover` assumes (`exists_val_eq_add_of_val_eq`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): coefficient extraction as a stack recursion Packet entries expand at most L affine row factors and keep the coefficient of a mode monomial (section D.4.6). CoeffScheme gives this as a StackRecursion scheme on GaloisRingArith coefficient lists: a node with rows has m + 1 children (the local term and each mode, lowering its exponent in a dense list), a node without rows is a leaf. val_value proves the value is listCoeff along the modes; eval_value gives the derivation with at most (m + 2)^L nodes and L open calls. From polynomial-time data the components are polynomial-time, and valueCertificate_le bounds one native machine by time K (m + 2)^L Z^K and space K Z^K. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): take the number of slots L as a parameter of kernel values Kernel values iterate over the 2^(a+1) grid points, so a native certificate needs the number of slots L = 2^a in unary. The native functions now take L, and the correctness theorems assume L = 2^a. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(circuit/frontier): mode terms vanish when a packet has no exponents With nb = 0 the exponent k % nb is k itself; guard it so that the exponent of a mode term is always below nb. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(combinatorics): enumerate the tuples of bounded weight with a successor `budgetTuples ws p` lists the tuples of weight below `p` in lexicographic order and `budgetNext` is the successor that walks it from the zero tuple: the polynomial-delay enumeration of the mode exponents in §D.4.5 (p. 63) of the Boolean tensor contraction proof. `sum_filter_weight_lt_eq` turns a sum over the mode budget into a sum along the list. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): the successor of a tuple of bounded weight in polynomial time `budgetNextScan` computes `budgetNext` by one left scan over the coordinates (`budgetNextScan_eq`), and `computableInPolyTime_budgetNext` certifies it, so the enumeration of the mode exponents has polynomial delay. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native packet evaluator in time exp(O(L log s)) and polynomial space Row terms of packet entries are polynomial-time: kernel values, cross ratios, local forms, mode coefficients and values, with the counts in unary and the integers in binary sign-magnitude form; the 2-adic valuation needs at most size |n| halvings. A packet context gives coefficient extraction for a packet as polynomial-time CoeffScheme data. packetEntryNative multiplies the stack recursion's value by the source mode powers; val_packetEntryNative_eq proves it is packetEntry in A_p, and entryCertificate_le bounds one native machine by time K (m + 2)^L Z^K and space K Z^K. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): descriptors of packet vertices and their native evaluator PacketDesc is a packet context, the ports (isRow, slot) in port order and the dense exponents. packetVertexEntry reads the row and column ports from the bits; vertexCertificate is its native machine, the evaluator of the described-network direct summation at coefficient lists, with val_packetVertexEntry and the bounds vertexCertificate_le. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging main Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging the base Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the cursor over the children of an active call `cursorNext` walks the indices `(t, k, β, g)` of the children of an active call: the next group, else the next exponent tuple (`budgetNext`), else the next point, else the next node. `cursorList` lists them, and the walk from `cursorStart` follows it (`cursorList_walk`). One step is polynomial-time (`computableInPolyTime_cursorStep`), so the children have polynomial delay. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(combinatorics): count the feasible coordinate values with Mathlib's ceiling division Review of cslib-community#1942: replace the parallel `headCount` with `p ⌈/⌉ w`, which is definitionally `(p + w - 1) / w`; `lt_ceilDiv_iff` now follows from `ceilDiv_le_iff_le_mul`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the values a call stores along the cursor `absorbAt` multiplies a child's value into the product over the groups, adds the product to the sum over the exponent tuples after the last group, and stores the sum after the last tuple. `runAcc_cursorList`: along `cursorList` it stores, for each node and point, the sum over the tuples of the products over the groups, seen through any map respecting the operations. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the stored values are the sums over the mode budget `sumAt_eq_sum_filter` turns the value a call stores for a node and point into the sum over the mode budget, through `sum_filter_weight_lt_eq`. Adds a test of the accumulator on two nodes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): vertex descriptors and the entries of native child networks (Theorem D.1, T2.9) VertexDesc (a table or a packet descriptor) with one native evaluator and its resource bound; a described network with port lists has the contraction of the network it describes; retained vertices keep their tensors; the packet vertices of a Cauchy child have the child's entries for ports in any order with tags computed from the same port list; reductionLift maps the Galois ring back into O / 2^n with reductionLift ∘ reduction = mk. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merges Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): share the port/descriptor record between explicit and described networks `DescribedNetwork T` moves to `TensorNetwork/Explicit.lean` with `equivProd`, `wordBits`, `contraction` and `map_contraction`, and `ExplicitTensorNetwork R` becomes the abbreviation `DescribedNetwork (List R)`: an explicit network is a described network whose descriptors are tables. `DescribedNetwork.ofExplicit` is removed (it is the identity), and `contraction_ofExplicit` becomes `DescribedNetwork.contraction_entry`, for any commutative semiring. `DirectContraction` uses the shared `DescribedNetwork.equivProd` in place of its own copy. Addresses reviewer-codex-edemaine's request on cslib-community#1928. Written by worker-claude-e6cf7b0d-eval-fixer, taking over from worker-claude-e6cf7b0d-t2-evaluator. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(circuit/frontier): name IsRowsFirstBipartite explicitly on an anonymous explicit network An anonymous constructor ascribed ExplicitTensorNetwork ℕ elaborates at the shared record DescribedNetwork (List ℕ), so field notation no longer finds the explicit-network namespace. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): number packet modes with Mathlib's finProdFinEquiv Replace `NativePacket.modeIndex` (with `modeIndex_div`, `modeIndex_mod` and `modeIndex_apply`) by `finProdFinEquiv.toEmbedding.trans Fin.valEmbedding`, which numbers the mode `(y₀, b)` as `b + nb y₀`, the same number. `val_packetEntryList` and `map_val_packetEntryList` now read the exponents at `finProdFinEquiv Z`. Addresses reviewer-codex-edemaine's request on cslib-community#1932. Written by worker-claude-e6cf7b0d-eval-fixer, taking over from worker-claude-e6cf7b0d-t2-evaluator. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(GenericRAM/Native): derivations of stack recursions from recursion trees Loop.counted (counted children), exists_eval_of_counted (an Eval derivation from a value function on the recursion tree, with the node count Nat.recursionBound and the stack depth), and value_of_run_eq_some (a value returned by the clocked run satisfies the root derivation's invariant, for any fuel). For the T2.9 instance of cslib-community#1538. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): read packet exponents at finProdFinEquiv in the native evaluator Follows cslib-community#1932's switch from `modeIndex` to Mathlib's `finProdFinEquiv`: the statements of `val_packetEntryNative_eq`, `map_val_packetEntryNative` and `val_packetVertexEntry` read the dense exponents at `finProdFinEquiv Z` (the same number as `Z.1 * nb + Z.2`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): read packet exponents at finProdFinEquiv for vertex descriptors Follows cslib-community#1932's switch from `modeIndex` to Mathlib's `finProdFinEquiv`: `map_val_entry_inr` and the dense-exponent hypothesis of `map_val_entry_child_inr` read the exponents at `finProdFinEquiv Z` (the same number as `Z.1 * nb + Z.2`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(GenericRAM/Native): derivations by well-founded recursion; DescribedContraction uses the moved Loop.counted Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: described lift and native child (in progress) * feat(circuit/frontier): the native contraction recursion as a stack recursion, its derivations and correctness from the step Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging the base Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native machine of the fast contraction algorithm, correct for every fuel Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * Merge cslib-community#1952's review fixes; adapt to ExplicitTensorNetwork = DescribedNetwork (List R) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): native child networks and their contraction (wip) * feat(circuit/frontier): the call count with a constant explicit in C (as #PR-B) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the guard of the fast contraction algorithm and its small exceptions Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): one native active call is correct when its stored values are (wip) * chore: adapt to the shared described-network record and finProdFinEquiv exponents * test(circuit/frontier): native child on a tiny network * wip: fast machine resources scaffolding Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native child is rows-first * style(circuit/frontier): wrap long lines and pin flexible simps in the native child Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the fast machine within the interface's bounds, given the resource analysis Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the contraction algorithm from the fast machine's remaining obligations Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the modulus is irreducible modulo 2; tests of the fast machine Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the guard of the fast algorithm is polynomial-time Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the values stored by an active call, at each node's precision Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): an active call has at least 64^a edges Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the step of the native recursion is correct, given the points (bridge to cslib-community#1967) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the contraction algorithm from the native recursion, with the step, child well-formedness and roots proved Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): binary-digit points have lifts with unit differences isUnit_liftO_sub: lifts of 0/1 lists that differ below fl.length differ by a unit, through AdjoinRoot.integerDigitLift. pairwise_isUnit_liftO_sub_digits: the binary digits of 0, ..., n - 1 (n <= 2 ^ fl.length) give the hζ hypothesis of NativeCall.val_recover_eq_contraction. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native child in polynomial time, and its shape computableInPolyTime_nativeChild and computableInPolyTime_childRows in composition form over the native encodings, with their specializations to the native parent packing (numPackets_nativeParentPacking_le bounds its packets by M (2 ^ a) ^ 12). The shape lemmas numEdges_nativeChild_le, length_vertices_nativeChild and mem_vertices_nativeChild support node-size bounds along the recursion. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): one rows-first predicate on described networks ExplicitTensorNetwork R is DescribedNetwork (List R), so ExplicitTensorNetwork.IsRowsFirstBipartite and DescribedNetwork.IsRowsFirstBipartite were the same definition twice. Keep only DescribedNetwork.IsRowsFirstBipartite, defined beside DescribedNetwork in Explicit.lean; dot notation on explicit networks resolves to it. Remove isRowsFirstBipartite_explicit and update the docs and the test that named the explicit predicate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(circuit/frontier): keep the rows-first bullet's first line Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(circuit/frontier): docstrings of the betaSlice lemmas Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the components of the native contraction recursion in polynomial time `FastContraction.scheme_nativeMk_polyTime : (scheme nativeMk).PolyTime encCall encFrame encValue`, the `hpoly` hypothesis of `contractionAlgorithmOfNative` (cslib-community#1538, cslib-community#1970), from the native child in polynomial time (cslib-community#1973). `contractionAlgorithmOfNative` now takes only the resource analysis: `stepCorrect_nativeMk` is unconditional, with the points' unit differences from cslib-community#1973's `pairwise_isUnit_liftO_sub_digits`. - `FastContractionPolyTime.lean`: the schedule (`taper`, `slotBits`, `taperStep`, `leafSize`, `degreeBound`) and the data of a call (`active`, nodes, levels, `nodePrec`, the packing and its number of packets, the weights, points and table) in polynomial time on every call; `scheme_polyTime` for any polynomial-time builder; `nativeMk_polyTime`. - `nativeMk` caps the rows at the number of vertices (`rowCap`, also used by `packing`) and the exponents at the node's precision, since both are binary on arbitrary frames; `nativeMk_eq` shows the caps are inactive on well-formed active calls and cursor states. - `BudgetTuples.lt_of_mem_budgetTuples`: entries of tuples of weight below `p` are below `p`. - `FastAlgorithm.lean` reuses the public `degreeBound_polyTime`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(Classes/CountingSimulation): unfold the unified rows-first predicate in the guard ExplicitTensorNetwork.IsRowsFirstBipartite is now DescribedNetwork.IsRowsFirstBipartite (cslib-community#1967). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(circuit/frontier): restore the exact quotation of the child edge bound The manuscript (§D.4.6, p. 63) reads "at most 6M/r = 3M/32 < M/8 edges". This restores the parent's text, so ChildSize.lean is unchanged by this PR. 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>

…on recursion (FastAnalysis, T2.9) (cslib-community#1988) * feat(circuit/frontier): Boolean tensor networks and their contraction 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 * feat(circuit/frontier): deformed contraction and the Cauchy kernel 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 * refactor(circuit/frontier): index explicit tables by BitString.lsbValue 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 * feat(foundations): Galois rings, ring Lagrange interpolation and the 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 * feat(circuit/frontier): Lemma D.4, integral local coordinates of the 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 * refactor(foundations): move integer valuation bounds to RatValuation 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 * feat(circuit/frontier): mode expansion and the child identity (D.16) 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 * feat(circuit/frontier): modes of the Cauchy matrix, the geometric expansion (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 * feat(circuit/frontier): local deformation and finite-precision tapered 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 * refactor(foundations): move AdjoinRoot coefficient reduction to its own 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 * doc(foundations): scope GaloisRing to the manuscript's base ring O/(2^n) 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 * feat(circuit/frontier): correctness of one active call, packing bridge and child sizes One active call of the contraction recursion of OpenAI2026ETH (§D.4.4–§D.4.7, pp. 60–64): interpolation of values congruent to F(t + αζ) mod 2^p_t followed by tapered recovery gives the contraction mod 2^p. Also the Lemma D.3 (2) orientation bridge for PacketPacking.Packing, the child degree and edge bounds of §D.4.6, and field lemmas for cauchyModeSplitting. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test: make the tapered recovery test module public Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(GenericRAM/Native): depth-first stack recursion with native bounds A generic recursion scheme (leaf test, leaf step, start/next/absorb/finish) run by an explicit stack machine. Derivations `Eval I x y n h` (n nodes, h stack levels) are evaluated in 2n - 1 steps through states with at most h open frames. One native certificate runs the machine for a natively computed fuel; its time is (fuel + 1) times a polynomial in (h+1)(F+1) plus the leaf time, and its space a polynomial plus the leaf space. Also the node count of a recursion tree and its 2^O(n/sqrt(log n)) bound (Foundations/Data/Nat/RecursionTree.lean), for the call count of [OpenAI2026ETH, Appendix D.4.7]. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: merge main and regenerate Complexity.lean Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): arithmetic in (Z/2^p)[U]/(f) on coefficient lists 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 * doc(GenericRAM/Native): qualify the module path in the stack recursion docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime/Nat): the clock 2^(K n / sqrt(floor(log2 n))) in polynomial time The fuel of the stack recursion on the scale of ContractionAlgorithm, computed in binary from n in unary. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): unit and powers in (Z/2^p)[U]/(f) 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 * feat(PolyTime): negation, subtraction and Newton inversion in (Z/2^p)[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 * refactor(circuit/frontier): packingGroup takes the edge ends directly packingGroup and its lemmas now take a packing of arbitrary edge ends src/tgt instead of a network, so the orientation hypothesis of cauchyModeSplitting can be supplied for N.map f. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): renaming and lifting tensor networks TensorNetwork.reindex transports a network along bijections of its vertices and edges and keeps its contraction; TensorNetwork.mapFun maps the entries by a function, and reducing a lift along a ring homomorphism recovers the network. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(foundations): digit lifts in Z_(p)[X]/(f) have unit differences The O-side counterpart of GaloisRing.isUnit_digitLift_sub: the binary-coordinate lifts of [OpenAI2026ETH] (§D.4.1, p. 58) in the valuation ring of AdjoinRoot.padicValuation differ by units. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the contraction recursion and its correctness (T2.7) contractRec evaluates a network by active calls (callValue: packing, mode splitting at each active node, children through a contraction oracle, interpolation and tapered recovery), with direct summation at leaves, inactive calls and children that are not smaller. It is well founded on the number of edges, and exists_contractRec_eq_add proves it returns the contraction modulo 2^p for every schedule, given interpolation points with unit differences. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(foundations): count tuples of bounded weight by the partition generating function The number of tuples beta : iota -> N of total weight sum w_i beta_i < p, with at most m coordinates of each positive weight, is at most exp(theta p + m pi^2/(6 theta)) for every theta > 0, hence at most 2^(4 floor(sqrt(m p)) + 4). This is the mode count (D.15) of the Boolean tensor contraction theorem of [OpenAI2026ETH] (#1538). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): children of an active call have at most M/16 edges under (D.6) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): polynomials over (Z/2^p)[U]/(f) and Lagrange interpolation Addition, scaling, multiplication by z - v and Horner evaluation of coefficient-list polynomials, and Lagrange interpolation with Newton inverses of the denominators, proved to take the given values and certified polynomial-time with the precision in unary. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): unfolding lemmas for an active call and a leaf of the recursion Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): parameter schedule of the contraction recursion, (D.11) and (D.15) The schedule (D.4)-(D.6) of the Boolean tensor contraction recursion of [OpenAI2026ETH] on the floor-log / Nat.sqrt scale of #1865, with the certificate exists_activeBounds: for large s every active call satisfies the packing conditions (D.6), the precision bound (D.11) p_t u <= 34 M D_t, polynomial precisions and depth <= log s - 2. The mode count (D.15) card_modeBudget_le bounds the mode tuples by 2^e_d, and the e_d sum to O(s / sqrt(log s)) (#1538). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): fields of the active-node splitting; expose oracle correctness Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): mode count at a certified active call ActiveBounds.card_modeBudget_le supplies the hypotheses of card_modeBudget_le from the certificate, and ActiveBounds.two_le. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the contraction recursion has 2^O(s/sqrt(log s)) calls Compose ContractionSchedule.sum_branchExponent_le with Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): run the recursion with the parameter schedule of #1908 The recursion now uses ContractionSchedule.nodePrecision for p_t, carries a degree bound in CallParams and guards active calls by CallParams.Guard (admissible parameters, rows to columns, at most Δ ports per vertex end). Children lifted by finLift keep this guard (rowsToColumnsLE_finLift_child). ScheduledRecursion.lean defines the schedule of call parameters (leaf iff M ≤ leafSize s, a = slotBits, u = taper, h = ⌈3M/u⌉, Δ = degreeBound) and, at an active call with ActiveBounds, the per-call facts a runtime certificate needs: the call is callValue, its children have at most M/16 edges and precisions within the schedule, and the mode count (D.15). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): direct summation over networks with described tensors Networks whose tensors are given by descriptors and an evaluator, and their direct summation as a stack recursion: one native machine for the contraction modulo 2^P from any native certificate of the evaluator, with time (2^m (k+1) + 1) (poly + 2E) and space poly + ES. This is the leaf step of [OpenAI2026ETH, Appendix D.4.7] with implicit packet tensors. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): Newton inversion inverts every unit of a Galois ring 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 * wip: native recovery definitions and constants Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): explicit packet entries of the child networks (Theorem D.1, T2.9 item 1) The child networks of an active call keep their packet tensors implicit (§D.4.6 of OpenAI2026ETH). This adds the explicit evaluation formula on the packet data and proves that it is the entry of the child network of `cauchyModeSplitting`: * `listCoeff`: coefficient extraction along a list of factors, equal to the sum over all choices (`sum_eq_listCoeff`) and to `blockCoeff` for any mode splitting and any order of the rows (`blockCoeff_eq_listCoeff`); * `packetEntry` and its terms, with `packetTensor_cauchyModeSplitting` and `child_tensor_inr_cauchyModeSplitting`; * `map_packetEntry`: the formula commutes with ring homomorphisms when 2 is nilpotent, so an evaluation in A_p transfers to the recursion's quotients; * the field lemmas of `cauchyModeSplitting` beyond side/group/packet. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: reciprocal and multiplier correctness Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): native tapered recovery components (Lemma D.5) Native recovery in A_(p+Δ) on coefficient lists: interpolation, the truncated reciprocal of E_t(t + αz) as a product of geometric series, the multipliers 2^Δ E_t(0)(-t/α)^j as 2-adic integers, and cancellation of 2^Δ. Proved: the slope constants, the reciprocal and the multipliers against any ring map from Z_(2), and the precision estimate that the multipliers annihilate 2^p_t. Supporting coordinates, precision changes and truncated products over A_p. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the local Cauchy kernel as a product of units (Lemma D.4 evaluation) `kernelValue_eq_prod`: with t - q = 2^v_q u_q, u_q odd, W_d(t + αζ) is κ(kernelUnit a) times ∏_{q ≠ d, t} (u_q + 2^(a+1-v_q) ζ), times 2^(a+1-v_d) ζ when d ≠ t, where kernelUnit a is the inverse of the odd part of C'(0). The powers of two cancel exactly by `sum_padicValInt_sub_eq`, so kernel values need only ring operations and inverses of odd integers, as the source evaluates them (p. 60). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): native recovery computes recoverFromValues mod 2^p Bridge #1906's native interpolation to `Lagrange.ringInterpolate` through a ring map `π : B →+* A_N` (`exists_pval_interp_eq_add`), show that the reciprocal series inverts `E_t(t + α z)` so the Hermite quotient of a polynomial over `B` is integral (`hermiteQuotient_map_subtype`), and assemble: `2 ^ Δ * recoverFromValues` is a sum over `B` (`two_pow_mul_recoverFromValues`), and when the recovered value lies in `B`, `val p (recover …) = reduce (π R)` (`val_recover`, `val_recover_of_eq_add`). Adds the unfolding lemmas `taperedRecovery_def` and `recoverFromValues_def`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): direct summation over described networks with ring operations on values Generalize the leaf of #1914 from natural numbers modulo 2^P to any ring operations on values (SumOps), with their reduced values, homomorphisms and polynomial-time certificates. The scheme computes the fold of the operations (sumValue); a homomorphism takes it to the contraction of the mapped entries. Instances: natural numbers modulo 2^P (SumOps.mod, the previous behaviour, with sumValue_mod and modContractionCertificate) and coefficient lists of (Z/2^p)[U]/(f) with GaloisRingArith (SumOps.galois, val_sumValue_galois). The resource theorem takes a bound Rv on reduced values. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): native recovery is polynomial-time Certify `NativeRecovery.recover` in polynomial time, with the precision, the shift, the parameters and `2 ^ a` in unary (`computableInPolyTime_recover`), through certificates for each loop: the capped 2-adic valuation, the multiplicities, the other node indices, the slope constants, the geometric series, the reciprocal, the multipliers and the node contributions; and for `tmul`, `cauchyCoeff` and `shiftDown` in `GaloisRingSeries`. `twoVal` now counts the `i < b` with `2 ^ (i + 1) ∣ d` (a filter, so its certificate is a filtered range), with the same `twoVal_eq`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): evaluate packet entries on coefficient lists of A_p Native evaluation of the packet entries of the child networks (Theorem D.1, section D.4.6) on GaloisRingArith coefficient lists: kernel values by the product formula of Lemma D.4's evaluation, cross ratios by Newton inversion of an element that is one modulo two, local forms, mode coefficients and values, row terms, and coefficient extraction along a list of modes. val_packetEntryList proves the value in A_p is packetEntry at the reduction of Z_(2); map_val_packetEntryList transports it along any ring map, using that ring maps from Z_(2) are unique when 2 is nilpotent (padicInteger_ringHom_ext). The 2-adic valuation is computed by halving (twoVal), so the functions reduce; tests check tiny packets by decide. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(circuit/frontier): terminal rewrites in twoVal_eq Replace the two non-terminal `simp` calls flagged by source hygiene with explicit rewrites. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): packet modes by dense index y0 * nb + b Read the exponents of the packet modes at dense indices, matching a dense beta-slice in the packet descriptor, so coefficient extraction runs over a list of indices with a dense exponent list. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the value table of native recovery `NativeRecovery.storeValue` appends a value to the row of a node index in the table that `recover` reads: the accumulator update of a recursive call once the value at an interpolation point is complete. Storing a sequence of values gives each node index its values in order (`getD_foldl_storeValue`), in polynomial time (`computableInPolyTime_storeValue`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): the kernel of reduction A_N → A_n is 2^n A_N `exists_eq_add_of_reduce_eq`: elements of `(ℤ/2^N)[U]/(f)` with equal reductions to precision `n` differ by `2 ^ n` times an element; so a native value computed at precision `p_t` lifts to `A_(p+Δ)` in the form that `NativeRecovery.val_recover` assumes (`exists_val_eq_add_of_val_eq`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): coefficient extraction as a stack recursion Packet entries expand at most L affine row factors and keep the coefficient of a mode monomial (section D.4.6). CoeffScheme gives this as a StackRecursion scheme on GaloisRingArith coefficient lists: a node with rows has m + 1 children (the local term and each mode, lowering its exponent in a dense list), a node without rows is a leaf. val_value proves the value is listCoeff along the modes; eval_value gives the derivation with at most (m + 2)^L nodes and L open calls. From polynomial-time data the components are polynomial-time, and valueCertificate_le bounds one native machine by time K (m + 2)^L Z^K and space K Z^K. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): take the number of slots L as a parameter of kernel values Kernel values iterate over the 2^(a+1) grid points, so a native certificate needs the number of slots L = 2^a in unary. The native functions now take L, and the correctness theorems assume L = 2^a. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(circuit/frontier): mode terms vanish when a packet has no exponents With nb = 0 the exponent k % nb is k itself; guard it so that the exponent of a mode term is always below nb. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(combinatorics): enumerate the tuples of bounded weight with a successor `budgetTuples ws p` lists the tuples of weight below `p` in lexicographic order and `budgetNext` is the successor that walks it from the zero tuple: the polynomial-delay enumeration of the mode exponents in §D.4.5 (p. 63) of the Boolean tensor contraction proof. `sum_filter_weight_lt_eq` turns a sum over the mode budget into a sum along the list. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): the successor of a tuple of bounded weight in polynomial time `budgetNextScan` computes `budgetNext` by one left scan over the coordinates (`budgetNextScan_eq`), and `computableInPolyTime_budgetNext` certifies it, so the enumeration of the mode exponents has polynomial delay. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native packet evaluator in time exp(O(L log s)) and polynomial space Row terms of packet entries are polynomial-time: kernel values, cross ratios, local forms, mode coefficients and values, with the counts in unary and the integers in binary sign-magnitude form; the 2-adic valuation needs at most size |n| halvings. A packet context gives coefficient extraction for a packet as polynomial-time CoeffScheme data. packetEntryNative multiplies the stack recursion's value by the source mode powers; val_packetEntryNative_eq proves it is packetEntry in A_p, and entryCertificate_le bounds one native machine by time K (m + 2)^L Z^K and space K Z^K. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): descriptors of packet vertices and their native evaluator PacketDesc is a packet context, the ports (isRow, slot) in port order and the dense exponents. packetVertexEntry reads the row and column ports from the bits; vertexCertificate is its native machine, the evaluator of the described-network direct summation at coefficient lists, with val_packetVertexEntry and the bounds vertexCertificate_le. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging main Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging the base Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the cursor over the children of an active call `cursorNext` walks the indices `(t, k, β, g)` of the children of an active call: the next group, else the next exponent tuple (`budgetNext`), else the next point, else the next node. `cursorList` lists them, and the walk from `cursorStart` follows it (`cursorList_walk`). One step is polynomial-time (`computableInPolyTime_cursorStep`), so the children have polynomial delay. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(combinatorics): count the feasible coordinate values with Mathlib's ceiling division Review of #1942: replace the parallel `headCount` with `p ⌈/⌉ w`, which is definitionally `(p + w - 1) / w`; `lt_ceilDiv_iff` now follows from `ceilDiv_le_iff_le_mul`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the values a call stores along the cursor `absorbAt` multiplies a child's value into the product over the groups, adds the product to the sum over the exponent tuples after the last group, and stores the sum after the last tuple. `runAcc_cursorList`: along `cursorList` it stores, for each node and point, the sum over the tuples of the products over the groups, seen through any map respecting the operations. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the stored values are the sums over the mode budget `sumAt_eq_sum_filter` turns the value a call stores for a node and point into the sum over the mode budget, through `sum_filter_weight_lt_eq`. Adds a test of the accumulator on two nodes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): vertex descriptors and the entries of native child networks (Theorem D.1, T2.9) VertexDesc (a table or a packet descriptor) with one native evaluator and its resource bound; a described network with port lists has the contraction of the network it describes; retained vertices keep their tensors; the packet vertices of a Cauchy child have the child's entries for ports in any order with tags computed from the same port list; reductionLift maps the Galois ring back into O / 2^n with reductionLift ∘ reduction = mk. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merges Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): share the port/descriptor record between explicit and described networks `DescribedNetwork T` moves to `TensorNetwork/Explicit.lean` with `equivProd`, `wordBits`, `contraction` and `map_contraction`, and `ExplicitTensorNetwork R` becomes the abbreviation `DescribedNetwork (List R)`: an explicit network is a described network whose descriptors are tables. `DescribedNetwork.ofExplicit` is removed (it is the identity), and `contraction_ofExplicit` becomes `DescribedNetwork.contraction_entry`, for any commutative semiring. `DirectContraction` uses the shared `DescribedNetwork.equivProd` in place of its own copy. Addresses reviewer-codex-edemaine's request on #1928. Written by worker-claude-e6cf7b0d-eval-fixer, taking over from worker-claude-e6cf7b0d-t2-evaluator. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(circuit/frontier): name IsRowsFirstBipartite explicitly on an anonymous explicit network An anonymous constructor ascribed ExplicitTensorNetwork ℕ elaborates at the shared record DescribedNetwork (List ℕ), so field notation no longer finds the explicit-network namespace. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): number packet modes with Mathlib's finProdFinEquiv Replace `NativePacket.modeIndex` (with `modeIndex_div`, `modeIndex_mod` and `modeIndex_apply`) by `finProdFinEquiv.toEmbedding.trans Fin.valEmbedding`, which numbers the mode `(y₀, b)` as `b + nb y₀`, the same number. `val_packetEntryList` and `map_val_packetEntryList` now read the exponents at `finProdFinEquiv Z`. Addresses reviewer-codex-edemaine's request on #1932. Written by worker-claude-e6cf7b0d-eval-fixer, taking over from worker-claude-e6cf7b0d-t2-evaluator. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(GenericRAM/Native): derivations of stack recursions from recursion trees Loop.counted (counted children), exists_eval_of_counted (an Eval derivation from a value function on the recursion tree, with the node count Nat.recursionBound and the stack depth), and value_of_run_eq_some (a value returned by the clocked run satisfies the root derivation's invariant, for any fuel). For the T2.9 instance of #1538. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): read packet exponents at finProdFinEquiv in the native evaluator Follows #1932's switch from `modeIndex` to Mathlib's `finProdFinEquiv`: the statements of `val_packetEntryNative_eq`, `map_val_packetEntryNative` and `val_packetVertexEntry` read the dense exponents at `finProdFinEquiv Z` (the same number as `Z.1 * nb + Z.2`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): read packet exponents at finProdFinEquiv for vertex descriptors Follows #1932's switch from `modeIndex` to Mathlib's `finProdFinEquiv`: `map_val_entry_inr` and the dense-exponent hypothesis of `map_val_entry_child_inr` read the exponents at `finProdFinEquiv Z` (the same number as `Z.1 * nb + Z.2`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(GenericRAM/Native): derivations by well-founded recursion; DescribedContraction uses the moved Loop.counted Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: described lift and native child (in progress) * feat(circuit/frontier): the native contraction recursion as a stack recursion, its derivations and correctness from the step Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging the base Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native machine of the fast contraction algorithm, correct for every fuel Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * Merge #1952's review fixes; adapt to ExplicitTensorNetwork = DescribedNetwork (List R) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): native child networks and their contraction (wip) * feat(circuit/frontier): the call count with a constant explicit in C (as #PR-B) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the guard of the fast contraction algorithm and its small exceptions Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): one native active call is correct when its stored values are (wip) * chore: adapt to the shared described-network record and finProdFinEquiv exponents * test(circuit/frontier): native child on a tiny network * wip: fast machine resources scaffolding Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native child is rows-first * style(circuit/frontier): wrap long lines and pin flexible simps in the native child Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the fast machine within the interface's bounds, given the resource analysis Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the contraction algorithm from the fast machine's remaining obligations Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the modulus is irreducible modulo 2; tests of the fast machine Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the guard of the fast algorithm is polynomial-time Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the values stored by an active call, at each node's precision Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): an active call has at least 64^a edges Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the step of the native recursion is correct, given the points (bridge to #1967) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the contraction algorithm from the native recursion, with the step, child well-formedness and roots proved Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): binary-digit points have lifts with unit differences isUnit_liftO_sub: lifts of 0/1 lists that differ below fl.length differ by a unit, through AdjoinRoot.integerDigitLift. pairwise_isUnit_liftO_sub_digits: the binary digits of 0, ..., n - 1 (n <= 2 ^ fl.length) give the hζ hypothesis of NativeCall.val_recover_eq_contraction. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native child in polynomial time, and its shape computableInPolyTime_nativeChild and computableInPolyTime_childRows in composition form over the native encodings, with their specializations to the native parent packing (numPackets_nativeParentPacking_le bounds its packets by M (2 ^ a) ^ 12). The shape lemmas numEdges_nativeChild_le, length_vertices_nativeChild and mem_vertices_nativeChild support node-size bounds along the recursion. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): one rows-first predicate on described networks ExplicitTensorNetwork R is DescribedNetwork (List R), so ExplicitTensorNetwork.IsRowsFirstBipartite and DescribedNetwork.IsRowsFirstBipartite were the same definition twice. Keep only DescribedNetwork.IsRowsFirstBipartite, defined beside DescribedNetwork in Explicit.lean; dot notation on explicit networks resolves to it. Remove isRowsFirstBipartite_explicit and update the docs and the test that named the explicit predicate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(circuit/frontier): keep the rows-first bullet's first line Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(circuit/frontier): docstrings of the betaSlice lemmas Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): derivations over the reached calls, and the native child's edge and degree bounds The calls reached from a root of the native recursion, with derivations of the root's value over them: with their height (the bound plus the depth never increases) and, given a bound on the children of each call, their node count. The native child has at most M/16 edges under (D.6) and keeps the degree bound when 2L <= Delta: round 10's child facts in the native numbering. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the cost of a leaf of the fast contraction recursion Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native recursion follows the schedule Every call reached from a root on the schedule stays on it once the schedule's certificate holds: it keeps the scale, modulus, well-formedness and degree bound, and is small or an active call of the schedule, which then passes the machine's test. So the leaves have at most leafSize m edges and the active calls lie above depth log m - 2. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the packet shape of the native recursion and the leaf cost under it Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the call count of the native recursion on the schedule An active call on the schedule has at most 2^(2 log m + e_d) children (the mode count (D.15) in the native numbering, with Lemma D.3 (1) for the native packing), so the root has a derivation with at most 2^((245760 C + 37) m / sqrt(log m)) nodes and log m stack levels. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the leaf bound of the fast contraction analysis, with tests Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the resource analysis of the native recursion from sizes and leaves FastAnalysis nativeMk follows from FastSizes (polynomial sizes of the reached calls, frames and values) and FastLeaves (the leaf bounds). The derivation of the root over the reached calls has at most m + 1 stack levels, and from some size on at most 2^((245760 C' + 37) m / sqrt(log m)) nodes for C' = p/m + 1, which fit in the clock. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style: wrap long lines Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style: wrap a long line Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the leaf bounds of the native recursion from the reached-call facts Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test: the reached root of a guarded input has the packet shape Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): unfold nativeMk through one lemma; helpers for call shapes Every unfolding of nativeMk in the analysis goes through nativeMk_apply_of_active (well-formed, active, cursor state), so the caps on rows and exponents change one proof. Adds the arithmetic of the schedule at an active call and the bounds of the exponent tuples, points and node sizes used by the shape invariant. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the components of the native contraction recursion in polynomial time `FastContraction.scheme_nativeMk_polyTime : (scheme nativeMk).PolyTime encCall encFrame encValue`, the `hpoly` hypothesis of `contractionAlgorithmOfNative` (#1538, #1970), from the native child in polynomial time (#1973). `contractionAlgorithmOfNative` now takes only the resource analysis: `stepCorrect_nativeMk` is unconditional, with the points' unit differences from #1973's `pairwise_isUnit_liftO_sub_digits`. - `FastContractionPolyTime.lean`: the schedule (`taper`, `slotBits`, `taperStep`, `leafSize`, `degreeBound`) and the data of a call (`active`, nodes, levels, `nodePrec`, the packing and its number of packets, the weights, points and table) in polynomial time on every call; `scheme_polyTime` for any polynomial-time builder; `nativeMk_polyTime`. - `nativeMk` caps the rows at the number of vertices (`rowCap`, also used by `packing`) and the exponents at the node's precision, since both are binary on arbitrary frames; `nativeMk_eq` shows the caps are inactive on well-formed active calls and cursor states. - `BudgetTuples.lt_of_mem_budgetTuples`: entries of tuples of weight below `p` are below `p`. - `FastAlgorithm.lean` reuses the public `degreeBound_polyTime`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): structural shapes of the calls of the native recursion Every call reached from a well-formed root with m edges keeps the scale, modulus and well-formedness, has at most 2m edges, precision at most p0 + 40 m^2 d and at most V0 + m^2 d vertices at depth d, and every descriptor is a root table or a bounded packet descriptor. These hold for every input, whatever the schedule. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style: wrap a docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): unfold nativeMk once in packetShape_child Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): encoded lengths of calls and packet descriptors The encoded length of a call is at most 64 (B+1)^3 + 2 B R when its numbers, lists and ports are at most B and its descriptors at most R long; a bounded packet descriptor is at most 200 (B+1)^2 long. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): encoded lengths of values and frames The values of the calls are reduced at their precision, and frames whose accumulator is reduced have encoded length polynomial in their numbers; the accumulator stays reduced along the children and its stored values only grow. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the frames of an active call are polynomially long Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): packetShape_child through nativeMk_eq, for the capped builder of #1982 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style: wrap long lines Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the sizes of the calls, values and frames along the recursion Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): polynomial sizes along the native recursion FastSizes is proved: every call reached from a guarded root, its frames and its tagged value are at most 2^55 (n+1)^24 long. So FastAnalysis nativeMk now needs only the leaf bounds (fastAnalysis_nativeMk). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the facts at the reached calls for the leaf bounds Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(circuit/frontier): checked instances of the resource analysis Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the resource analysis of the native recursion holds FastAnalysis nativeMk is proved (fastAnalysis_nativeMk_holds): the leaf bounds of #1979 from the reached-call facts (at most twice the scale in edges; from some size on, precision at most the fourth power of the scale and at most leafSize edges at a leaf) and the sizes. The glue's hypotheses now use the (c, d) form of FastSizes and precision exponent 4. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(Classes/CountingSimulation): unfold the unified rows-first predicate in the guard ExplicitTensorNetwork.IsRowsFirstBipartite is now DescribedNetwork.IsRowsFirstBipartite (#1967). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(circuit/frontier): restore the exact quotation of the child edge bound The manuscript (§D.4.6, p. 63) reads "at most 6M/r = 3M/32 < M/8 edges". This restores the parent's text, so ChildSize.lean is unchanged by this PR. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): the analysis through nativeMk_eq, for the capped builder of #1982 With #1982's capped child builder, nativeMk is no longer unfolded by rfl. The analysis unfolds it through nativeMk_eq (replacing nativeMk_apply_of_active), reads the packing through packing_eq, and uses #1982's BudgetTuples.lt_of_mem_budgetTuples instead of a local copy. 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>

…O(T/√log T) and polynomial space, unconditionally (cslib-community#1995) * feat(circuit/frontier): Boolean tensor networks and their contraction 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 * feat(circuit/frontier): deformed contraction and the Cauchy kernel 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 * refactor(circuit/frontier): index explicit tables by BitString.lsbValue 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 * feat(foundations): Galois rings, ring Lagrange interpolation and the 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 * feat(circuit/frontier): Lemma D.4, integral local coordinates of the 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 * refactor(foundations): move integer valuation bounds to RatValuation 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 * feat(circuit/frontier): mode expansion and the child identity (D.16) 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 * feat(circuit/frontier): modes of the Cauchy matrix, the geometric expansion (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 * feat(circuit/frontier): local deformation and finite-precision tapered 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 * refactor(foundations): move AdjoinRoot coefficient reduction to its own 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 * doc(foundations): scope GaloisRing to the manuscript's base ring O/(2^n) 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 * feat(circuit/frontier): correctness of one active call, packing bridge and child sizes One active call of the contraction recursion of OpenAI2026ETH (§D.4.4–§D.4.7, pp. 60–64): interpolation of values congruent to F(t + αζ) mod 2^p_t followed by tapered recovery gives the contraction mod 2^p. Also the Lemma D.3 (2) orientation bridge for PacketPacking.Packing, the child degree and edge bounds of §D.4.6, and field lemmas for cauchyModeSplitting. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test: make the tapered recovery test module public Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(GenericRAM/Native): depth-first stack recursion with native bounds A generic recursion scheme (leaf test, leaf step, start/next/absorb/finish) run by an explicit stack machine. Derivations `Eval I x y n h` (n nodes, h stack levels) are evaluated in 2n - 1 steps through states with at most h open frames. One native certificate runs the machine for a natively computed fuel; its time is (fuel + 1) times a polynomial in (h+1)(F+1) plus the leaf time, and its space a polynomial plus the leaf space. Also the node count of a recursion tree and its 2^O(n/sqrt(log n)) bound (Foundations/Data/Nat/RecursionTree.lean), for the call count of [OpenAI2026ETH, Appendix D.4.7]. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: merge main and regenerate Complexity.lean Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): arithmetic in (Z/2^p)[U]/(f) on coefficient lists 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 * doc(GenericRAM/Native): qualify the module path in the stack recursion docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime/Nat): the clock 2^(K n / sqrt(floor(log2 n))) in polynomial time The fuel of the stack recursion on the scale of ContractionAlgorithm, computed in binary from n in unary. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): unit and powers in (Z/2^p)[U]/(f) 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 * feat(PolyTime): negation, subtraction and Newton inversion in (Z/2^p)[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 * refactor(circuit/frontier): packingGroup takes the edge ends directly packingGroup and its lemmas now take a packing of arbitrary edge ends src/tgt instead of a network, so the orientation hypothesis of cauchyModeSplitting can be supplied for N.map f. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): renaming and lifting tensor networks TensorNetwork.reindex transports a network along bijections of its vertices and edges and keeps its contraction; TensorNetwork.mapFun maps the entries by a function, and reducing a lift along a ring homomorphism recovers the network. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(foundations): digit lifts in Z_(p)[X]/(f) have unit differences The O-side counterpart of GaloisRing.isUnit_digitLift_sub: the binary-coordinate lifts of [OpenAI2026ETH] (§D.4.1, p. 58) in the valuation ring of AdjoinRoot.padicValuation differ by units. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the contraction recursion and its correctness (T2.7) contractRec evaluates a network by active calls (callValue: packing, mode splitting at each active node, children through a contraction oracle, interpolation and tapered recovery), with direct summation at leaves, inactive calls and children that are not smaller. It is well founded on the number of edges, and exists_contractRec_eq_add proves it returns the contraction modulo 2^p for every schedule, given interpolation points with unit differences. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(foundations): count tuples of bounded weight by the partition generating function The number of tuples beta : iota -> N of total weight sum w_i beta_i < p, with at most m coordinates of each positive weight, is at most exp(theta p + m pi^2/(6 theta)) for every theta > 0, hence at most 2^(4 floor(sqrt(m p)) + 4). This is the mode count (D.15) of the Boolean tensor contraction theorem of [OpenAI2026ETH] (#1538). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): children of an active call have at most M/16 edges under (D.6) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): polynomials over (Z/2^p)[U]/(f) and Lagrange interpolation Addition, scaling, multiplication by z - v and Horner evaluation of coefficient-list polynomials, and Lagrange interpolation with Newton inverses of the denominators, proved to take the given values and certified polynomial-time with the precision in unary. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): unfolding lemmas for an active call and a leaf of the recursion Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): parameter schedule of the contraction recursion, (D.11) and (D.15) The schedule (D.4)-(D.6) of the Boolean tensor contraction recursion of [OpenAI2026ETH] on the floor-log / Nat.sqrt scale of #1865, with the certificate exists_activeBounds: for large s every active call satisfies the packing conditions (D.6), the precision bound (D.11) p_t u <= 34 M D_t, polynomial precisions and depth <= log s - 2. The mode count (D.15) card_modeBudget_le bounds the mode tuples by 2^e_d, and the e_d sum to O(s / sqrt(log s)) (#1538). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): fields of the active-node splitting; expose oracle correctness Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): mode count at a certified active call ActiveBounds.card_modeBudget_le supplies the hypotheses of card_modeBudget_le from the certificate, and ActiveBounds.two_le. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the contraction recursion has 2^O(s/sqrt(log s)) calls Compose ContractionSchedule.sum_branchExponent_le with Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): run the recursion with the parameter schedule of #1908 The recursion now uses ContractionSchedule.nodePrecision for p_t, carries a degree bound in CallParams and guards active calls by CallParams.Guard (admissible parameters, rows to columns, at most Δ ports per vertex end). Children lifted by finLift keep this guard (rowsToColumnsLE_finLift_child). ScheduledRecursion.lean defines the schedule of call parameters (leaf iff M ≤ leafSize s, a = slotBits, u = taper, h = ⌈3M/u⌉, Δ = degreeBound) and, at an active call with ActiveBounds, the per-call facts a runtime certificate needs: the call is callValue, its children have at most M/16 edges and precisions within the schedule, and the mode count (D.15). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): direct summation over networks with described tensors Networks whose tensors are given by descriptors and an evaluator, and their direct summation as a stack recursion: one native machine for the contraction modulo 2^P from any native certificate of the evaluator, with time (2^m (k+1) + 1) (poly + 2E) and space poly + ES. This is the leaf step of [OpenAI2026ETH, Appendix D.4.7] with implicit packet tensors. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): Newton inversion inverts every unit of a Galois ring 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 * wip: native recovery definitions and constants Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): explicit packet entries of the child networks (Theorem D.1, T2.9 item 1) The child networks of an active call keep their packet tensors implicit (§D.4.6 of OpenAI2026ETH). This adds the explicit evaluation formula on the packet data and proves that it is the entry of the child network of `cauchyModeSplitting`: * `listCoeff`: coefficient extraction along a list of factors, equal to the sum over all choices (`sum_eq_listCoeff`) and to `blockCoeff` for any mode splitting and any order of the rows (`blockCoeff_eq_listCoeff`); * `packetEntry` and its terms, with `packetTensor_cauchyModeSplitting` and `child_tensor_inr_cauchyModeSplitting`; * `map_packetEntry`: the formula commutes with ring homomorphisms when 2 is nilpotent, so an evaluation in A_p transfers to the recursion's quotients; * the field lemmas of `cauchyModeSplitting` beyond side/group/packet. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: reciprocal and multiplier correctness Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): native tapered recovery components (Lemma D.5) Native recovery in A_(p+Δ) on coefficient lists: interpolation, the truncated reciprocal of E_t(t + αz) as a product of geometric series, the multipliers 2^Δ E_t(0)(-t/α)^j as 2-adic integers, and cancellation of 2^Δ. Proved: the slope constants, the reciprocal and the multipliers against any ring map from Z_(2), and the precision estimate that the multipliers annihilate 2^p_t. Supporting coordinates, precision changes and truncated products over A_p. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the local Cauchy kernel as a product of units (Lemma D.4 evaluation) `kernelValue_eq_prod`: with t - q = 2^v_q u_q, u_q odd, W_d(t + αζ) is κ(kernelUnit a) times ∏_{q ≠ d, t} (u_q + 2^(a+1-v_q) ζ), times 2^(a+1-v_d) ζ when d ≠ t, where kernelUnit a is the inverse of the odd part of C'(0). The powers of two cancel exactly by `sum_padicValInt_sub_eq`, so kernel values need only ring operations and inverses of odd integers, as the source evaluates them (p. 60). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): native recovery computes recoverFromValues mod 2^p Bridge #1906's native interpolation to `Lagrange.ringInterpolate` through a ring map `π : B →+* A_N` (`exists_pval_interp_eq_add`), show that the reciprocal series inverts `E_t(t + α z)` so the Hermite quotient of a polynomial over `B` is integral (`hermiteQuotient_map_subtype`), and assemble: `2 ^ Δ * recoverFromValues` is a sum over `B` (`two_pow_mul_recoverFromValues`), and when the recovered value lies in `B`, `val p (recover …) = reduce (π R)` (`val_recover`, `val_recover_of_eq_add`). Adds the unfolding lemmas `taperedRecovery_def` and `recoverFromValues_def`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): direct summation over described networks with ring operations on values Generalize the leaf of #1914 from natural numbers modulo 2^P to any ring operations on values (SumOps), with their reduced values, homomorphisms and polynomial-time certificates. The scheme computes the fold of the operations (sumValue); a homomorphism takes it to the contraction of the mapped entries. Instances: natural numbers modulo 2^P (SumOps.mod, the previous behaviour, with sumValue_mod and modContractionCertificate) and coefficient lists of (Z/2^p)[U]/(f) with GaloisRingArith (SumOps.galois, val_sumValue_galois). The resource theorem takes a bound Rv on reduced values. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): native recovery is polynomial-time Certify `NativeRecovery.recover` in polynomial time, with the precision, the shift, the parameters and `2 ^ a` in unary (`computableInPolyTime_recover`), through certificates for each loop: the capped 2-adic valuation, the multiplicities, the other node indices, the slope constants, the geometric series, the reciprocal, the multipliers and the node contributions; and for `tmul`, `cauchyCoeff` and `shiftDown` in `GaloisRingSeries`. `twoVal` now counts the `i < b` with `2 ^ (i + 1) ∣ d` (a filter, so its certificate is a filtered range), with the same `twoVal_eq`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): evaluate packet entries on coefficient lists of A_p Native evaluation of the packet entries of the child networks (Theorem D.1, section D.4.6) on GaloisRingArith coefficient lists: kernel values by the product formula of Lemma D.4's evaluation, cross ratios by Newton inversion of an element that is one modulo two, local forms, mode coefficients and values, row terms, and coefficient extraction along a list of modes. val_packetEntryList proves the value in A_p is packetEntry at the reduction of Z_(2); map_val_packetEntryList transports it along any ring map, using that ring maps from Z_(2) are unique when 2 is nilpotent (padicInteger_ringHom_ext). The 2-adic valuation is computed by halving (twoVal), so the functions reduce; tests check tiny packets by decide. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(circuit/frontier): terminal rewrites in twoVal_eq Replace the two non-terminal `simp` calls flagged by source hygiene with explicit rewrites. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): packet modes by dense index y0 * nb + b Read the exponents of the packet modes at dense indices, matching a dense beta-slice in the packet descriptor, so coefficient extraction runs over a list of indices with a dense exponent list. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the value table of native recovery `NativeRecovery.storeValue` appends a value to the row of a node index in the table that `recover` reads: the accumulator update of a recursive call once the value at an interpolation point is complete. Storing a sequence of values gives each node index its values in order (`getD_foldl_storeValue`), in polynomial time (`computableInPolyTime_storeValue`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): the kernel of reduction A_N → A_n is 2^n A_N `exists_eq_add_of_reduce_eq`: elements of `(ℤ/2^N)[U]/(f)` with equal reductions to precision `n` differ by `2 ^ n` times an element; so a native value computed at precision `p_t` lifts to `A_(p+Δ)` in the form that `NativeRecovery.val_recover` assumes (`exists_val_eq_add_of_val_eq`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): coefficient extraction as a stack recursion Packet entries expand at most L affine row factors and keep the coefficient of a mode monomial (section D.4.6). CoeffScheme gives this as a StackRecursion scheme on GaloisRingArith coefficient lists: a node with rows has m + 1 children (the local term and each mode, lowering its exponent in a dense list), a node without rows is a leaf. val_value proves the value is listCoeff along the modes; eval_value gives the derivation with at most (m + 2)^L nodes and L open calls. From polynomial-time data the components are polynomial-time, and valueCertificate_le bounds one native machine by time K (m + 2)^L Z^K and space K Z^K. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): take the number of slots L as a parameter of kernel values Kernel values iterate over the 2^(a+1) grid points, so a native certificate needs the number of slots L = 2^a in unary. The native functions now take L, and the correctness theorems assume L = 2^a. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(circuit/frontier): mode terms vanish when a packet has no exponents With nb = 0 the exponent k % nb is k itself; guard it so that the exponent of a mode term is always below nb. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(combinatorics): enumerate the tuples of bounded weight with a successor `budgetTuples ws p` lists the tuples of weight below `p` in lexicographic order and `budgetNext` is the successor that walks it from the zero tuple: the polynomial-delay enumeration of the mode exponents in §D.4.5 (p. 63) of the Boolean tensor contraction proof. `sum_filter_weight_lt_eq` turns a sum over the mode budget into a sum along the list. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(PolyTime): the successor of a tuple of bounded weight in polynomial time `budgetNextScan` computes `budgetNext` by one left scan over the coordinates (`budgetNextScan_eq`), and `computableInPolyTime_budgetNext` certifies it, so the enumeration of the mode exponents has polynomial delay. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native packet evaluator in time exp(O(L log s)) and polynomial space Row terms of packet entries are polynomial-time: kernel values, cross ratios, local forms, mode coefficients and values, with the counts in unary and the integers in binary sign-magnitude form; the 2-adic valuation needs at most size |n| halvings. A packet context gives coefficient extraction for a packet as polynomial-time CoeffScheme data. packetEntryNative multiplies the stack recursion's value by the source mode powers; val_packetEntryNative_eq proves it is packetEntry in A_p, and entryCertificate_le bounds one native machine by time K (m + 2)^L Z^K and space K Z^K. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): descriptors of packet vertices and their native evaluator PacketDesc is a packet context, the ports (isRow, slot) in port order and the dense exponents. packetVertexEntry reads the row and column ports from the bits; vertexCertificate is its native machine, the evaluator of the described-network direct summation at coefficient lists, with val_packetVertexEntry and the bounds vertexCertificate_le. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging main Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging the base Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the cursor over the children of an active call `cursorNext` walks the indices `(t, k, β, g)` of the children of an active call: the next group, else the next exponent tuple (`budgetNext`), else the next point, else the next node. `cursorList` lists them, and the walk from `cursorStart` follows it (`cursorList_walk`). One step is polynomial-time (`computableInPolyTime_cursorStep`), so the children have polynomial delay. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(combinatorics): count the feasible coordinate values with Mathlib's ceiling division Review of #1942: replace the parallel `headCount` with `p ⌈/⌉ w`, which is definitionally `(p + w - 1) / w`; `lt_ceilDiv_iff` now follows from `ceilDiv_le_iff_le_mul`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the values a call stores along the cursor `absorbAt` multiplies a child's value into the product over the groups, adds the product to the sum over the exponent tuples after the last group, and stores the sum after the last tuple. `runAcc_cursorList`: along `cursorList` it stores, for each node and point, the sum over the tuples of the products over the groups, seen through any map respecting the operations. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the stored values are the sums over the mode budget `sumAt_eq_sum_filter` turns the value a call stores for a node and point into the sum over the mode budget, through `sum_filter_weight_lt_eq`. Adds a test of the accumulator on two nodes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): vertex descriptors and the entries of native child networks (Theorem D.1, T2.9) VertexDesc (a table or a packet descriptor) with one native evaluator and its resource bound; a described network with port lists has the contraction of the network it describes; retained vertices keep their tensors; the packet vertices of a Cauchy child have the child's entries for ports in any order with tags computed from the same port list; reductionLift maps the Galois ring back into O / 2^n with reductionLift ∘ reduction = mk. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merges Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): share the port/descriptor record between explicit and described networks `DescribedNetwork T` moves to `TensorNetwork/Explicit.lean` with `equivProd`, `wordBits`, `contraction` and `map_contraction`, and `ExplicitTensorNetwork R` becomes the abbreviation `DescribedNetwork (List R)`: an explicit network is a described network whose descriptors are tables. `DescribedNetwork.ofExplicit` is removed (it is the identity), and `contraction_ofExplicit` becomes `DescribedNetwork.contraction_entry`, for any commutative semiring. `DirectContraction` uses the shared `DescribedNetwork.equivProd` in place of its own copy. Addresses reviewer-codex-edemaine's request on #1928. Written by worker-claude-e6cf7b0d-eval-fixer, taking over from worker-claude-e6cf7b0d-t2-evaluator. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(circuit/frontier): name IsRowsFirstBipartite explicitly on an anonymous explicit network An anonymous constructor ascribed ExplicitTensorNetwork ℕ elaborates at the shared record DescribedNetwork (List ℕ), so field notation no longer finds the explicit-network namespace. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): number packet modes with Mathlib's finProdFinEquiv Replace `NativePacket.modeIndex` (with `modeIndex_div`, `modeIndex_mod` and `modeIndex_apply`) by `finProdFinEquiv.toEmbedding.trans Fin.valEmbedding`, which numbers the mode `(y₀, b)` as `b + nb y₀`, the same number. `val_packetEntryList` and `map_val_packetEntryList` now read the exponents at `finProdFinEquiv Z`. Addresses reviewer-codex-edemaine's request on #1932. Written by worker-claude-e6cf7b0d-eval-fixer, taking over from worker-claude-e6cf7b0d-t2-evaluator. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(GenericRAM/Native): derivations of stack recursions from recursion trees Loop.counted (counted children), exists_eval_of_counted (an Eval derivation from a value function on the recursion tree, with the node count Nat.recursionBound and the stack depth), and value_of_run_eq_some (a value returned by the clocked run satisfies the root derivation's invariant, for any fuel). For the T2.9 instance of #1538. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): read packet exponents at finProdFinEquiv in the native evaluator Follows #1932's switch from `modeIndex` to Mathlib's `finProdFinEquiv`: the statements of `val_packetEntryNative_eq`, `map_val_packetEntryNative` and `val_packetVertexEntry` read the dense exponents at `finProdFinEquiv Z` (the same number as `Z.1 * nb + Z.2`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): read packet exponents at finProdFinEquiv for vertex descriptors Follows #1932's switch from `modeIndex` to Mathlib's `finProdFinEquiv`: `map_val_entry_inr` and the dense-exponent hypothesis of `map_val_entry_child_inr` read the exponents at `finProdFinEquiv Z` (the same number as `Z.1 * nb + Z.2`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(GenericRAM/Native): derivations by well-founded recursion; DescribedContraction uses the moved Loop.counted Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: described lift and native child (in progress) * feat(circuit/frontier): the native contraction recursion as a stack recursion, its derivations and correctness from the step Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate Complexity.lean after merging the base Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native machine of the fast contraction algorithm, correct for every fuel Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * Merge #1952's review fixes; adapt to ExplicitTensorNetwork = DescribedNetwork (List R) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): native child networks and their contraction (wip) * feat(circuit/frontier): the call count with a constant explicit in C (as #PR-B) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the guard of the fast contraction algorithm and its small exceptions Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): one native active call is correct when its stored values are (wip) * chore: adapt to the shared described-network record and finProdFinEquiv exponents * test(circuit/frontier): native child on a tiny network * wip: fast machine resources scaffolding Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native child is rows-first * style(circuit/frontier): wrap long lines and pin flexible simps in the native child Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the fast machine within the interface's bounds, given the resource analysis Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the contraction algorithm from the fast machine's remaining obligations Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the modulus is irreducible modulo 2; tests of the fast machine Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the guard of the fast algorithm is polynomial-time Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the values stored by an active call, at each node's precision Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): an active call has at least 64^a edges Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the step of the native recursion is correct, given the points (bridge to #1967) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the contraction algorithm from the native recursion, with the step, child well-formedness and roots proved Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): binary-digit points have lifts with unit differences isUnit_liftO_sub: lifts of 0/1 lists that differ below fl.length differ by a unit, through AdjoinRoot.integerDigitLift. pairwise_isUnit_liftO_sub_digits: the binary digits of 0, ..., n - 1 (n <= 2 ^ fl.length) give the hζ hypothesis of NativeCall.val_recover_eq_contraction. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native child in polynomial time, and its shape computableInPolyTime_nativeChild and computableInPolyTime_childRows in composition form over the native encodings, with their specializations to the native parent packing (numPackets_nativeParentPacking_le bounds its packets by M (2 ^ a) ^ 12). The shape lemmas numEdges_nativeChild_le, length_vertices_nativeChild and mem_vertices_nativeChild support node-size bounds along the recursion. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): one rows-first predicate on described networks ExplicitTensorNetwork R is DescribedNetwork (List R), so ExplicitTensorNetwork.IsRowsFirstBipartite and DescribedNetwork.IsRowsFirstBipartite were the same definition twice. Keep only DescribedNetwork.IsRowsFirstBipartite, defined beside DescribedNetwork in Explicit.lean; dot notation on explicit networks resolves to it. Remove isRowsFirstBipartite_explicit and update the docs and the test that named the explicit predicate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(circuit/frontier): keep the rows-first bullet's first line Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(circuit/frontier): docstrings of the betaSlice lemmas Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): derivations over the reached calls, and the native child's edge and degree bounds The calls reached from a root of the native recursion, with derivations of the root's value over them: with their height (the bound plus the depth never increases) and, given a bound on the children of each call, their node count. The native child has at most M/16 edges under (D.6) and keeps the degree bound when 2L <= Delta: round 10's child facts in the native numbering. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the cost of a leaf of the fast contraction recursion Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the native recursion follows the schedule Every call reached from a root on the schedule stays on it once the schedule's certificate holds: it keeps the scale, modulus, well-formedness and degree bound, and is small or an active call of the schedule, which then passes the machine's test. So the leaves have at most leafSize m edges and the active calls lie above depth log m - 2. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the packet shape of the native recursion and the leaf cost under it Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the call count of the native recursion on the schedule An active call on the schedule has at most 2^(2 log m + e_d) children (the mode count (D.15) in the native numbering, with Lemma D.3 (1) for the native packing), so the root has a derivation with at most 2^((245760 C + 37) m / sqrt(log m)) nodes and log m stack levels. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the leaf bound of the fast contraction analysis, with tests Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the resource analysis of the native recursion from sizes and leaves FastAnalysis nativeMk follows from FastSizes (polynomial sizes of the reached calls, frames and values) and FastLeaves (the leaf bounds). The derivation of the root over the reached calls has at most m + 1 stack levels, and from some size on at most 2^((245760 C' + 37) m / sqrt(log m)) nodes for C' = p/m + 1, which fit in the clock. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style: wrap long lines Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style: wrap a long line Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the leaf bounds of the native recursion from the reached-call facts Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test: the reached root of a guarded input has the packet shape Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): unfold nativeMk through one lemma; helpers for call shapes Every unfolding of nativeMk in the analysis goes through nativeMk_apply_of_active (well-formed, active, cursor state), so the caps on rows and exponents change one proof. Adds the arithmetic of the schedule at an active call and the bounds of the exponent tuples, points and node sizes used by the shape invariant. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the components of the native contraction recursion in polynomial time `FastContraction.scheme_nativeMk_polyTime : (scheme nativeMk).PolyTime encCall encFrame encValue`, the `hpoly` hypothesis of `contractionAlgorithmOfNative` (#1538, #1970), from the native child in polynomial time (#1973). `contractionAlgorithmOfNative` now takes only the resource analysis: `stepCorrect_nativeMk` is unconditional, with the points' unit differences from #1973's `pairwise_isUnit_liftO_sub_digits`. - `FastContractionPolyTime.lean`: the schedule (`taper`, `slotBits`, `taperStep`, `leafSize`, `degreeBound`) and the data of a call (`active`, nodes, levels, `nodePrec`, the packing and its number of packets, the weights, points and table) in polynomial time on every call; `scheme_polyTime` for any polynomial-time builder; `nativeMk_polyTime`. - `nativeMk` caps the rows at the number of vertices (`rowCap`, also used by `packing`) and the exponents at the node's precision, since both are binary on arbitrary frames; `nativeMk_eq` shows the caps are inactive on well-formed active calls and cursor states. - `BudgetTuples.lt_of_mem_budgetTuples`: entries of tuples of weight below `p` are below `p`. - `FastAlgorithm.lean` reuses the public `degreeBound_polyTime`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): structural shapes of the calls of the native recursion Every call reached from a well-formed root with m edges keeps the scale, modulus and well-formedness, has at most 2m edges, precision at most p0 + 40 m^2 d and at most V0 + m^2 d vertices at depth d, and every descriptor is a root table or a bounded packet descriptor. These hold for every input, whatever the schedule. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style: wrap a docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): unfold nativeMk once in packetShape_child Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): encoded lengths of calls and packet descriptors The encoded length of a call is at most 64 (B+1)^3 + 2 B R when its numbers, lists and ports are at most B and its descriptors at most R long; a bounded packet descriptor is at most 200 (B+1)^2 long. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): encoded lengths of values and frames The values of the calls are reduced at their precision, and frames whose accumulator is reduced have encoded length polynomial in their numbers; the accumulator stays reduced along the children and its stored values only grow. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the frames of an active call are polynomially long Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): packetShape_child through nativeMk_eq, for the capped builder of #1982 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style: wrap long lines Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(circuit/frontier): the sizes of the calls, values and frames along the recursion Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): polynomial sizes along the native recursion FastSizes is proved: every call reached from a guarded root, its frames and its tagged value are at most 2^55 (n+1)^24 long. So FastAnalysis nativeMk now needs only the leaf bounds (fastAnalysis_nativeMk). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the facts at the reached calls for the leaf bounds Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(circuit/frontier): checked instances of the resource analysis Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the resource analysis of the native recursion holds FastAnalysis nativeMk is proved (fastAnalysis_nativeMk_holds): the leaf bounds of #1979 from the reached-call facts (at most twice the scale in edges; from some size on, precision at most the fourth power of the scale and at most leafSize edges at a leaf) and the sizes. The glue's hypotheses now use the (c, d) form of FastSizes and precision exponent 4. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(Classes/CountingSimulation): unfold the unified rows-first predicate in the guard ExplicitTensorNetwork.IsRowsFirstBipartite is now DescribedNetwork.IsRowsFirstBipartite (#1967). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(circuit/frontier): restore the exact quotation of the child edge bound The manuscript (§D.4.6, p. 63) reads "at most 6M/r = 3M/32 < M/8 edges". This restores the parent's text, so ChildSize.lean is unchanged by this PR. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(circuit/frontier): the analysis through nativeMk_eq, for the capped builder of #1982 With #1982's capped child builder, nativeMk is no longer unfolded by rfl. The analysis unfolds it through nativeMk_eq (replacing nativeMk_apply_of_active), reads the packing through packing_eq, and uses #1982's BudgetTuples.lt_of_mem_budgetTuples instead of a local copy. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): the contraction algorithm of Theorem D.1, unconditionally With #1982's capped child builder, hpoly and the points' unit differences are proved, and FastAnalysis nativeMk holds (#1988), so contractionAlgorithmOfNative fastAnalysis_nativeMk_holds is the contraction algorithm for admissible explicit networks, with no remaining hypothesis. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Classes/CountingSimulation): NTIME, BPTIME and PPTIME in time 2^O(T/sqrt(log T)) and polynomial space The containments of BlockNetworks with fastContractionAlgorithm in place of their hypothesis: for time-constructible T with max n 2 <= T n, every problem in NTIME[T], BPTIME[T] or PPTIME[T] is decided by one deterministic machine in time 2^(C T n / sqrt(log2 (T n))) and workspace T n ^ d. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(Classes/CountingSimulation): the containments at a proved polynomial clock The test now instantiates the containments at T n = (n + 1)^2 + 1, which is proved time-constructible, instead of assuming a clock. FastSimulation.lean cites Hopcroft–Paul–Valiant, and the conditional modules point to the unconditional theorems (audit round 20). 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>

SamuelSchlesinger and others added 5 commits October 30, 2026 22:19

doc(GenericRAM/Native): qualify the module path in the stack recursio…

27d0311

…n docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Merge remote-tracking branch 'origin/main' into claude/t2-native-recu…

164f4b2

…rsion

This was referenced Oct 31, 2026

feat(Classes/CountingSimulation): a contraction algorithm from a guarded fast algorithm #1915

Merged

Formalize Appendix D: recursive tensor contraction and the sharper Theorem 1.1 bound for #k-SAT #1538

Open

This was referenced Oct 31, 2026

Deterministic simulation of NTIME, BPTIME and PPTIME in 2^{O(T/√log T)} via HPV blocking and tensor contraction #1833

Open

feat(circuit/frontier): described-network direct summation over ring operations, with A_p coefficient lists #1928

Merged

Merge origin/main into claude/t2-described-leaf

9e5bd2b

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

SamuelSchlesinger closed this Oct 31, 2026

Navigation Menu

Repository navigation

feat(circuit/frontier): direct summation over networks with described tensors - #1914

feat(circuit/frontier): direct summation over networks with described tensors#1914
SamuelSchlesinger wants to merge 6 commits into
mainfrom
claude/t2-described-leaf

SamuelSchlesinger commented Oct 31, 2026

Uh oh!

SamuelSchlesinger commented Oct 31, 2026

Uh oh!

SamuelSchlesinger commented Oct 31, 2026

Uh oh!

SamuelSchlesinger commented Oct 31, 2026

Uh oh!

SamuelSchlesinger commented Oct 31, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

SamuelSchlesinger commented Oct 31, 2026

Change

Validation

AI assistance

Uh oh!

SamuelSchlesinger commented Oct 31, 2026

Uh oh!

SamuelSchlesinger commented Oct 31, 2026

Uh oh!

SamuelSchlesinger commented Oct 31, 2026

Uh oh!

SamuelSchlesinger commented Oct 31, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant