9. Main Theorems🔗

Theorem9.1

uses 1used by 1✓L∃∀N

There does not in fact exist a noperthedron Rupert 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 Theorem9.1●1 theorem

theoremdefined in Noperthedron/NoperthedronIsNotRupert.lean

complete

theorem Noperthedron.no_nopert_tight_pose (vtab : Solution.ValidTable) :
  ¬∃ v, tightInterval.contains v ∧ RupertPose v exactPolyhedron.hull

theorem Noperthedron.no_nopert_tight_pose
  (vtab : Solution.ValidTable) :
  ¬∃ v,
      tightInterval.contains v ∧
        RupertPose v exactPolyhedron.hull

There is no tight pose that makes the Noperthedron have the Rupert property

Proof for Theorem 9.1

Proof uses 2

Proof dependency previews

Preview

Theorem 8.1

Loading preview

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

By this theorem, there is a valid solution table containing a valid row whose pose interval is a superset of the 5-dimensional interval above. By this theorem, there is no Rupert solution in that interval.

Theorem9.2

Group: Reductions from general poses to certified subcases. (2)

Group member previews

Preview

Theorem 9.3

Loading preview

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

uses 0used by 1✓L∃∀N

There is no 5-parameter pose that makes the noperthedron have the Rupert property.

Lean code for Theorem9.2●1 theorem

theoremdefined in Noperthedron/NoperthedronIsNotRupert.lean

complete

theorem Noperthedron.no_nopert_pose (vtab : Solution.ValidTable) :
  ¬∃ v, RupertPose v exactPolyhedron.hull

theorem Noperthedron.no_nopert_pose
  (vtab : Solution.ValidTable) :
  ¬∃ v, RupertPose v exactPolyhedron.hull

There is no pose that makes the Noperthedron have the Rupert property

Proof for Theorem 9.2

Proof uses 2

Proof dependency previews

Preview

Corollary 2.2.2

Loading preview

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

Theorem Theorem 9.1 says there is no tight pose that makes the noperthedron Rupert. Corollary Corollary 2.2.2 says that this suffices for the general case.

Theorem9.3

Group: Reductions from general poses to certified subcases. (2)

Group member previews

Preview

Theorem 9.2

Loading preview

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

uses 0used by 1✓L∃∀N

There is no purely rotational pose that makes the noperthedron have the Rupert property.

Lean code for Theorem9.3●1 theorem

theoremdefined in Noperthedron/NoperthedronIsNotRupert.lean

complete

theorem Noperthedron.no_nopert_rot_pose (vtab : Solution.ValidTable) :
  ¬∃ p, RupertPose p.zeroOffset exactPolyhedron.hull

theorem Noperthedron.no_nopert_rot_pose
  (vtab : Solution.ValidTable) :
  ¬∃ p,
      RupertPose p.zeroOffset
        exactPolyhedron.hull

There is no purely rotational pose that makes the Noperthedron have the Rupert property

Proof for Theorem 9.3

Proof uses 2

Proof dependency previews

Preview

Theorem 4.2.1

Loading preview

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

Suppose there were a purely rotational pose. Then convert that to an equivalent 5-parameter pose with Theorem Theorem 4.2.1 and appeal to Theorem Theorem 9.2.

Theorem9.4

Group: Reductions from general poses to certified subcases. (2)

Group member previews

Preview

Theorem 9.2

Loading preview

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

uses 0used by 1✓L∃∀N

There is no pose that makes the noperthedron have the Rupert property.

Lean code for Theorem9.4●1 theorem

theoremdefined in Noperthedron/NoperthedronIsNotRupert.lean

complete

theorem Noperthedron.no_nopert_matrix_pose (vtab : Solution.ValidTable) :
  ¬∃ p, RupertPose p exactPolyhedron.hull

theorem Noperthedron.no_nopert_matrix_pose
  (vtab : Solution.ValidTable) :
  ¬∃ p, RupertPose p exactPolyhedron.hull

There is no pose that makes the Noperthedron have the Rupert property

Proof for Theorem 9.4

Proof uses 3

Proof dependency previews

Preview

Lemma 2.1.9

Loading preview

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

By Theorem Theorem 4.3.1, we need only show that the noperthedron is pointsymmetric to see that if it is Rupert, then it must be Rupert via a purely rotational pose. But Lemma Lemma 2.1.9 shows exactly this. And yet we know via Theorem Theorem 9.3 that the noperthedron is not rotationally Rupert, so we have a contradiction, hence the noperthedron has no pose that makes it Rupert.

Theorem9.5

groupuses 1used by 1✓L∃∀N

The noperthedron is not a Rupert set.

Lean code for Theorem9.5●1 theorem

theoremdefined in Noperthedron/NoperthedronIsNotRupert.lean

complete

theorem Noperthedron.nopert_not_rupert_set (vtab : Solution.ValidTable) :
  ¬IsRupertSet exactPolyhedron.hull

theorem Noperthedron.nopert_not_rupert_set
  (vtab : Solution.ValidTable) :
  ¬IsRupertSet exactPolyhedron.hull

The Noperthedron (as a subset of ℝ³) is not Rupert

Proof for Theorem 9.5

uses 1

By Theorem Theorem 9.4, there is no pose that makes the noperthedron a Rupert set.

Theorem9.6

groupuses 0used by 0✓L∃∀N

The noperthedron is not a Rupert polyhedron.

Lean code for Theorem9.6●1 theorem

theoremdefined in Noperthedron/NoperthedronIsNotRupert.lean

complete

theorem Noperthedron.nopert_not_rupert (vtab : Solution.ValidTable) :
  ¬IsRupert exactVerts

theorem Noperthedron.nopert_not_rupert
  (vtab : Solution.ValidTable) :
  ¬IsRupert exactVerts

The Noperthedron is not Rupert.

Proof for Theorem 9.6

Proof uses 2

Proof dependency previews

Preview

Theorem 4.1.1

Loading preview

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

By Theorem 4.1.1, it suffices to show that the convex hull of noperthedron vertices is not a Rupert set, which is exactly the previous theorem.