| # | Description | Status | Sources |
|---|---|---|---|
| A. Inputs | |||
| A1p01001 | Finite-field algebra: $\Fpx$ is cyclic of order $\p-1$ with primitive roots; $\gen^{\p-1}=1$; $-1$ is a square in $\Fp$ iff $\p\equiv1\pmod4$ (Euler’s criterion); the affine maps $x\mapsto a+bx$, $b\neq0$, are the bijections preserving the field structure up to relabelling. | I | [Burton 2010; Dummit & Foote 2004] |
| A2p01002 | The sign of the quarter-turn exponent: the oriented quarter-turn is $\im=\gen^{-\kap}=-\gen^{\kap}$, the exponent negative by pullback covariance (00:C7); the positive-exponent reading is the conjugate chart. Declared here, derived in the corpus. | I | master: 00:C7 |
| A3p01025 | The finite subgroups of $SO(3)$: cyclic, dihedral, tetrahedral ($12$), octahedral ($24$), icosahedral ($60$) — Klein’s classification; the binary icosahedral group as the $600$-cell’s vertices. Imported for E5. | I | [Klein 1884; Coxeter 1973] |
| B. The shell and its frame | |||
| B1p01003 | The shell, capacity-first: $\kap$ primary, $\p=4\kap+1$ prime; the Subject’s frame $(\tau;0,1,\gen)$ with $\gen$ a primitive root and the drive $x\mapsto\gen x$; the cycle $\Phi_\p\cong C_{\p-1}$; $\im:=-\gen^{\kap}$ (A2), $-1=\gen^{2\kap}$. | D | Def. 1, Section 2 master: 00:C1 |
| B2p01004 | Symmetry completeness (Thm. 2.1): the fourth roots of unity form the unique order-four subgroup $Q_4=\{1,\im,-1,-\im\}$; under the Klein four-group $\langle x\mapsto-x,\,x\mapsto x^{-1}\rangle$, $Q_4$ is the union of the two size-two orbits $\{\pm1\}$, $\{\pm\im\}$, and $\Fpx\setminus Q_4$ splits into exactly $\kap-1$ orbits of size four. For $\p\equiv3\pmod4$ no $\im$ exists. | T |    |
| B3p01005 | The oriented quarter-turn: $\im=-\gen^{\kap}$ satisfies $\im^{2}=-1$ for every primitive root $\gen$; the two square roots of $-1$ are $\{-\gen^{\kap},\gen^{\kap}\}$, so the drive fixes which is $\im$. On $\F_{13}$, $\gen=2$: $\im=5$. | T | master: 00:C7 |
| B4p01006 | Affine reframing (Def. 2, Lemma 2.2): $\varphi_{a,b}(x)=a+bx$, $b\neq0$, is a ring isomorphism $(\Fp,+,\cdot)\to(\Fp,\oplus,\otimes)$ with origin $a$ and unit $a+b$; every polynomial identity is frame-covariant. | T | master: 00:A6 |
| B5p01007 | Origin and unit are observer data (affine gauge); the generator $\gen$ is the Subject’s drive, not gauge; the observer’s window is the naturals below $\sqrt\p$ (00:B8). | D | |
| C. Arithmetic symmetries and the orbital complex | |||
| C1p01008 | The four symmetries as maps of the shell: the successor $C_1:k\mapsto k+1$; translations $T_a$, $a\in\Fp$, the cycle $C_\p$; scalings $S_m$, $m\in\Fpx$, the cycle $C_{\p-1}$; power maps $P_\varepsilon:x\mapsto x^{\varepsilon}$, $\varepsilon\in C_{\p-1}$, bijective iff $\gcd(\varepsilon,\p-1)=1$. | D | Section 3, (3.1)–(3.4) |
| C2p01009 | The frame group (Prop. 1): $\langle T_a,S_m\rangle$ is the affine group of order $\p(\p-1)$, acting simply transitively on the frames $(a,b)$, $b\neq0$; the set of frames is a torsor under it (00:C5, 00:D13). | T | manuscript |
| C3p01010 | Meridians and latitudes (Def. 3): $M_n(a)=a\gen^{n}$, $a\in\Fp$, the ordered list of the shell with step $\gen^{n}$; $L_a(m)=a\gen^{m}$, $m\in C_{\p-1}$, $a\neq0$, the multiplicative cycle from $a$; the orbital complex $\Sp$ with vertex set $\{(n,\pm a)\}\cup\{0\}$. The $2$-sphere reading is 2-geometry’s [Akhtman 2025]. | D | Def. 3 |
| C4p01011 | Involutions and counts (Def. 3 (a)–(c)): $M_n(a)=M_{n+2\kap}(-a)$ and $L_a(m)=L_{-a}(m+2\kap)$ since $\gen^{2\kap}=-1$; $\p-1$ distinct meridian lists in $2\kap$ great circles; $2\kap$ latitude pairs; one-sided vertex count $(\p-1)^{2}/2+1$, the double cover $(\p-1)^{2}$ (00:B11). | T | |
| D. Framed numbers | |||
| D1p01012 | Framed integers (Def. 4): the window $W_H=\{z\in\Z:|z|\le H\}$, $2H<\p$, embedded by $z\mapsto z\bmod\p$; sign, order and magnitude are the window’s; sums read back for $4H<\p$, products for $2H^{2}<\p$ — the corpus window $\sqrt\p$ (00:B1). | D | Def. 4; 00:B1 master: 00:B1 |
| D2p01013 | The window law: $z\mapsto z\bmod\p$ is injective on $W_H$ when $2H<\p$; for $x,y\in W_H$ the residue of $x\pm y$ reads back the integer when $4H<\p$, and that of $xy$ when $2H^{2}<\p$ (the same injectivity on the windows $2H$ and $H^{2}$). | T | |
| D3p01014 | Framed rationals (Def. 5): $a/b$ with $a,b\in W_H$, $b\not\equiv0$, of value $ab^{-1}\in\Fp$; the scale grid $[x,n]:=x\gen^{-n}$, $x\in\{0,\dots,\p-1\}$, $n\in C_{\p-1}$; $G_n$ the ordered list $(x\gen^{-n})_x$, the meridian $M_{-n}$ of C3. | D | Def. 5; 6:B1 master: 00:B1 |
| D4p01015 | Scale-periodicity (Lemma 4.1, in the field): $S_n(x)=x\gen^{-n}$ satisfies $S_{n+(\p-1)}=S_n$; the grids $G_n$ are $(\p-1)$-periodic as ordered lists; the zoom $[x,n]\mapsto[x,n+1]$ has order $\p-1$. As lists of rationals $x/\gen^{n}$ ($\gen$ lifted to $\Z$) the grids are not periodic: the periodicity is a relation of the field. | T | |
| D6p01017 | The continuum as chart (Def. 6, Props. 3–4, Cor. 1): the framed real line is the reading of the nested grids against $\R$, a labelled idealisation entered nowhere as an object (00:B1); no completion, compactness or “complete continuum” is claimed. | D | Section 4.4; 00:B1 master: 00:B1 |
| D7p01027 | Limit-like approximation (second clause), across the tower: for every real $r$ and $\varepsilon>0$ some shell $\p=4\kap+1$ carries a framed rational $x/2^{n}$, $|x|\le2\kap$, within $\varepsilon$ of $r$ (primes $\equiv1\pmod4$ beyond every bound). One shell trades range for resolution; the limit is the tower, not a completion. | T | |
| E. The complex chart, polynomial equations and continuous symmetry | |||
| E1p01018 | The framed complex chart (Def. 7): the pair $(a,b)\in W_H^{2}$ read as $a+b\im\in\Fp$; the quarter-turn acts on the shell as the rotation $x\mapsto\im x$ of order four; the chart is the plane picture of $Q_4$ acting on the shell, not an extension of $\Fp$. | D | Def. 7 |
| E2p01019 | The extension by $X^{2}+1$ is trivial (Prop. 5 reversed): on the shell $\Fp[X]/(X^{2}+1)\cong\Fp\times\Fp$ has zero divisors, $(X+\im)(X-\im)=0$, so it is not a field; $\Fp[X]/(X^{2}+1)$ is a field exactly when $\p\equiv3\pmod4$; the quadratic extension of the shell is $\Fp[\eta]$, $\eta^{2}=\nu$ a non-square (8-dirac B6). | T | |
| E3p01026 | Solving in the substrate (first clause): $f\in\Fp[X]$ has a root in $\Fp$ iff $f$ and $X^{\p}-X=\prod_{a}(X-a)$ are not coprime; the gcd counts the distinct roots and Cantor–Zassenhaus splitting finds them, exactly. An equation without a root in $\Fp$ is recognised, not extended (E2). | T | |
| E4p01028 | Continuous symmetry, the abelian case (third clause): $\Fpx\simeq C_{\p-1}\simeq SO(2,\Fp)$ (6:E2) is a $\pi/(\p-1)$-net of $U(1)$ under $k\mapsto e^{2\pi\im k/(\p-1)}$; the rounding $k(\theta)=\lfloor(\p-1)\theta/2\pi+\tfrac12\rfloor$ has angle and chord error $\le\pi/(\p-1)$ and group-law defect at most one step. | T | |
| E5p01029 | Continuous symmetry, the non-abelian obstruction: no finite subgroup of $SO(3)$ is an $\varepsilon$-net for $\varepsilon<\varepsilon_0=\arccos\big((3\sqrt5-1)/8\big)\approx44.5^\circ$, the covering radius of the icosahedral group (A3); the tetrahedral, cyclic and dihedral groups have radius $\ge\pi/2$, the octahedral $\approx62.8^\circ$. Finite subgroups cannot approximate $SO(3)$; the window does (E6). | T | |
| E6p01030 | Continuous symmetry, the non-abelian case resolved by the window: the framed quaternions $W_H^{4}$, read in a shell $\p>8H^{2}$, compose exactly (products land in $W_{4H^{2}}$); normalised, they are an $\varepsilon$-net of $SO(3)$ with $\varepsilon\le2\arcsin(1/H)$ (round $Hs$ to the lattice). At $H=3$, $\p=73$: $38.9^\circ<\varepsilon_0$, finer than any finite subgroup; measured $30.0^\circ$. | T | Section 6 |
| E7p01032 | The Lie-algebra layer, one axis: on a shell $\p>8H^{2}$, for $q=a+v\in W_H^{4}$ with $v\ne0$, the rotation $\rho_q\colon x\mapsto qxq^{-1}$ is the Cayley step (8:C3) of the self-adjoint $\eta S_v$ (E2’s $\eta$, $S_vx=v\times x$, $N(v)=v\cdot v$) at $\alpha=\eta/(\nu a)$, and the half-turn $U_\infty=I+2N(v)^{-1}S_v^{2}$ at $a=0$. With $U_\infty$ these steps form a cyclic group of order $\p-\bigl(\tfrac{N(v)}{\p}\bigr)$ containing every iterate; at most $2H^{2}+2H$ of its elements are window rotations. | T | |
| E8p01033 | The Lie-algebra layer, two axes and range: for pure quaternions $u,w$ with $1+N(u)$, $1+N(w)$ and $1-u\cdot w$ nonzero, $\rho_{1+u}\rho_{1+w}=\rho_{1+u\circ w}$ with $u\circ w=(u+w+u\times w)/(1-u\cdot w)$, the bracket being $[u,w]=2u\times w$; at $u\cdot w=1$ the product is the half-turn about $u+w+u\times w$. The entries of $q^{m}$, $q\in W_H^{4}$, are at most $(2H)^{m}$, and $q^{m}$ reads back from the shell iff $2\|q^{m}\|_\infty<\p$ (D2). | T | Section 6; D2 |
| Z. The horizon | |||
| Z1p01020 | No element of additive order two (Thm. 5.1): $2s=0$ forces $s=0$; the antipode of the origin on the additive cycle is not a residue; it sits between $2\kap=(\p-1)/2$ and $2\kap+1=(\p+1)/2=2^{-1}$ (20-rh B8). | T | |
| Z2p01021 | The antipode named $\infty$: the horizon of the observer at $0$ (00:C25, 00:D13), the compactification point of the framed line [chart]; its reading as classical infinity is the chart, not a residue. | D | |
Nothing matches that filter.
Status
- I
- Import. A standard 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.
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 (
p01004) — 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).