CenterCertificate.lean`

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem356.CenterCertificate.point line 11
Source documentation
The center and the two opposite pairs used in the local construction.
```
def point : Fin 5 → E3 :=
…
```
Mentions: OAI.Problem356.E3
theorem OAI.Problem356.CenterCertificate.point_injective line 14
def OAI.Problem356.CenterCertificate.potential line 25
Source documentation
The prescribed value of the supporting potential at each center.
```
def potential (i : Fin 5) : ℝ≥0∞ := if i = 0 then 5 / 2 else 0
```
def OAI.Problem356.CenterCertificate.Good line 28
Source documentation
A center triple belongs to one of the two intended contact families.
```
def Good (i j k : Fin 5) : Prop :=
…
```
theorem OAI.Problem356.CenterCertificate.good_iff_perm line 33
Source documentation
The finite-set characterization matches permutation of a canonical branch.
```
theorem good_iff_perm (i j k : Fin 5) :
    Good i j k ↔
      List.Perm [i, j, k] [0, 1, 2] ∨ List.Perm [i, j, k] [0, 3, 4] := by
…
```
Mentions: OAI.Problem356.CenterCertificate.Good
theorem OAI.Problem356.CenterCertificate.perm_points_of_good line 39
Source documentation
Point-valued permutation form of the good-type condition.
```
theorem perm_points_of_good (i j k : Fin 5) (h : Good i j k) :
    List.Perm [point i, point j, point k] [point 0, point 1, point 2] ∨
      List.Perm [point i, point j, point k] [point 0, point 3, point 4] := by
…
```
Mentions: OAI.Problem356.CenterCertificate.Good, OAI.Problem356.CenterCertificate.point
def OAI.Problem356.CenterCertificate.distance line 47
Source documentation
The pairwise distances of the five centers.
```
def distance (i j : Fin 5) : ℝ :=
…
```
theorem OAI.Problem356.CenterCertificate.norm_sub_point line 53
theorem OAI.Problem356.CenterCertificate.invDistance_point line 57
theorem OAI.Problem356.CenterCertificate.cross_pair_gap line 61
theorem OAI.Problem356.CenterCertificate.supporting_inequality line 75
theorem OAI.Problem356.CenterCertificate.strict_of_not_good line 96
Source documentation
Every undesired component type has a strict supporting gap at its centers.
```
theorem strict_of_not_good (i j k : Fin 5) (h : ¬ Good i j k) :
    potential i + potential j + potential k <
      coulombCost (point i, (point j, point k)) := by
…
```
Mentions: OAI.Problem356.CenterCertificate.Good, OAI.Problem356.CenterCertificate.potential, OAI.Problem356.coulombCost, OAI.Problem356.CenterCertificate.point
theorem OAI.Problem356.CenterCertificate.equality_of_good line 114
Source documentation
Both intended contact types attain equality at the centers.
```
theorem equality_of_good (i j k : Fin 5) (h : Good i j k) :
    coulombCost (point i, (point j, point k)) =
      potential i + potential j + potential k := by
…
```
Mentions: OAI.Problem356.CenterCertificate.Good, OAI.Problem356.coulombCost, OAI.Problem356.CenterCertificate.point, OAI.Problem356.CenterCertificate.potential
theorem OAI.Problem356.CenterCertificate.equality_iff_good line 131
Source documentation
The five-center supporting certificate has exactly the desired equality types.
```
theorem equality_iff_good (i j k : Fin 5) :
    coulombCost (point i, (point j, point k)) =
      potential i + potential j + potential k ↔ Good i j k := by
…
```
Mentions: OAI.Problem356.coulombCost, OAI.Problem356.CenterCertificate.point, OAI.Problem356.CenterCertificate.potential, OAI.Problem356.CenterCertificate.Good