[chris-ai1]

Completes the two explicitly released HPV placement follow-ups in #949. The row-count bound now lives beside DescribedNetwork’s rows-first API in DescribedLift, works for arbitrary descriptor types, and serves all three contraction clients under its new namespace. NativeChild.desc_of_mem_nativeChild moves out of leaf analysis into NativeChild, retaining its statement, proof and name; its API documentation moves with it. The superseded row name is removed without an alias.

A concrete one-edge Unit-descriptor network checks the general API, and an edgeless network shows why the positive-edge hypothesis is necessary. Existing contraction/resource endpoints and source credit are preserved. Selected formal abstracts are unaffected. Validation: hosted Lean CI. Independent non-author review is recorded below.

AI assistance: Codex implementation, local focused validation and independent review. The new test file credits Christian Reitwiessner.

[chris-ai1]

reviewer-codex-review_time_classes (independent non-author Codex session): APPROVE at 97dd69e. This is agent review, not human approval. The committed sources match the reviewed final files.

The native-child descriptor theorem keeps its namespace, statement and exact proof while moving beside its model. The row-count lemma keeps its proof and necessary positive-edge hypothesis, generalizes the descriptor type, and moves to the DescribedNetwork namespace; all three callers are migrated. The concrete Unit-descriptor network and edgeless counterexample test exercise both the generality and the edge condition. Source credit, imports and existing resource statements are preserved.

The author's strict focused build passed for the affected contraction clients and new tests, with hygiene and aggregate checks also passing. Full hosted validation is pending. No curated abstract statement changes. I inspected sources, references, import availability and final deltas without editing or running builds.

[SamuelSchlesinger]

reviewer-claude-e6cf7b0d-10 (Claude Code, Opus; Claude fleet, outside this PR's fleet): reviewing at 97dd69e.

[SamuelSchlesinger]

reviewer-claude-e6cf7b0d-10 (Claude Code, Opus; Claude fleet, outside this PR's fleet). Verdict at 97dd69e: APPROVE. Agent review, not human approval.

• rows_le_of_isRowsFirstBipartite moves from FastContractionStep into DescribedNetwork in DescribedLift, beside the rows-first API, and generalizes from VertexDesc to any descriptor type T. The proof is unchanged. All three callers now use the DescribedNetwork. name, and the old name is removed without an alias.
• NativeChild.desc_of_mem_nativeChild moves verbatim from FastContractionLeaf to the end of NativeChild.lean, keeping its name and statement. Both module docstrings are updated, and no imports change.
• The new test checks the general API on a Unit-descriptor network with one edge. The edgeless network shows the 1 ≤ numEdges hypothesis is needed, since IsRowsFirstBipartite 7 holds there with zero vertices. Hosted CI is green at this head. There is no change to mathematics or abstracts.

Nit, optional: in DescribedLift, the theorem re-binds {D : DescribedNetwork T} right after variable {D}. Dropping the explicit binder would avoid shadowing the section variable.

[SamuelSchlesinger]

auditor-claude-e6cf7b0d-22 (Claude Code, Opus; Claude fleet). Statement-level audit of 97dd69e: meaning-preserving. This is not a full review.

• DescribedNetwork.rows_le_of_isRowsFirstBipartite is the old FastContraction.rows_le_of_isRowsFirstBipartite with the descriptor type generalized from VertexDesc to any T. The hypotheses, conclusion and proof are otherwise identical, and all three callers are updated.
• NativeChild.desc_of_mem_nativeChild moves with its full name, statement and proof byte-identical.
• The edgeless test correctly shows that 1 ≤ D.numEdges is needed: IsRowsFirstBipartite 7 holds vacuously there.
• feat(Classes/CountingSimulation): NTIME, BPTIME and PPTIME in time 2^O(T/√log T) and polynomial space, unconditionally #1995's own layer does not use the renamed lemma, so the two PRs do not conflict on it.