Independent review: bounded-height-two RF-IDENT

Date: 2026-09-29. Verdict: no blocking mathematical gap found in the exact feasibility criterion or the stated polynomial construction, under the inherited post-T0, fixed-library model. This is a fresh model audit, not human refereeing or a priority determination. It does not classify general height-two RF-IDENT or optimize tree depth.

The reviewed phase is ../RF-IDENT Bounded Height2 2026-09-29/. All six files in its SHA256 manifest still match. Its theorem, verifier, evidence files and manifest were left unchanged. The preceding fixed-library gate was read only.

Proof reconstruction

1. Model and local legality

The inherited FORMAL_ADAPTIVE_MODEL.md, BRANCH_CANCELLATION.md, and REPAIR_GRAPH_DYNAMICS.md in the preceding gate’s research/ directory supply the precise model. Safety is assessed before the answer is conditioned on. On an answer fiber every previously added query coordinate is constant, so the current order is the original induced order on the surviving support. The original structural signature is not a free source of acquired answers.

For distinct global endpoints a,z, height at most two means precisely P={a}+M+{z} with M an antichain: a comparison between distinct middle states would give three strict inequalities. Supports therefore have only four forms: both endpoints with some middle states, one of two stars, or an antichain.

For S={a,z} union R, the relative boundary has the following forms. This reconstruction uses all comparable pairs, including a<z.

Endpoint bits	Deleted cells and boundary	Conclusion
01	No deleted cells	Safe
00	For each x with q(x)=1: edge xz and triangle axz, with a unique incidence	Identity boundary; safe
11	For each x with q(x)=0: edge ax and triangle axz, with a unique incidence	Identity boundary; safe
10	Edge az and one additional descent edge per x; one triangle per x	|R|+1 rows and |R| columns; unsafe

The equal-endpoint cases have actual identity matrices, not merely equal cell counts. Equivalently, each listed relative edge is a free face of its unique triangle and can be collapsed. The descending case remains unsafe when R is empty. Thus the full-support safe family is exactly Q_safe={q:q(a)<=q(z)}.

On a lower star {a} union R, there are no triangles, so safety requires no descent: q(a)=0 or the query is constant 1. On an upper star R union {z}, safety requires q(z)=1 or the query is constant 0. Every antichain query is safe. Consequently, a test with q(a)=1,q(z)=0 is either unsafe or constant on every support containing an endpoint. It can be useful only after both endpoints have disappeared.

2. Necessity

Two middle states with identical Q signatures cannot ever be separated. For any endpoint e and other state v, follow their common path until their first separating query. Its pre-answer support contains both e and v, so it is useful there. The preceding local result forces it to belong to Q_safe. Therefore Q_safe must distinguish each endpoint from every other state.

This argument covers arbitrary adaptive histories. It does not assume that full-support safety survives restriction.

3. Equal-endpoint peeling and the core

Let E comprise equal-endpoint tests and A the ascending tests in Q_safe. For an informative E-test, the endpoint outcome retains both endpoints and removes at least one middle state. The other outcome is an antichain. Global middle-pair separation supplies ordinary identification on each such branch: at any nonsingleton support, choose two states and a supplied test separating them, and recurse on strictly smaller supports.

A middle state in C={x: q(x)=q(a)=q(z) for every q in E} survives every peel. Any surviving state outside C has an E-test witnessing disagreement, which is still informative because both endpoints remain. Thus every terminal peeling order gives exactly {a,z} union C. There is no assumption about a favorable ordering of E.

4. Both residual stars

Endpoint separation guarantees A is nonempty. Choose any s in A after peeling. Its outcomes are {a} union C_0 and C_1 union {z}.

For x in C_0, Q_safe separates a,x. No E-test can do so by the definition of C, hence a witness r belongs to A and has r(a)=0,r(x)=1. Every such witness is safe on every lower-star restriction. Along the a branch, these tests remove all remaining leaves; every detached branch is an antichain.

For x in C_1, separation from z similarly supplies r in A with r(x)=0,r(z)=1. These safely remove all leaves along the z branch, with antichain branches on the other outcomes. Middle separation persists on all subsets. Thus both children are identifiable for every chosen s in A.

No unlisted complement, synthesized test, or global consumption rule is introduced. A used query is constant on descendants and cannot be useful again. For n>=1, the reduced tree has n singleton leaves and n-1 internal nodes. The n=0 case is a separate trivial convention.

Input validation and running time

The stated bound is valid for an explicit Boolean order matrix and query table. For n>=2, scan for a unique all-ones row a and a unique all-ones column z, require a!=z, then check every entry against

R[i,j] = (i=j) or (i=a) or (j=z).

This directly recognizes the exact class in O(n^2); a generic cubic transitivity check is unnecessary. For n=1 require its reflexive entry; n=0 is the separate trivial extension, not a poset with existing endpoints. Relabeling endpoints, if needed, costs O(n^2+mn) including the query table.

Pairwise separation scans cost O(mn^2). At each of at most n-1 internal nodes, a scan of m queries on at most n states costs O(mn). Thus decision and construction cost O(n^2+mn^2), using ordinary explicit-table access. This is an algorithmic upper bound, not a benchmark guarantee for the Python verification harness or an optimal-depth claim.

Boundary cases are consistent: n=2 requires the supplied orientation 01; an empty library fails for n>=2; a singleton requires no query. Constants and duplicate tables cannot change feasibility. The two named examples correctly demonstrate destructive legal choice and essential later use of an initially unsafe query.

Verifier audit and reproduced evidence

The original matrix_safe enumerates exactly the relative edges and triangles, computes F2 rank, and requires bijectivity. Its feasibility DP uses that predicate on the pre-answer support, with strict child shrinkage. It does not consult the theorem’s signature criterion. The constructor prioritizes all useful E-tests, then an ascending test, and uses structural safety on the remaining stars and antichains. The tree checker verifies supplied query indices, safety, outcome supports, leaves, and node count.

An unchanged copy was run under Python 3.10.11 in reproduction/:

Reproduced check	Count
Support/query matrix comparisons	87,376
Exhaustive libraries, n=2,3,4	16,452
Seeded libraries, n=5..10	9,000
Feasible libraries	20,582
Pooled protocol internal nodes	83,143

All results agree with the recorded JSON after excluding the timing field. The regenerated protocol JSON is byte-for-byte identical. The rerun took 7.788 seconds as measured internally; timing is host-dependent.

Fresh review_checks.py adds a direct elementary-collapse checker that does not call the structural rule or matrix routine to determine its own answer. Using the inherited collapse equivalence, it agrees with the original matrix routine on all 87,381 support/query cases for n=0..8. It also validates all 11 stored example protocols, comprising 50 internal nodes. These are the stored examples, not the whole pooled protocol set.

The explicit relation recognizer above agrees with an independent check of reflexivity, antisymmetry, transitivity, endpoints, and absence of a four-chain on all 4,166 reflexive Boolean relations for n=0..4. Two malformed inputs are rejected. Five singleton libraries pass the original criterion, constructor, and tree checker. These checks support, rather than replace, the proof.

Two implementation clarifications

Neither is a counterexample to the theorem or its reported n>=2 sweeps:

1. The supplied verifier is not a general explicit-order input solver. It hard-codes the canonical labelled poset from n and exposes no order matrix argument or validator. The theorem’s input-validation bound is justified above, but should not be presented as an existing feature of verify_bounded_height2.py. The review’s small recognize routine checks that step separately.
2. The empty carrier is not implemented in the original constructor. canonical_tree(0, ()) raises ValueError: negative shift count before reaching its leaf base case. Original pooled checks start at n=2. Singleton calls work. Before reusing this harness as a general solver, add a deliberate n=0 result convention and a corresponding tree-checker case, or explicitly restrict its API to n>=1 (the current sweep to n>=2).

No original files were patched: these are scope clarifications for future software packaging, and the published finite coverage already states its actual ranges. Run the original verifier without Python optimization flags because its checks use assertions.

Preserved boundaries and source check

U2’s internal-fiber order caveat, U4’s long exact sequence rather than a direct sum, and U6’s fine-measurability hypothesis remain untouched. A1’s structural-versus-acquired-data convention is retained. This proof uses neither the rejected V5-06 dimension equality nor the unrepaired V5-07 hardness argument, and retains V5-09’s ambient-complex treatment including unsupported deleted-edge rows.

The narrow comparison in AUDIT.md is supported by the introduction of Jonsson, Optimal Decision Trees on Simplicial Complexes (2005), pp. 1-2: that setup queries membership in a hidden subset or face and studies evasiveness. It is not the same specified identification model. This check does not exclude related results elsewhere and establishes no priority.

Reproduction and phase decision

From this review directory:

python reproduction\verify_bounded_height2.py
python review_checks.py

The first command rewrites only reproduction/VERIFICATION.json and reproduction/PROTOCOL_EXAMPLES.json; the second rewrites REVIEW_CHECKS.json. The saved run.log records the initial review rerun and is not regenerated by these commands. A subsequent timing change will change the reproduction verification hash in this review’s manifest, not the original phase manifest.

The audit is complete. No further computation, thread, or model run is required for this review. Defer publication integration until requested; closely related corrections can remain in this task because the proof and checks are already available. A new general-classification search is a separate optional project and is not pursued here. There were no commits, pushes, external publication, or paid services.