2. The Noperthedron🔗

2.1. Definition of the Noperthedron🔗

We define three points C_1,C_2,C_3\in \mathbb{Q}^3. C_1\coloneqq \frac{1}{259375205} \begin{pmatrix} {152024884} \\ 0 \\ {210152163} \end{pmatrix}, \qquad C_2\coloneqq \frac{1}{10^{10}} \begin{pmatrix} 6632738028 \\ 6106948881 \\ 3980949609 \end{pmatrix}, C_3\coloneqq \frac{1}{10^{10}} \begin{pmatrix} 8193990033 \\ 5298215096 \\ 1230614493 \end{pmatrix}.

Lemma2.1.1

groupuses 0used by 1✓L∃∀N

\| C_1 \| = 1, {98 \over 100} < \| C_2 \| < {99 \over 100}, and {98 \over 100} < \| C_3 \| < {99 \over 100}.

Lean code for Lemma2.1.1●3 theorems

theoremdefined in Noperthedron/Vertices/Exact.lean

complete

theorem Noperthedron.c1_norm_one : ‖C1R‖ = 1

theorem Noperthedron.c1_norm_one : ‖C1R‖ = 1

theoremdefined in Noperthedron/Vertices/Exact.lean

complete

theorem Noperthedron.c2_norm_bound : ‖C2R‖ ∈ Set.Ioo (98 / 100) (99 / 100)

theorem Noperthedron.c2_norm_bound :
  ‖C2R‖ ∈ Set.Ioo (98 / 100) (99 / 100)

theoremdefined in Noperthedron/Vertices/Exact.lean

complete

theorem Noperthedron.c3_norm_bound : ‖C3R‖ ∈ Set.Ioo (98 / 100) (99 / 100)

theorem Noperthedron.c3_norm_bound :
  ‖C3R‖ ∈ Set.Ioo (98 / 100) (99 / 100)

Proof for Lemma 2.1.1

uses 0

Trivial arithmetic.

Rotations about the x, y, z axes R_x,R_y,R_z: \mathbb{R}\to \mathbb{R}^{3\times 3} are defined in the usual way: R_x(\alpha)\coloneqq \begin{pmatrix} 1 & 0 & 0\\ 0 & \cos\alpha & -\sin\alpha\\ 0 & \sin\alpha & \cos\alpha \end{pmatrix}, \hspace{1cm} R_y(\alpha)\coloneqq \begin{pmatrix} \cos\alpha & 0 & -\sin\alpha\\ 0 & 1 & 0\\ \sin\alpha & 0 & \cos\alpha \end{pmatrix}, R_z(\alpha)\coloneqq \begin{pmatrix} \cos\alpha & -\sin\alpha &0\\ \sin\alpha & \cos\alpha &0\\ 0 & 0 & 1 \end{pmatrix}.

We define a 30-element set C_{30} \mathcal{C}_{30} \coloneqq \left\{(-1)^\ell R_z\left(\frac{2\pi k}{15}\right) \colon k=0,\dots,14; \ell=0,1\right\}. of rotations.

We write \mathcal{C}_{30} \cdot P = \{c P \,\text{ for } \, c \in \mathcal{C}_{30}\} for the orbit of P under the action of \mathcal{C}_{30}.

Definition2.1.2

groupuses 0

Used by 5

Reverse dependency previews

Preview

Lemma 2.1.5

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The Noperthedron is the polyhedron given by the vertex set \mathcal{C}_{30} \cdot C_1 \cup \mathcal{C}_{30} \cdot C_2 \cup \mathcal{C}_{30} \cdot C_3.

Lean code for Definition2.1.2●1 definition

defdefined in Noperthedron/Vertices/Exact.lean

complete

def Noperthedron.exactVertex (idx : VertexIndex) : Euc(3)

def Noperthedron.exactVertex
  (idx : VertexIndex) : Euc(3)

Lemma2.1.3

groupuses 0used by 1✓L∃∀N

The norm of any vertex in the Noperthedron is no more than 1.

Lean code for Lemma2.1.3●1 theorem

theoremdefined in Noperthedron/Vertices/Exact.lean

complete

theorem Noperthedron.exactVertex_norm_le_one (j : VertexIndex) :
  ‖exactVertex j‖ ≤ 1

theorem Noperthedron.exactVertex_norm_le_one
  (j : VertexIndex) : ‖exactVertex j‖ ≤ 1

Proof for Lemma 2.1.3

uses 0

Evident from definitions.

Definition2.1.4

groupuses 0used by 1✓L∃∀N

A set S \subseteq \R^3 is point-symmetric if x \in S implies -x \in S.

Lean code for Definition2.1.4●1 definition

defdefined in Noperthedron/PointSym.lean

complete

def PointSym {n : ℕ} (A : Set Euc(n)) : Prop

def PointSym {n : ℕ} (A : Set Euc(n)) : Prop

Lemma2.1.5

Statement uses 2

Statement dependency previews

Preview

Definition 2.1.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

The noperthedron is point-symmetric.

Lean code for Lemma2.1.5●1 theorem

theoremdefined in Noperthedron/Vertices/Exact.lean

complete

theorem Noperthedron.exactPoly_point_symmetric : PointSym exactPoly.hull

theorem Noperthedron.exactPoly_point_symmetric :
  PointSym exactPoly.hull

The noperthedron is pointsymmetric.

Proof for Lemma 2.1.5

uses 0

Follows directly from the definition of the exact vertex set.

2.2. Refined Rupert's property for the Noperthedron🔗

Lemma2.2.1

groupuses 0used by 1✓L∃∀N

Let \PPP = \NOP, then for all \theta, \varphi, \alpha \in \R, the following three identities hold (as sets):

\begin{align*} M({\theta+2\pi/15,\varphi})\cdot \PPP &=M(\theta, \phi) \cdot \PPP,\\ R(\alpha+\pi)M(\theta, \phi) \cdot \PPP &=R(\alpha)M(\theta, \phi) \cdot \PPP,\\ \begin{pmatrix} 1&0\\ 0&-1 \end{pmatrix} M(\theta, \phi) \cdot \PPP&= M({\theta+\pi/15,\pi-\varphi}) \cdot \PPP. \end{align*}

Lean code for Lemma2.2.1●3 theorems

theoremdefined in Noperthedron/Tightening.lean

complete

theorem Noperthedron.Tightening.lemma7_1 (θ φ : ℝ) :
  ⇑(rotM (θ + 2 / 15 * Real.pi) φ) '' exactPolyhedron.hull =
    ⇑(rotM θ φ) '' exactPolyhedron.hull

theorem Noperthedron.Tightening.lemma7_1
  (θ φ : ℝ) :
  ⇑(rotM (θ + 2 / 15 * Real.pi) φ) ''
      exactPolyhedron.hull =
    ⇑(rotM θ φ) '' exactPolyhedron.hull

theoremdefined in Noperthedron/Tightening.lean

complete

theorem Noperthedron.Tightening.lemma7_2 (θ φ α : ℝ) :
  ⇑(rotR (α + Real.pi)) ∘ ⇑(rotM θ φ) '' exactPolyhedron.hull =
    ⇑(rotR α) ∘ ⇑(rotM θ φ) '' exactPolyhedron.hull

theorem Noperthedron.Tightening.lemma7_2
  (θ φ α : ℝ) :
  ⇑(rotR (α + Real.pi)) ∘ ⇑(rotM θ φ) ''
      exactPolyhedron.hull =
    ⇑(rotR α) ∘ ⇑(rotM θ φ) ''
      exactPolyhedron.hull

theoremdefined in Noperthedron/Tightening.lean

complete

theorem Noperthedron.Tightening.lemma7_3 (θ φ : ℝ) :
  ⇑(flip_y ∘SL rotM θ φ) '' exactPolyhedron.hull =
    ⇑(rotM (θ + Real.pi / 15) (Real.pi - φ)) '' exactPolyhedron.hull

theorem Noperthedron.Tightening.lemma7_3
  (θ φ : ℝ) :
  ⇑(flip_y ∘SL rotM θ φ) ''
      exactPolyhedron.hull =
    ⇑(rotM (θ + Real.pi / 15)
          (Real.pi - φ)) ''
      exactPolyhedron.hull

Proof for Lemma 2.2.1

uses 0

See polyhedron.without.rupert, Lemma 7.

Corollary2.2.2

groupuses 0used by 1✓L∃∀N

If the noperthedron is Rupert, then there exists a solution with

\begin{align*} \theta_1,\theta_2&\in[0,2\pi/15] \subset [0,0.42], \\ \varphi_1&\in [0,\pi] \subset [0,3.15],\\ \varphi_2&\in [0,\pi/2] \subset [0,1.58],\\ \alpha &\in [-\pi/2,\pi/2] \subset [-1.58,1.58]. \end{align*}

Lean code for Corollary2.2.2●1 theorem

theoremdefined in Noperthedron/Tightening.lean

complete

theorem Noperthedron.Tightening.rupert_tightening (p : Pose ℝ)
  (r : RupertPose p exactPolyhedron.hull) :
  ∃ p', tightInterval.contains p' ∧ RupertPose p' exactPolyhedron.hull

theorem Noperthedron.Tightening.rupert_tightening
  (p : Pose ℝ)
  (r :
    RupertPose p exactPolyhedron.hull) :
  ∃ p',
    tightInterval.contains p' ∧
      RupertPose p' exactPolyhedron.hull

Proof for Corollary 2.2.2

uses 1

See polyhedron.without.rupert, Lemma 8.