Theme/Fourier.lean — FrcCore

1import FrcCore.Ring2import FrcCore.Meridian3import FrcCore.Transform45/-!6# FrcCore.Theme.Fourier — the fractional family on the cycle, and the conjugate frame (the fourier theme)78The shell transform `F = i W` (`W k j = g^{jk}`, `i = −g^κ`, `Transform.lean`) has `F² = J` and `F⁴ = I` on the cycle of9`n = p − 1 = 4κ` indices. Its spectral projectors `Π_ℓ = 4⁻¹ Σ_m i^{−ℓm} F^m` (`4⁻¹ = −κ`) give the fractional family10`F^{[s]} = Σ_{ℓ<4} z^{ℓs} Π_ℓ`, `z = g⁻¹` the refinement base (6:C3). Every such combination is `c₀ I + c₁ F + c₂ J +11c₃ F J`, and the product of two is the cyclic convolution of their coefficients (`comb_mul`), so the family is a12representation of the cycle, `F^{[s+r]} = F^{[s]} F^{[r]}`, `(n)`-periodic, with the cardinal values `F^{[0]} = I`,13`F^{[κ]} = F`, `F^{[2κ]} = J`, `F^{[3κ]} = F J = F⁻¹` (`frft_add`, `frft_cardinal`). With the meridian covariance of14`Meridian.lean` this is the master's C2 (`scale_shift`). The conjugate frame `g⁻¹` has the transform `−F J` and the15projectors `Π_{ℓ+2}` (6:C9), and the Carrier's quarter-turn `ħ` has `ħ^S = ±1` when `S` is even: the master's C716(`orientation`). Task LM25 of the ledger migration. No axioms.17-/1819namespace FRC20namespace Shell21namespace Frame2223variable {p : Nat} [Pos p]2425/-! ## Ring identities for the coefficients (generated; `RE.sound`, decided by the kernel) -/2627theorem red1 {L T a X : Shell p} (h : L = T + a * X) (ha : a = 0) : L = T := by28  rw [h, ha, zero_mul, add_zero]2930theorem red2 {L T a b X Y : Shell p} (h : L = T + a * X + b * Y) (ha : a = 0) (hb : b = 0) : L = T := by31  rw [h, ha, hb, zero_mul, zero_mul, add_zero, add_zero]3233theorem frft_aux (q jj u I F J G : Shell p) :34    1 * (q * I + (q * 1) * F + (q * 1) * J + (q * 1) * G) + (1 * u) * (q * I + (q * (1 * jj)) * F + (q * ((1 * jj) * jj)) * J + (q * (((1 * jj) * jj) * jj)) * G) + ((1 * u) * u) * (q * I + (q * ((1 * jj) * jj)) * F + (q * ((((1 * jj) * jj) * jj) * jj)) * J + (q * ((((((1 * jj) * jj) * jj) * jj) * jj) * jj)) * G) + (((1 * u) * u) * u) * (q * I + (q * (((1 * jj) * jj) * jj)) * F + (q * ((((((1 * jj) * jj) * jj) * jj) * jj) * jj)) * J + (q * (((((((((1 * jj) * jj) * jj) * jj) * jj) * jj) * jj) * jj) * jj)) * G) =35      (q * (1 + u + u * u + u * u * u)) * I + (q * (1 + jj * u + -(u * u) + -(jj * (u * u * u)))) * F + (q * (1 + -u + u * u + -(u * u * u))) * J + (q * (1 + -(jj * u) + -(u * u) + jj * (u * u * u))) * G + (jj * jj + 1) * (q * jj * jj * jj * jj * jj * jj * jj * u * u * u * G + -(q * jj * jj * jj * jj * jj * u * u * u * G) + q * jj * jj * jj * jj * u * u * u * J + q * jj * jj * jj * jj * u * u * G + q * jj * jj * jj * u * u * u * G + -(q * jj * jj * u * u * u * J) + q * jj * jj * u * u * J + -(q * jj * jj * u * u * G) + q * jj * u * u * u * F + -(q * jj * u * u * u * G) + q * jj * u * G + q * u * u * u * J + q * u * u * F + -(q * u * u * J) + q * u * u * G + q * u * J) :=36  Shell.Frame.RE.sound (Shell.Frame.look [q, jj, u, I, F, J, G])37    (.add (.add (.add (.mul .one (.add (.add (.add (.mul (.var 0) (.var 3)) (.mul (.mul (.var 0) .one) (.var 4))) (.mul (.mul (.var 0) .one) (.var 5))) (.mul (.mul (.var 0) .one) (.var 6)))) (.mul (.mul .one (.var 2)) (.add (.add (.add (.mul (.var 0) (.var 3)) (.mul (.mul (.var 0) (.mul .one (.var 1))) (.var 4))) (.mul (.mul (.var 0) (.mul (.mul .one (.var 1)) (.var 1))) (.var 5))) (.mul (.mul (.var 0) (.mul (.mul (.mul .one (.var 1)) (.var 1)) (.var 1))) (.var 6))))) (.mul (.mul (.mul .one (.var 2)) (.var 2)) (.add (.add (.add (.mul (.var 0) (.var 3)) (.mul (.mul (.var 0) (.mul (.mul .one (.var 1)) (.var 1))) (.var 4))) (.mul (.mul (.var 0) (.mul (.mul (.mul (.mul .one (.var 1)) (.var 1)) (.var 1)) (.var 1))) (.var 5))) (.mul (.mul (.var 0) (.mul (.mul (.mul (.mul (.mul (.mul .one (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1))) (.var 6))))) (.mul (.mul (.mul (.mul .one (.var 2)) (.var 2)) (.var 2)) (.add (.add (.add (.mul (.var 0) (.var 3)) (.mul (.mul (.var 0) (.mul (.mul (.mul .one (.var 1)) (.var 1)) (.var 1))) (.var 4))) (.mul (.mul (.var 0) (.mul (.mul (.mul (.mul (.mul (.mul .one (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1))) (.var 5))) (.mul (.mul (.var 0) (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul .one (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1))) (.var 6)))))38    (.add (.add (.add (.add (.mul (.mul (.var 0) (.add (.add (.add .one (.var 2)) (.mul (.var 2) (.var 2))) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.var 3)) (.mul (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.var 2))) (.neg (.mul (.var 2) (.var 2)))) (.neg (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))))) (.var 4))) (.mul (.mul (.var 0) (.add (.add (.add .one (.neg (.var 2))) (.mul (.var 2) (.var 2))) (.neg (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.var 5))) (.mul (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.var 2)))) (.neg (.mul (.var 2) (.var 2)))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.var 6))) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 6)) (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 6)))) (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 5))) (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 6))) (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 6))) (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 5)))) (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 5))) (.neg (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 6)))) (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 4))) (.neg (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 6)))) (.mul (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.var 6))) (.mul (.mul (.mul (.mul (.var 0) (.var 2)) (.var 2)) (.var 2)) (.var 5))) (.mul (.mul (.mul (.var 0) (.var 2)) (.var 2)) (.var 4))) (.neg (.mul (.mul (.mul (.var 0) (.var 2)) (.var 2)) (.var 5)))) (.mul (.mul (.mul (.var 0) (.var 2)) (.var 2)) (.var 6))) (.mul (.mul (.var 0) (.var 2)) (.var 5))))) (by decide +kernel)3940theorem conv0_aux (q jj u v : Shell p) :41    (q * (1 + u + u * u + u * u * u)) * (q * (1 + v + v * v + v * v * v)) + (q * (1 + jj * u + -(u * u) + -(jj * (u * u * u)))) * (q * (1 + -(jj * v) + -(v * v) + jj * (v * v * v))) + (q * (1 + -u + u * u + -(u * u * u))) * (q * (1 + -v + v * v + -(v * v * v))) + (q * (1 + -(jj * u) + -(u * u) + jj * (u * u * u))) * (q * (1 + jj * v + -(v * v) + -(jj * (v * v * v)))) =42      q * (1 + (u * v) + (u * v) * (u * v) + (u * v) * (u * v) * (u * v)) + (jj * jj + 1) * (-((1 + 1) * q * q * u * u * u * v * v * v) + (1 + 1) * q * q * u * u * u * v + (1 + 1) * q * q * u * v * v * v + -((1 + 1) * q * q * u * v)) + ((1 + 1 + 1 + 1) * q + -1) * (q * u * u * u * v * v * v + q * u * u * v * v + q * u * v + q) :=43  Shell.Frame.RE.sound (Shell.Frame.look [q, jj, u, v])44    (.add (.add (.add (.mul (.mul (.var 0) (.add (.add (.add .one (.var 2)) (.mul (.var 2) (.var 2))) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.var 0) (.add (.add (.add .one (.var 3)) (.mul (.var 3) (.var 3))) (.mul (.mul (.var 3) (.var 3)) (.var 3))))) (.mul (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.var 2))) (.neg (.mul (.var 2) (.var 2)))) (.neg (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))))) (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.var 3)))) (.neg (.mul (.var 3) (.var 3)))) (.mul (.var 1) (.mul (.mul (.var 3) (.var 3)) (.var 3))))))) (.mul (.mul (.var 0) (.add (.add (.add .one (.neg (.var 2))) (.mul (.var 2) (.var 2))) (.neg (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.var 0) (.add (.add (.add .one (.neg (.var 3))) (.mul (.var 3) (.var 3))) (.neg (.mul (.mul (.var 3) (.var 3)) (.var 3))))))) (.mul (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.var 2)))) (.neg (.mul (.var 2) (.var 2)))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.var 3))) (.neg (.mul (.var 3) (.var 3)))) (.neg (.mul (.var 1) (.mul (.mul (.var 3) (.var 3)) (.var 3))))))))45    (.add (.add (.mul (.var 0) (.add (.add (.add .one (.mul (.var 2) (.var 3))) (.mul (.mul (.var 2) (.var 3)) (.mul (.var 2) (.var 3)))) (.mul (.mul (.mul (.var 2) (.var 3)) (.mul (.var 2) (.var 3))) (.mul (.var 2) (.var 3))))) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.add (.add (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.add .one .one) (.var 0)) (.var 0)) (.var 2)) (.var 2)) (.var 2)) (.var 3)) (.var 3)) (.var 3))) (.mul (.mul (.mul (.mul (.mul (.mul (.add .one .one) (.var 0)) (.var 0)) (.var 2)) (.var 2)) (.var 2)) (.var 3))) (.mul (.mul (.mul (.mul (.mul (.mul (.add .one .one) (.var 0)) (.var 0)) (.var 2)) (.var 3)) (.var 3)) (.var 3))) (.neg (.mul (.mul (.mul (.mul (.add .one .one) (.var 0)) (.var 0)) (.var 2)) (.var 3)))))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) (.add (.add (.add (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 2)) (.var 2)) (.var 2)) (.var 3)) (.var 3)) (.var 3)) (.mul (.mul (.mul (.mul (.var 0) (.var 2)) (.var 2)) (.var 3)) (.var 3))) (.mul (.mul (.var 0) (.var 2)) (.var 3))) (.var 0)))) (by decide +kernel)4647theorem conv1_aux (q jj u v : Shell p) :48    (q * (1 + u + u * u + u * u * u)) * (q * (1 + jj * v + -(v * v) + -(jj * (v * v * v)))) + (q * (1 + jj * u + -(u * u) + -(jj * (u * u * u)))) * (q * (1 + v + v * v + v * v * v)) + (q * (1 + -u + u * u + -(u * u * u))) * (q * (1 + -(jj * v) + -(v * v) + jj * (v * v * v))) + (q * (1 + -(jj * u) + -(u * u) + jj * (u * u * u))) * (q * (1 + -v + v * v + -(v * v * v))) =49      q * (1 + jj * (u * v) + -((u * v) * (u * v)) + -(jj * ((u * v) * (u * v) * (u * v)))) + (jj * jj + 1) * (0) + ((1 + 1 + 1 + 1) * q + -1) * (-(q * jj * u * u * u * v * v * v) + q * jj * u * v + -(q * u * u * v * v) + q) :=50  Shell.Frame.RE.sound (Shell.Frame.look [q, jj, u, v])51    (.add (.add (.add (.mul (.mul (.var 0) (.add (.add (.add .one (.var 2)) (.mul (.var 2) (.var 2))) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.var 3))) (.neg (.mul (.var 3) (.var 3)))) (.neg (.mul (.var 1) (.mul (.mul (.var 3) (.var 3)) (.var 3))))))) (.mul (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.var 2))) (.neg (.mul (.var 2) (.var 2)))) (.neg (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))))) (.mul (.var 0) (.add (.add (.add .one (.var 3)) (.mul (.var 3) (.var 3))) (.mul (.mul (.var 3) (.var 3)) (.var 3)))))) (.mul (.mul (.var 0) (.add (.add (.add .one (.neg (.var 2))) (.mul (.var 2) (.var 2))) (.neg (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.var 3)))) (.neg (.mul (.var 3) (.var 3)))) (.mul (.var 1) (.mul (.mul (.var 3) (.var 3)) (.var 3))))))) (.mul (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.var 2)))) (.neg (.mul (.var 2) (.var 2)))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.var 0) (.add (.add (.add .one (.neg (.var 3))) (.mul (.var 3) (.var 3))) (.neg (.mul (.mul (.var 3) (.var 3)) (.var 3)))))))52    (.add (.add (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.mul (.var 2) (.var 3)))) (.neg (.mul (.mul (.var 2) (.var 3)) (.mul (.var 2) (.var 3))))) (.neg (.mul (.var 1) (.mul (.mul (.mul (.var 2) (.var 3)) (.mul (.var 2) (.var 3))) (.mul (.var 2) (.var 3))))))) (.mul (.add (.mul (.var 1) (.var 1)) .one) .zero)) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) (.add (.add (.add (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 3)) (.var 3)) (.var 3))) (.mul (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.var 3))) (.neg (.mul (.mul (.mul (.mul (.var 0) (.var 2)) (.var 2)) (.var 3)) (.var 3)))) (.var 0)))) (by decide +kernel)5354theorem conv2_aux (q jj u v : Shell p) :55    (q * (1 + u + u * u + u * u * u)) * (q * (1 + -v + v * v + -(v * v * v))) + (q * (1 + jj * u + -(u * u) + -(jj * (u * u * u)))) * (q * (1 + jj * v + -(v * v) + -(jj * (v * v * v)))) + (q * (1 + -u + u * u + -(u * u * u))) * (q * (1 + v + v * v + v * v * v)) + (q * (1 + -(jj * u) + -(u * u) + jj * (u * u * u))) * (q * (1 + -(jj * v) + -(v * v) + jj * (v * v * v))) =56      q * (1 + -(u * v) + (u * v) * (u * v) + -((u * v) * (u * v) * (u * v))) + (jj * jj + 1) * ((1 + 1) * q * q * u * u * u * v * v * v + -((1 + 1) * q * q * u * u * u * v) + -((1 + 1) * q * q * u * v * v * v) + (1 + 1) * q * q * u * v) + ((1 + 1 + 1 + 1) * q + -1) * (-(q * u * u * u * v * v * v) + q * u * u * v * v + -(q * u * v) + q) :=57  Shell.Frame.RE.sound (Shell.Frame.look [q, jj, u, v])58    (.add (.add (.add (.mul (.mul (.var 0) (.add (.add (.add .one (.var 2)) (.mul (.var 2) (.var 2))) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.var 0) (.add (.add (.add .one (.neg (.var 3))) (.mul (.var 3) (.var 3))) (.neg (.mul (.mul (.var 3) (.var 3)) (.var 3)))))) (.mul (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.var 2))) (.neg (.mul (.var 2) (.var 2)))) (.neg (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))))) (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.var 3))) (.neg (.mul (.var 3) (.var 3)))) (.neg (.mul (.var 1) (.mul (.mul (.var 3) (.var 3)) (.var 3)))))))) (.mul (.mul (.var 0) (.add (.add (.add .one (.neg (.var 2))) (.mul (.var 2) (.var 2))) (.neg (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.var 0) (.add (.add (.add .one (.var 3)) (.mul (.var 3) (.var 3))) (.mul (.mul (.var 3) (.var 3)) (.var 3)))))) (.mul (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.var 2)))) (.neg (.mul (.var 2) (.var 2)))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.var 3)))) (.neg (.mul (.var 3) (.var 3)))) (.mul (.var 1) (.mul (.mul (.var 3) (.var 3)) (.var 3)))))))59    (.add (.add (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 2) (.var 3)))) (.mul (.mul (.var 2) (.var 3)) (.mul (.var 2) (.var 3)))) (.neg (.mul (.mul (.mul (.var 2) (.var 3)) (.mul (.var 2) (.var 3))) (.mul (.var 2) (.var 3)))))) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.add (.add (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.add .one .one) (.var 0)) (.var 0)) (.var 2)) (.var 2)) (.var 2)) (.var 3)) (.var 3)) (.var 3)) (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.add .one .one) (.var 0)) (.var 0)) (.var 2)) (.var 2)) (.var 2)) (.var 3)))) (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.add .one .one) (.var 0)) (.var 0)) (.var 2)) (.var 3)) (.var 3)) (.var 3)))) (.mul (.mul (.mul (.mul (.add .one .one) (.var 0)) (.var 0)) (.var 2)) (.var 3))))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) (.add (.add (.add (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 2)) (.var 2)) (.var 2)) (.var 3)) (.var 3)) (.var 3))) (.mul (.mul (.mul (.mul (.var 0) (.var 2)) (.var 2)) (.var 3)) (.var 3))) (.neg (.mul (.mul (.var 0) (.var 2)) (.var 3)))) (.var 0)))) (by decide +kernel)6061theorem conv3_aux (q jj u v : Shell p) :62    (q * (1 + u + u * u + u * u * u)) * (q * (1 + -(jj * v) + -(v * v) + jj * (v * v * v))) + (q * (1 + jj * u + -(u * u) + -(jj * (u * u * u)))) * (q * (1 + -v + v * v + -(v * v * v))) + (q * (1 + -u + u * u + -(u * u * u))) * (q * (1 + jj * v + -(v * v) + -(jj * (v * v * v)))) + (q * (1 + -(jj * u) + -(u * u) + jj * (u * u * u))) * (q * (1 + v + v * v + v * v * v)) =63      q * (1 + -(jj * (u * v)) + -((u * v) * (u * v)) + jj * ((u * v) * (u * v) * (u * v))) + (jj * jj + 1) * (0) + ((1 + 1 + 1 + 1) * q + -1) * (q * jj * u * u * u * v * v * v + -(q * jj * u * v) + -(q * u * u * v * v) + q) :=64  Shell.Frame.RE.sound (Shell.Frame.look [q, jj, u, v])65    (.add (.add (.add (.mul (.mul (.var 0) (.add (.add (.add .one (.var 2)) (.mul (.var 2) (.var 2))) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.var 3)))) (.neg (.mul (.var 3) (.var 3)))) (.mul (.var 1) (.mul (.mul (.var 3) (.var 3)) (.var 3)))))) (.mul (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.var 2))) (.neg (.mul (.var 2) (.var 2)))) (.neg (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))))) (.mul (.var 0) (.add (.add (.add .one (.neg (.var 3))) (.mul (.var 3) (.var 3))) (.neg (.mul (.mul (.var 3) (.var 3)) (.var 3))))))) (.mul (.mul (.var 0) (.add (.add (.add .one (.neg (.var 2))) (.mul (.var 2) (.var 2))) (.neg (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.var 3))) (.neg (.mul (.var 3) (.var 3)))) (.neg (.mul (.var 1) (.mul (.mul (.var 3) (.var 3)) (.var 3)))))))) (.mul (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.var 2)))) (.neg (.mul (.var 2) (.var 2)))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.var 0) (.add (.add (.add .one (.var 3)) (.mul (.var 3) (.var 3))) (.mul (.mul (.var 3) (.var 3)) (.var 3))))))66    (.add (.add (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.mul (.var 2) (.var 3))))) (.neg (.mul (.mul (.var 2) (.var 3)) (.mul (.var 2) (.var 3))))) (.mul (.var 1) (.mul (.mul (.mul (.var 2) (.var 3)) (.mul (.var 2) (.var 3))) (.mul (.var 2) (.var 3)))))) (.mul (.add (.mul (.var 1) (.var 1)) .one) .zero)) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) (.add (.add (.add (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 3)) (.var 3)) (.var 3)) (.neg (.mul (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.var 3)))) (.neg (.mul (.mul (.mul (.mul (.var 0) (.var 2)) (.var 2)) (.var 3)) (.var 3)))) (.var 0)))) (by decide +kernel)6768theorem card00_aux (q jj : Shell p) :69    q * (1 + (1) + (1) * (1) + (1) * (1) * (1)) =70      1 + (jj * jj + 1) * (0) + ((1 + 1 + 1 + 1) * q + -1) * (1) :=71  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])72    (.mul (.var 0) (.add (.add (.add .one .one) (.mul .one .one)) (.mul (.mul .one .one) .one)))73    (.add (.add .one (.mul (.add (.mul (.var 1) (.var 1)) .one) .zero)) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .one)) (by decide +kernel)7475theorem card01_aux (q jj : Shell p) :76    q * (1 + jj * (1) + -((1) * (1)) + -(jj * ((1) * (1) * (1)))) =77      0 + (jj * jj + 1) * (0) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=78  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])79    (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) .one)) (.neg (.mul .one .one))) (.neg (.mul (.var 1) (.mul (.mul .one .one) .one)))))80    (.add (.add .zero (.mul (.add (.mul (.var 1) (.var 1)) .one) .zero)) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)8182theorem card02_aux (q jj : Shell p) :83    q * (1 + -(1) + (1) * (1) + -((1) * (1) * (1))) =84      0 + (jj * jj + 1) * (0) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=85  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])86    (.mul (.var 0) (.add (.add (.add .one (.neg .one)) (.mul .one .one)) (.neg (.mul (.mul .one .one) .one))))87    (.add (.add .zero (.mul (.add (.mul (.var 1) (.var 1)) .one) .zero)) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)8889theorem card03_aux (q jj : Shell p) :90    q * (1 + -(jj * (1)) + -((1) * (1)) + jj * ((1) * (1) * (1))) =91      0 + (jj * jj + 1) * (0) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=92  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])93    (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) .one))) (.neg (.mul .one .one))) (.mul (.var 1) (.mul (.mul .one .one) .one))))94    (.add (.add .zero (.mul (.add (.mul (.var 1) (.var 1)) .one) .zero)) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)9596theorem card10_aux (q jj : Shell p) :97    q * (1 + (-jj) + (-jj) * (-jj) + (-jj) * (-jj) * (-jj)) =98      0 + (jj * jj + 1) * (-(q * jj) + q) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=99  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])100    (.mul (.var 0) (.add (.add (.add .one (.neg (.var 1))) (.mul (.neg (.var 1)) (.neg (.var 1)))) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1)))))101    (.add (.add .zero (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.neg (.mul (.var 0) (.var 1))) (.var 0)))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)102103theorem card11_aux (q jj : Shell p) :104    q * (1 + jj * (-jj) + -((-jj) * (-jj)) + -(jj * ((-jj) * (-jj) * (-jj)))) =105      1 + (jj * jj + 1) * (q * jj * jj + -((1 + 1 + 1) * q)) + ((1 + 1 + 1 + 1) * q + -1) * (1) :=106  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])107    (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.neg (.var 1)))) (.neg (.mul (.neg (.var 1)) (.neg (.var 1))))) (.neg (.mul (.var 1) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1)))))))108    (.add (.add .one (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.neg (.mul (.add (.add .one .one) .one) (.var 0)))))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .one)) (by decide +kernel)109110theorem card12_aux (q jj : Shell p) :111    q * (1 + -(-jj) + (-jj) * (-jj) + -((-jj) * (-jj) * (-jj))) =112      0 + (jj * jj + 1) * (q * jj + q) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=113  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])114    (.mul (.var 0) (.add (.add (.add .one (.neg (.neg (.var 1)))) (.mul (.neg (.var 1)) (.neg (.var 1)))) (.neg (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1))))))115    (.add (.add .zero (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.mul (.var 0) (.var 1)) (.var 0)))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)116117theorem card13_aux (q jj : Shell p) :118    q * (1 + -(jj * (-jj)) + -((-jj) * (-jj)) + jj * ((-jj) * (-jj) * (-jj))) =119      0 + (jj * jj + 1) * (-(q * jj * jj) + q) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=120  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])121    (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.neg (.var 1))))) (.neg (.mul (.neg (.var 1)) (.neg (.var 1))))) (.mul (.var 1) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1))))))122    (.add (.add .zero (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.neg (.mul (.mul (.var 0) (.var 1)) (.var 1))) (.var 0)))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)123124theorem card20_aux (q jj : Shell p) :125    q * (1 + (-1) + (-1) * (-1) + (-1) * (-1) * (-1)) =126      0 + (jj * jj + 1) * (0) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=127  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])128    (.mul (.var 0) (.add (.add (.add .one (.neg .one)) (.mul (.neg .one) (.neg .one))) (.mul (.mul (.neg .one) (.neg .one)) (.neg .one))))129    (.add (.add .zero (.mul (.add (.mul (.var 1) (.var 1)) .one) .zero)) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)130131theorem card21_aux (q jj : Shell p) :132    q * (1 + jj * (-1) + -((-1) * (-1)) + -(jj * ((-1) * (-1) * (-1)))) =133      0 + (jj * jj + 1) * (0) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=134  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])135    (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.neg .one))) (.neg (.mul (.neg .one) (.neg .one)))) (.neg (.mul (.var 1) (.mul (.mul (.neg .one) (.neg .one)) (.neg .one))))))136    (.add (.add .zero (.mul (.add (.mul (.var 1) (.var 1)) .one) .zero)) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)137138theorem card22_aux (q jj : Shell p) :139    q * (1 + -(-1) + (-1) * (-1) + -((-1) * (-1) * (-1))) =140      1 + (jj * jj + 1) * (0) + ((1 + 1 + 1 + 1) * q + -1) * (1) :=141  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])142    (.mul (.var 0) (.add (.add (.add .one (.neg (.neg .one))) (.mul (.neg .one) (.neg .one))) (.neg (.mul (.mul (.neg .one) (.neg .one)) (.neg .one)))))143    (.add (.add .one (.mul (.add (.mul (.var 1) (.var 1)) .one) .zero)) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .one)) (by decide +kernel)144145theorem card23_aux (q jj : Shell p) :146    q * (1 + -(jj * (-1)) + -((-1) * (-1)) + jj * ((-1) * (-1) * (-1))) =147      0 + (jj * jj + 1) * (0) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=148  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])149    (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.neg .one)))) (.neg (.mul (.neg .one) (.neg .one)))) (.mul (.var 1) (.mul (.mul (.neg .one) (.neg .one)) (.neg .one)))))150    (.add (.add .zero (.mul (.add (.mul (.var 1) (.var 1)) .one) .zero)) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)151152theorem card30_aux (q jj : Shell p) :153    q * (1 + (jj) + (jj) * (jj) + (jj) * (jj) * (jj)) =154      0 + (jj * jj + 1) * (q * jj + q) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=155  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])156    (.mul (.var 0) (.add (.add (.add .one (.var 1)) (.mul (.var 1) (.var 1))) (.mul (.mul (.var 1) (.var 1)) (.var 1))))157    (.add (.add .zero (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.mul (.var 0) (.var 1)) (.var 0)))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)158159theorem card31_aux (q jj : Shell p) :160    q * (1 + jj * (jj) + -((jj) * (jj)) + -(jj * ((jj) * (jj) * (jj)))) =161      0 + (jj * jj + 1) * (-(q * jj * jj) + q) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=162  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])163    (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.var 1))) (.neg (.mul (.var 1) (.var 1)))) (.neg (.mul (.var 1) (.mul (.mul (.var 1) (.var 1)) (.var 1))))))164    (.add (.add .zero (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.neg (.mul (.mul (.var 0) (.var 1)) (.var 1))) (.var 0)))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)165166theorem card32_aux (q jj : Shell p) :167    q * (1 + -(jj) + (jj) * (jj) + -((jj) * (jj) * (jj))) =168      0 + (jj * jj + 1) * (-(q * jj) + q) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=169  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])170    (.mul (.var 0) (.add (.add (.add .one (.neg (.var 1))) (.mul (.var 1) (.var 1))) (.neg (.mul (.mul (.var 1) (.var 1)) (.var 1)))))171    (.add (.add .zero (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.neg (.mul (.var 0) (.var 1))) (.var 0)))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)172173theorem card33_aux (q jj : Shell p) :174    q * (1 + -(jj * (jj)) + -((jj) * (jj)) + jj * ((jj) * (jj) * (jj))) =175      1 + (jj * jj + 1) * (q * jj * jj + -((1 + 1 + 1) * q)) + ((1 + 1 + 1 + 1) * q + -1) * (1) :=176  Shell.Frame.RE.sound (Shell.Frame.look [q, jj])177    (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.var 1)))) (.neg (.mul (.var 1) (.var 1)))) (.mul (.var 1) (.mul (.mul (.var 1) (.var 1)) (.var 1)))))178    (.add (.add .one (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.neg (.mul (.add (.add .one .one) .one) (.var 0)))))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .one)) (by decide +kernel)179180/-! ## The four basis matrices on the cycle -/181182variable {κ : Nat} {g : Shell p}183184/-- The identity matrix. -/185def idm (k j : Nat) : Shell p := if k = j then 1 else 0186187/-- `F J`, entrywise `F k (rev j)`. -/188def FJ (g : Shell p) (κ k j : Nat) : Shell p := Fmat g κ k (rev (p - 1) j)189190/-- The combination `c₀ I + c₁ F + c₂ J + c₃ F J`. -/191def comb (g : Shell p) (κ : Nat) (c0 c1 c2 c3 : Shell p) (k j : Nat) : Shell p :=192  c0 * idm k j + c1 * Fmat g κ k j + c2 * J (p - 1) k j + c3 * FJ g κ k j193194theorem mm_I_X (X : Nat → Nat → Shell p) {k j : Nat} (hk : k < p - 1) :195    sumRange (fun l => idm k l * X l j) (p - 1) = X k j := by196  rw [sum_eq_single hk (fun l _ hne => by unfold idm; rw [ite_eq_right (fun e => hne e.symm), zero_mul])]197  unfold idm; rw [ite_eq_left rfl, one_mul]198199theorem mm_X_I (X : Nat → Nat → Shell p) {k j : Nat} (hj : j < p - 1) :200    sumRange (fun l => X k l * idm l j) (p - 1) = X k j := by201  rw [sum_eq_single hj (fun l _ hne => by unfold idm; rw [ite_eq_right hne, mul_zero])]202  unfold idm; rw [ite_eq_left rfl, mul_one]203204theorem mm_J_X (X : Nat → Nat → Shell p) {k j : Nat} (hk : k < p - 1) :205    sumRange (fun l => (J (p - 1) k l : Shell p) * X l j) (p - 1) = X (rev (p - 1) k) j := by206  have hn : 0 < p - 1 := Nat.lt_of_le_of_lt (Nat.zero_le k) hk207  rw [sum_eq_single (rev_lt hn k) (fun l hl hne => by rw [J_eq hk hl, ite_eq_right hne, zero_mul])]208  rw [J_eq hk (rev_lt hn k), ite_eq_left rfl, one_mul]209210theorem mm_X_J (X : Nat → Nat → Shell p) {k j : Nat} (hj : j < p - 1) :211    sumRange (fun l => X k l * (J (p - 1) l j : Shell p)) (p - 1) = X k (rev (p - 1) j) := by212  have hn : 0 < p - 1 := Nat.lt_of_le_of_lt (Nat.zero_le j) hj213  rw [sum_eq_single (rev_lt hn j) (fun l hl hne => by214    rw [J_eq hl hj, ite_eq_right (fun e => hne (by rw [e, rev_rev hl])), mul_zero])]215  rw [J_eq (rev_lt hn j) hj, ite_eq_left (rev_rev hj).symm, mul_one]216217theorem J_rev_right {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :218    (J (p - 1) k (rev (p - 1) j) : Shell p) = idm k j := by219  have hn : 0 < p - 1 := Nat.lt_of_le_of_lt (Nat.zero_le k) hk220  rw [J_eq hk (rev_lt hn j)]221  unfold idm222  exact match Nat.decEq k j with223    | isTrue e => by rw [ite_eq_left (by rw [e]), ite_eq_left e]224    | isFalse e => by225        rw [ite_eq_right (fun h => e (by rw [← rev_rev hk, ← rev_rev hj, h])), ite_eq_right e]226227theorem J_rev_left {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :228    (J (p - 1) (rev (p - 1) k) j : Shell p) = idm k j := by229  have hn : 0 < p - 1 := Nat.lt_of_le_of_lt (Nat.zero_le k) hk230  rw [J_eq (rev_lt hn k) hj, rev_rev hk]231  unfold idm232  exact match Nat.decEq k j with233    | isTrue e => by rw [ite_eq_left e.symm, ite_eq_left e]234    | isFalse e => by rw [ite_eq_right (fun h => e h.symm), ite_eq_right e]235236theorem J_rev_rev {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :237    (J (p - 1) (rev (p - 1) k) (rev (p - 1) j) : Shell p) = J (p - 1) k j := by238  have hn : 0 < p - 1 := Nat.lt_of_le_of_lt (Nat.zero_le k) hk239  rw [J_eq (rev_lt hn k) (rev_lt hn j), rev_rev hk, J_eq hk hj]240  exact match Nat.decEq j (rev (p - 1) k) with241    | isTrue e => by rw [ite_eq_left e, ite_eq_left (by rw [e, rev_rev hk])]242    | isFalse e => by rw [ite_eq_right e, ite_eq_right (fun h => e (by rw [← h, rev_rev hj]))]243244/-- `F (rev k) j = F k (rev j)`: both carry `g^{−jk}`. -/245theorem F_rev (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :246    Fmat g κ (rev (p - 1) k) j = Fmat g κ k (rev (p - 1) j) := by247  have hn := F.n_pos248  unfold Fmat W249  have e1 : g ^ (j * rev (p - 1) k) * g ^ (j * k) = 1 := by250    rw [← pow_add, ← Nat.left_distrib, F.pow_mod, ← FRC.Nat.mul_mod_mod _ _ _ hn, rev_add_mod hk, Nat.mul_zero,251      FRC.Nat.zero_mod, pow_zero]252  have e2 : g ^ (rev (p - 1) j * k) * g ^ (j * k) = 1 := by253    rw [← pow_add, ← FRC.Nat.add_mul, F.pow_mod, ← FRC.Nat.mod_mul_mod _ _ _ hn, rev_add_mod hj, Nat.zero_mul,254      FRC.Nat.zero_mod, pow_zero]255  rw [inv_unique e1 e2]256257/-! The sixteen products of the basis `I, F, J, G = F J`: the cyclic group of order four. -/258259theorem mm_II {k j : Nat} (hk : k < p - 1) (_hj : j < p - 1) :260    sumRange (fun l => idm k l * idm l j) (p - 1) = (idm k j : Shell p) := mm_I_X idm hk261theorem mm_IF {k j : Nat} (hk : k < p - 1) (_hj : j < p - 1) :262    sumRange (fun l => idm k l * Fmat g κ l j) (p - 1) = Fmat g κ k j := mm_I_X (Fmat g κ) hk263theorem mm_IJ {k j : Nat} (hk : k < p - 1) (_hj : j < p - 1) :264    sumRange (fun l => idm k l * J (p - 1) l j) (p - 1) = (J (p - 1) k j : Shell p) := mm_I_X (J (p - 1)) hk265theorem mm_IG {k j : Nat} (hk : k < p - 1) (_hj : j < p - 1) :266    sumRange (fun l => idm k l * FJ g κ l j) (p - 1) = FJ g κ k j := mm_I_X (FJ g κ) hk267theorem mm_FI {k j : Nat} (_hk : k < p - 1) (hj : j < p - 1) :268    sumRange (fun l => Fmat g κ k l * idm l j) (p - 1) = Fmat g κ k j := mm_X_I (Fmat g κ) hj269theorem mm_JI {k j : Nat} (_hk : k < p - 1) (hj : j < p - 1) :270    sumRange (fun l => (J (p - 1) k l : Shell p) * idm l j) (p - 1) = J (p - 1) k j := mm_X_I (J (p - 1)) hj271theorem mm_GI {k j : Nat} (_hk : k < p - 1) (hj : j < p - 1) :272    sumRange (fun l => FJ g κ k l * idm l j) (p - 1) = FJ g κ k j := mm_X_I (FJ g κ) hj273274theorem mm_FF (F : Frame p κ g) {k j : Nat} (_hk : k < p - 1) (_hj : j < p - 1) :275    sumRange (fun l => Fmat g κ k l * Fmat g κ l j) (p - 1) = J (p - 1) k j := F.F_sq k j276theorem mm_FJ {k j : Nat} (_hk : k < p - 1) (hj : j < p - 1) :277    sumRange (fun l => Fmat g κ k l * J (p - 1) l j) (p - 1) = FJ g κ k j := mm_X_J (Fmat g κ) hj278theorem mm_FG (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :279    sumRange (fun l => Fmat g κ k l * FJ g κ l j) (p - 1) = idm k j := by280  show sumRange (fun l => Fmat g κ k l * Fmat g κ l (rev (p - 1) j)) (p - 1) = idm k j281  rw [F.F_sq k (rev (p - 1) j), J_rev_right hk hj]282theorem mm_JF (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :283    sumRange (fun l => (J (p - 1) k l : Shell p) * Fmat g κ l j) (p - 1) = FJ g κ k j := by284  rw [mm_J_X (Fmat g κ) hk, F_rev F hk hj]; rfl285theorem mm_JJ (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :286    sumRange (fun l => (J (p - 1) k l : Shell p) * J (p - 1) l j) (p - 1) = idm k j := F.J_sq hk hj287theorem mm_JG (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :288    sumRange (fun l => (J (p - 1) k l : Shell p) * FJ g κ l j) (p - 1) = Fmat g κ k j := by289  have hn := F.n_pos290  rw [mm_J_X (FJ g κ) hk]291  show Fmat g κ (rev (p - 1) k) (rev (p - 1) j) = Fmat g κ k j292  rw [F_rev F hk (rev_lt hn j), rev_rev hj]293theorem mm_GF (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :294    sumRange (fun l => FJ g κ k l * Fmat g κ l j) (p - 1) = idm k j := by295  have hn := F.n_pos296  rw [sum_congr _ (fun l hl => by297    show Fmat g κ k (rev (p - 1) l) * Fmat g κ l j = Fmat g κ (rev (p - 1) k) l * Fmat g κ l j298    rw [F_rev F hk hl])]299  rw [F.F_sq (rev (p - 1) k) j, J_rev_left hk hj]300theorem mm_GJ {k j : Nat} (_hk : k < p - 1) (hj : j < p - 1) :301    sumRange (fun l => FJ g κ k l * J (p - 1) l j) (p - 1) = Fmat g κ k j := by302  rw [mm_X_J (FJ g κ) hj]303  show Fmat g κ k (rev (p - 1) (rev (p - 1) j)) = Fmat g κ k j304  rw [rev_rev hj]305theorem mm_GG (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :306    sumRange (fun l => FJ g κ k l * FJ g κ l j) (p - 1) = J (p - 1) k j := by307  rw [sum_congr _ (fun l hl => by308    show Fmat g κ k (rev (p - 1) l) * Fmat g κ l (rev (p - 1) j) = Fmat g κ (rev (p - 1) k) l * Fmat g κ l (rev (p - 1) j)309    rw [F_rev F hk hl])]310  have hn := F.n_pos311  rw [F.F_sq (rev (p - 1) k) (rev (p - 1) j), J_rev_rev hk hj]312313/-- The product of two combinations is the cyclic convolution of their coefficients. -/314theorem comb_mul (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) (a0 a1 a2 a3 b0 b1 b2 b3 : Shell p) :315    sumRange (fun l => comb g κ a0 a1 a2 a3 k l * comb g κ b0 b1 b2 b3 l j) (p - 1) =316      comb g κ (a0 * b0 + a1 * b3 + a2 * b2 + a3 * b1) (a0 * b1 + a1 * b0 + a2 * b3 + a3 * b2)317        (a0 * b2 + a1 * b1 + a2 * b0 + a3 * b3) (a0 * b3 + a1 * b2 + a2 * b1 + a3 * b0) k j := by318  have e : ∀ l, comb g κ a0 a1 a2 a3 k l * comb g κ b0 b1 b2 b3 l j =319      a0 * b0 * (idm k l * idm l j) + a0 * b1 * (idm k l * Fmat g κ l j) + a0 * b2 * (idm k l * J (p - 1) l j) + a0 * b3 * (idm k l * FJ g κ l j) + a1 * b0 * (Fmat g κ k l * idm l j) + a1 * b1 * (Fmat g κ k l * Fmat g κ l j) + a1 * b2 * (Fmat g κ k l * J (p - 1) l j) + a1 * b3 * (Fmat g κ k l * FJ g κ l j) + a2 * b0 * (J (p - 1) k l * idm l j) + a2 * b1 * (J (p - 1) k l * Fmat g κ l j) + a2 * b2 * (J (p - 1) k l * J (p - 1) l j) + a2 * b3 * (J (p - 1) k l * FJ g κ l j) + a3 * b0 * (FJ g κ k l * idm l j) + a3 * b1 * (FJ g κ k l * Fmat g κ l j) + a3 * b2 * (FJ g κ k l * J (p - 1) l j) + a3 * b3 * (FJ g κ k l * FJ g κ l j) := fun l =>320    Shell.Frame.RE.sound (Shell.Frame.look [a0, a1, a2, a3, b0, b1, b2, b3, idm k l, Fmat g κ k l, J (p - 1) k l, FJ g κ k l, idm l j, Fmat g κ l j, J (p - 1) l j, FJ g κ l j])321      (.mul (.add (.add (.add (.mul (.var 0) (.var 8)) (.mul (.var 1) (.var 9))) (.mul (.var 2) (.var 10))) (.mul (.var 3) (.var 11))) (.add (.add (.add (.mul (.var 4) (.var 12)) (.mul (.var 5) (.var 13))) (.mul (.var 6) (.var 14))) (.mul (.var 7) (.var 15))))322      (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.mul (.mul (.var 0) (.var 4)) (.mul (.var 8) (.var 12))) (.mul (.mul (.var 0) (.var 5)) (.mul (.var 8) (.var 13)))) (.mul (.mul (.var 0) (.var 6)) (.mul (.var 8) (.var 14)))) (.mul (.mul (.var 0) (.var 7)) (.mul (.var 8) (.var 15)))) (.mul (.mul (.var 1) (.var 4)) (.mul (.var 9) (.var 12)))) (.mul (.mul (.var 1) (.var 5)) (.mul (.var 9) (.var 13)))) (.mul (.mul (.var 1) (.var 6)) (.mul (.var 9) (.var 14)))) (.mul (.mul (.var 1) (.var 7)) (.mul (.var 9) (.var 15)))) (.mul (.mul (.var 2) (.var 4)) (.mul (.var 10) (.var 12)))) (.mul (.mul (.var 2) (.var 5)) (.mul (.var 10) (.var 13)))) (.mul (.mul (.var 2) (.var 6)) (.mul (.var 10) (.var 14)))) (.mul (.mul (.var 2) (.var 7)) (.mul (.var 10) (.var 15)))) (.mul (.mul (.var 3) (.var 4)) (.mul (.var 11) (.var 12)))) (.mul (.mul (.var 3) (.var 5)) (.mul (.var 11) (.var 13)))) (.mul (.mul (.var 3) (.var 6)) (.mul (.var 11) (.var 14)))) (.mul (.mul (.var 3) (.var 7)) (.mul (.var 11) (.var 15)))) (by decide +kernel)323  rw [sum_congr _ (fun l _ => e l)]324  rw [sum_add, sum_add, sum_add, sum_add, sum_add, sum_add, sum_add, sum_add, sum_add, sum_add, sum_add, sum_add, sum_add, sum_add, sum_add]325  rw [sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left]326  rw [mm_II hk hj, mm_IF hk hj, mm_IJ hk hj, mm_IG hk hj, mm_FI hk hj, mm_FF F hk hj, mm_FJ hk hj, mm_FG F hk hj, mm_JI hk hj, mm_JF F hk hj, mm_JJ F hk hj, mm_JG F hk hj, mm_GI hk hj, mm_GF F hk hj, mm_GJ hk hj, mm_GG F hk hj]327  exact Shell.Frame.RE.sound (Shell.Frame.look [a0, a1, a2, a3, b0, b1, b2, b3, idm k j, Fmat g κ k j, J (p - 1) k j, FJ g κ k j])328    (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.add (.mul (.mul (.var 0) (.var 4)) (.var 8)) (.mul (.mul (.var 0) (.var 5)) (.var 9))) (.mul (.mul (.var 0) (.var 6)) (.var 10))) (.mul (.mul (.var 0) (.var 7)) (.var 11))) (.mul (.mul (.var 1) (.var 4)) (.var 9))) (.mul (.mul (.var 1) (.var 5)) (.var 10))) (.mul (.mul (.var 1) (.var 6)) (.var 11))) (.mul (.mul (.var 1) (.var 7)) (.var 8))) (.mul (.mul (.var 2) (.var 4)) (.var 10))) (.mul (.mul (.var 2) (.var 5)) (.var 11))) (.mul (.mul (.var 2) (.var 6)) (.var 8))) (.mul (.mul (.var 2) (.var 7)) (.var 9))) (.mul (.mul (.var 3) (.var 4)) (.var 11))) (.mul (.mul (.var 3) (.var 5)) (.var 8))) (.mul (.mul (.var 3) (.var 6)) (.var 9))) (.mul (.mul (.var 3) (.var 7)) (.var 10)))329    (.add (.add (.add (.mul (.add (.add (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) (.var 7))) (.mul (.var 2) (.var 6))) (.mul (.var 3) (.var 5))) (.var 8)) (.mul (.add (.add (.add (.mul (.var 0) (.var 5)) (.mul (.var 1) (.var 4))) (.mul (.var 2) (.var 7))) (.mul (.var 3) (.var 6))) (.var 9))) (.mul (.add (.add (.add (.mul (.var 0) (.var 6)) (.mul (.var 1) (.var 5))) (.mul (.var 2) (.var 4))) (.mul (.var 3) (.var 7))) (.var 10))) (.mul (.add (.add (.add (.mul (.var 0) (.var 7)) (.mul (.var 1) (.var 6))) (.mul (.var 2) (.var 5))) (.mul (.var 3) (.var 4))) (.var 11))) (by decide +kernel)330331/-! ## The fractional family -/332333/-- The coefficients of `Σ_ℓ u^ℓ Π_ℓ` reduced with `j² = −1` (`j = i⁻¹ = −i`). -/334def NF0 (q _jj u : Shell p) : Shell p := q * (1 + u + u * u + u * u * u)335def NF1 (q jj u : Shell p) : Shell p := q * (1 + jj * u + -(u * u) + -(jj * (u * u * u)))336def NF2 (q _jj u : Shell p) : Shell p := q * (1 + -u + u * u + -(u * u * u))337def NF3 (q jj u : Shell p) : Shell p := q * (1 + -(jj * u) + -(u * u) + jj * (u * u * u))338339/-- The spectral projector `Π_ℓ = 4⁻¹ Σ_{m<4} i^{−ℓm} F^m`, with `4⁻¹ = −κ` and `i⁻¹ = −i`. -/340def proj (g : Shell p) (κ ℓ : Nat) (k j : Nat) : Shell p :=341  comb g κ (-(ofNat κ)) (-(ofNat κ) * (-(quarterTurn g κ)) ^ ℓ) (-(ofNat κ) * (-(quarterTurn g κ)) ^ (2 * ℓ))342    (-(ofNat κ) * (-(quarterTurn g κ)) ^ (3 * ℓ)) k j343344/-- The fractional family `F^{[s]} = Σ_{ℓ<4} z^{ℓs} Π_ℓ` (6:C3), `z` the refinement base. -/345def frft (g : Shell p) (κ : Nat) (z : Shell p) (s : Nat) (k j : Nat) : Shell p :=346  (z ^ s) ^ 0 * proj g κ 0 k j + (z ^ s) ^ 1 * proj g κ 1 k j + (z ^ s) ^ 2 * proj g κ 2 k j +347    (z ^ s) ^ 3 * proj g κ 3 k j348349/-- Matrix powers on the cycle. -/350def mpow (A : Nat → Nat → Shell p) : Nat → Nat → Nat → Shell p351  | 0 => idm352  | m + 1 => fun k j => sumRange (fun l => mpow A m k l * A l j) (p - 1)353354theorem hjj (F : Frame p κ g) : -(quarterTurn g κ) * -(quarterTurn g κ) + 1 = 0 := by355  rw [neg_mul_neg, F.quarter_turn_sq, neg_add]356357theorem hq (F : Frame p κ g) : (1 + 1 + 1 + 1 : Shell p) * -(ofNat κ) + -1 = 0 := by358  have e4 : (1 + 1 + 1 + 1 : Shell p) = ofNat 4 := by359    rw [show (ofNat 4 : Shell p) = ofNat (3 + 1) from rfl, ofNat_succ, show (ofNat 3 : Shell p) = ofNat (2 + 1) from rfl,360      ofNat_succ, show (ofNat 2 : Shell p) = ofNat (1 + 1) from rfl, ofNat_succ]; rfl361  rw [e4, ← mul_neg, ofNat_mul, ← F.n_eq, F.ofNat_n, neg_neg, add_neg]362363/-- 6:E7, the expansion `F^{[s]} = Σ_r c_r(s) F^r` in the basis `I, F, J, FJ`: the coefficients `c_r(s) = NF_r(z^s)`364(their geometric-sum form is `frft_coeff` of `Theme/Heisenberg.lean`). -/365theorem frft_eq (F : Frame p κ g) (z : Shell p) (s k j : Nat) :366    frft g κ z s k j = comb g κ (NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s)) (NF1 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s))367      (NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s)) (NF3 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s)) k j := by368  have h := frft_aux (-(ofNat κ) : Shell p) (-(quarterTurn g κ)) (z ^ s) (idm k j) (Fmat g κ k j) (J (p - 1) k j)369    (FJ g κ k j)370  exact red1 h (hjj F)371372section conv373variable {q jj : Shell p} (h1 : jj * jj + 1 = 0) (h2 : (1 + 1 + 1 + 1 : Shell p) * q + -1 = 0)374include h1 h2375376theorem conv0 (u v : Shell p) : NF0 q jj u * NF0 q jj v + NF1 q jj u * NF3 q jj v + NF2 q jj u * NF2 q jj v +377    NF3 q jj u * NF1 q jj v = NF0 q jj (u * v) := by378  exact red2 (conv0_aux q jj u v) h1 h2379theorem conv1 (u v : Shell p) : NF0 q jj u * NF1 q jj v + NF1 q jj u * NF0 q jj v + NF2 q jj u * NF3 q jj v +380    NF3 q jj u * NF2 q jj v = NF1 q jj (u * v) := by381  exact red2 (conv1_aux q jj u v) h1 h2382theorem conv2 (u v : Shell p) : NF0 q jj u * NF2 q jj v + NF1 q jj u * NF1 q jj v + NF2 q jj u * NF0 q jj v +383    NF3 q jj u * NF3 q jj v = NF2 q jj (u * v) := by384  exact red2 (conv2_aux q jj u v) h1 h2385theorem conv3 (u v : Shell p) : NF0 q jj u * NF3 q jj v + NF1 q jj u * NF2 q jj v + NF2 q jj u * NF1 q jj v +386    NF3 q jj u * NF0 q jj v = NF3 q jj (u * v) := by387  exact red2 (conv3_aux q jj u v) h1 h2388end conv389390section card391variable {q jj : Shell p} (h1 : jj * jj + 1 = 0) (h2 : (1 + 1 + 1 + 1 : Shell p) * q + -1 = 0)392include h1 h2393394theorem card_one : NF0 q jj (1) = 1 ∧ NF1 q jj (1) = 0 ∧ NF2 q jj (1) = 0 ∧ NF3 q jj (1) = 0 := by395  refine ⟨?_, ?_, ?_, ?_⟩396  · exact red2 (card00_aux q jj) h1 h2397  · exact red2 (card01_aux q jj) h1 h2398  · exact red2 (card02_aux q jj) h1 h2399  · exact red2 (card03_aux q jj) h1 h2400401theorem card_i : NF0 q jj (-jj) = 0 ∧ NF1 q jj (-jj) = 1 ∧ NF2 q jj (-jj) = 0 ∧ NF3 q jj (-jj) = 0 := by402  refine ⟨?_, ?_, ?_, ?_⟩403  · exact red2 (card10_aux q jj) h1 h2404  · exact red2 (card11_aux q jj) h1 h2405  · exact red2 (card12_aux q jj) h1 h2406  · exact red2 (card13_aux q jj) h1 h2407408theorem card_m1 : NF0 q jj (-1) = 0 ∧ NF1 q jj (-1) = 0 ∧ NF2 q jj (-1) = 1 ∧ NF3 q jj (-1) = 0 := by409  refine ⟨?_, ?_, ?_, ?_⟩410  · exact red2 (card20_aux q jj) h1 h2411  · exact red2 (card21_aux q jj) h1 h2412  · exact red2 (card22_aux q jj) h1 h2413  · exact red2 (card23_aux q jj) h1 h2414415theorem card_mi : NF0 q jj (jj) = 0 ∧ NF1 q jj (jj) = 0 ∧ NF2 q jj (jj) = 0 ∧ NF3 q jj (jj) = 1 := by416  refine ⟨?_, ?_, ?_, ?_⟩417  · exact red2 (card30_aux q jj) h1 h2418  · exact red2 (card31_aux q jj) h1 h2419  · exact red2 (card32_aux q jj) h1 h2420  · exact red2 (card33_aux q jj) h1 h2421422end card423424/-- The inverse drive: `z^κ = i` and `z^{p−1} = 1` for `g z = 1`. -/425theorem inv_pow_kappa (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) : z ^ κ = quarterTurn g κ := by426  have e1 : z ^ κ * g ^ κ = 1 := by rw [← mul_pow, mul_comm, hz, one_pow]427  have e2 : quarterTurn g κ * g ^ κ = 1 := by428    show -(g ^ κ) * g ^ κ = 1429    rw [← neg_mul, ← pow_add, ← Nat.two_mul, F.half_period, neg_neg]430  exact inv_unique e1 e2431432theorem inv_pow_n (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) : z ^ (p - 1) = 1 := by433  have e : g ^ (p - 1) * z ^ (p - 1) = 1 := by rw [← mul_pow, hz, one_pow]434  rw [F.pow_n, one_mul] at e; exact e435436/-- 6:C3, the cardinal values: `F^{[0]} = I`, `F^{[κ]} = F`, `F^{[2κ]} = J`, `F^{[3κ]} = F J`. -/437theorem frft_cardinal (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) (k j : Nat) :438    frft g κ z 0 k j = idm k j ∧ frft g κ z κ k j = Fmat g κ k j ∧ frft g κ z (2 * κ) k j = J (p - 1) k j ∧439      frft g κ z (3 * κ) k j = FJ g κ k j := by440  have hzk := inv_pow_kappa F hz441  have h1 := hjj F; have h2 := hq F442  have z1 : z ^ κ = -(-(quarterTurn g κ)) := by rw [neg_neg]; exact hzk443  have z2 : z ^ (2 * κ) = -1 := by rw [Nat.two_mul, pow_add, hzk, F.quarter_turn_sq]444  have z3 : z ^ (3 * κ) = -(quarterTurn g κ) := by445    rw [show 3 * κ = 2 * κ + κ by rw [Nat.succ_mul, Nat.add_comm], pow_add, z2, hzk, ← neg_mul, one_mul]446  refine ⟨?_, ?_, ?_, ?_⟩447  · obtain ⟨e0, e1, e2, e3⟩ := card_one h1 h2448    rw [frft_eq F z 0 k j, pow_zero, e0, e1, e2, e3]449    show 1 * idm k j + 0 * Fmat g κ k j + 0 * J (p - 1) k j + 0 * FJ g κ k j = idm k j450    rw [one_mul, zero_mul, zero_mul, zero_mul, add_zero, add_zero, add_zero]451  · obtain ⟨e0, e1, e2, e3⟩ := card_i h1 h2452    rw [frft_eq F z κ k j, z1, e0, e1, e2, e3]453    show 0 * idm k j + 1 * Fmat g κ k j + 0 * J (p - 1) k j + 0 * FJ g κ k j = Fmat g κ k j454    rw [one_mul, zero_mul, zero_mul, zero_mul, zero_add, add_zero, add_zero]455  · obtain ⟨e0, e1, e2, e3⟩ := card_m1 h1 h2456    rw [frft_eq F z (2 * κ) k j, z2, e0, e1, e2, e3]457    show 0 * idm k j + 0 * Fmat g κ k j + 1 * J (p - 1) k j + 0 * FJ g κ k j = J (p - 1) k j458    rw [one_mul, zero_mul, zero_mul, zero_mul, zero_add, zero_add, add_zero]459  · obtain ⟨e0, e1, e2, e3⟩ := card_mi h1 h2460    rw [frft_eq F z (3 * κ) k j, z3, e0, e1, e2, e3]461    show 0 * idm k j + 0 * Fmat g κ k j + 0 * J (p - 1) k j + 1 * FJ g κ k j = FJ g κ k j462    rw [one_mul, zero_mul, zero_mul, zero_mul, zero_add, zero_add, zero_add]463464/-- 6:C3, additivity: `F^{[s+r]} = F^{[s]} F^{[r]}` on the cycle, a representation of `ℤ/(p−1)`. -/465theorem frft_add (F : Frame p κ g) (z : Shell p) (s r : Nat) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :466    frft g κ z (s + r) k j = sumRange (fun l => frft g κ z s k l * frft g κ z r l j) (p - 1) := by467  rw [sum_congr _ (fun l _ => by rw [frft_eq F z s k l, frft_eq F z r l j]), comb_mul F hk hj, frft_eq F z (s + r) k j,468    pow_add, conv0 (hjj F) (hq F), conv1 (hjj F) (hq F), conv2 (hjj F) (hq F), conv3 (hjj F) (hq F)]469470/-- 6:C3, the period: the family is periodic over the cycle, `F^{[s + (p−1)]} = F^{[s]}`, so `F^{[4κ]} = I`. -/471theorem frft_period (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) (s k j : Nat) :472    frft g κ z (s + (p - 1)) k j = frft g κ z s k j := by473  unfold frft; rw [pow_add, inv_pow_n F hz, mul_one]474475/-- 6:C3, the root: `F^{[m s]} = (F^{[s]})^m`; in particular `(F^{[1]})^κ = F^{[κ]} = F`. -/476theorem frft_pow (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) (s : Nat) :477    ∀ m k j, k < p - 1 → j < p - 1 → frft g κ z (m * s) k j = mpow (frft g κ z s) m k j478  | 0, k, j, _, _ => by rw [Nat.zero_mul]; exact (frft_cardinal F hz k j).1479  | m + 1, k, j, hk, hj => by480    rw [Nat.succ_mul, frft_add F z (m * s) s hk hj]481    exact sum_congr _ (fun l hl => by rw [frft_pow F hz s m k l hk hl])482483/-- **C2 (p00022), scale-shift duality.** Dilation `x ↦ g x` is phase evolution of the frame: it advances the484meridian index (`S_r(M_m) = M_{m+r}`), with period `p − 1`; over the cycle it is the fractional Fourier family, a485representation of `ℤ/(p−1)` (`F^{[s+r]} = F^{[s]} F^{[r]}`, period `p − 1`) whose quarter-turn value `F^{[κ]}` is the486transform `F` itself, with `F^{[0]} = I`, `F^{[2κ]} = J`, `F^{[3κ]} = F J = F⁻¹` and `(F^{[1]})^κ = F`. -/487theorem scale_shift (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) :488    (∀ m r, (meridian g κ m).map (scale g r) = meridian g κ (m + r)) ∧489    (∀ r x, scale g (r + (p - 1)) x = scale g r x) ∧490    (∀ s r k j, k < p - 1 → j < p - 1 →491      frft g κ z (s + r) k j = sumRange (fun l => frft g κ z s k l * frft g κ z r l j) (p - 1)) ∧492    (∀ s k j, frft g κ z (s + (p - 1)) k j = frft g κ z s k j) ∧493    (∀ k j, frft g κ z 0 k j = idm k j ∧ frft g κ z κ k j = Fmat g κ k j ∧ frft g κ z (2 * κ) k j = J (p - 1) k j ∧494      frft g κ z (3 * κ) k j = FJ g κ k j) ∧495    (∀ k j, k < p - 1 → j < p - 1 → sumRange (fun l => FJ g κ k l * Fmat g κ l j) (p - 1) = idm k j) ∧496    (∀ k j, k < p - 1 → j < p - 1 → mpow (frft g κ z 1) κ k j = Fmat g κ k j) :=497  ⟨fun m r => meridian_scale g κ m r, fun r x => FRC.Shell.scale_periodic F r x,498   fun s r k j hk hj => frft_add F z s r hk hj, fun s k j => frft_period F hz s k j,499   fun k j => frft_cardinal F hz k j, fun k j hk hj => mm_GF F hk hj,500   fun k j hk hj => by rw [← frft_pow F hz 1 κ k j hk hj, Nat.mul_one]; exact (frft_cardinal F hz k j).2.1⟩501502/-- 00:C2 — the transform follows the dilation: `g^s = g^{s'}` gives `F^{[s]} = F^{[s']}`, so the fractional Fourier503family is indexed by the dilations themselves. -/504theorem frft_dilation (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {s s' : Nat} (h : g ^ s = g ^ s') (k j : Nat) :505    frft g κ z s k j = frft g κ z s' k j := by506  have hper : ∀ n u, frft g κ z (u + n * (p - 1)) k j = frft g κ z u k j := fun n u => by507    induction n with508    | zero => rw [Nat.zero_mul, Nat.add_zero]509    | succ n ih => rw [Nat.succ_mul, ← Nat.add_assoc, frft_period F hz, ih]510  have hred : ∀ u, frft g κ z u k j = frft g κ z (u % (p - 1)) k j := fun u => by511    obtain ⟨q, hq⟩ := FRC.Nat.mod_spec (p - 1) F.n_pos u512    conv => lhs; rw [hq, Nat.add_comm, Nat.mul_comm]513    exact hper q _514  have hm : s % (p - 1) = s' % (p - 1) :=515    F.pow_inj (Nat.mod_lt _ F.n_pos) (Nat.mod_lt _ F.n_pos) (by rw [← F.pow_mod, ← F.pow_mod]; exact h)516  rw [hred s, hred s', hm]517518/-! ## C7: the conjugate frame, and the Carrier's quarter-turn -/519520/-- 6:C9, the conjugate frame: the inverse drive `g⁻¹` is a frame of the same shell and capacity. -/521theorem inv_frame (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) : Frame p κ z := by522  have hpow : ∀ l, g ^ l * z ^ l = 1 := fun l => by rw [← mul_pow, hz, one_pow]523  exact ⟨F.cap, F.cap_pos, ⟨by have := hpow (p - 1); rwa [F.pow_n, one_mul] at this,524    fun l hl hl0 e => F.prim.2 l hl hl0 (by have := hpow l; rwa [e, mul_one] at this)⟩⟩525526theorem inv_quarter (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) : quarterTurn z κ = -quarterTurn g κ := by527  show -(z ^ κ) = -quarterTurn g κ528  rw [inv_pow_kappa F hz]529530/-- 6:C9, the conjugate frame's transform is `−F J = −F⁻¹`. -/531theorem Fmat_conj (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {k j : Nat} (_hk : k < p - 1) (hj : j < p - 1) :532    Fmat z κ k j = -(FJ g κ k j) := by533  have hn := F.n_pos534  have e1 : z ^ (j * k) * g ^ (j * k) = 1 := by rw [← mul_pow, mul_comm, hz, one_pow]535  have e2 : g ^ (rev (p - 1) j * k) * g ^ (j * k) = 1 := by536    rw [← pow_add, ← FRC.Nat.add_mul, F.pow_mod, ← FRC.Nat.mod_mul_mod _ _ _ hn, rev_add_mod hj, Nat.zero_mul,537      FRC.Nat.zero_mod, pow_zero]538  show quarterTurn z κ * z ^ (j * k) = -(quarterTurn g κ * g ^ (rev (p - 1) j * k))539  rw [inv_quarter F hz, inv_unique e1 e2, neg_mul]540541theorem FJ_conj (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :542    FJ z κ k j = -(Fmat g κ k j) := by543  have hn := F.n_pos544  show Fmat z κ k (rev (p - 1) j) = -(Fmat g κ k j)545  rw [Fmat_conj F hz hk (rev_lt hn j)]546  show -(Fmat g κ k (rev (p - 1) (rev (p - 1) j))) = -(Fmat g κ k j)547  rw [rev_rev hj]548549theorem comb_conj (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1)550    (c0 c1 c2 c3 : Shell p) : comb z κ c0 c1 c2 c3 k j = comb g κ c0 (-c3) c2 (-c1) k j := by551  show c0 * idm k j + c1 * Fmat z κ k j + c2 * J (p - 1) k j + c3 * FJ z κ k j =552    c0 * idm k j + -c3 * Fmat g κ k j + c2 * J (p - 1) k j + -c1 * FJ g κ k j553  rw [Fmat_conj F hz hk hj, FJ_conj F hz hk hj]554  exact Shell.Frame.RE.sound (Shell.Frame.look [c0, c1, c2, c3, idm k j, Fmat g κ k j, J (p - 1) k j, FJ g κ k j])555    (.add (.add (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) (.neg (.var 7)))) (.mul (.var 2) (.var 6)))556      (.mul (.var 3) (.neg (.var 5))))557    (.add (.add (.add (.mul (.var 0) (.var 4)) (.mul (.neg (.var 3)) (.var 5))) (.mul (.var 2) (.var 6)))558      (.mul (.neg (.var 1)) (.var 7))) (by decide +kernel)559560theorem neg_sq_pow {i : Shell p} (h : i * i = -1) : (-i) ^ 2 = -1 := by rw [pow_two, neg_mul_neg]; exact h561theorem cube_pow {i : Shell p} (h : i * i = -1) : i ^ 3 = -i := by562  rw [pow_succ, pow_two, h, ← neg_mul, one_mul]563theorem neg_cube_pow {i : Shell p} (h : i * i = -1) : (-i) ^ 3 = i := by564  rw [pow_succ, neg_sq_pow h, neg_mul_neg, one_mul]565566/-- 6:C9, the conjugate frame's projectors are the shifted ones, `Π'_ℓ = Π_{ℓ+2}`. -/567theorem proj_conj (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) (ℓ : Nat) {k j : Nat} (hk : k < p - 1)568    (hj : j < p - 1) : proj z κ ℓ k j = proj g κ (ℓ + 2) k j := by569  have h := F.quarter_turn_sq570  unfold proj571  rw [inv_quarter F hz, neg_neg, comb_conj F hz hk hj]572  have a1 : -(-(ofNat κ : Shell p) * quarterTurn g κ ^ (3 * ℓ)) = -(ofNat κ) * (-(quarterTurn g κ)) ^ (ℓ + 2) := by573    rw [pow_mul, cube_pow h, pow_add, neg_sq_pow h, ← mul_neg, mul_one, mul_neg]574  have a2 : -(ofNat κ : Shell p) * quarterTurn g κ ^ (2 * ℓ) = -(ofNat κ) * (-(quarterTurn g κ)) ^ (2 * (ℓ + 2)) := by575    rw [pow_mul, pow_mul, pow_two, h, neg_sq_pow h, pow_add, pow_two (-1 : Shell p), neg_mul_neg, one_mul, mul_one]576  have a3 : -(-(ofNat κ : Shell p) * quarterTurn g κ ^ ℓ) = -(ofNat κ) * (-(quarterTurn g κ)) ^ (3 * (ℓ + 2)) := by577    rw [pow_mul, neg_cube_pow h, pow_add, pow_two, h, ← mul_neg, mul_one, mul_neg]578  rw [a1, a2, a3]579580/-- **C7 (p00172), orientation is derived.** On every Carrier the quarter-turn `ħ` (`ħ² = −1`) has `ħ^S = ±1` when581`S` is even: no orientation survives transport. On every frame the oriented quarter-turn is the conjugate drive's582power, `i = −g^κ = (g⁻¹)^κ`; the conjugate `g⁻¹` is a frame with quarter-turn `−i`, its transform is `−F J = −F⁻¹`,583and its projectors are `Π_{ℓ+2}`: the joint flip permutes the registration channels and preserves their family. -/584theorem orientation (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) :585    (∀ {Ω : Nat} [Pos Ω] (h : Shell Ω) (S : Nat), h * h = -1 → S % 2 = 0 → h ^ S = 1 ∨ h ^ S = -1) ∧586    z ^ κ = quarterTurn g κ ∧ Frame p κ z ∧ quarterTurn z κ = -quarterTurn g κ ∧587    (∀ k j, k < p - 1 → j < p - 1 → Fmat z κ k j = -(FJ g κ k j)) ∧588    (∀ ℓ k j, k < p - 1 → j < p - 1 → proj z κ ℓ k j = proj g κ (ℓ + 2) k j) := by589  refine ⟨fun h S hh hS => ?_, inv_pow_kappa F hz, inv_frame F hz, inv_quarter F hz,590    fun k j hk hj => Fmat_conj F hz hk hj, fun ℓ k j hk hj => proj_conj F hz ℓ hk hj⟩591  obtain ⟨m, hm⟩ := FRC.Nat.mod_spec 2 (by decide) S592  rw [hS, Nat.add_zero] at hm593  rw [hm, pow_mul, pow_two, hh, neg_one_pow]594  exact match Nat.decEq (m % 2) 0 with595    | isTrue e => .inl (by rw [ite_eq_left e])596    | isFalse e => .inr (by rw [ite_eq_right e])597598end Frame599end Shell600end FRC601