Directed forcing forces a homomorphism to the edge (Proposition 23)
DisprovedDirS.dir_force_needs_edgeProposition 23 of the paper: if the oriented graph B has the directed forcing property, then B has a homomorphism to the directed edge K_2. The proof argues with the one-parameter family of graphons W^(lambda) of Figure 1: the mean of each is 1/16, and if B has no homomorphism to the edge, the B-density moves continuously from at most (1/16)^{e(B)} at lambda = 0 to (1/2)^{v(B)} (1/4)^{e(B)} at lambda = 1, so some lambda_0 realizes the random value while the kernel is not constant, contradicting forcing. In the mission the forcing hypothesis is the finitary epsilon-delta form, and the contradiction is reached by realizing the witnesses G_n of the approximation scheme on the non-constant kernels.
Formalization Note The continuity argument over lambda is the analytic core here; the reflection of the sequential definition in the finitary form is what lets the proof consume only finite graphs and the approximation data.
import Mathlib import Definitions.Def_DirS_gr import Definitions.Def_DirS_gw
namespace DirS
/-! Milestone 5 (Proposition 23): directed forcing forces a homomorphism
to the edge. If the oriented graph B has the directed forcing property,
then B has a homomorphism to the directed edge K_2. The proof of the
paper argues with the one-parameter family of graphons W^(lambda): if B
has no homomorphism to the edge, a continuity argument produces a value of
lambda at which the B-density matches the random value while the kernel is
not constant, contradicting forcing. -/
theorem dir_force_needs_edge {m : ℕ} (B : OriGraph m) (h : DirForcing B) :
homToEdge 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 admits a Boolean colouring of its vertices such that every edge goes from a false-coloured vertex to a true-coloured vertex. No other hypotheses appear.
False as stated because DirForcing is trivially true (see DirS_gr): the directed path 0 → 1 → 2 satisfies DirForcing and has no homomorphism to the directed edge. The platform already records an accepted disproof.