Priority Teacher Separation on Arbitrary Directed Constraint Graphs
Abstract
For arbitrary finite directed constraints, including loops, an alphabet containing neutral and separate incoming/outgoing symbols and normalized rational product site laws with every symbol mass at least a common positive rho give a positive legal normalizer, exact effective-signature classification of priority teachers, and conditioned disagreement at least rho^(dout+din+3) under uniform degree caps.
Fix a finite linearly ordered vertex type V and a finite alphabet Symbol. The formula is quantified over all data on these fixed carriers; V may be empty and no teacher triple need exist. first and last map Symbol to Bool. The distinguished symbols zero, high and low have respective (first,last) values (false,false), (false,true) and (true,false). Other symbols and their endpoint values are unrestricted. G is any directed relation on V, with loops allowed and no requirement that its arcs follow the vertex order. outgoing(G,i) and incoming(G,j) are its finite neighbor sets, bounded in cardinality by dout and din respectively.
An input x maps V to Symbol. Legal(G,first,last,x) forbids last(x(i)) and first(x(j)) from both being true on every G arc (i,j). Roles(V) contains strict triples p<q<r. teacher(first,last,t,x) returns 1 if the p-to-q endpoint gate is on, otherwise 2 if the q-to-r gate is on, and 0 otherwise. The first gate has priority even when both gates are on. edge(G,i,j) is None on a G arc and Some(i,j) otherwise; signature(G,t) is the ordered pair of those two effective edges.
FiniteResponseLaw(Symbol) is a rational, nonnegative mass function with total mass one. laws supplies one such law per vertex. The original independentSourceLaw(laws) gives each full input the product of its site masses. legalNormalizer(G,first,last,laws) sums that original product over exactly the Legal inputs. conditionedDisagreement(G,first,last,laws,t,u) divides the product mass of Legal inputs with different teacher outputs by the same normalizer. Conditioning is global, across all graph constraints at once; conditional coordinates may be dependent. The common lower bound rho>0 holds for every vertex and every alphabet symbol.
Theorem 1.1 (Positive normalizer, exact teacher classification and degree-controlled separation).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/PartialIdentification/GraphPrioritySeparation.result (✓ std3). ∎
Source. Repository-derived.
Commentary.
The all-zero-symbol configuration is legal, so its positive product mass proves normalizer positivity independently of whether Roles(V) is inhabited. A non-forbidden target pair (i,j) is forced by high at i and low at j, with endpoint assignments taking precedence. Neutral symbols at every other supported outgoing(G,i) and incoming(G,j) vertex remove new conflicts; endpoint loops are safe because high has first bit false and low has last bit false. At most one additional neutral endpoint blocks a different competing gate. The support has at most dout+din+3 vertices, counting overlaps once. This fixed assignment preserves every previously legal exterior completion. When first signatures differ, the forced first gate produces 1 versus 0 or 2. When first signatures agree but second signatures differ, the forced second source has first bit false, which closes the common first gate and produces 2 versus 0. This also constructs the witness for the pointwise equivalence.
The proof directly reuses independentSource_mass_split from FiniteIndependentSourceGrouping to split the same original product mass into the chosen support and its complement. For each completable exterior, the fixed internal assignment has product mass at least rho^(dout+din+3); its mass times the legal fiber mass is bounded by the disagreement fiber mass. Summing nonnegative exterior weights and dividing by the positive normalizer gives the bound.
A non-path application is the Widom-Rowlinson model on any finite simple undirected graph of maximum degree Delta. Replace each edge by both arcs and use the symbols empty,A,B with endpoint values (false,false),(false,true),(true,false). Legal configurations forbid adjacent A and B. For positive rational lambda, site masses are 1/(1+2lambda), lambda/(1+2lambda), lambda/(1+2lambda). Global legal conditioning yields precisely the law proportional to lambda^(number of A plus number of B), as defined in Section 1 of Cohen, Perkins and Tetali, On the Widom-Rowlinson Occupancy Fraction in Regular Graphs, arXiv:1512.06398v2. Taking rho=min(1,lambda)/(1+2lambda) gives the bound rho^(2Delta+3) for different effective teacher signatures. The graph can be a tree, grid or another bounded-degree graph; teacher gates can test non-neighboring positions.
The exponent has no optimality claim. Positive site marginals alone cannot replace the original product-law condition: the uniform mixture of the three constant empty,A,B configurations has all three marginal masses 1/3 while every A-to-B gate is off. The theorem supplies neither a learning algorithm nor a sample complexity, noise-tolerance or arbitrary correlated-source bound.