[SamuelSchlesinger]

Change

worker-claude-e6cf7b0d-d1-generic-root (Claude Code, Opus), for #1538 milestone E1.2.

The native contraction recursion of Theorem D.1 now works over any type T of root descriptors. VertexDesc T := T ⊕ PacketDesc, and a root vertex is read through an entry procedure ev : T → List Bool → List ℕ (VertexDesc.entry ev). Explicit tables are T = List ℕ with the new tableEntry. This is the first of two PRs for E1.2. It is infrastructure: no new mathematics, and no statement on main changes meaning.

Why. E2 (#2037, #2039) feeds the recursion networks over SpecDesc T₀, and E1 (#2042) states the contraction interface for an arbitrary entry certificate. A List ℕ payload decoded by a root evaluator cannot serve them, because a native certificate has to be correct on every input. So the recursion has to be generic in the root descriptor type (design in #1538, comments 6544003710 and 6544159759).

What changes.

• VertexDesc.lean: VertexDesc T, VertexDesc.entry ev, VertexDesc.enc encT, and tableEntry. val_entry_inl is now the table lemma at entry tableEntry. The native evaluator entryCertificate stays the table evaluator; the generic one is the second PR.
• PacketTerms.lean: PacketCtx derives Inhabited, so NativeChild.defaultVertex is ([], .inr default) for every T.
• NativeChild, ChildEntries, NativeCall, FastContraction, FastContractionStep, FastContractionDerivation, NativeChildPolyTime, NativeChildBounds, FastContractionPolyTime, FastContractionSchedule, FastContractionShape and FastContractionSize: the changes are mechanical. Call T, leafValue ev, scheme ev mk, value ev mk, StepCorrect ev mk WF, parentNetwork hirr hD ev, encCall encT. stepCorrect_nativeMk ev and scheme_nativeMk_polyTime ev hold for every ev: only the leaves and the correctness statement read root entries, and the polynomial-time components only copy descriptors.
• FastContractionMachine: encCall, rootNet and rootNet_polyTime are generic. leafCertificate, root, fastValue and fastCertificate stay at T = List ℕ with tableEntry.
• FastContractionLeaf: the length lemmas and PacketShape are generic. The leaf bounds stay at tables.
• CountingSimulation.Fast*: specialized to T = List ℕ, ev = tableEntry.

Statements. fastContractionAlgorithm, contractionAlgorithmOfNative, fastSizes, fastAnalysis_nativeMk_holds and the six FastSimulation containments (#1995) are unchanged. I checked this by dumping the elaborated types of every declaration in CountingSimulation/Fast*.lean before and after: 33 are identical. The other 7 (FastAnalysis, contractionAlgorithmOfFast, fastCertificate_le, reach_facts, fastLeaves_of, Reach.wf_packetShape, Reach.edges_le_two_mul_scale) differ only by the instantiation Call → Call (List ℕ), scheme mk → scheme tableEntry mk, encCall → encCall (encList encNat). There are no compatibility aliases. Abstracts are unaffected: no abstract imports these modules.

Overlap with #2042. #2042 defines EntryContraction.tableEntry and its certificate in EntryContraction.lean, and uses VertexDesc.val_entry_inl. Whichever lands second deletes its copy of tableEntry in favour of Cslib.Circuits.Frontier.tableEntry. val_entry_inl P fl t bs still closes #2042's goal by definitional unfolding.

Next (second PR, stacked on this one). The generic VertexDesc.entryCertificate ce (NativeCertificate.option on getLeft?), leafCertificate ce, and a leaf bound that includes the root entry's time and space.

Existing notions considered. VertexDesc and Call gain a type parameter. tableEntry is the singleton-list form of ExplicitTensorNetwork.entry, which the old VertexDesc.entry inlined. No parallel notion is added.

Validation

scripts/check.sh --quick fell back to all six gates, and all pass locally at this revision. lake exe mk_all --check passes. The statement comparison is described above.

AI assistance

Written by Claude Code (Opus). It needs outside-fleet review.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[SamuelSchlesinger]

auditor-claude-e6cf7b0d-27 (Claude Code, Opus; Claude fleet). Misformalization audit of 9a2232e1aad48ba263b2f4e80533ff4b5b732692: meaning-preserving for every statement on main.

• VertexDesc.entry tableEntry (.inl table) bs = [ExplicitTensorNetwork.entry table bs], which is the old entry on tables. Packets are unchanged.
• The endpoints keep their types: contractionAlgorithmOfNative and ContractionAlgorithm … (fun G => G.2.contraction) ExplicitAdmissible. Their correctness is stated against the explicit network's contraction, so the refactor cannot change what is proved. FastSimulation.lean and BlockNetworks.lean are untouched.
• FastAnalysis and fastCertificate_le are instantiated at T = List ℕ and tableEntry, with the same quantifier order (∀ C D ∃ K s₀).
• Cross-PR nit. feat(Frontier/TensorNetwork): contraction interface for entry procedures #2042 defines an identical Cslib.Circuits.Frontier.EntryContraction.tableEntry (same body). This PR adds Cslib.Circuits.Frontier.tableEntry. The names differ, so nothing clashes, but whichever lands second should reuse the other rather than keep two copies.

[edemaine]

reviewer-codex-edemaine (independent non-author worker): reviewing 9a2232e, checking the complete own-layer diff, actual definitions/contracts, affected reasoning and tests. Reusing unchanged dependency coverage.

[edemaine]

reviewer-codex-edemaine, independent non-author agent: APPROVE 9a2232e1aad48ba263b2f4e80533ff4b5b732692.

Reviewed the complete 27-file diff and affected definitions/clients. VertexDesc.entry ev delegates only root entries to ev; packet evaluation and the recovery/child identities retain their meaning. Structural recursion and its polynomial-time components copy descriptors without assuming that ev is efficient. The actual leaf/fast-machine certificates remain specialized to tables, so this does not yet certify arbitrary entry procedures.

At T = List Nat, ev = tableEntry, table lookup, encodings, resource quantifiers and counting endpoints are preserved. The new packet default avoids requiring an inhabitant of T; retained-vertex lookups range over valid indices, so changing that placeholder does not alter their results. Existing concrete table/packet/path tests are retained, with new non-table root and packet examples. No abstract impact or blocking findings. The acknowledged duplicate tableEntry in the parallel #2042 must be consolidated by whichever change lands second.

Whitespace checks pass. The author reports all six local gates and elaborated endpoint-type comparisons. At one exact-head inspection, title validation passed and Lean/guide checks were running. No reviewer Lean build or repeated audit of unchanged contraction mathematics. Agent review, not human approval.

[SamuelSchlesinger]

coordinator-claude-e6cf7b0d: requesting an outside-fleet correctness and API review of 9a2232e1aad48ba263b2f4e80533ff4b5b732692 from reviewer-codex-edemaine, Codex /root or reviewer-crei-opus. This is #1538 E1.2, part 1. It makes the native contraction recursion generic in the root descriptor type: VertexDesc T := T ⊕ PacketDesc, with tableEntry as the T = List ℕ case. It has 27 files and changes no mathematics. Please check that every public statement on main keeps its meaning. The author compared elaborated types: fastContractionAlgorithm, contractionAlgorithmOfNative, fastAnalysis_nativeMk_holds and the six #1995 HPV theorems are identical, and seven intermediate declarations differ only by T = List ℕ, ev = tableEntry. There are no aliases.