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}.

Lean code

def C1 : Fin 3 → ℚ := (1/259375205) * ![152024884, 0, 210152163]
def C2 : Fin 3 → ℚ := (1/10^10) * ![6632738028, 6106948881, 3980949609]
def C3 : Fin 3 → ℚ := (1/10^10) * ![8193990033, 5298215096, 1230614493]

noncomputable
def C1R : EuclideanSpace ℝ (Fin 3) := WithLp.toLp 2 (fun i => C1 i)

noncomputable
def C2R : EuclideanSpace ℝ (Fin 3) := WithLp.toLp 2 (fun i => C2 i)

noncomputable
def C3R : EuclideanSpace ℝ (Fin 3) := WithLp.toLp 2 (fun i => C3 i)

Lemma2.1.1

Group: Radius and norm control for noperthedron vertices. (2)

Group member previews

Preview

Lemma 2.1.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 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.

Lemma2.1.2

Group: Radius and norm control for noperthedron vertices. (2)

Group member previews

Preview

Lemma 2.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

The radius of the Noperthedron is one.

Lean code for Lemma2.1.2●1 theorem

theoremdefined in Noperthedron/Vertices/Exact.lean

complete

theorem Noperthedron.exactVertex_radius_one : { v := exactVertex }.radius = 1

theorem Noperthedron.exactVertex_radius_one :
  { v := exactVertex }.radius = 1

The radius of the noperthedron is 1.

Proof for Lemma 2.1.2

Proof uses 4

Proof dependency previews

Lemma 2.1.1c1_c2_c3_normsproof
Lemma 2.1.7«lemma:half_nopert_verts_norm_le_one»proof
Theorem 4.3.3«thm:pointsymmetrize_pres_radius»proof
«thm:polyhedron_radius_def»«thm:polyhedron_radius_def»proof

Preview

Lemma 2.1.1

Loading preview

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

By Lemma 2.1.1, Theorem 4.3.3, [??], and Lemma 2.1.7.

Lean code

Noperthedron.exactVertex_radius_one : { v := exactVertex }.radius = 1#check exactVertex_radius_one
Noperthedron.exactVertex_norm_le_one (j : VertexIndex) : ‖exactVertex j‖ ≤ 1#check exactVertex_norm_le_one
Noperthedron.exactPoly_point_symmetric : PointSym exactPoly.hull#check exactPoly_point_symmetric

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}.

Where Steininger and Yurkevich 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 instead define

Definition2.1.3

Group: Noperthedron construction and core definitions. (3)

Group member previews

Preview

Definition 2.1.4

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

\mathcal{C}_{15} \coloneqq \left\{ R_z\left(\frac{2\pi k}{15}\right) \colon k=0,\dots,14 \right\}.

Lean code for Definition2.1.3●1 definition

defdefined in Chapters/Noperthedron.lean

complete

def NopertInline.C15 (pt : Euc(3)) : Finset Euc(3)

def NopertInline.C15 (pt : Euc(3)) :
  Finset Euc(3)

This is half of the C30 defined in \[SY25\]. In order
to see that this is pointsymmetric, it's convenient to
do explicit pointsymmetrization later.

without point-symmetricness "baked in" as it is in C_{30}. It's more convenient for the formalization to apply C_{15} to the points C_1, C_2, C_3, and then point-symmetrize that set afterwards.

Definition2.1.4

Group: Noperthedron construction and core definitions. (3)

Group member previews

Preview

Definition 2.1.3

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 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

Definition2.1.5

Group: Noperthedron construction and core definitions. (3)

Group member previews

Preview

Definition 2.1.3

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1XL∃∀N

The pointsymmetrization of a collection of vertices v_1, \ldots, v_n \in \R^3 is v_1, \ldots, v_n, -v_1, \ldots, -v_n.

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

Definition2.1.6

Group: Noperthedron construction and core definitions. (3)

Group member previews

Preview

Definition 2.1.3

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 2.1.3

Loading preview

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

Used by 5

Reverse dependency previews

Preview

Lemma 2.1.9

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 that is the pointsymmetrization of \mathcal{C}_{15} \cdot C_1 \cup \mathcal{C}_{15} \cdot C_2 \cup \mathcal{C}_{15} \cdot C_3

Lean code for Definition2.1.6●2 definitions

defdefined in Noperthedron/Vertices/Exact.lean

complete

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

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

defdefined in Noperthedron/Vertices/Exact.lean

complete

def Noperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3)

def Noperthedron.exactPolyhedron :
  Polyhedron VertexIndex Euc(3)

Lemma2.1.7

Group: Radius and norm control for noperthedron vertices. (2)

Group member previews

Preview

Lemma 2.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

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

Lean code for Lemma2.1.7●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.7

uses 0

Evident from definitions.

Lemma2.1.8

groupuses 0used by 1XL∃∀N

The pointsymmetrization of any set is point-symmetric.

Proof for Lemma 2.1.8

uses 0

Evident from definitions.

Lemma2.1.9

group

Statement uses 2

Statement dependency previews

Preview

Definition 2.1.4

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.9●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.9

uses 1

Follows from Lemma 2.1.8

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.