OAI/Combinatorics/HoneycombChords/Geometry.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CriticalHoneycomb.Center line 16

   Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:8 (same declaration text).

2. def OAI.CriticalHoneycomb.up line 18

   Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:10 (same declaration text).

3. def OAI.CriticalHoneycomb.down line 19

   Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:11 (same declaration text).

4. def OAI.CriticalHoneycomb.Adj line 22

   Source documentation

   Adjacency across a full triangular edge.

   Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:14 (same declaration text).

   def Adj (v w : Center) : Prop :=
   …

   Mentions: OAI.CriticalHoneycomb.Center

5. def OAI.CriticalHoneycomb.rowSpacing line 32

   Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:24 (same declaration text).

6. def OAI.CriticalHoneycomb.centerPosition line 35

   Source documentation

   The fixed Euclidean embedding in the unit triangular tiling.

   Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:27 (same declaration text).

   noncomputable def centerPosition (v : Center) : ℝ × ℝ :=
   …

   Mentions: OAI.CriticalHoneycomb.Center

7. structure OAI.CriticalHoneycomb.Port line 44

   Source documentation

   A midpoint port, oriented into the triangle domain.

   Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:36 (same declaration text).

   structure Port (D : Set Center) where
   …

   Mentions: OAI.CriticalHoneycomb.Center

8. def OAI.CriticalHoneycomb.Port.position line 51

   Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:43 (same declaration text).

9. def OAI.CriticalHoneycomb.IsTrace line 56

   Source documentation

   A simple center trace, with no premature boundary exit.

   Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:48 (same declaration text).

   def IsTrace (D : Set Center) (p : List Center) : Prop :=
   …

   Mentions: OAI.CriticalHoneycomb.Center

10. def OAI.CriticalHoneycomb.Chord line 59
11. def OAI.CriticalHoneycomb.kappa line 63

    Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:51 (same declaration text).

12. def OAI.CriticalHoneycomb.weight line 66

    Source documentation

    Length counts centers; the port half-edges contribute no factors.

    Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:54 (same declaration text).

    noncomputable def weight (p : List Center) : ℝ≥0∞ :=
    …

    Mentions: OAI.CriticalHoneycomb.Center

13. def OAI.CriticalHoneycomb.chordMass line 69
14. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.adj_symmetric line 78
15. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.adj_irrefl line 82
16. abbrev OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.Interior line 86
17. abbrev OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.Vertices line 87
18. def OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.portInside line 89
19. def OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.hardWallGraph line 92
20. structure OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.Configuration line 115

    Source documentation

    All hard-wall, unoriented 0/2-degree configurations with the two specified ports occupied. This is finite graph data, not a probabilistic input.

    structure Configuration (D : Finset Center) (a b : Port (D : Set Center)) where
    …

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port

21. theorem OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.configuration_contains_chord line 125

    Source documentation

    The unique open component supplied by a local physical configuration is an actual source center trace, with no other exit and with no repeated center. Only the additionally detached cycle graph remains.

    theorem configuration_contains_chord {D : Finset Center} {a b : Port (D : Set Center)}
        (C : Configuration D a b) :
        ∃ (γ : Chord (D : Set Center) a b) (xs : List (Interior D))
          (p : C.graph.Walk (.inr false) (.inr true)),
          xs.map Subtype.val = γ.val ∧ p.IsPath ∧
          p.support = Sum.inr false :: (xs.map Sum.inl ++ [Sum.inr true]) ∧
          (C.graph \ p.toSubgraph.spanningCoe).IsCycles := by
    …

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.Configuration, OAI.CriticalHoneycomb.Chord, OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.Interior

22. theorem OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.chord_has_hardWall_path line 169

    Source documentation

    Conversely, every actual center chord determines a simple path in the hard-wall graph with the exact two specified boundary markers.

    theorem chord_has_hardWall_path {D : Finset Center} {a b : Port (D : Set Center)}
        (γ : Chord (D : Set Center) a b) :
        ∃ (xs : List (Interior D))
          (p : (hardWallGraph D a b).Walk (.inr false) (.inr true)),
          xs.map Subtype.val = γ.val ∧ p.IsPath ∧
          p.support = Sum.inr false :: (xs.map Sum.inl ++ [Sum.inr true]) := by
    …

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Chord, OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.Interior, OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.hardWallGraph

23. abbrev OAI.CriticalHoneycomb.Wire line 211

    Source documentation

    A full triangular edge indexed from its up-triangle side: middle, south, west. All tensor wires are actual edges, not abstract crossings.

    abbrev Wire := ℤ × ℤ × Fin 3

24. def OAI.CriticalHoneycomb.neighbor line 213
25. def OAI.CriticalHoneycomb.incidentWire line 217
26. lemma OAI.CriticalHoneycomb.neighbor_neighbor line 221
27. lemma OAI.CriticalHoneycomb.neighbor_ne line 225
28. lemma OAI.CriticalHoneycomb.neighbor_injective line 229
29. lemma OAI.CriticalHoneycomb.incidentWire_neighbor line 234
30. lemma OAI.CriticalHoneycomb.incidentWire_injective line 239
31. lemma OAI.CriticalHoneycomb.incidentWire_eq_iff line 244
32. lemma OAI.CriticalHoneycomb.adj_iff_neighbor line 251
33. def OAI.CriticalHoneycomb.Port.side line 256
34. lemma OAI.CriticalHoneycomb.Port.neighbor_side line 259
35. def OAI.CriticalHoneycomb.Port.wire line 263
36. lemma OAI.CriticalHoneycomb.Port.wire_eq_incident line 268

    Source documentation

    A selected exterior midpoint may become a prescribed boundary vertex only at its original inside center.

    lemma Port.wire_eq_incident {D : Set Center} (p : Port D) {v : Center} (hv : v∈D)
        {k : Fin 3} (h : incidentWire v k=p.wire) : v=p.inside ∧ k=p.side := by
    …

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.incidentWire

37. lemma OAI.CriticalHoneycomb.Port.wire_ext line 278
38. def OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.portAt line 290
39. def OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.BoundarySelection line 294

    Source documentation

    Occupied actual midpoint edges, with only the two prescribed exits.

    def BoundarySelection {D : Finset Center} (a b : Port (D : Set Center))
        (s : Wire → Bool) : Prop :=
    …

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Wire

40. def OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.selectedRel line 300
41. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.selectedRel_symm line 307
42. def OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.selectedGraph line 321
43. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.selectedGraph_allowed line 331
44. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.selectedGraph_port_neighbors line 343
45. def OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.sideNeighbor line 355

    Source documentation

    The neighbor of a center represented by one of its three actual edges.

    def sideNeighbor {D : Finset Center} (a b : Port (D : Set Center))
        (v : Interior D) (k : Fin 3) : Vertices D → Prop
      | .inl w => neighbor v.val k = w.val
      | .inr q => v.val=(portAt a b q).inside ∧ k=(portAt a b q).side

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Transfer.v, OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.Interior, OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.Vertices, OAI.CriticalHoneycomb.neighbor, OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.portAt

46. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.sideNeighbor_side_unique line 360
47. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.sideNeighbor_neighbor_unique line 367
48. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.selected_side_has_neighbor line 386
49. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.sideNeighbor_adj line 396
50. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.adj_sideNeighbor line 406
51. def OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.centerNeighborEquiv line 424

    Source documentation

    Selected geometric sides and selected graph neighbors are in exact bijection; the hard-wall condition is used only for the missing exterior neighbors. Distinct ports may share an inside center.

    noncomputable def centerNeighborEquiv {D : Finset Center} (a b : Port (D : Set Center))
        (hab : a≠b) (s : Wire → Bool) (hs : BoundarySelection a b s) (v : Interior D) :
        {k : Fin 3 // s (incidentWire v.val k)=true} ≃
          (selectedGraph a b s).neighborSet (.inl v) := by
    …

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Wire, OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.BoundarySelection, OAI.CriticalHoneycomb.Transfer.v, OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.Interior, OAI.CriticalHoneycomb.incidentWire, OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.selectedGraph

52. def OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.selectedSideCount line 451
53. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.selectedSideCount_eq_card line 454
54. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.selectedGraph_center_degree line 462
55. def OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.configurationOfSides line 472

    Source documentation

    The exact local 0/2 rule, rather than an assumed path partition, gives an admissible finite configuration on the actual honeycomb graph.

    noncomputable def configurationOfSides {D : Finset Center} (a b : Port (D : Set Center))
        (hab : a≠b) (s : Wire → Bool) (hs : BoundarySelection a b s)
        (hdeg : ∀ v∈D, selectedSideCount s v=0 ∨ selectedSideCount s v=2) :
        Configuration D a b where
    …

    Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Port, OAI.CriticalHoneycomb.Wire, OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.BoundarySelection, OAI.CriticalHoneycomb.Transfer.v, OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.selectedSideCount, OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.Configuration