| # | Description | Status | Sources |
|---|---|---|---|
| A. Inputs: imported, not derived here | |||
| A1p06001 | The framed shell: $\Fp(\chron;0,1,\gen)$ with $\p=4\kap+1$, its register $\pi=2\kap$, $\im=-\gen^{\kap}=\gen^{-\kap}$, $e=\gen^{\im}$; the frame-relative labels and the atlas of presentations $\gen\mapsto\gen^{u}$. | I | |
| A2p06002 | The Weil representation $\omega_\p$ of $\SL(2,\Fp)$ and its Schrödinger model, the finite Fourier transform representing the rotation $w$, the finite harmonic oscillator; the scalar convention $\omega_\p(w)^{2}=\omega_\p(-I)$, $\omega_\p(w)^{4}=I$. | I | |
| A3p06003 | The sign of the quadratic Gauss sum: $G=\sum_k\gen^{k^{2}}=\varepsilon(1+\im)$ for a sign $\varepsilon\in\{\pm1\}$, the in-field form of the classical evaluation $\sum_k\zeta_n^{k^{2}}=(1+i)\sqrt n$ for $4\mid n$. | I | [Berndt et al. 1998; Gurevich et al. 2010] |
| A5p06005 | The framed-rational zoom: the grids $G_n$ and their $(\p-1)$-periodicity $G_{n+(\p-1)}=G_n$, the meridian shift $m\mapsto m-1$ as the refinement step. | I | [Akhtman 2025, §4.3, Lemma 2] |
| A7p06007 | The continuum fractional Fourier transform and the finite constructions the family is placed against: the eigenbasis transforms, the eigenvector-free and matrix-function transforms, the canonical DFT eigenbasis, the arithmetic FrFT of the rotation group. | I | [Namias 1980; Ozaktas et al. 2001; Lima & Campello de Souza 2012; Pei et al. 2011; Lima & Campello de Souza 2016; Lima et al. 2017; Gurevich & Hadani 2009; Floratos & Pavlidis 2024] |
| A8p06055 | The framework’s definition of the substrate: the Carrier, a finite totality whose count bounds the coordinate plane $\Fp\times\Fp$ of an embedded observer, $\p^{2}<\Om$; the shell of capacity $\kap$ as the observer’s register, its phase cycle of $4\kap=\p-1$ points read as the area. | I | [Akhtman 2026, §2] master: 00:D15 |
| B. The shell: the frame datum and the Fourier operator | |||
| B1p06008 | Shell data, capacity-first: $\kap$ primary, $\p=4\kap+1$, the phase cycle $\Phit=\Z_{4\kap}$, the oriented quarter-turn $\im=-\gen^{\kap}$ (clockwise phase convention), $\pi=2\kap$, $e=\gen^{\im}$; the meridians $M_s=\{a\gen^{s}:a\in I_\p\}$; the six shells of Table 1 with their roots and quarter-turns. | D |  § 2, (2.1), (2.2), Def. 1 |
| B2p06009 | The Euler identity is a property of the chart class: $e^{\im\pi}=\gen^{2\kap(\im\bmod2)}\equiv-1$ exactly when the quarter-turn residue is odd; the conjugate chart $(\gen,\im)\mapsto(\gen^{-1},-\im)$ toggles the parity, so one member of each conjugate pair carries it; on $\F_{13}(\chron;0,1,2)$, $\im=5$ and $6^{6}=-1$. Every primitive frame of the six shells. | T |  Rem. 2 master: 00:C14 |
| B3p06010 | Chart covariance: under $\gen'=\gen^{u}$, $u\in\Zp^{\times}$, the quarter-turn name flips exactly on $u\equiv3\pmod4$ and the exponential-unit name moves already at $u\equiv1\pmod4$ whenever $\im(u-1)\not\equiv0\pmod{4\kap}$ ($\p=13$, $u=5$: $e'=2\neq6$); the objects of C3, C4 and C9 are invariant. | T | Rem. 3 |
| B4p06011 | The shell Fourier matrix $\Wt_{kj}=\gen^{jk}$ on $\Vt=\Fp^{\Phit}$, the reversal $J$, the normalized shell Fourier operator $\Ft=\im\Wt$. | D | (3.2), (3.1), § 3 |
| B5p06012 | $\Wt^{2}=-J$, $\Ft^{2}=J$, $\Ft^{4}=I$: the normalized operator generates the four-cycle, on the six shells of Table 1. | T |  Lem. 1, Prop. 1 master: 00:C2 |
| B6p06013 | The normalization is the unitary constant read in the field: $1/n\equiv-1$, its square roots in $\Fp$ are exactly $\pm\im$, and $(c\Wt)^{2}=J$ if and only if $c=\pm\im$. | T | Rem. 4 |
| B7p06014 | $\Wt J=J\Wt$, hence $\Ft J=J\Ft$; every $v$ is uniquely $v^{+}+v^{-}$ with $Jv^{\pm}=\pm v^{\pm}$, a symmetric vector determined by its $2\kap+1$ entries at $0,\dots,2\kap$ and an antisymmetric one by its $2\kap-1$ entries at $1,\dots,2\kap-1$. | T | Lem. 3 |
| C. The fractional family | |||
| C1p06015 | The projectors $\Pi_\ell=\tfrac14\sum_{r=0}^{3}\im^{-\ell r}\Ft^{r}$ and the principal framed character lift $\Ft^{[s]}=\sum_\ell\gen^{-\ell s}\Pi_\ell$, $s\in\Phit$: the refinement base is the inverse root, $(\gen^{-1})^{\kap}=\im$, each projector’s character the $\ell$-th power of the meridian phase $z_s=\gen^{-s}$. | D | (4.1), (4.2), Rem. 5 |
| C2p06016 | $\Pi_\ell^{2}=\Pi_\ell$, $\Pi_\ell\Pi_m=0$ for $\ell\neq m$, $\sum_\ell\Pi_\ell=I$, $\Ft\Pi_\ell=\im^{\ell}\Pi_\ell$. | T | Lem. 2 |
| C3p06017 | The exact finite-field FrFT: $s\mapsto\Ft^{[s]}$ is a representation of $\Phit$, $\Ft^{[s+r]}=\Ft^{[s]}\Ft^{[r]}$ for all $s,r$ (every pair on the six shells by the package), with the cardinal values $\Ft^{[0]}=I$, $\Ft^{[\kap]}=\Ft$, $\Ft^{[2\kap]}=J$, $\Ft^{[3\kap]}=\Ft^{-1}$, and $(\Ft^{[1]})^{\kap}=\Ft$. | T | Thm. 1 master: 00:C2 |
| C4p06018 | Faithfulness: $s\mapsto\Ft^{[s]}$ is injective on $\Z_{4\kap}$ for every $\kap\ge1$; at $\p=5$ the surviving odd projector carries the faithful character. | T | Thm. 3 |
| C5p06019 | The projector sums $\Pi_0+\Pi_2=\tfrac12(I+J)$ and $\Pi_1+\Pi_3=\tfrac12(I-J)$; $\Pi_0,\Pi_2\neq0$ for every $\kap\ge1$ and $\Pi_1,\Pi_3\neq0$ for $\kap\ge2$, each by one explicit entry; at $\p=5$ exactly one of $\Pi_1,\Pi_3$ vanishes. | T | Lem. 4 |
| C6p06020 | The projectors are chart data: for $u$ odd and a unit mod $4\kap$ the index relabelling $m\mapsto um$ carries $\Ft(\gen)$ to $\Ft(\gen^{u^{2}})$ by a coordinate permutation, $\Ft(\gen^{u^{2}})_{kj}=\Ft(\gen)_{uk,uj}$; at $\p=13$ the frames $\gen=2$ and $\gen=6$ give the trace tuples $(3,3,4,2)$ and $(4,2,3,3)$, with $\operatorname{Tr}\Ft=4,9$. | T | Rem. 6 |
| C7p06021 | The multiplicity dichotomy in trace form: with $G=\sum_{k}\gen^{k^{2}}$ and $G^{*}=\sum_k\gen^{-k^{2}}$ the traces are $\operatorname{Tr}\Ft=\im G$, $\operatorname{Tr}\Ft^{2}=2$, $\operatorname{Tr}\Ft^{3}=\im G^{*}$ and $\operatorname{Tr}\Pi_\ell=\tfrac14\sum_r\im^{-\ell r}\operatorname{Tr}\Ft^{r}$; $GG^{*}=-2$ and $\varepsilon(\gen^{-1})=-\varepsilon(\gen)$; when $G=\varepsilon(1+\im)$ (A3) the tuple of traces is $(\kap,\kap,\kap+1,\kap-1)$ for $\varepsilon=+1$ and $(\kap+1,\kap-1,\kap,\kap)$ for $\varepsilon=-1$, read in $\Fp$; the sign and the tuples on the six shells of Table 1. Exact on the $38$ primitive frames of $\p\in\{5,13,17,29,37\}$ and the $16$ of $\p=41$. | T | Thm. 2 |
| C8p06022 | Exponent lifts: every lift $a_\ell\equiv\ell\pmod4$, $U^{(a)}_s=\sum_\ell\gen^{-a_\ell s}\Pi_\ell$, is additive with the same cardinal skeleton, $U^{(a)}_{s+r}=U^{(a)}_sU^{(a)}_r$ and $U^{(a)}_{m\kap}=\Ft^{m}$. | T | Rem. 5 |
| C9p06023 | The conjugate chart $(\gen,\im)\mapsto(\gen^{-1},-\im)$: exactly $\Ft'=-\Ft^{-1}$ and $\Pi'_\ell=\Pi_{\ell+2}$; the operator relations, cardinal values, additivity and faithfulness hold on the conjugate frame, and its trace tuple is the other pattern of C7. | T | Rem. 3, Thm. 2 master: 00:C7 |
| C11p06052 | Charts outside the classified lifts: for $u$ a unit mod $4\kap$, $\Wt(\gen^{u})=\Wt P_u$ with $P_u$ the index relabelling $j\mapsto uj$, so $\Wt\,\Wt(\gen^{u})=-JP_u$ and $\Wt(\gen^{u})\,\Wt=-JP_{u^{-1}}$, and the two differ at the entry $(-u,1)$ when $u^{2}\not\equiv1\pmod{4\kap}$: a family canonical in such a chart does not commute with $\Ft$; $\p=29$, $u=5$, and every such chart of the six shells of Table 1 checked. | T | Rem. 5 |
| D. Meridional domains and the scale-shift | |||
| D1p06024 | The meridional domain $D_s=(\Vt,\mathcal B_s)$, $\mathcal B_s=\Ft^{[s]}\mathcal B_0$, every $\Ft^{[s]}$ invertible with inverse $\Ft^{[n-s]}$; the cardinal domains spatial, spectral, parity, inverse-spectral. | D | Def. 5 |
| D2p06025 | The $4\kap$ framed domains are pairwise distinct; read as unordered bases $B_{s+2\kap}=B_s$, since $\Ft^{[s+2\kap]}=\Ft^{[s]}J$ and $J$ permutes the standard basis. | T | Thm. 3, Rem. 7 |
| D3p06026 | The meridian-step interval $I_\p=\{0,1,\dots,\pi\}$, the scale-shift $S_r(x)=\gen^{r}x$, the dilation by $\gen^{r}$, and the local scale chart $\gen\mapsto\lambda>1$ reading the effective step $\gen^{m}$ as $\lambda^{\tilde m}$ [chart]: the forward shift a zoom-out and the inverse shift a zoom-in, the return of the lift the scale-periodicity of A5, the readings valid while $w\gen^{r}<\p$. | D | (5.1), Def. 6, Def. 7 |
| D4p06027 | Scale-shift covariance: $S_r(M_m)=M_{m+r}$ for all $m$ and $r$, as ordered lists; consecutive entries of $M_m$ differ by the effective step $\gen^{m}$; $S_{r+(\p-1)}=S_r$, the periodicity of A5 in meridian form; at $\p=13$, $\gen=2$ the ladder $M_0,\dots,M_3$ at the steps $1,2,4,8$ (Section 7). | T | Prop. 2, Cor. 1 master: 00:C2 |
| D6p06029 | Scope of the two readings: the representation-side rotation and the coordinate-side scale-shift act on carriers of different dimension and are not equal as operators; they share the index group $\Phit$ and the cardinal labels, and the operator-level relation is E5–E9. | D | Rem. 8 |
| D7p06053 | The cycle carries exactly $2\kap$ unordered bases: every entry $(0,k)$, $k\neq0$, of $\Ft^{[t]}$ is $\tfrac{\im}{2}(1-\gen^{-2t})$, nonzero for $t\notin\{0,2\kap\}$, so $\Ft^{[t]}$ is not monomial and $B_{s+t}\neq B_s$; the six shells of Table 1. | T | Rem. 7 |
| E. The rotations, the Weil dictionary and the operator-level comparison | |||
| E1p06030 | The Weil-side data: $z_s=\gen^{-s}$, $c_s=(z_s+z_s^{-1})/2$, $d_s=(z_s-z_s^{-1})/(2\im)$, the rotation $R_s$; the pulled-back family $\operatorname{FrFT}^{\rm Weil}_\kap(s)=\omega_\p(R_s)$; cardinal Weil correspondence of two families. | D | (6.1), Def. 8 |
| E2p06031 | $R_s\in SO(2,\Fp)$, and $s\mapsto R_s$ is an isomorphism $\Phit\simeq SO(2,\Fp)$ with $|SO(2,\Fp)|=\p-1=4\kap$: the full rotation group of the $\p^{2}$-point plane is the phase cycle. | T | Prop. 3 |
| E3p06032 | The cardinal-skeleton dictionary $M_s\leftrightarrow s\leftrightarrow z_s\leftrightarrow R_s$ with $R_0=I$, $R_\kap=w$, $R_{2\kap}=-I$, $R_{3\kap}=w^{-1}$ (the $R_\kap$ column of Table 1), $z_\kap=\im$; the shell’s family and the Weil family stand in cardinal Weil correspondence, the Weil side by the normalization of A2 (an import). | T | Thm. 4 and the paragraph after it |
| E4p06033 | Scope of the dictionary: agreement on the four cardinal indices only, the two families on spaces of different dimension over different coefficient rings, the Weil model one dimension larger as a count; no relation at an intermediate index is asserted. | D | Rem. 9 |
| E5p06034 | Spectral obstruction: for $\kap\ge2$ no invertible $T$ on $\Vt$ satisfies $T\sigma T^{-1}=\Ft^{[s]}$ for any $s$; the cyclic groups $\langle\sigma\rangle$ and $\langle\Ft^{[1]}\rangle$, each of order $4\kap$ ($\Ft^{[1]}$ by C4; $\sigma$ permutes the $4\kap$ labels cyclically), are not conjugate. | T | Prop. 4 |
| E6p06035 | Common character sector: $\Ft^{[s]}\Pi_1=\gen^{-s}\Pi_1$, so on $E_1=\operatorname{im}\Pi_1\neq0$ ($\kap\ge2$) the family acts by the meridian character; the intertwiner $\Ft^{[s]}T_v=T_vS_{-s}$ on every $x\in\Fp$ and $s$, and $R_s(1,-\im)^{\mathsf T}=\gen^{-s}(1,-\im)^{\mathsf T}$. | T | Prop. 5 |
| E7p06036 | Cardinal Heisenberg covariance: $\Ft\sigma\Ft^{-1}=D_1$, $\Ft D_1\Ft^{-1}=\sigma^{-1}$; $\Ft^{r}\sigma=\sigma_r\Ft^{r}$ with $(\sigma,D_1,\sigma^{-1},D_1^{-1})$; the expansion (6.3), $\Ft^{[s]}=\sum_r c_r(s)\Ft^{r}$ with $c_r(s)=\tfrac14\sum_\ell(\gen^{r\kap-s})^{\ell}$. | T | Prop. 6, § 6.1 |
| E8p06050 | Cardinal exclusivity: the conjugate $\Ft^{[s]}\sigma\Ft^{[s]\,-1}$ of (6.3) is not monomial for every $s\notin\{0,\kap,2\kap,3\kap\}$ — off $j\in\{-1,0,1\}$ its row $0$ is $x^{-1}$ times a quadratic in $x=\gen^{j}$ with leading coefficient $\im\,[c_0(s)+c_2(s)]\,c_3(-s)\neq0$, $c_0(s)+c_2(s)=\tfrac12(1+\gen^{-2s})$, so the row vanishes at no three distinct indices off those three and, by counting, has at least $4\kap-5$ nonzero entries; the count checked on every shell below $200$. | T | Thm. 5 |
| E9p06054 | The spectra behind E5: every nonzero residue $b$ is an eigenvalue of $\sigma$, with the geometric eigenvector $(b^{-j})_j$ (so $\sigma$ is diagonalizable over $\Fp$ with the $4\kap$ simple eigenvalues $\Fpx$, the Mathlib reading); an eigenvalue of $\Ft^{[s]}=\sum_\ell\gen^{-\ell s}\Pi_\ell$ is one of the four $\gen^{-\ell s}$ ($\Ft^{[1]}$ on the six shells). | T | Prop. 4 |
| E10p06056 | The plane as orbits of the cycle: $R_s$ scales $u=x+\im y$ by $z_s$ and $v=x-\im y$ by $z_s^{-1}$, so every point off the origin has a free orbit of size $4\kap=|SO(2,\Fp)|$, and $\p^{2}=1+(4\kap+2)\,4\kap$ is the count of the origin and $4\kap+2$ orbits (the $4\kap$ circles of nonzero norm and the two isotropic lines, by counting); $\dim\Vt=4\kap$. | T | Cor. 2 |
Nothing matches that filter.
Status
- I
- Import. A standard result, a corpus result, or a convention used here without reproof.
- D
- Definition. A naming, a declared dictionary, or a set-up move, carrying no empirical content.
- T
- Theorem. Derived within this paper, checked in exact arithmetic by the named python check, and proved in Lean 4 in the framework’s core library with no axioms.
Sources
- Gold: the python check that decides the predicate, at its line in the script (the source, rendered on this site); on hover the deciding family and the families that corroborate it, and the verdict of the last run (red when it fails). The script page's bar runs the predicate's cell of the package's notebook on Google Colab (one cell per predicate; the whole notebook from the header badge).
- The predicate as one Lean declaration, named by its accession key (
p06008) — the conjunction of the theorems that prove it — at its line in the rendered module, one mark per library that proves it, the core's first. Green: the core (lean/FrcCore) — the statement on the shell ring, by computation and induction, no Mathlib, no axioms: the finitist witness. Violet: Mathlib (lean/FrcLedger) — the classical statement for every shell on Mathlib's hierarchy (its axioms,propext,Classical.choice,Quot.sound, on hover). Red: a proof the gate rejects (an unfinished proof,native_decide) — not a witness. A predicate proved in both libraries shows both marks; one mark, one proof. The module page's bar opens the module as one executable file in Lean Live (the core on plain Lean, no Mathlib; the file elaborates in the browser and prints every predicate's axioms at its end); the header's two Lean badges count the marks of each colour and open the two executables. - section
- The statement in the paper's body that carries the predicate: a proposition, a remark or a section.
- rests on
- The predicates it rests on, by label: realisations, definitions and imports of this ledger, predicates of other ledgers (
32:B3) and of the master (00:D15).