[SamuelSchlesinger]

Change

Part of #1538 (Lemma D.2, network side), items 1–2 of the handoff in comment 6545915436. worker-claude-e6cf7b0d-lemma-d2-net-2 (Claude Code, Opus). The branch is stacked by merge on #2079 (base claude/lemma-d2-network, including its review fixes at cf823fdf3). It does not merge #2076, since nothing here uses incidenceSum yet.

This PR adds the entry procedure of the incidence network and one native machine that evaluates it, with time poly · 2^(group incidences) and polynomial space. It is infrastructure toward Lemma D.2 and proves no counting statement.

B_{P,ℓ} arithmetic (TruncatedRing.lean). No new multiplication is needed. GaloisRingArith.Ring P (truncFl ℓ), with lower coefficients truncFl ℓ = replicate ℓ 0, is (ℤ/2^P)[V]/(V^ℓ) (monicOf_truncFl). So the existing GaloisRingArith.add/mul/sub/one/zero, with their val_* and polynomial-time lemmas, are arithmetic in B_{P,ℓ}. Bridges: truncRingHom/truncNatHom, truncRingHom_eq_iff (equality is agreement of the coefficients below ℓ mod 2^P), truncNatHom_coeffPoly, and DescribedNetwork.truncNatHom_polyContraction.

Unranker made public (SubsetPairFold.lean), without aliases. pureUnrankComb, unrankComb_eq_pure, length_pureUnrankComb, count_true_pureUnrankComb and pureUnrankComb_injective lose private. computableInPolyTime_unrankComb becomes unrankComb_polyTime, and pureUnrankComb_polyTime is new.

Entries (IncidenceEntry.lean). Each source claim maps to Lean as follows:

• Indices (p. 55: ⌈log₂ C_gh⌉ wires, lexicographic order, "Any unused bit string gives tensor entry zero"). blockIndices reads each block's chunk little-endian. selectBlock unranks it with pureUnrankComb. validIndices tests ι < C(N, d).
• Rows (p. 56). The entry is ∏_{i∈T_g} [z_{i,S_i}] B̄_i = ∏_i Σ_{T⊆S_i} (−1)^{|S_i|−|T|} B_i(1_T, V) in B. B_i(1_T, V) has coefficients e_j(L̃_i(1_T)) h(L̃_i(1_T))^j for j < ℓ, where L̃_i(1_T) is the number of monomials inside T (monomialsIn). factorCoeffs reduces a_j, b_j of parityLinearCoeffs ℓ mod 2^P ("Reduce their coefficients modulo 2^p", p. 55).
  • Difference from the source: the product of the per-test subset sums is computed as one sum over the words on all selected incidences of the group (rowTerm, rowBody, rowSum). The exponent of the cost is therefore the group's incidences, not max |S_i|. The two are equal as elements of B, but that equality belongs to the correctness milestone and is not proved here.
• Columns (p. 56). The entry is [2^{#unselected vars} mod 2^P] (colEntry). Tables use tableEntry.
• encDesc encodes P, ℓ and the selected counts in unary.

Certificate (IncidenceEntryPolyTime.lean, IncidenceEntryCertificate.lean).

• incCertificate: the decoding, the row context, each row term, columns and tables are polynomial-time, and a row's sum runs through BooleanFold.certificate (rowSumCertificate).
• exists_incCertificate_le : ∃ c, ∀ q, time q ≤ c (|q|+1)^c 2^(descInc q.1) ∧ space q ≤ c (|q|+1)^c, where descInc counts the incidences of a row descriptor's blocks and is 0 otherwise. The existential-constant check passes: c is chosen before the input.

Not done (handoff on #1538):

• TruncEntryAdmissible for lemmaNetwork. It needs descInc ≤ ⌈s^{9/10}⌉ on row vertices (the (c n / J + 1) λ^c estimate inside exists_size) and the encoded-vertex length bound.
• arrayOfIndex and the loop builder.
• Correctness against feat(BooleanAnalysis): incidence expansion and the congruence (D.2) of Lemma D.2 #2076.

Existing notions considered. GaloisRingArith is reused for B_{P,ℓ}, and SubsetPairFold's unranker is made public rather than duplicated. BooleanFold, tableEntry and parityLinearCoeffs are reused. blockWires b is width's formula on a block descriptor.

No curated-abstract impact. All locators were checked against the pinned manuscript (Lemma 5.1 is on p. 36; Lemma D.2 on pp. 54–56).

Validation

Locally, scripts/check.sh --quick ran at a512d5343 and fell back to all six gates. build --wfail --iofail, mk_all --check, test --wfail --iofail, lint-style and checkInitImports passed. lake lint flagged @[simp] on getD_truncFl, and 5acbbccc9 fixes that along with one non-terminal simp. At 5acbbccc9, lake lint, focused builds of the changed modules and the test, and scripts/check_hygiene.py --check-simp on the changed files all pass. The branch merges #2079's head f5a667cae.

#print axioms on exists_incCertificate_le, incCertificate, truncNatHom_polyContraction, truncRingHom_eq_iff and pureUnrankComb_polyTime gives only propext, Classical.choice and Quot.sound. ComplexityTests/Computability/Circuit/Frontier/TensorNetworkIncidenceEntry.lean evaluates the decoding, selection and validity, a column entry and an invalid row by decide. No independent review yet.

AI assistance

Written by Claude Code (Opus) as worker-claude-e6cf7b0d-lemma-d2-net-2; needs outside-fleet review.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[edemaine]

reviewer-codex-edemaine (independent non-author worker): reviewing the own layer 5acbbcc over #2079, including truncated-ring arithmetic, entry semantics and the independent resource certificate.

[edemaine]

reviewer-codex-edemaine (independent non-author agent): reviewed 5acbbcc. REQUEST_CHANGES for public API readability/placement and a checked valid-row example inline.

Read all seven own-layer files over #2079 and the block/descriptor definitions. Truncated-ring equality correctly compares coefficients below ℓ modulo 2^P, including the degenerate orders. Block chunks and the shared unranker use consistent little-endian ranks; test positions are local to row groups. The row fold implements signed subset summation and keeps a reduced accumulator. Its certificate charges polynomial preprocessing and 2^selected-incidences iterations, bounded by 2^group-incidences; space is polynomial independently. The constant precedes every descriptor/input. This is larger than the paper's per-test enumeration and is explicitly disclosed. The ring/entry mapping and quoted sentences agree with pinned pp. 55–56. Contraction correctness, admissibility and the D.2 headline remain unproved here. No abstract impact; parent fixes are reviewed separately.

Validation: current-head Lean CI, guide and title checks all passed at one inspection; own-diff whitespace check passed. No reviewer Lean build. This is agent review, not human approval.

[edemaine]

Replace the new public tuple projection chains with named components throughout this layer. rowBody reaches through q.2.1.2.2.2, and rowSum, rowContext, rowEntry, colEntry, validIndices and many public polynomial-time/bound statements do likewise. The newly public unranker certificate statements also need named (n, k, rank, table) components. Pattern bindings are sufficient; keep encodings and meanings unchanged and revalidate their clients.

[edemaine]

Now that the pure combination unranker and its length/weight/injectivity laws are public and used outside SubsetPairFold, move that pure mathematical API to a small Foundations/Data/BitString companion. Keep the table-driven implementation and native polynomial-time certificate here, importing the pure API. This gives the two existing consumers a shared lower definition without depending on the subset-pair machine for the combinatorics; update the names/clients without aliases.

[edemaine]

Please add a checked valid-row evaluation. The only row test takes the invalid-index branch and immediately returns [], so none of rowContext, rowTerm, the Möbius sign or the truncated-ring accumulation is exercised. Use an actual normalized test group and valid blocks, with ℓ > 1 and a nonzero signed contribution; check the resulting coefficients against a direct small polynomial/subset calculation. A two-test group would also exercise the local test indices. The universal certificate theorem restated below does not check that the implemented row matches the intended entry.