| # | Description | Status | Sources |
|---|---|---|---|
| A. Inputs | |||
| A1p02001 | Finite-field algebra: $\Fpx$ is cyclic of order $\p-1$; its generators are the $\gen^{u}$, $u\in\Zp^{\times}$; $\gen^{(\p-1)/2}=-1$; $-1$ is a square in $\Fp$ iff $\p\equiv1\pmod4$; the fourth roots of unity form the unique subgroup of order four (1:A1, 1:B2). | I | |
| A2p02002 | The sign of the quarter-turn exponent: $\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 |
| A3p02003 | Topology: a closed connected surface with Euler characteristic $2$ is the two-sphere; the suspension of a circle is $S^{2}$ (Hatcher, Ex. 0.14); a quotient of a regular CW complex by a subcomplex is a CW complex. | I | Hatcher |
| A4p02004 | The framed-rational charts of 1-algebra: on one shell the scale grids $x/\gen^{n}$, $|x|\le2\kap$, trade range for resolution; across shells the tower resolves every real (1:D7). | I | |
| B. The shell and its frame | |||
| B1p02005 | The shell $(\kap,\Fp)$, capacity-first: $\kap$ primary, $\p=4\kap+1$ prime; the half-period $\pi:=2\kap$; the meridian steps $I_{\p}=\{0,\dots,\pi\}$; the phase cycle $\Phi_{\p}\cong C_{\p-1}$, $m\mapsto\gen^{m}$ (Defs. 2.1, 2.5; 00:C1). | D | Section 2; 00:C1 master: 00:C1 |
| B2p02006 | The frame $\Fp(\chron;0,1,\gen)$: origin, unit, and the Subject’s drive generator $\gen$, a primitive generator of $\Fpx$; $\chron$ the chronon (00:C1, convention 3). | D | Def. 2.3; 00:C1 master: 00:C1 |
| B3p02007 | Primitive generators form one orbit: every generator is $\gen^{u}$ with $u\in\Zp^{\times}$, a torsor for $\operatorname{Aut}(C_{\p-1})$ (Props. 2.7, 4.5). | T |    |
| B4p02008 | Cellular automorphisms of the index grid: $m\mapsto\pm m+c$, the dihedral group of the phase cycle; on the completion also meridian reversal $a\mapsto\pi-a$, exchanging the poles. The reindexing $\rho_{u}\colon m\mapsto um$ preserves latitude adjacency only for $u\equiv\pm1\pmod{\p-1}$; $\sigma$ is not a map of $\Sp$ ($\north$ one vertex, $L_{\pi}$ has $\p-1$); decided on $\p\le29$. | T | Prop. 2.8 |
| C. The orbital shell and its completion | |||
| C1p02009 | The orbital shell $\Sp$: vertices $\north$ and $v_{a,m}$ ($1\le a\le\pi$, $m\in\Phi_{\p}$), meridian and latitude edges, north triangles, quadrilaterals (Def. 3.1). The action reading $v_{a,m}\equiv a\gen^{m}$ is $\pi$-to-one onto $\Fpx$: the surface is two-faced (00:B11, 1:C4). | D | Def. 3.1; 1:C4 |
| C2p02010 | Counts: $|V|=\pi(\p-1)+1$, $|E|=2\pi(\p-1)$, $|F|=\pi(\p-1)$, $\chi(\Sp)=1$; the completion has $(\pi-1)(\p-1)+2$ vertices, $(2\pi-1)(\p-1)$ edges, $\pi(\p-1)$ faces, $\chi=2$ (Rem. 3.4). | T | |
| C3p02011 | Canonical spherical completion: collapsing $L_{\pi}$ to $\south$ gives a closed orientable surface — every edge in two faces, every vertex link a cycle — with $\chi=2$, hence $S^{2}$ (A3), on every shell (Thm. 3.3; decided on $\p\in\{5,13,17,29\}$ by exhaustive incidence). | T | |
| C4p02012 | Frame covariance: $\Sp$ is one complex for every generator — the index grid $I_{\p}\times\Phi_{\p}$ with its step relations; the frame $\gen'=\gen^{u}$ moves the field labels, $a\gen^{m}\mapsto a\gen^{um}$, by the automorphism $\rho_{u}$ of $\Phi_{\p}$, not the cells. The map $\varphi_{u}$ of Prop. 3.5 is cellular only for $u\equiv\pm1$. | T | Prop. 3.5 |
| D. The Euclidean datum and the involutions | |||
| D1p02013 | The half-period: $\gen^{\pi}=-1$ for every primitive $\gen$, $\pi=2\kap$ (Prop. 4.1); $2\pi\equiv-1$ (00:C1). | T | master: 00:C1 |
| D2p02014 | The quarter-turn subgroup $\Qp=\{x:x^{4}=1\}$ is the unique subgroup of order four; $\gen^{\kap}$ has order four with $(\gen^{\kap})^{2}=-1$; $\Qp=\{\pm1,\pm\im\}$ (Def. 4.2, Prop. 4.3; 1:B2). | T | |
| D3p02015 | The oriented quarter-turn $\im=-\gen^{\kap}=\gen^{-\kap}$, $\im^{2}=-1$, orientation by A2 (Rem. 4.6); on $\F_{13}(\chron;0,1,2)$: $\im=5$, $-\im=8$, $\pi=6$ [value] (Fig. 3). | D | |
| D4p02016 | The exponential unit $\eu:=\gen^{\im}$, $\im$ read as an exponent in $\Phi_{\p}$ through its residue representative; derived, generator-dependent (Rem. 4.7; 00:C1, convention 3); on $\F_{13}$, $\eu=6=\pi$ [value]. | D | Section 4; 00:C1 master: 00:C1 |
| D5p02017 | Orientation classes: for $\gen'=\gen^{u}$, $\im'=-\gen'^{\kap}$ equals $\im$ when $u\equiv1\pmod4$ and $-\im$ when $u\equiv3\pmod4$; the oriented quarter-turn is frame-covariant within one class of generators, not under every generator change. | T | Rem. 4.11 |
| D6p02018 | The Euler identity on the shell: $\eu^{\im\pi}=\gen^{2\kap\im^{2}}=(-1)^{\im}$, equal to $-1$ exactly when the representative of $\im$ is odd (00:C14); the oriented frames of a shell are those with $-\gen^{\kap}$ odd — on $\F_{13}$, $\gen=2$ ($\im=5$) is one, on $\F_{17}$, $\gen=3$ ($\im=4$) is not. | T | Section 4; 00:C14 master: 00:C14 |
| D7p02019 | Negation $R(x)=-x$ and inversion $I(x)=x^{-1}$ are commuting involutions; off $\Qp$ the $\langle R,I\rangle$-orbit $\{x,-x,x^{-1},-x^{-1}\}$ has four elements, and $\Fpx\setminus\Qp$ splits into $\kap-1$ such orbits (Props. 4.8, 4.9; 1:B2). | T | |
| D8p02020 | Euclidean conjugation $C_{\gen}\colon(a,b)\mapsto(a,-b)$ is an involution of the coordinate pairs $\Fp^{2}$; on the shell $a+b\im$ is a field element and the pair map $\Fp^{2}\to\Fp$ is $\p$-to-one (1:E2), so $C_{\gen}$ is a chart-level involution, not a field automorphism. | D | Prop. 4.13; 1:E2 |
| E. The external spherical comparison | |||
| E1p02021 | The comparison map $\Xi_{\p,\gen}$ [chart]: $\north\mapsto(0,0,1)$, $v_{a,m}\mapsto(\sin\theta_{a}\cos\phi_{m},\sin\theta_{a}\sin\phi_{m},\cos\theta_{a})$ with $\theta_{a}=\pi_{\R}a/(2\kap)$, $\phi_{m}=2\pi_{\R}m/(\p-1)$, $\pi_{\R}$ the chart constant (00:N2); $L_{\pi}\mapsto(0,0,-1)$ (Def. 5.1). | D | Def. 5.1; 00:N2 |
| E2p02022 | Base-grid estimate [chart]: every point of $S^{2}$ lies within geodesic distance $\sqrt2\,\pi_{\R}/(\p-1)$ of $\Xi_{\p,\gen}(V(\Sp))$; measured covering radius $0.360$ at $\p=13$ against the bound $0.370$ (Prop. 5.2). | T | |
| E3p02023 | Fixed-shell refinement is bounded: with $m=\lfloor\log_{\gen}(2\kap+1)\rfloor$ no point $x/\gen^{n}$, $|x|\le2\kap$, lies in $(\max(1-\gen^{-m},2\kap\gen^{-m-1}),1)$ at any depth, so the covering radius of the scale grid in $[0,1]$ is $\ge\tfrac12\min(\gen^{-m},1-2\kap\gen^{-m-1})$ for every $N$: $1/8$ at $(13,2)$, $5/22$ at $(13,11)$. | T | Section 5 |
| E4p02024 | Finite precision across the tower [chart]: for every $L$-bounded observable family, $\varepsilon>0$ and configuration on $(S^{2})^{r}$ some shell $\p$ carries grid points within $\varepsilon$ (1:D7 with the path bound of E2); on one shell the precision is bounded by E3. | T | Thm. 5.7; 1:D7 |
| F. Fourier duality on the phase cycle | |||
| F1p02025 | $\gen$ is a principal $n$-th root of unity, $n=\p-1$: $\gen^{n}=1$, $\sum_{j<n}\gen^{jk}=0$ for $0<k<n$, and $n^{-1}=-1$ in $\Fp$ (Prop. 6.1; $2\pi\equiv-1$). | T | |
| F2p02026 | The ring Fourier transform on the phase cycle: $\mathcal F_{\gen}(v)_{k}=\sum_{j<n}v_{j}\gen^{jk}$ on $V_{\gen}=\Fp^{n}$; the matrix $(W_{\gen})_{kj}=\gen^{jk}$ (Def. 6.2, Rem. 6.4). | D | Def. 6.2 |
| F3p02027 | Inversion: $v_{j}=-\sum_{k<n}\mathcal F_{\gen}(v)_{k}\gen^{-jk}$, i.e. $W_{\gen}^{-1}=-(\gen^{-jk})_{jk}=-W_{\gen}J$ (Prop. 6.3; 6:B5), exact on every shell. | T | |
| F4p02028 | Polynomial reading: $\mathcal F_{\gen}(v)_{k}=P_{v}(\gen^{k})$ with $P_{v}=\sum_{j}v_{j}X^{j}$; the transform exchanges coefficients with values on the phase cycle (Prop. 6.5). | T | |
| F5p02029 | Covariance under generator change: for $\gen'=\gen^{u}$, $v^{(\gen')}_{j}=v^{(\gen)}_{uj}$ and $\mathcal F_{\gen'}(v^{(\gen')})=\mathcal F_{\gen}(v^{(\gen)})$ (Prop. 6.7). | T | |
| F6p02030 | Exact external transport [chart]: $\chi(\gen^{m})=e^{-2\pi_{\R}\im m/n}$ is an isomorphism of $\Fpx$ onto the complex $n$-th roots of unity with $\chi(\gen^{m+1})=e^{-2\pi_{\R}\im/n}\chi(\gen^{m})$, $\chi(\gen^{m+\pi})=-\chi(\gen^{m})$, $\chi(\im\gen^{m})=\im\,\chi(\gen^{m})$, $\chi(\gen^{jr})=e^{-2\pi_{\R}\im jr/n}$ (Prop. 6.8). | T | |
| F7p02031 | The large-$\p$ reading [chart]: the phase cycle read as the $n$-point grid $\phi_{m}=2\pi_{\R}m/n$ on $S^{1}$; the classical sampled DFT, exact recovery for $n>2N$, and trapezoidal convergence are the degenerate comparison case, imported (Rem. 6.12). | D | Whittaker; Shannon; Trefethen |
| T. Tasks | |||
| T1p02034 | The observer-local chart: a metric, geodesics and curvature on the completion, in which local Euclidean geometry would be written; deferred by the paper (Discussion, “Boundary of the Approximation Claim”); no Gromov–Hausdorff statement is made or claimed. | O | Discussion |
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.
- 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 (
p02007) — 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).