Documentation

Complexity.Foundations.Geometry.Orthogonal.PairedSpokes

Four disjoint offset spokes #

A rotational choice of one of the paired ports on each side gives four proper orthogonal spokes from the center of the square. Distinct spokes meet only at that center. These are finite certificates about entire real route supports.

Main definitions #

Main results #

References #

The finite offset star is original.

source
def Cslib.Orthogonal.PairedPorts.spokeLane (s : Fin 4) :
Fin 2

One selected lane on each side, in rotational order around the center.

Instances For
    source
    def Cslib.Orthogonal.PairedPorts.spokeElbow (s : Fin 4) :
    Point

    A spoke first travels toward its bend and then toward its selected boundary point.

    Instances For
      source
      def Cslib.Orthogonal.PairedPorts.spokeRoute (s : Fin 4) :
      Route

      A two-segment route from the center to the selected side port.

      Instances For
        source
        theorem Cslib.Orthogonal.PairedPorts.spoke_endpoints (s : Fin 4) :
        IsOrthogonal (spokeRoute s) ∧ List.head? (spokeRoute s) = some (120, 120) ∧ List.getLast? (spokeRoute s) = some (boundaryPort s (spokeLane s))

        Every spoke is proper and orthogonal with its prescribed endpoints.

        source
        theorem Cslib.Orthogonal.PairedPorts.spoke_bend_check (s : Fin 4) :
        segmentContactCheck [spokeElbow s] (120, 120) (spokeElbow s) (spokeElbow s) (boundaryPort s (spokeLane s)) = true

        The two segments of a spoke meet only at their shared bend.

        source
        theorem Cslib.Orthogonal.PairedPorts.spoke_isSimple (s : Fin 4) :
        IsSimple (spokeRoute s)

        Each spoke is simple over its full real support.

        source
        theorem Cslib.Orthogonal.PairedPorts.spokes_contact_check (s t : Fin 4) :
        s ≠ t → routeContactCheck [(120, 120)] (spokeRoute s) (spokeRoute t) = true

        Distinct spokes have only the center as an allowed continuous contact.

        source
        theorem Cslib.Orthogonal.PairedPorts.spokes_contact {s t : Fin 4} (hst : s ≠ t) {p : ℝ × ℝ} (hp : p ∈ support (spokeRoute s)) (hq : p ∈ support (spokeRoute t)) :
        p = realPoint (120, 120)

        Every real intersection of distinct spokes is their common center.