Rupert Counterexample

9. Main Theorems🔗

Theorem9.1
✓L∃∀Nused by 1

Using Definition 2.9.

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_poseNoperthedron.no_nopert_tight_pose (vtab : Solution.ValidTable) :
  ¬∃ v, tightInterval.contains v ∧ RupertPose v exactPolyhedron.hullThere is no tight pose that makes the Noperthedron have the Rupert property
 (vtabSolution.ValidTable : Solution.ValidTableNoperthedron.Solution.ValidTable : Type) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ vPose ℝ, tightIntervaltightInterval : PoseInterval ℝThe 5d box in parameter space that represents what constraints we can
impose on angles taking advantage of the particular symmetries of the
Noperthedron.
.containsPoseInterval.contains {R : Type} [PartialOrder R] (iv : PoseInterval R) (vp : Pose R) : Prop`iv.contains p` ↔ `p ∈ Set.Icc iv.min iv.max` ↔ `p ∈ iv`. Provided as a
named alias for legibility at call sites; `iv.contains p` and `p ∈ iv` are
definitionally equal.  vPose ℝ ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`. RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 vPose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)
    theorem Noperthedron.no_nopert_tight_poseNoperthedron.no_nopert_tight_pose (vtab : Solution.ValidTable) :
  ¬∃ v, tightInterval.contains v ∧ RupertPose v exactPolyhedron.hullThere is no tight pose that makes the Noperthedron have the Rupert property

  (vtabSolution.ValidTable : Solution.ValidTableNoperthedron.Solution.ValidTable : Type) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ vPose ℝ,
      tightIntervaltightInterval : PoseInterval ℝThe 5d box in parameter space that represents what constraints we can
impose on angles taking advantage of the particular symmetries of the
Noperthedron.
.containsPoseInterval.contains {R : Type} [PartialOrder R] (iv : PoseInterval R) (vp : Pose R) : Prop`iv.contains p` ↔ `p ∈ Set.Icc iv.min iv.max` ↔ `p ∈ iv`. Provided as a
named alias for legibility at call sites; `iv.contains p` and `p ∈ iv` are
definitionally equal.  vPose ℝ ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.
        RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 vPose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)
    There is no tight pose that makes the Noperthedron have the Rupert property
Proof

Using Theorem 8.1 and Corollary 8.5.

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)
Hover another entry in this group to preview it.
Preview
Theorem 9.3
Loading preview
Hover a group entry to preview it.
✓L∃∀Nused by 1

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_poseNoperthedron.no_nopert_pose (vtab : Solution.ValidTable) : ¬∃ v, RupertPose v exactPolyhedron.hullThere is no pose that makes the Noperthedron have the Rupert property
 (vtabSolution.ValidTable : Solution.ValidTableNoperthedron.Solution.ValidTable : Type) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ vPose ℝ, RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 vPose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)
    theorem Noperthedron.no_nopert_poseNoperthedron.no_nopert_pose (vtab : Solution.ValidTable) : ¬∃ v, RupertPose v exactPolyhedron.hullThere is no pose that makes the Noperthedron have the Rupert property

  (vtabSolution.ValidTable : Solution.ValidTableNoperthedron.Solution.ValidTable : Type) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ vPose ℝ, RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 vPose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)
    There is no pose that makes the Noperthedron have the Rupert property
Proof

Using Theorem 9.1 and Corollary 2.14.

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

Theorem9.3
Group: Reductions from general poses to certified subcases. (2)
Hover another entry in this group to preview it.
Preview
Theorem 9.2
Loading preview
Hover a group entry to preview it.
✓L∃∀Nused by 1

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_poseNoperthedron.no_nopert_rot_pose (vtab : Solution.ValidTable) : ¬∃ p, RupertPose p.zeroOffset exactPolyhedron.hullThere is no purely rotational pose that makes the Noperthedron have the Rupert property
 (vtabSolution.ValidTable : Solution.ValidTableNoperthedron.Solution.ValidTable : Type) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ pMatrixPose, RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 pMatrixPose.zeroOffsetMatrixPose.zeroOffset (p : MatrixPose) : MatrixPose exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)
    theorem Noperthedron.no_nopert_rot_poseNoperthedron.no_nopert_rot_pose (vtab : Solution.ValidTable) : ¬∃ p, RupertPose p.zeroOffset exactPolyhedron.hullThere is no purely rotational pose that makes the Noperthedron have the Rupert property

  (vtabSolution.ValidTable : Solution.ValidTableNoperthedron.Solution.ValidTable : Type) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ pMatrixPose,
      RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 pMatrixPose.zeroOffsetMatrixPose.zeroOffset (p : MatrixPose) : MatrixPose
        exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)
    There is no purely rotational pose that makes the Noperthedron have the Rupert property
Proof

Using Theorem 4.2 and Theorem 9.2.

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

Theorem9.4
Group: Reductions from general poses to certified subcases. (2)
Hover another entry in this group to preview it.
Preview
Theorem 9.2
Loading preview
Hover a group entry to preview it.
✓L∃∀Nused by 1

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_poseNoperthedron.no_nopert_matrix_pose (vtab : Solution.ValidTable) : ¬∃ p, RupertPose p exactPolyhedron.hullThere is no pose that makes the Noperthedron have the Rupert property
 (vtabSolution.ValidTable : Solution.ValidTableNoperthedron.Solution.ValidTable : Type) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ pMatrixPose, RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 pMatrixPose exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)
    theorem Noperthedron.no_nopert_matrix_poseNoperthedron.no_nopert_matrix_pose (vtab : Solution.ValidTable) : ¬∃ p, RupertPose p exactPolyhedron.hullThere is no pose that makes the Noperthedron have the Rupert property

  (vtabSolution.ValidTable : Solution.ValidTableNoperthedron.Solution.ValidTable : Type) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ pMatrixPose, RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 pMatrixPose exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)
    There is no pose that makes the Noperthedron have the Rupert property
Proof

Using Lemma 2.12, Theorem 9.3, and Theorem 4.3.

By Theorem Theorem 4.3, 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.12 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
group✓L∃∀Nused by 1

Using Definition 2.9.

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_setNoperthedron.nopert_not_rupert_set (vtab : Solution.ValidTable) : ¬IsRupertSet exactPolyhedron.hullThe Noperthedron (as a subset of ℝ³) is not Rupert
 (vtabSolution.ValidTable : Solution.ValidTableNoperthedron.Solution.ValidTable : Type) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.IsRupertSetIsRupertSet (S : Set Euc(3)) : PropThe Rupert Property for a subset S of ℝ³. S has the Rupert property if there
are rotations and translations such that one 2-dimensional "shadow" of S can
be made to fit entirely inside the interior of another such "shadow".  exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)
    theorem Noperthedron.nopert_not_rupert_setNoperthedron.nopert_not_rupert_set (vtab : Solution.ValidTable) : ¬IsRupertSet exactPolyhedron.hullThe Noperthedron (as a subset of ℝ³) is not Rupert

  (vtabSolution.ValidTable : Solution.ValidTableNoperthedron.Solution.ValidTable : Type) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.IsRupertSetIsRupertSet (S : Set Euc(3)) : PropThe Rupert Property for a subset S of ℝ³. S has the Rupert property if there
are rotations and translations such that one 2-dimensional "shadow" of S can
be made to fit entirely inside the interior of another such "shadow".  exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)
    The Noperthedron (as a subset of ℝ³) is not Rupert
Proof

Using Theorem 9.4.

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

Theorem9.6
group✓L∃∀Nused by 0

The noperthedron is not a Rupert polyhedron.

Lean code for Theorem9.6●1 theorem
  • theoremdefined in Noperthedron/NoperthedronIsNotRupert.lean
    complete
    theorem Noperthedron.nopert_not_rupertNoperthedron.nopert_not_rupert (vtab : Solution.ValidTable) : ¬IsRupert exactVertsThe Noperthedron is not Rupert.
 (vtabSolution.ValidTable : Solution.ValidTableNoperthedron.Solution.ValidTable : Type) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.IsRupertIsRupert (vertices : Finset Euc(3)) : PropThe Rupert Property for a convex polyhedron given as a finite set of vertices.  exactVertsNoperthedron.exactVerts : Finset Euc(3)
    theorem Noperthedron.nopert_not_rupertNoperthedron.nopert_not_rupert (vtab : Solution.ValidTable) : ¬IsRupert exactVertsThe Noperthedron is not Rupert.

  (vtabSolution.ValidTable : Solution.ValidTableNoperthedron.Solution.ValidTable : Type) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.IsRupertIsRupert (vertices : Finset Euc(3)) : PropThe Rupert Property for a convex polyhedron given as a finite set of vertices.  exactVertsNoperthedron.exactVerts : Finset Euc(3)
    The Noperthedron is not Rupert.
Proof

Using Theorem 4.1 and Theorem 9.5.

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