Directed forcing forces a homomorphism to the edge and an underlying cycle (Theorem 6)
DisprovedDirS.dir_force_needs_cycleTheorem 6 of the paper: if the oriented graph B has the directed forcing property, then B has a homomorphism to the directed edge K_2 and the underlying undirected graph of B contains a cycle. The edge half is Proposition 23 (the preceding milestone). For the cycle half, the paper observes that if the underlying graph is a forest, the density counts of B track a family that is not quasirandom - the reflected constructions of the concluding section - contradicting forcing. In the mission the conclusion is the conjunction of the homomorphism-to-edge property and the injective cyclic walk recorded by hasCycle.
Formalization Note The cycle is recorded as an injective cyclic sequence of vertices with undirected steps, which for a finite graph is equivalent to the paper's formulation through the containment of a cycle.
import Mathlib import Definitions.Def_DirS_gr import Definitions.Def_DirS_gw
namespace DirS
/-! Milestone 6 (Theorem 6): directed forcing forces a homomorphism to
the edge and an underlying cycle. If the oriented graph B has the directed
forcing property, then B has a homomorphism to the directed edge K_2 and
the underlying undirected graph of B contains a cycle. The edge half is
Proposition 23 (milestone 5); the cycle half of the paper's proof
evaluates the forcing condition on the reflected-graph family - if the
underlying graph is a forest, the density counts track a non-quasirandom
family, contradicting forcing. -/
theorem dir_force_needs_cycle {m : ℕ} (B : OriGraph m) (h : DirForcing B) :
homToEdge B ∧ hasCycle B := by sorry
end DirS
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: every oriented graph B with the directed forcing property both admits a Boolean colouring whose edges go from false to true and contains a cycle in its underlying undirected graph: there are a length k at least three and k distinct vertices whose consecutive cyclic pairs are adjacent in the underlying undirected sense. No other hypotheses appear.
False as stated for the same reason as dir_force_needs_edge; the platform already records an accepted disproof.