Shadows, Rupert pairs and the separation criterion

shadow R is the projection of the Noperthedron under the matrix R. A Rupert pair (Ro, Ri) has the closure of the inner shadow inside the interior of the outer one. We reduce IsRupert exactVerts to the existence of a Rupert pair of rotations (using the existing offset-removal argument), and prove the only non-Rupert criterion the checker uses: an inner vertex that no outer vertex beats in some direction w ≠ 0.

noncomputable def Cayley.shadow (R : Matrix (Fin 3) (Fin 3) ℝ) : Set Euc(2)

The shadow of the Noperthedron under R.

Equations

• Cayley.shadow R = (fun (p : Euc(3)) => proj_xyL ((Matrix.toEuclideanLin R) p)) '' Noperthedron.exactHull

def Cayley.RupPair (Ro Ri : Matrix (Fin 3) (Fin 3) ℝ) : Prop

A Rupert passage with outer rotation Ro and inner rotation Ri (offset zero).

Equations

• Cayley.RupPair Ro Ri = (closure (Cayley.shadow Ri) ⊆ interior (Cayley.shadow Ro))

theorem Cayley.rupert_set_implies_pose_rupert' {S : Set Euc(3)} (r : IsRupertSet S) : ∃ (p : MatrixPose), RupertPose p S

Copied from NoperthedronIsNotRupert.lean (it lives there next to the trig proof).

theorem Cayley.exists_rupPair (h : IsRupert Noperthedron.exactVerts) : ∃ Ro ∈ SO3, ∃ Ri ∈ SO3, RupPair Ro Ri

def Cayley.lin (w0 w1 : ℝ) (x : Fin 3 → ℝ) : ℝ

The linear functional x ↦ w₀ x₀ + w₁ x₁ on the first two coordinates.

Equations

• Cayley.lin w0 w1 x = w0 * x 0 + w1 * x 1

theorem Cayley.exactVertex_mem_hull (S : Noperthedron.VertexIndex) : Noperthedron.exactVertex S ∈ Noperthedron.exactHull

theorem Cayley.proj_xy_mat_mulVec_mul (R : Matrix (Fin 3) (Fin 3) ℝ) (x : Fin 3 → ℝ) : (proj_xy_mat * R).mulVec x 0 = R.mulVec x 0 ∧ (proj_xy_mat * R).mulVec x 1 = R.mulVec x 1

theorem Cayley.not_rupPair_of_sep (Ro Ri : Matrix (Fin 3) (Fin 3) ℝ) (S : Noperthedron.VertexIndex) (w0 w1 : ℝ) (hw : w0 ≠ 0 ∨ w1 ≠ 0) (h : ∀ (T : Noperthedron.VertexIndex), lin w0 w1 (Ro.mulVec (Noperthedron.exactVertex T).ofLp) ≤ lin w0 w1 (Ri.mulVec (Noperthedron.exactVertex S).ofLp)) : ¬RupPair Ro Ri

The separation criterion.