Lean: make real-vector facts decidable by casting integer formulas (sign vectors, triple products)

For configurations with ±1 coordinates (cube vertices in EuclideanSpace ℝ (Fin 3)), define sgnZ : Bool → ℤ and integer versions innerZ p q, detZ p q t of the inner and triple products, and prove once by simp that ⟪sv p, sv q⟫ = (innerZ p q : ℝ) and ⟪sv p, cross (sv q) (sv t)⟫ = (detZ p q t : ℝ) (needs a lemma sgn b = (sgnZ b : ℝ)). Then statements like 'every triple of corners of every face is positively oriented' or 'neighbouring corners have inner product 1' become decide over Fin 3 × Bool and ℕ-bounded quantifiers (∀ k ≤ 3, ∀ j < k, ∀ i < j, 0 < detZ ...), closed with exact_mod_cast. This replaced 24 separate simp computations and doubles as a check that the hand-written corner ordering is really counterclockwise.