Refinement.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Matching refined crossing pieces and arc directions with truncated angle coordinates.

theorem OAI.Paper170Geometry.normalized_piece_vertex_not_crossing line 18
theorem OAI.Paper170Geometry.normalized_crossing_unique_piece line 27
theorem OAI.Paper170Geometry.openSegmentTrace_of_mem_segment_avoiding line 55
theorem OAI.Paper170Geometry.minimum_crossing_piece_unique line 64
theorem OAI.Paper170Geometry.truncated_crossing_unique_piece line 87

theorem OAI.Paper170Geometry.polygonalArcPath_piece_interval line 109

Source documentation

Every actual polygonal-chain piece is traversed along an increasing affine parameter interval.

theorem polygonalArcPath_piece_interval (v : ℕ → Plane) : ∀ n i, i<n →
    ∃a b : unitInterval, a<b ∧ ∀t : unitInterval,
      polygonalArcPath v n (intervalSegment a b t)=segmentPoint (v i) (v (i+1)) t.val
  | 0, i, hi => by omega
  | 1, i, hi => by
    have he : i=0 := by omega
…

theorem OAI.Paper170Geometry.truncated_direction_pos_mul_original line 147

Source documentation

At an actual crossing, the truncated chain and original subdivision point in the same direction.

theorem truncated_direction_pos_mul_original (N : Paper170.NormalizedDrawing graph)
    (V : VertexTruncation N.toContinuousDrawing) (e : Edge)
    (i : Fin (V.pieces e)) (k : Fin (N.polygonal e).pieces) (x : Plane)
    (hx : x∈Paper170.crossingPoints N.toContinuousDrawing)
    (hxi : x∈openSegmentTrace (V.vertices e i.val) (V.vertices e (i.val+1)))
    (hxk : x∈openSegmentTrace ((N.polygonal e).vertices k.val) ((N.polygonal e).vertices (k.val+1))) :
    ∃r : ℝ, 0<r ∧ V.vertices e (i.val+1)-V.vertices e i.val =
      r • ((N.polygonal e).vertices (k.val+1)-(N.polygonal e).vertices k.val) := by
…

Mentions: OAI.Paper170.NormalizedDrawing, OAI.Paper170Geometry.VertexTruncation

theorem OAI.Paper170Geometry.minimum_first_direction line 196
theorem OAI.Paper170Geometry.minimum_last_direction line 217
theorem OAI.Paper170Geometry.spokePort_pos_mul_outward line 249
Source documentation
The truncation port lies on the positive ray of the original outward spoke.
```
theorem spokePort_pos_mul_outward (N : Paper170.NormalizedDrawing graph)
    (V : VertexTruncation N.toContinuousDrawing) (j : Vertex) (e : IncidentEdges graph j) :
    ∃r : ℝ, 0 < r ∧ V.spokePort j e - N.vertex j = r • Paper170.outwardSpoke N j e.val := by
…
```
Mentions: OAI.Paper170.NormalizedDrawing, OAI.Paper170Geometry.VertexTruncation, OAI.Paper170Geometry.IncidentEdges, OAI.Paper170.outwardSpoke
theorem OAI.Paper170Geometry.exists_truncatedSpokeCoordinates_compatible line 297

theorem OAI.Paper170Geometry.signedIntersection_eq_of_matching_signs line 367

Source documentation

The only remaining geometric input is equality of the local oriented crossing signs.

theorem signedIntersection_eq_of_matching_signs (N : Paper170.NormalizedDrawing graph)
    (V : VertexTruncation N.toContinuousDrawing) (e f : Edge) (hef : e≠f)
    (hmatch : ∀ (i : Fin (V.pieces e)) (j : Fin (V.pieces f))
      (k : Fin (N.polygonal e).pieces) (l : Fin (N.polygonal f).pieces) (x : Plane),
      x∈openSegmentTrace (V.vertices e i.val) (V.vertices e (i.val+1)) →
      x∈openSegmentTrace (V.vertices f j.val) (V.vertices f (j.val+1)) →
      x∈openSegmentTrace ((N.polygonal e).vertices k.val) ((N.polygonal e).vertices (k.val+1)) →
      x∈openSegmentTrace ((N.polygonal f).vertices l.val) ((N.polygonal f).vertices (l.val+1)) →
      segmentCrossingSign (V.vertices e i.val) (V.vertices e (i.val+1))
        (V.vertices f j.val) (V.vertices f (j.val+1)) =
      segmentCrossingSign ((N.polygonal e).vertices k.val) ((N.polygonal e).vertices (k.val+1))
        ((N.polygonal f).vertices l.val) ((N.polygonal f).vertices (l.val+1))) :
…

Mentions: OAI.Paper170.NormalizedDrawing, OAI.Paper170Geometry.VertexTruncation

theorem OAI.Paper170Geometry.VertexTruncation.signedIntersection_eq_interiorIntersection line 468