Remark. What the recurrence does not classify [fcap-0016]
Remark. What the recurrence does not classify [fcap-0016]
Hyperbolic reduction determines the matrix factor coming from matched positive and negative axes. It leaves a one-sided algebra \(\mathcal {C}\kern -2pt\ell _{r,0}\) or \(\mathcal {C}\kern -2pt\ell _{0,r}\). The signature-switch recurrence of Theorem [fcap-001X] provides a second move, and Example [fcap-0015] fixes the first real, complex, quaternionic, and matrix entries. These facts still have to be assembled into recurrences that close on each one-sided axis.
A reviewed local candidate called SPINREP-050 establishes the quaternion recurrence \[\mathcal {C}\kern -2pt\ell _{p,q+2}\simeq \mathcal {C}\kern -2pt\ell _{q,p}\otimes _{\mathbb R}\mathbb H,\] and another local candidate, SPINREP-053, iterates the recurrence chain to \[\mathcal {C}\kern -2pt\ell _{p+8,q}\simeq \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb R}M_{16}(\mathbb R).\] Neither candidate is a merged TauCeti declaration or a public TauCeti pull request, so neither receives a Lean marker here.
The residue-indexed mod-eight classification table remains unformalized. In particular, the mixed \((1,1)\) recurrence alone only removes matched axes; it cannot classify the one-sided remainder. Lawson--Michelsohn give the full classical periodicity and table in [lawson2016spin, I.4, Theorem 4.3 and Tables I--II, pp. 27--29].