4. Preliminaries🔗

TODO: This whole chapter needs organization, it's just a grab bag of miscellaneous results for now.

4.1. Rupert Sets🔗

Theorem4.1.1

uses 0used by 1✓L∃∀N

The following are equivalent:

The convex polyhedron with vertex set v is Rupert.
The convex closure of v is a Rupert set.

Lean code for Theorem4.1.1●1 theorem

theoremdefined in Noperthedron/Rupert/Equivalences/RupertEquivRupertSet.lean

complete

theorem rupert_iff_rupert_set (v : Finset Euc(3)) :
  IsRupert v ↔ IsRupertSet ((convexHull ℝ) ↑v)

theorem rupert_iff_rupert_set
  (v : Finset Euc(3)) :
  IsRupert v ↔
    IsRupertSet ((convexHull ℝ) ↑v)

Proof for Theorem 4.1.1

uses 0

TODO: import this from the other repo

4.2. Poses🔗

TODO

Theorem4.2.1

uses 0used by 1✓L∃∀N

Given a pose with zero offset, there exists a 5-parameter pose that is equivalent to it.

Lean code for Theorem4.2.1●2 theorems

theoremdefined in Noperthedron/ConvertPose.lean

complete

theorem pose_of_matrix_pose (p : MatrixPose) :
  ∃ δ pp, pp.matrixPoseOfPose = p.zeroOffset.rotateBy δ

theorem pose_of_matrix_pose (p : MatrixPose) :
  ∃ δ pp,
    pp.matrixPoseOfPose =
      p.zeroOffset.rotateBy δ

For any MatrixPose p, after rotating by the right δ, there exists a Pose
that equals the rotated zeroOffset.

theoremdefined in Noperthedron/ConvertPose.lean

complete

theorem converted_pose_rupert_iff (v : Pose ℝ) (S : Set Euc(3)) :
  RupertPose v S ↔ RupertPose v.matrixPoseOfPose S

theorem converted_pose_rupert_iff (v : Pose ℝ)
  (S : Set Euc(3)) :
  RupertPose v S ↔
    RupertPose v.matrixPoseOfPose S

Proof for Theorem 4.2.1

uses 0

By putting the pose into a canonical form as a Z rotation followed by a Y followed by a Z.

4.3. Pointsymmetry and Rupertness🔗

Theorem4.3.1

uses 0used by 1✓L∃∀N

If a set is point symmetric and convex, then it being Rupert implies it being purely rotationally Rupert.

Lean code for Theorem4.3.1●1 theorem

theoremdefined in Noperthedron/CommonCenter.lean

complete

theorem rupert_implies_rot_rupert {S : Set Euc(3)} (s_sym : PointSym S)
  (s_convex : Convex ℝ S) (p : MatrixPose) (r : RupertPose p S) :
  RupertPose p.zeroOffset S

theorem rupert_implies_rot_rupert {S : Set Euc(3)}
  (s_sym : PointSym S)
  (s_convex : Convex ℝ S) (p : MatrixPose)
  (r : RupertPose p S) :
  RupertPose p.zeroOffset S

If a set is point symmetric and convex, then it being rupert implies
being purely rotationally rupert.

Proof for Theorem 4.3.1

uses 0

TODO: informalize proof