# RF-IDENT on bounded posets of height at most two

Date: 2026-09-29. Status: proved here, with a separate matrix-based finite check;
not independently refereed and no priority claim.

## Scope and statement

Here **bounded** means that the poset has a least element a and a greatest
element z. It does not mean bounded cardinality. Height counts strict
inequalities. For n >= 2 every such poset of height at most two is exactly

    P = {a} + M + {z},

where M is an antichain, every a < x < z for x in M, and a < z is included.
Indeed a comparison between two middle elements would give a chain with three
strict inequalities. For M nonempty the height is exactly two. This includes
the three-chain and all the bottom/middle/top posets used in H5 of the earlier
gate, with **arbitrary** explicitly supplied oriented Boolean query libraries.

Fix such a library Q, with m tests, and put

    Q_safe = {q in Q : q(a) <= q(z)}.

Two states are separated by a family when at least one supplied test gives
different values on them. Then:

**Theorem.** Repair-safe identification is feasible if and only if

1. Q separates every pair of distinct states in M;
2. Q_safe separates each of a and z from every other state of P.

Equivalently, a and z are singleton signature classes for Q_safe, and all
middle-state signatures for Q are distinct. Q_safe is exactly the family safe
on the full initial poset. The theorem does **not** require Q_safe to separate
all middle pairs.

Both decision and construction of a successful identifying tree take
O(n^2 + m n^2) time by direct scans, including checking that a supplied explicit
order matrix has the stated form. A successful reduced tree has n leaves and
n-1 internal nodes. Its depth need not be optimal. Empty and singleton carriers
are trivially identifiable and handled separately.

## Proof of the local safety rule

Use the inherited one-bit relative-boundary characterization over F2, whose
collapse proof is in the earlier gate's REPAIR_GRAPH_DYNAMICS.md. For a support
S containing both endpoints, write R = S intersect M. There are only the
triangles a < x < z with x in R. Consider endpoint values:

| q(a), q(z) | Relative boundary | Safety |
|---|---|---|
| 0,1 | No deleted edges or triangles | Safe |
| 0,0 | Each x with q(x)=1 gives just descent xz and triangle axz, word 010 | Safe: identity matrix |
| 1,1 | Each x with q(x)=0 gives just descent ax and triangle axz, word 101 | Safe: identity matrix |
| 1,0 | One descent az, plus exactly one of ax,xz per x; one column per x | Unsafe: |R|+1 rows, |R| columns |

Thus q is safe on every support containing a,z if and only if q(a)<=q(z).
This also covers R empty. No count-equality shortcut is used to infer general
matrix invertibility: the safe cases exhibit the actual matrices.

If only a remains, the support is a lower star a<R, and safety means no
descent: either q(a)=0 or q is constant 1. If only z remains, it is an upper
star R<z: either q(z)=1 or q is constant 0. With neither endpoint the support
is an antichain and every query is safe. These exhaust all induced supports.

**Consequence.** A query outside Q_safe can be useful and legal only on a
support containing neither endpoint. With both endpoints it is unsafe; with
just a, legality forces it constant 1; with just z, legality forces it constant
0. Its later usefulness is confined to antichain branches.

## Necessity

Indistinguishable middle states cannot be identified by any Q-tree, proving
condition 1.

For an endpoint e and any other state v, follow their shared history until
the first query separating them. Its support contains e and v and the query
is useful. By the preceding consequence it belongs to Q_safe. Thus every
endpoint/state pair must be separated by Q_safe, proving condition 2. This
argument permits arbitrary adaptive histories and does not assume that
initial safety is hereditary.

## Sufficiency and a canonical construction

Partition Q_safe as

    E = {q : q(a)=q(z)},
    A = {q : q(a)=0, q(z)=1}.

Condition 2 for a,z implies A is nonempty. Maintain the unique branch
containing both endpoints. While some E-query is nonconstant on this branch,
ask it. It is safe by the local rule. Its opposite-to-endpoint outcome contains
only middle states, hence is an antichain; identify that branch by arbitrary
supplied separating queries from Q. Condition 1 guarantees this is possible.
The endpoint outcome retains a,z and strictly fewer middle states. Previously
asked queries are constant there, so they require no special exclusion rule.

After these peels the endpoint branch is {a,z} union C, where

    C = {x in M : q(x)=q(a)=q(z) for every q in E}.

This set is independent of the order of the informative peels. Ask any s in A.
Its children are the lower star {a} union C_0 and the upper star C_1 union {z},
where C_b = {x in C : s(x)=b}.

For each x in C_0, condition 2 supplies a Q_safe test r separating a,x.
It cannot belong to E by the definition of C. Thus r belongs to A and
r(a)=0,r(x)=1. Such tests are safe everywhere on the lower star and, along
the a outcome, eventually remove every leaf. Every detached branch is an
antichain whose states remain separated by Q. Hence this star is identifiable.

For each x in C_1, the same argument using separation of x,z gives an A-test
r with r(x)=0,r(z)=1. These safely remove every leaf along the z outcome of
the upper star, again leaving identifiable antichain branches.

This constructs an identifying tree using only actual supplied queries.
Every useful query strictly shrinks both outcome supports; therefore the
reduced tree has exactly n leaves and n-1 internal nodes. Directly scanning
m queries over at most n states at each node gives O(m n^2) construction time.
Checking the two conditions by pairwise query scans has the same bound.

## Equivalent core criterion

The same theorem says that Q must separate all states, A must be nonempty,
and for every x in C the string (q(x))_(q in A) must contain both 0 and 1.
Indeed E cannot distinguish a core state from either endpoint. A value 1 is
needed to distinguish it from a and a value 0 to distinguish it from z.
States outside C already have an E-query distinguishing them from both.

This also proves that after all E-peels, **any** ascending endpoint query is a
successful first split of the residual problem. It does not say that any
initially legal query is safe to choose first.

## Essential boundary examples

**Legal greedy choice still fails.** On a<x<z, Q={010,011}, where words list
values in that state order, both tests are initially safe. The canonical
construction asks 010, isolates x, then uses 011 on {a,z}. Asking 011 first
leaves {x,z}, where 010 is the unsafe descent 10 and 011 is constant. The
problem is feasible but this legal first choice destroys feasibility.

**Initially unsafe tests can be essential.** On a<x,y<z, use state order
(a,x,y,z) and Q={0110,0001,1100}. The first two tests are initially safe;
1100 is not. Ask 0110 to produce {a,z} and {x,y}. Use 0001 on the former and
1100 on the latter. Without 1100, x,y have identical signatures. Thus the
criterion cannot be replaced by pairwise separation under Q_safe alone.

**Both global endpoints matter.** The proof uses that every support with
both endpoints has the same simple boundary pattern and that losing either
endpoint leaves a star. It makes no assertion for arbitrary height-two posets,
for disjoint unions of these bounded posets, or for posets having only a least
or only a greatest element. General height-two RF-IDENT remains in NP with its
classification unresolved by this result. No RF-DEPTH hardness argument is used.

## Relationship to the inherited gate

This is a new subclass feasibility theorem, not a change to the completed
gate's general classification. It extends that gate's specified-library
bottom/middle/top examples to arbitrary oriented libraries on that poset class.
Its mechanism explicitly accommodates both deactivation and essential later
activation. It relies only on the verified branch-cancellation and boundary
criteria. U2's internal-fiber caveat, U4's exact-sequence terminology, U6's
fine-measurability hypothesis, A1, and V5-06/07/09 corrections are untouched.