;;
;; Parameters
;;

(define $x [| φ θ ψ y α |])

;;
;; Riemann metric of S2 x S3
;;

(define $g__
  [|[| (/ (+ (* 3 '(+ 1 (* -1 y))^2 (sin θ)^2 '(+ a (* -1 y^2))) (* 2 '(+ a (* -3 y^2) (* 2 y^3)) (cos θ)^2 '(+ 1 (* -1 y))) (* '(+ a (* -2 y) y^2)^2 (cos θ)^2)) (* 18 '(+ a (* -1 y^2)) '(+ 1 (* -1 y)))) 0 (/ (+ (* -2 '(+ a (* -3 y^2) (* 2 y^3)) (cos θ) '(+ 1 (* -1 y))) (* -1 '(+ a (* -2 y) y^2)^2 (cos θ))) (* 18 '(+ a (* -1 y^2)) '(+ 1 (* -1 y)))) 0 (/ (* -1 '(+ a (* -2 y) y^2) (cos θ)) (* 3 '(+ 1 (* -1 y)))) |]
    [| 0 (/ '(+ 1 (* -1 y)) 6) 0 0 0 |]
    [| (/ (+ (* -2 '(+ a (* -3 y^2) (* 2 y^3)) (cos θ) '(+ 1 (* -1 y))) (* -1 '(+ a (* -2 y) y^2)^2 (cos θ))) (* 18 '(+ a (* -1 y^2)) '(+ 1 (* -1 y)))) 0 (/ (+ (* 2 '(+ a (* -3 y^2) (* 2 y^3)) '(+ 1 (* -1 y))) '(+ a (* -2 y) y^2)^2) (* 18 '(+ a (* -1 y^2)) '(+ 1 (* -1 y)))) 0 (/ (* 1 '(+ a (* -2 y) y^2)) (* 3 '(+ 1 (* -1 y)))) |]
    [| 0 0 0 (/ '(+ 1 (* -1 y)) (* 2 '(+ a (* -3 y^2) (* 2 y^3)))) 0 |]
    [| (/ (* -1 '(+ a (* -2 y) y^2) (cos θ)) (* 3 '(+ 1 (* -1 y)))) 0 (/ (* 1 '(+ a (* -2 y) y^2)) (* 3 '(+ 1 (* -1 y)))) 0 (/ (* 2 '(+ a (* -1 y^2))) '(+ 1 (* -1 y))) |]
    |]_#_#)

(define $g~~ (M.inverse g_#_#))
g~#~#

;;
;; Christoffel symbols of the first kind
;;

(define $Γ_j_k_l
  (* (/ 1 2)
     (+ (∂/∂ g_j_l x~k)
        (∂/∂ g_j_k x~l)
        (* -1 (∂/∂ g_k_l x~j)))))

Γ_#_#_#

;;
;; Christoffel symbols of the second kind
;;

(define $Γ~__ (with-symbols {i} (. g~#~i Γ_i_#_#)))

Γ~#_#_#

;;
;; Riemann curvature tensor
;;

(define $R~i_j_k_l
  (with-symbols {m}
    (+ (- (∂/∂ Γ~i_j_l x~k) (∂/∂ Γ~i_j_k x~l))
       (- (. Γ~m_j_l Γ~i_m_k) (. Γ~m_j_k Γ~i_m_l)))))

R~#_#_#_#

;;
;; Ricci curvature
;;

(define $Ric__ (with-symbols {i} (contract + R~i_#_i_#)))
Ric_#_#

(expand-all' (with-symbols {i j} (-' Ric_i_j (*' 4 g_i_j))))
;[| [| 0 0 0 0 0 |] [| 0 0 0 0 0 |] [| 0 0 0 0 0 |] [| 0 0 0 0 0 |] [| 0 0 0 0 0 |] |]

;;
;; Wodzicki-Chern-Simons class
;;

(define $ret (let {[[$es $os] (even-and-odd-permutations 5)]}
               (- (sum' (map (lambda [$σ] (.' R~u_5_s_(σ 1) R~s_t_(σ 3)_(σ 2) R~t_u_(σ 5)_(σ 4))) es))
                  (sum' (map (lambda [$σ] (.' R~u_5_s_(σ 1) R~s_t_(σ 3)_(σ 2) R~t_u_(σ 5)_(σ 4))) os)))))

(define $ret2 (/ (expand-all' (numerator ret)) (denominator ret)))

ret2
;(/ (+ (* -128 a^6 y (sin θ)) (* 832 a^5 y^3 (sin θ)) (* -2240 a^4 y^5 (sin θ)) (* 3200 a^3 y^7 (sin θ)) (* -2560 a^2 y^9 (sin θ)) (* 1088 a y^11 (sin θ)) (* 384 a^6 y^2 (sin θ)) (* -1984 a^5 y^4 (sin θ)) (* 4160 a^4 y^6 (sin θ)) (* -4480 a^3 y^8 (sin θ)) (* 2560 a^2 y^10 (sin θ)) (* -704 a y^12 (sin θ)) (* -704 a^6 y^3 (sin θ)) (* 2560 a^5 y^5 (sin θ)) (* -4480 a^4 y^7 (sin θ)) (* 4160 a^3 y^9 (sin θ)) (* -1984 a^2 y^11 (sin θ)) (* 384 a y^13 (sin θ)) (* 1088 a^6 y^4 (sin θ)) (* -2560 a^5 y^6 (sin θ)) (* 3200 a^4 y^8 (sin θ)) (* -2240 a^3 y^10 (sin θ)) (* 832 a^2 y^12 (sin θ)) (* -128 a y^14 (sin θ)) (* -960 a^6 y^5 (sin θ)) (* 1920 a^5 y^7 (sin θ)) (* -1920 a^4 y^9 (sin θ)) (* 960 a^3 y^11 (sin θ)) (* -192 a^2 y^13 (sin θ)) (* 320 a^6 y^6 (sin θ)) (* -640 a^5 y^8 (sin θ)) (* 640 a^4 y^10 (sin θ)) (* -320 a^3 y^12 (sin θ)) (* 64 a^2 y^14 (sin θ)) (* 64 y^14 (sin θ)) (* 64 a^7 y (sin θ)) (* -192 a^7 y^2 (sin θ)) (* 192 a^7 y^3 (sin θ)) (* -64 a^7 y^4 (sin θ)) (* -192 a^5 (sin θ) y^2) (* 960 a^4 (sin θ) y^4) (* -1920 a^3 (sin θ) y^6) (* 1920 a^2 y^8 (sin θ)) (* -960 a y^10 (sin θ)) (* -320 y^3 a^4 (sin θ)) (* 640 y^5 a^3 (sin θ)) (* -640 y^7 a^2 (sin θ)) (* 320 y^9 a (sin θ)) (* -64 y^11 (sin θ)) (* 192 y^12 (sin θ)) (* 64 a^5 y (sin θ)) (* -192 y^13 (sin θ))) (* 3 '(+ 1 (* -1 y))^8 '(+ a (* -1 y^2))^5))

(define $ret3 (/ (2#%1 (P./ (numerator ret2) (* (+ 1 (* -1 y))^3 (+ a (* -1 y^2))^5) y))
                 (/ (denominator ret2) (* '(+ 1 (* -1 y))^3 '(+ a (* -1 y^2))^5))))

ret3
;(/ (+ (* 128 a (sin θ) y) (* -64 a^2 (sin θ) y) (* -64 (sin θ) y)) (* 3 '(+ 1 (* -1 y))^5))