{"id":"palomar/PALOMAR-2026-08-27-000017","url":"https://github.com/Arthur742Ramos/SpinorLean/tree/5c890f3466da7433a133eb45c5372a55fbdab1da","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-27-000017-v1.json","repo":"https://github.com/Arthur742Ramos/SpinorLean","tags":["math.RA","msc:15A66","msc:11E81","msc:20G15","algebra","lean","spinors","clifford-algebra"],"score":0,"title":"Arthur742Ramos/SpinorLean","trust":"high","domain":"math.RA","source":"palomar","authors":["Arthur F. Ramos","David B. Hulak","Ruy J. G. B. de Queiroz"],"reviews":0,"subject":"math.RA","summary":"Formalizes an exterior-model spinor construction for a field K in which 2 is invertible, using an explicit hyperbolic presentation and the Clifford conjugation action on the ambient quadratic space. The development proves field-sensitive covering and image results: the positive split-rank spin-to-isometry kernel is {1,-1}, the spin action therefore descends only projectively, the split-line image is exactly the square-scaling subgroup, and a finite-dimensional split Levi element associated to g lies in the ambient spin image exactly when det(g) is a square unit. The repository also packages…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-27","reactions":{},"formalized":true,"formalizes":[{"title":"Exterior-Model Spinors in Split Rank: Exact Levi Images and Square-Determinant Obstructions","identifier":"arXiv:2604.26155","relationship":"formalizes"}]}