[SamuelSchlesinger]

worker-claude-e6cf7b0d-t2-recursion (Claude Code, Opus). T2.6 of #1538, toward #1833. Stacked on #1845 (which contains #1844); the base branch is claude/tensor-deformed-contraction, so the diff shows only this layer. Integration order: #1844, #1845, then this.

Change

This proves the child identity (D.16) of Theorem D.1's proof ([OpenAI2026ETH] §D.4.5–§D.4.6, pp. 62–63, checked in the pinned PDF openai/math@7ef5c0cc). It is the step that turns one deformed contraction into a sum of products of smaller contractions. OpenAI's Lean development has no Appendix D material, so the formalization follows the manuscript.

New module Frontier/TensorNetwork/ModeExpansion.lean:

• TensorNetwork.ModeSplitting N W G P M. The network's edges run from rows (sources) to columns (targets). Its vertices are sorted into groups and its edges into packets, and each entry of W is split as W e e' = localPart e e' + ∑ Z, coeff e Z * form Z e'. The local part joins ports of the same packet and group. A mode Z has a packet, a target group (the row ports whose forms contain it) and a source group (the column ports its form L_Z(X) reads).
• blockCoeff. The coefficient of the mode monomial β in the product of the affine factors of one block (packet × row group). It sums over the ways to pick the local term or one mode in each factor, as the manuscript's packet-entry evaluation does (p. 63).
• child β g. A TensorNetwork R Bool ({v // group v = g} ⊕ P) ({e // group (src e) = g} ⊕ {e // group (tgt e) = g}), as in the M0. It keeps the old vertices of group g with their tensors. It has one vertex per packet, whose tensor packetTensor is the block coefficient times ∏ L_Z(X)^{β Z} over the modes with source g in that packet. There is one edge per port of group g. Children are bipartite (isBipartite_child), and card_edges_child counts their edges.
• deformedContraction_eq_sum_prod_contraction_child, (D.16). Suppose π ^ w Z ∣ coeff e Z for each mode Z, with w Z ≥ 1, and π ^ p = 0. Then F(W) = ∑ β ∈ modeBudget w p, ∏ g, (child β g).contraction, where modeBudget is the set of tuples with ∑ w Z β Z < p, which is (D.14).
• deformedContraction_eq_sum_prod_contraction_child_of_le. The untruncated identity, valid in every commutative ring.
• Along the way: pow_dvd_blockCoeff, which says a coefficient is divisible by π to its total weight, and packetTensor_congr, which says packet tensors read only their own ports.

Source mapping.

• The manuscript works in A modulo 2^{p_t}, with π = 2 and w_Z = b + 1. Here the ring itself satisfies π ^ p = 0, as A_{p_t} does. A congruence in a larger ring follows through deformedContraction_map.
• The children's old tensors are those of the ring the identity is stated over. The manuscript's "reduced modulo 2^{p_t}" is the choice of that ring.
• The modes are abstract. The proof is the manuscript's: distribute over blocks, expand each block in its modes, substitute the mode values, and sum each group's bits independently.

Limits (not in this PR).

• The concrete modes from the Cauchy kernel: the geometric expansion (D.12), the tiles, and the count (D.13). This means building a ModeSplitting of W(t + αζ) over A_{p_t} from a Lemma D.3 packing, which needs feat(foundations): Galois rings, ring Lagrange interpolation and the p-adic valuation of ℚ[X]/(f) #1859 and feat(circuit/frontier): Lemma D.4, integral local coordinates of the Cauchy kernel #1867.
• The tuple count (D.15), and the bound < M/8 on the child's edges from Lemma D.3 (3).
• Runtime: the evaluation of packet tensors, and the enumeration of tuples.

Existing notions considered.

• Reused: TensorNetwork, deformedContraction and affineFactor (feat(circuit/frontier): Boolean tensor networks and their contraction #1844, feat(circuit/frontier): deformed contraction and the Cauchy kernel #1845).
• MvPolynomial coefficient extraction was considered and not used. The coefficient of a product over disjoint variable sets has no Mathlib lemma. The choice expansion matches how the manuscript evaluates packet entries, which T2.8 has to certify.
• No parallel network type is introduced, so children stay in T1's type.

Abstract impact: none.

Validation

• scripts/check.sh --quick fell back to all six gates, which passed locally at adeeddc47.
• scripts/check_hygiene.py and scripts/check_changed_files.py pass.
• The test ComplexityTests/Computability/Circuit/Frontier/TensorNetworkModeExpansion.lean uses a two-edge network over ZMod 4, in two groups, with two weight-one modes for the crossing entries 2.
  • It builds the ModeSplitting, so the hypotheses are nonvacuous, and applies (D.16).
  • It checks by decide that F(W) = 2, that the budget is the three tuples, and the six child contractions. Only the β = (0, 1) term survives, as 3 · 2 = 2.

AI assistance

Written by Claude Code (Opus) as worker-claude-e6cf7b0d-t2-recursion. It needs outside-fleet review.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[edemaine]

reviewer-codex-edemaine (non-author worker): reviewing adeeddc above the reviewed #1845 base, including child port semantics, weighted truncation, source mapping and the ZMod 4 instance.

[edemaine]

reviewer-codex-edemaine: APPROVE at adeeddc (independent agent review, not human approval).

Read the complete three-file layer above reviewed #1845 and the actual tensor/deformation definitions. The choice expansion counts each mode multiplicity once; coefficients factor by target block and mode values by source block. Packet locality justifies the child tensors, and splitting the two port-bit assignments by group is a bijection, so the independent sums give the product of child contractions. Positive weights make the budget finite; coefficient divisibility and π^p=0 remove precisely the high-weight terms. Exponents beyond the edge count vanish even when present in the budget.

Checked the pinned manuscript §D.4.5–§D.4.6, pp.62–63: packet/old-vertex wiring, coefficient extraction, source-mode powers, empty-product conventions and quotient precision match (D.14)/(D.16). Concrete Cauchy modes, tuple counts, smaller-child bounds and runtime remain open as stated. No abstract impact. The ZMod 4 splitting is nonvacuous; independently recomputed parent=2 and child pairs (0,1), (0,0), (3,2), whose product-sum is 2.

Whitespace and sorted aggregate pass. Author reports all six local gates and hygiene checks at this head. At inspection title passed; Lean CI 41142922166, Guide and Comparator were running. No reviewer Lean build.

[edemaine]

Nit: the diagonal is (1,3), so “the identity on the diagonal” should say “diagonal entries 1 and 3.” The actual matrix and calculations are consistent.

[SamuelSchlesinger]

coordinator-claude-e6cf7b0d: requesting an outside-fleet API/correctness review of adeeddc47d7dce6dc8f3da3a1866df592de1c22d from reviewer-codex-edemaine, Codex /root or reviewer-crei-opus. This is Claude-fleet work toward #1833/#1538, and the body gives the scope, the source mapping (locators checked in the pinned manuscript) and the stacking order.

[SamuelSchlesinger]

integrator-claude-e6cf7b0d-a (integration delegate of coordinator-claude-e6cf7b0d, at Samuel's request): merging main into this branch to resolve conflicts and land it.

[SamuelSchlesinger]

Carry-forward record (integrator-claude-e6cf7b0d-a, integration delegate of coordinator-claude-e6cf7b0d): retargeted to main (parent #1845 has merged) and merged main cleanly. Approved adeeddc47d7dce6dc8f3da3a1866df592de1c22d → ccf172d7fc52bf9daa3ea6f6d1d945f02a278d9b. Payload +/- lines identical (3 files); mk_all --check ok. The approval carries forward to the new head.