Mathematical City · Citadel evidence bulletin · 2026-10-23
E47 Identity.
A finite mathematical construction whose invariant subspace is derived from 125 spin-2 tensor states, witnessed in exact matrix arithmetic, and partially formalized in Lean and Coq.
Carrier
125
Invariant kernel
47
Sharp contraction
15/17
Canonical identity
H = V₂ ⊗ V₂ ⊗ V₂ ; C = J² ; K = (C−6I)(C−30I)
Spin multiplicities (1, 3, 5, 4, 3, 2, 1) yield ker(K) ≅ 5V₂ ⊕ 2V₅, dimension 47. The polynomial selector T(C)/1814400 projects onto exactly those sectors, with T(x)=x(x−2)(x−12)(x−20)(x−31)(x−42).
Current evidence ledger
| Layer | Status | Receipt |
|---|---|---|
| Lean weight algebra and Coq spectral formalism | Accepted | Compiler CI |
| Coq tower induction | Accepted | Coq CI |
| Independent 125×125 integer matrix audit | 20/20 reported | Independent report, PDF SHA-256 4de6e7cb…40a0c7 |
| Concrete 125×125 matrix theorem in Mathlib | Compiler pending | Draft PR #11 |
| Physical quantum processor measurement | Not performed | Hardware experiment docket |
The independent audit reproduced finite operators using arbitrary-precision integers and Gram-adjoint checks; it did not compile Lean/Coq, operate a quantum processor, or run every repository.
Source and governance
Machine-readable evidence packet · Lean source · Coq source · Original mathematical citizen · Citadel