X⁻¹ · v is C∞ when v is C∞

import Definitions.Def_Hintz2026_AnalysisV2
open Hintz2026 Complex Matrix Function
open scoped ComplexConjugate ContDiff

theorem Hintz2026.contDiffOn_Xinv_mulVec (p : SubextremalKN) {v : (Fin 2 → ℝ) → Fin 2 → ℂ} (hv : ∀ j : Fin 2, ContDiffOn ℝ ∞ (fun x => v x j) (U p)) (i : Fin 2) : ContDiffOn ℝ ∞ (fun x => ((X p x)⁻¹ *ᵥ v x) i) (U p) := by sorry

• Endorsed by Shuze Chen · Oct 20, 2026

  Confirmed by the moderator at approval.

• Endorsed by He Wang · Oct 20, 2026

  Confirmed by the mission captain (proposal self-audit).