Distinct exit directions at orthogonal drawing vertices

Two proper integer segments leaving the same vertex in the same cardinal direction overlap at a nonintegral real point. Thus incidence routes whose contacts are graph vertices must have distinct directions at any common initial vertex, including parallel listed incidences.

Main results

• nonGrid_contact_of_direction_eq: a common direction forces a nonintegral intersection.
• direction_ne_of_grid_contacts: endpoint-only geometric contacts imply distinct exits.

References

The elementary cardinal-ray separation and proofs are original.

theorem Cslib.Orthogonal.nonGrid_contact_of_direction_eq {a b c : Point} (hab : AxisAligned a b) (hac : AxisAligned a c) (hd : direction a b = direction a c) : ∃ p ∈ segment a b, p ∈ segment a c ∧ ∀ (v : Point), p ≠ realPoint v

Equal cardinal directions force a common point that is not an integer grid point.

theorem Cslib.Orthogonal.direction_ne_of_grid_contacts {a b c : Point} (hab : AxisAligned a b) (hac : AxisAligned a c) (hc : ∀ p ∈ segment a b, p ∈ segment a c → ∃ (v : Point), p = realPoint v) : direction a b ≠ direction a c

If common segment points must be integer graph vertices, two incidences cannot leave their shared initial vertex in the same direction.