Drawing.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

Continuous graph drawings, proper spatial crossings, incidence, and endpoint properties.

abbrev OAI.Paper170.Plane line 27
Also declared: ComparatorChallenges/CompleteCrossing.lean:13 (same declaration text).
def OAI.Paper170.squaredLength line 29
def OAI.Paper170.det2 line 31
def OAI.Paper170.segmentPoint line 33
structure OAI.Paper170.Graph line 36
Source documentation
One chosen orientation of each edge of a finite simple graph.
Distinct definitions of this name: ComparatorChallenges/CompleteCrossing.lean:15 (different declaration text). Qualify references as OAI.Paper170.Graph@path.
```
structure Graph (V E : Type) where
…
```
abbrev OAI.Paper170.CompleteEdge line 43
Distinct definitions of this name: ComparatorChallenges/CompleteCrossing.lean:22 (different declaration text). Qualify references as OAI.Paper170.CompleteEdge@path.
instance OAI.Paper170.(instance at line 45) line 45
def OAI.Paper170.completeGraph line 47
Distinct definitions of this name: ComparatorChallenges/CompleteCrossing.lean:24 (different declaration text). Qualify references as OAI.Paper170.completeGraph@path.
abbrev OAI.Paper170.Graph.IncidentEdge line 63
structure OAI.Paper170.ContinuousDrawing line 68
Source documentation
Actual injective continuous edge arcs, with unrestricted routing.
Distinct definitions of this name: ComparatorChallenges/CompleteCrossing.lean:38 (different declaration text). Qualify references as OAI.Paper170.ContinuousDrawing@path.
```
structure ContinuousDrawing where
…
```
def OAI.Paper170.edgeInterior line 78
Distinct definitions of this name: ComparatorChallenges/CompleteCrossing.lean:48 (different declaration text). Qualify references as OAI.Paper170.edgeInterior@path.
structure OAI.Paper170.ProperCrossing line 82
Source documentation
A proper double crossing is locally homeomorphic to two coordinate axes.
Distinct definitions of this name: ComparatorChallenges/CompleteCrossing.lean:51 (different declaration text). Qualify references as OAI.Paper170.ProperCrossing@path.
```
structure ProperCrossing (A B : Set Plane) (x : Plane) : Prop where
…
```
Mentions: OAI.Paper170.Plane
def OAI.Paper170.crossingPoints line 89
Source documentation
Spatial intersection points. Different meetings of the same pair remain distinct.
Distinct definitions of this name: ComparatorChallenges/CompleteCrossing.lean:57 (different declaration text). Qualify references as OAI.Paper170.crossingPoints@path.
```
def crossingPoints (D : ContinuousDrawing G) : Set Plane :=
…
```
Mentions: OAI.Paper170.Plane
structure OAI.Paper170.AdmissibleDrawing line 92
Distinct definitions of this name: ComparatorChallenges/CompleteCrossing.lean:61 (different declaration text). Qualify references as OAI.Paper170.AdmissibleDrawing@path.
def OAI.Paper170.crossingCount line 101
Distinct definitions of this name: ComparatorChallenges/CompleteCrossing.lean:72 (different declaration text). Qualify references as OAI.Paper170.crossingCount@path.
def OAI.Paper170.ordinaryCrossingNumber line 104
Source documentation
The minimum spatial crossing count over admissible drawings.
Distinct definitions of this name: ComparatorChallenges/CompleteCrossing.lean:75 (different declaration text). Qualify references as OAI.Paper170.ordinaryCrossingNumber@path.
```
def ordinaryCrossingNumber (G : Graph V E) : ℕ := sInf (range (@crossingCount V E G))
```
structure OAI.Paper170.PolygonalParametrization line 107
Source documentation
A finite affine parametrization of the actual path.
```
structure PolygonalParametrization {a b : Plane} (γ : Path a b) where
…
```
Mentions: OAI.Paper170.Plane
def OAI.Paper170.PolygonalParametrization.vertices line 119
structure OAI.Paper170.NormalizedDrawing line 125
Source documentation
A convenient subdivision of a normalized drawing. Avoiding subdivision knots at crossings is additional presentation data, obtained by the normalization theorem.
```
structure NormalizedDrawing (G : Graph V E) extends AdmissibleDrawing G where
…
```
def OAI.Paper170.segmentIntersection line 134
Source documentation
Directed open-segment intersection, with the ordinary determinant sign.
```
def segmentIntersection (a b c d : Plane) : ℝ :=
…
```
Mentions: OAI.Paper170.Plane
def OAI.Paper170.interiorIntersection line 141
def OAI.Paper170.outwardSpoke line 148
def OAI.Paper170.spokeAngle line 153
structure OAI.Paper170.SpokeOrders line 158
Source documentation
The linear local orders are witnessed by the actual counterclockwise angles, with a cut in a gap. No intersection identity is part of this data.
```
structure SpokeOrders (N : NormalizedDrawing G) where
…
```
Mentions: OAI.Paper170.NormalizedDrawing
def OAI.Paper170.endpointSign line 167
def OAI.Paper170.spokeComparison line 170
def OAI.Paper170.cycleIntersection line 178
def OAI.Paper170.edgePairing line 182
def OAI.Paper170.boundary line 185
def OAI.Paper170.completeEdgeVector line 188
def OAI.Paper170.rawCycleIntersection line 192
structure OAI.Paper170.SimpleCycle line 197
Source documentation
A simple combinatorial cycle with a chosen direction of traversal.
```
structure SimpleCycle (G : Graph V E) where
…
```
def OAI.Paper170.SimpleCycle.edgeChain line 209
def OAI.Paper170.polygonIntersection line 212
structure OAI.Paper170.TransversePolygons line 217
Source documentation
Only proper interior meetings between the two polygonal walks.
```
structure TransversePolygons (v w : ℕ → Plane) (n m : ℕ) : Prop where
…
```
Mentions: OAI.Paper170.Plane
def OAI.Paper170.circleComparison line 227
def OAI.Paper170.inversion line 231
theorem OAI.Paper170Geometry.edgeInterior_subset_range line 246
theorem OAI.Paper170Geometry.edgeInterior_of_range_not_vertices line 251
theorem OAI.Paper170Geometry.edgeInterior_not_vertex line 266
theorem OAI.Paper170Geometry.crossing_of_ranges_not_vertices line 271
theorem OAI.Paper170Geometry.drawing_edge_vertex_parameter line 286
structure OAI.Paper170Geometry.FiniteIntersectionDrawing line 312
abbrev OAI.Paper170Geometry.toFiniteIntersectionDrawing line 318
instance OAI.Paper170Geometry.admissibleToFiniteIntersectionDrawing line 324
def OAI.Paper170Geometry.finiteCrossingCount line 328
theorem OAI.Paper170Geometry.finiteCrossingCount_of_admissible line 331
theorem OAI.Paper170Geometry.finiteCrossingCount_eq_ncard line 334
abbrev OAI.Paper170.AdmissibleDrawing.toFiniteIntersectionDrawing line 342
theorem OAI.Paper170Geometry.crossingCount_attainment line 361
Source documentation
A minimum exists once an actual admissible drawing has been constructed. This is the well-ordering step; construction of a drawing remains a separate obligation.
```
theorem crossingCount_attainment (D₀ : Paper170.AdmissibleDrawing graph) :
    ∃ D : Paper170.AdmissibleDrawing graph, Paper170.crossingCount D = Paper170.ordinaryCrossingNumber graph := by
…
```
theorem OAI.Paper170Geometry.ordinaryCrossingNumber_le_count line 366
theorem OAI.Paper170Geometry.crossing_incident_iff line 370

theorem OAI.Paper170Geometry.crossing_two_edges line 388

Source documentation

Every spatial crossing has exactly two incident edges; no bound is imposed on the number of points common to that edge pair.

theorem crossing_two_edges (D : Paper170.AdmissibleDrawing graph) (x : Plane)
    (hx : x ∈ Paper170.crossingPoints D.toContinuousDrawing) :
    ∃ e f : Edge, e ≠ f ∧
      ∀ g, x ∈ Paper170.edgeInterior D.toContinuousDrawing g ↔ g = e ∨ g = f := by
…

def OAI.Paper170Geometry.pairCrossings line 396
Source documentation
The actual finite set of crossing points for a specified ordered edge pair.
```
def pairCrossings (D : Paper170.AdmissibleDrawing graph) (e f : Edge) : Finset Plane :=
…
```
theorem OAI.Paper170Geometry.pairCrossings_self line 400
theorem OAI.Paper170Geometry.pairCrossings_comm line 404

theorem OAI.Paper170Geometry.crossing_ordered_incidence line 413

Source documentation

Each crossing point contributes two ordered edge pairs.

theorem crossing_ordered_incidence (D : Paper170.AdmissibleDrawing graph) (x : Plane)
    (hx : x ∈ Paper170.crossingPoints D.toContinuousDrawing) :
    (∑ e : Edge, ∑ f : Edge,
      if e ≠ f ∧ x ∈ Paper170.edgeInterior D.toContinuousDrawing e ∧
        x ∈ Paper170.edgeInterior D.toContinuousDrawing f then (1 : ℕ) else 0) = 2 := by
…

theorem OAI.Paper170Geometry.sum_pairCrossings_card line 438
Source documentation
Sum over ordered edge pairs equals twice the number of spatial crossing points.
```
theorem sum_pairCrossings_card (D : Paper170.AdmissibleDrawing graph) :
    (∑ e : Edge, ∑ f : Edge, (pairCrossings D e f).card) =
      2 * Paper170.crossingCount D := by
…
```
Mentions: OAI.Paper170Geometry.pairCrossings