Computed examples of finite graph graphons

This file verifies the DenseGraphLimits roadmap's computed-value backstops for finite graph graphons: t(K₂, W_{K₄}) = 3/4 and t(K₃, W_{C₅}) = 0.

Main results

• TauCeti.DenseGraphLimits.homDensity_top_two_finiteGraphGraphon_top_four — the edge density of K₄;
• TauCeti.DenseGraphLimits.homDensity_top_three_finiteGraphGraphon_cycleGraph_five — C₅ is triangle-free.

References

• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Worked examples (acceptance gates).

theorem TauCeti.DenseGraphLimits.homDensity_top_two_finiteGraphGraphon_top_four : homDensity ⊤ (finiteGraphGraphon ⊤) = 3 / 4

The edge density of K₄. t(K₂, W_{K₄}) = 3/4: of the 16 ordered pairs of vertices of the complete graph on four vertices, the 12 with distinct entries are adjacent.

The roadmap's backstop value at the end of the pipeline: it pins the homomorphism count 12, the homDensityFin denominator 4 ^ 2, and the applicability of the compatibility theorem. The graphon-side integral and the cell volumes are inherited from that theorem.

theorem TauCeti.DenseGraphLimits.homDensity_top_three_finiteGraphGraphon_cycleGraph_five : homDensity ⊤ (finiteGraphGraphon (SimpleGraph.cycleGraph 5)) = 0

C₅ is triangle-free. t(K₃, W_{C₅}) = 0: no map Fin 3 → Fin 5 sends all three edges of a triangle to edges of the five-cycle, so the density vanishes exactly rather than approximately.