| # | Description | Status | Sources |
|---|---|---|---|
| A. Inputs | |||
| A1p03001 | Finite-field algebra: $\Fpx$ is cyclic of order $\p-1$ with two square classes $S=(\Fpx)^{2}$ and $N=\Fpx\setminus S$ of $(\p-1)/2$ each; $-1\in S$ for $\p\equiv1\pmod4$; $X^{2}-\nu$ is irreducible for $\nu\in N$ and $\Fpq=\Fp(\sqrt\nu)$; every element of $\Fp$ is a square in $\Fpq$. | I | |
| A2p03002 | Quadratic forms over finite fields of odd characteristic: nondegenerate forms are classified by dimension and discriminant, isotropic in dimension three and more; in dimension four the hyperbolic type (discriminant a square, Witt index two, $q^{3}+q^{2}-q$ zeros, $|O_{4}^{+}(q)|=2q^{2}(q^{2}-1)^{2}$) and the elliptic type (discriminant a nonsquare, Witt index one, $q^{3}-q^{2}+q$ zeros, $|O_{4}^{-}(q)|=2q^{2}(q^{4}-1)$); Witt’s theorem. | I | |
| A3p03003 | The framed substrate: the shell $\p=4\kap+1$ with frame $(\chron;0,1,\g)$ and quarter-turn $\im=-\g^{\kap}$ (1:B2, B3); the square class as drive-step parity, the drive $\g$ a nonsquare on every shell, $\nu=\g$ canonical (8:B3, B5; 00:C8); the boost cycle as the non-split torus (8:D5; 22:A2). | I | |
| A4p03004 | The continuum comparison: Minkowski’s form $-c^{2}t^{2}+x^{2}+y^{2}+z^{2}$ of signature $(1,3)$ and Witt index one over $\R$, its Lorentz group $O(1,3)$; the ordering of $\R$ that finite fields lack. | I | |
| B. Square classes and the signature | |||
| B1p03005 | The shell $\Fp$, $\p=4\kap+1$, with its classes $S$, $N$; the diagonal form $Q_{\nu}(t,x,y,z)=-\nu t^{2}+x^{2}+y^{2}+z^{2}$, $\nu\in\Fpx$, a form over $\Fp$: Euclidean when $\nu\in S$ (all coefficients in one class), Lorentzian when $\nu\in N$; $Q_{\nu}$ depends on $\nu$ only through its class ($\nu\mapsto\nu w^{2}$ is $t\mapsto wt$); $\nu=\g$ canonical. | D |  Eq. (1); 8:B2 master: 00:C3 |
| B2p03006 | Nonexistence of a causal square root: no $c\in\Fp$ has $c^{2}=\nu$ for $\nu\in N$; for $c\in\Fpx$ every coefficient of $-c^{2}t^{2}+x^{2}+y^{2}+z^{2}$ is a square ($-1=\im^{2}$), the form Euclidean with $\p^{3}+\p^{2}-\p$ zeros; $c=0$ gives a degenerate form. | T |   Thm. 1 master: 00:C3 |
| B3p03007 | Square-class absorption: if $a_{i}/a_{0}\in S$ for all $\im$ then $Q\simeq a_{0}\sum Y_{i}^{2}$ by $Y_{i}=w_{i}X_{i}$, $w_{i}^{2}=a_{i}/a_{0}$; no root of $a_{0}$ is needed, and none exists for $a_{0}\in N$ ($-a_{0}$ is a nonsquare with it). | T | Lemma 1 |
| B4p03008 | The dichotomy lives on the shell: $\operatorname{disc}Q_{\nu}\equiv\nu$ (as $-1\in S$); for $\nu\in N$ the form is elliptic, Witt index one, with $\p^{3}-\p^{2}+\p$ null points; for $\nu\in S$ hyperbolic, Witt index two, $\p^{3}+\p^{2}-\p$; every $\nu$ on $\p\le41$ ($2041$ and $2353$ at $13$; 8:B7). | T | Section 2 master: 00:C3 |
| B5p03009 | The Witt decomposition: for $\nu\in N$ the plane $x^{2}-\nu t^{2}$ (the norm of $\Fpq$) is anisotropic and $y^{2}+z^{2}=(y+iz)(y-iz)$ hyperbolic, so $Q_{\nu}=H\perp\langle1,-\nu\rangle$, index one; for $\nu=w^{2}$ the $(t,x)$-plane is hyperbolic too, $H\perp H$. Over $\Fpq$, $\nu=c^{2}$ and $Q_{\nu}\simeq\sum X_{i}^{2}$: hyperbolic ($16\,225$ zeros at $q=25$); the extension dissolves the split. | T | Cor. 1 |
| B6p03010 | The finite Lorentz group of the shell: $O(Q_{\nu},\Fp)=O_{4}^{-}(\p)$ of order $2\p^{2}(\p^{4}-1)$ ($31\,200$, $9\,653\,280$, $48\,274\,560$ at $5$, $13$, $17$, by frame counting); the Euclidean group $O_{4}^{+}(\p)$ of order $2\p^{2}(\p^{2}-1)^{2}$; over $\Fpq$, $O(Q_{\nu},\Fpq)=O_{4}^{+}(\p^{2})$ ($486\,720\,000$ at $\p=5$): split type means Witt index two. | T | Section 4 |
| B7p03011 | The causal classes: the null cone $\{Q_{\nu}=0\}$ ($\p^{3}-\p^{2}+\p$ points) and the two classes of non-null vectors by the square class of $Q_{\nu}(v)$, $(\p-1)(\p^{3}+\p)/2$ each, partition $\Fp^{4}$ and are invariant under $O(Q_{\nu},\Fp)$ and under rescaling: the shell’s null, timelike and spacelike separation ($\p=5$, $13$ exhaustive). | T | Section 4 master: 00:C3 |
| C. The Lorentz transform | |||
| C1p03012 | The boost datum: $K=\Fpq=\Fp(\sqrt\nu)$ with the Frobenius conjugation and the norm $N(\gamma+b\sqrt\nu)=\gamma^{2}-\nu b^{2}$; the boost $\Lambda(\gamma,b)=\bigl(\begin{smallmatrix}\gamma&b\\ \nu b&\gamma\end{smallmatrix}\bigr)$ for $N=1$; the rapidity parameter is a norm-one element of $K^{\times}$ (8:D4; C5 for $\g^{\Delta m}$). | D | Section 3; 8:D4 |
| C2p03013 | $\Lambda(\gamma,b)$ preserves $-\nu t^{2}+x^{2}$ exactly and $\Lambda(z_{1})\Lambda(z_{2})=\Lambda(z_{1}z_{2})$: the boosts are the norm-one cycle $N^{1}\simeq C_{\p+1}$, the non-split torus, and exhaust $SO(Q_{\nu},\Fp)$ in dimension $1{+}1$ ($6$, $14$, $18$ at $5$, $13$, $17$); with $\nu\in S$ the same construction is the split torus $C_{\p-1}$ — the two tori are the two signatures (00:C3). | T | Section 3 master: 00:C3 |
| C3p03014 | Velocity: $\gamma\neq0$ on every boost; $v=-\nu b/\gamma\in\Fp$; $\gamma^{2}(\nu-v^{2})=\nu$, the finite $\gamma=1/\sqrt{1-\beta^{2}}$ with $\beta^{2}=v^{2}/\nu$ ($\beta$ itself is no shell quantity, 8:B8); Einstein’s law $v_{12}=(v_{1}+v_{2})/(1+v_{1}v_{2}/\nu)$ exact, the denominator never zero; $v$ is two-to-one on $N^{1}$. | T | Section 3 |
| C4p03015 | Dimension $1{+}3$: the $x$-boost $\Lambda\oplus I_{2}$ lies in $O(Q_{\nu},\Fp)$; with $O(3,\Fp)$ on $(x,y,z)$, of order $2\p(\p^{2}-1)$, the $x$-boosts generate $O(Q_{\nu},\F_{5})=O_{4}^{-}(5)$ ($31\,200$ elements by closure); over the extension the group is $O_{4}^{+}(\p^{2})$, the Euclidean one (B6). | T | Section 3 |
| C5p03016 | The family $\Lambda(u)$, $u=\g^{\Delta m}\in\Fpx$: $\gamma=(u+u^{-1})/2\in\Fp$ but $a=(u-u^{-1})/(2c)\in c\Fp$, outside $\Fp$ for $u\neq\pm1$; it preserves $Q_{\nu}$ over $K$, where $Q_{\nu}$ is Euclidean; the $\p-1$ matrices form the split torus of $SO(Q_{\nu},K)$ — the extension’s rotations, not the shell’s boosts ($13$, $17$ exhaustive). | T | Section 3 |
| D. The worked shell | |||
| D1p03017 | $\F_{13}$ [value]: $S=\{1,3,4,9,10,12\}$, $N=\{2,5,6,7,8,11\}$; $\nu=2=\g$; $X^{2}-2$ irreducible, $c=\sqrt2\in K\setminus\F_{13}$; $2041$ null points of $Q_{2}$ on the shell, $4\,855\,201$ over $K$; $14$ boosts $(\gamma,b)$ with the $7$ velocities $\{0,2,3,6,7,10,11\}$; $\Lambda(u)$ at $u=2$ has $a=-5/(2c)\notin\F_{13}$. | T | Section 2 |
| E. The causal reading | |||
| E1p03018 | Causality is algebraic and lives on the shell: the time axis is the coordinate carrying the nonsquare class ($\nu=\g$), the null cone and the two non-null classes its invariant separation (B7), the boosts the non-split torus (C2); $\Fpq$ is where $c=\sqrt\nu$ is written and where the dichotomy collapses (B5). Falsifier: a registered one-way velocity (8:B8). | R | Section 4; 00:C3 master: 00:C3 |
| E2p03019 | Local correspondence [chart]: integer points with $|Q_{\nu}|<\p$ satisfy $Q_{\nu}=0$ in $\Z$ iff on the shell (the window law, 1:D2); the asymptotic claim of Remark 1 — density and equidistribution of the shell’s null points against the real cone — is not proved and stands as Y1. | D | Rem. 1; 1:D2 |
| Y. Hypotheses | |||
| Y1p03022 | The large-$\p$ correspondence of Remark 1: whether the window points of the shell’s null cone approach the real light cone with density and equidistribution as $\p$ grows through the shells of the totality; named by the paper as future work, not claimed, no witness. | O | Rem. 1 |
Nothing matches that filter.
Status
- I
- Import. A standard result, or a corpus result, used without reproof.
- D
- Definition. A naming or declared convention, carrying no empirical content.
- T
- Theorem. Derived, and machine-verified in exact arithmetic by the named witness.
- R
- Realisation. States what a physical term denotes in the substrate: constitutive, not interpretive, and carrying its falsifier.
- O
- Open. Genuinely unresolved.
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 (
p03005) — 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).