Winding.lean`

90 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ArtinCAT0.TriangleMesh.passIndex line 9
Source documentation
On a collapsed triangular face the two nonconstant sides are paired; on an uncollapsed face every side is a live terminal.
```
def passIndex (v : Fin 3 → Fin 3) (i : Fin 3) : Fin 3 :=
…
```
lemma OAI.ArtinCAT0.TriangleMesh.passIndex_active line 12
lemma OAI.ArtinCAT0.TriangleMesh.passIndex_involutive line 15
lemma OAI.ArtinCAT0.TriangleMesh.passIndex_fixed_iff line 18
lemma OAI.ArtinCAT0.TriangleMesh.passIndex_reverses line 21
lemma OAI.ArtinCAT0.TriangleMesh.passIndex_cases line 25
lemma OAI.ArtinCAT0.TriangleMesh.exists_constant_side line 30
lemma OAI.ArtinCAT0.TriangleMesh.passIndex_after_constant line 33
lemma OAI.ArtinCAT0.TriangleMesh.sum_three_rotate line 36
lemma OAI.ArtinCAT0.TriangleMesh.sum_collapsed line 40
structure OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling line 62
Source documentation
Simplicial labels permit a face to map onto an edge or a vertex. The mate conditions retain the labelled side, not merely its group endpoints.
```
structure SimplicialLabeling where
…
```
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.Active line 78
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.Full line 79
abbrev OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.FullFace line 80
abbrev OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.ActiveDart line 81
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.wire line 83
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.full_active line 91
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.wire_fixed_iff line 97
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.fullDartEquiv line 105
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.ZeroEdge line 114
Source documentation
Identify the endpoints of every constant side. Quot includes the reflexive, symmetric, and transitive closure automatically.
```
def ZeroEdge (v w : V) : Prop :=
…
```
abbrev OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.CollapsedVertex line 116
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.qvertex line 118
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.qvertex_zero line 120
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.collapsed_zero line 124
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.vertex_zero line 129
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.collapsedLabel line 135
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.pass_tail_head line 137
abbrev OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.WireColor line 157
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.reverseColor line 159
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.reverseColor_involutive line 161
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.wireColor line 165
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.wireColor_mate line 169
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.wireColor_pass line 177
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.fullOrder line 189
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.fullOrder_apply line 192
abbrev OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.oldDart line 195
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.reducedMate line 197
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.reducedMate_involutive line 200
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.reducedMesh line 205
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.reducedLabeling line 217
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.expandWeight line 226
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.expandWeight_active line 230
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.expandWeight_zero line 233
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.expandWeight_mate line 236
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.expandWeight_collapsed line 246
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.expandWeight_full line 259
lemma OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.reducedMesh_exact line 266
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.signedSum line 293
theorem OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.signed_counts_zero line 299
Source documentation
The sphere-counting dependency including every simplicial degeneracy. No unproved identification of a pinched diagram with a sphere is used.
```
theorem signed_counts_zero [Fintype F] (he : M.Exact) (w : TargetTriangle → ℤ) :
    L.signedSum w = 0 := by
…
```
Mentions: OAI.ArtinCAT0.TargetTriangle
lemma OAI.ArtinCAT0.mirrorPerm_sq line 312
lemma OAI.ArtinCAT0.mirrorGenerator_sq line 317
lemma OAI.ArtinCAT0.mirrorPerm_delta_sq line 327
lemma OAI.ArtinCAT0.mirrorGenerator_delta line 335
lemma OAI.ArtinCAT0.mirrorGenerator_center line 347
lemma OAI.ArtinCAT0.mirrorLinear_mul line 381
lemma OAI.ArtinCAT0.mirrorVector_inv line 385
lemma OAI.ArtinCAT0.mirrorVector_bounded line 391
lemma OAI.ArtinCAT0.orbit_uniformly_dense line 415

lemma OAI.ArtinCAT0.orbit_chain_control line 428

Source documentation

A local bound on an orbit becomes a coarse linear global bound. The constant two only avoids a special case for zero length geodesics.

lemma orbit_chain_control (hG : GeometricAction G X) (y : X)
    {R C : ℝ} (hR : 0 ≤ R) (hC : 0 ≤ C)
    (hdense : ∀ p : X, ∃ s : G, dist p (s • y) ≤ R)
    (f : G → ℝ)
    (hlocal : ∀ s t : G, dist (s • y) (t • y) ≤ 2*R+1 → |f t-f s| ≤ C)
    (s t : G) : |f t-f s| ≤ 2*C*(1+dist (s • y) (t • y)) := by
…

abbrev OAI.ArtinCAT0.RayIndex.Point line 499
def OAI.ArtinCAT0.RayIndex.det line 501
def OAI.ArtinCAT0.RayIndex.upward line 503
def OAI.ArtinCAT0.RayIndex.edge line 505
def OAI.ArtinCAT0.RayIndex.above line 507
lemma OAI.ArtinCAT0.RayIndex.edge_self line 509
lemma OAI.ArtinCAT0.RayIndex.edge_reverse line 510
lemma OAI.ArtinCAT0.RayIndex.det_pos_of_cross_right line 512
lemma OAI.ArtinCAT0.RayIndex.det_neg_of_cross_left line 519
lemma OAI.ArtinCAT0.RayIndex.edge_right line 526
lemma OAI.ArtinCAT0.RayIndex.edge_left line 538
lemma OAI.ArtinCAT0.RayIndex.edge_high line 547
lemma OAI.ArtinCAT0.RayIndex.edge_low line 550
def OAI.ArtinCAT0.RayIndex.face line 553
lemma OAI.ArtinCAT0.RayIndex.face_eq line 555
lemma OAI.ArtinCAT0.RayIndex.face_right line 560
lemma OAI.ArtinCAT0.RayIndex.face_left line 565
lemma OAI.ArtinCAT0.RayIndex.face_high line 568
lemma OAI.ArtinCAT0.RayIndex.face_low line 571
lemma OAI.ArtinCAT0.RayIndex.corner_order_cases line 574
lemma OAI.ArtinCAT0.RayIndex.face_permute line 579
lemma OAI.ArtinCAT0.RayIndex.face_collapsed line 586
lemma OAI.ArtinCAT0.RayIndex.face_bbox line 599
Source documentation
A nonzero local edge-index sum forces the coordinate bounding box to meet both axes. This avoids a separate topological winding-number API.
```
lemma face_bbox (p : Fin 3 → Point) (hp : face p ≠ 0) :
    (∃ i, (p i).1 ≤ 0) ∧ (∃ i, 0 ≤ (p i).1) ∧
      (∃ i, (p i).2 ≤ 0) ∧ (∃ i, 0 < (p i).2) := by
…
```
Mentions: OAI.ArtinCAT0.RayIndex.Point, OAI.ArtinCAT0.RayIndex.face
lemma OAI.ArtinCAT0.RayIndex.face_local line 618
lemma OAI.ArtinCAT0.RayIndex.edge_mate line 632
lemma OAI.ArtinCAT0.RayIndex.patch_boundary_sum line 640
Source documentation
Finite Stokes cancellation on any union of faces; no manifold hypotheses are needed because the oriented edge matching is explicit.
```
lemma patch_boundary_sum (P : F → Prop) [DecidablePred P] (p : V → Point) :
    (∑ f, if P f then face (fun i => p (M.tail (f,i))) else 0) =
      ∑ d : F × Fin 3, if P d.1 ∧ ¬ P (M.mate d).1 then
        edge (p (M.tail d)) (p (M.tail (TriangleMesh.rotate d))) else 0 := by
…
```
Mentions: OAI.ArtinCAT0.RayIndex.Point, OAI.ArtinCAT0.RayIndex.face, OAI.ArtinCAT0.RayIndex.edge, OAI.ArtinCAT0.TriangleMesh.rotate
def OAI.ArtinCAT0.RayIndex.occurrence line 671
def OAI.ArtinCAT0.RayIndex.target line 673
lemma OAI.ArtinCAT0.RayIndex.occurrence_full line 676
lemma OAI.ArtinCAT0.RayIndex.occurrence_collapsed line 683
theorem OAI.ArtinCAT0.RayIndex.localized_zero line 688