| # | Description | Status | Sources |
|---|---|---|---|
| A. Inputs: imported or declared, not derived here | |||
| A1p20001 | The framed substrate: the Carrier $\F_\Omega$ with $\Omega=4\dS+1$, the Subject $\Fp(\chron;0,1,\gen)$ with $\p=4\kp+1$ and its register $\pi=2\kp$, $\im=\gen^{-\kp}$, $\E=\gen^{\,\im}$; the four charts and the finite Fourier turns; time as scale-dilation; the frame-covariance of the height chart. | I | |
| A2p00004 | Finitude: for any reading of capacity $R$ the registered Universe embeds in the shell of $R$ members, and among $R+1$ members two share a residue; the totality is finite, its cardinality $\Omega$. A theorem of the master ledger (00:A2), proved in the core, cited as the closure’s first premise (F7). | T |   00:A2; § 6 |
| A3p00003 | Completeness: the registration of any totality is onto its registered Universe, so there is no outside and no host; two totalities each registered whole within the other have one count. A theorem of the master ledger (00:A3), proved in the core; the hypothesis of the Carrier is a statement about its own residues and nothing else. | T | |
| A4p00197 | Observation: every observation is a registration by an embedded part of $o<\Omega$ states; every reading identifies two members, and a complete reading needs the whole count; one translation carries each member to each. A theorem of the master ledger (00:A2), proved in the core, cited as the closure’s second premise (F7) and behind the horizon (Z1). | T | 00:A2; § 6 |
| A5p00008 | The Carrier: a timeless torsor of $\Omega$ elements, its cardinality its only absolute characteristic; reframings $x\mapsto ax+b$ are automorphisms, so $0$, $1$, $-1$ are frame data; a Subject’s frame charts it as the prime field $\F_\Omega$, never the Carrier (00:A4). A finite holographic substrate: capacity $\dS$ the horizon entropy, $\Omega=4\dS+1$ its exact content (00:A5, 10:A2), the Subject embedded under $\p^{2}<\Omega$. | D | |
| A6p20003 | The classical analytic apparatus: the count $\mathcal N(T)=\theta(T)/\pi+1+S(T)$, the Riemann–Siegel main sum with its $O(t^{-1/4})$ remainder, the explicit formula in its distributional form over the Weil class, Hardy’s Ramanujan-sum expansion of $\Lambda$, Möbius inversion. | I | [Edwards 1974; Weil 1952; Hardy 1921; Apostol 1976] |
| A7p20004 | Turing’s count: with $C(T)$ the sign changes of $Z$ on $(0,T)$, $C\le N_{\mathrm{crit}}\le\mathcal N$; $C=\mathcal N$ certifies the hypothesis below $T$ and forces every zero there to be simple. | I | |
| A8p20078 | The Davenport–Heilbronn function: a Dirichlet series with the functional equation and no Euler product, with zeros off the line, the first pair at $0.8085171825+85.6993484854\,i$ and $1-\bar s$; the treatment of linear combinations of $L$-functions by smoothed Euler products. | I | [Davenport & Heilbronn 1936; Titchmarsh 1986; Gonek 2012] |
| A9p20006 | The comparison data: no off-line zero of $\zeta$ to height $3\times10^{12}$, by Turing’s certificate, so every zero there is simple and every cell below $4.8\times10^{11}$ clean; GUE spacing statistics of the zeros; some $2600$ zeros to twelve digits from the primes to $10^{6}$ by harmonic inversion; the self-adjoint realisations of the Berry–Keating operator. | I | [Platt & Trudgian 2021; Montgomery 1973; Odlyzko 1987; Main et al. 1998; Berry & Keating 1999; Endres & Steiner 2010] |
| A10p20070 | Explicit bounds on the Riemann–Siegel remainder: Gabcke’s explicit error term, used by the verification of A6; with it the sign of $Z$ is certified wherever $|Z_M(t)|$ exceeds the bound (F1). | I | [Gabcke 1979]; Prop. 5.3 |
| A11p20082 | The density bounds, imported for every cycle: for a fixed tolerance the cells holding a zero farther than it from the line are a vanishing fraction of the cycle (Selberg), and at least two fifths of a cycle’s zeros lie on the line (Conrey) [chart]; bounds on the unclean cells of the physical Carrier, naming none. | I | |
| B. The shell: the modes, the antipode, the critical line | |||
| B1p20008 | The two frames on one substrate: the Carrier chart $\F_\Omega$, held by no embedded observer, and the Subject $\Fp$ embedded with $\Omega\gg \p^{2}$; what they share is the quarter-turn core $Q_4$ and nothing else, on the laboratory pair $(13,233)$ the cycles $C_{12}$ and $C_{232}$ admit no projection ($12\nmid232$); hardness by register ($\p$-hard, $\Omega$-hard). | D |  Def. 1.3 master: 00:C16 |
| B2p20009 | Frame coincidence below the horizon: for $n\le\sqrt \p$ the residue $n$ is the same integer in $\Fp$ and $\F_\Omega$, and primality of $n$ equals irreducibility in the Subject chart; the Subject-realised primes $\Pi_\p$ are the primes to $\sqrt \p$. | T | Prop. 2.1 |
| B3p20010 | The prime-counting vector $v(n)=\Lambda(n)$ on $\Fx{\p}$ and its windowed reading on $\{1,\dots,\lfloor\sqrt \p\rfloor\}$; $\psi(x)$ is the cumulative windowed reading; the horizon is a property of the reading, not of the vector. | D | Def. 2.2 |
| B4p20011 | Zero-slot: $Z_\Omega(k)=\sum_{x\in\Fx{\Omega}}x^{k}$ vanishes on every nonterminal exponent $1\le k\le\Omega-2$ and equals $-1$ on the full cycle; the nonterminal slots are the universal mode basis. | T | Thm. 3.1 |
| B5p20012 | Slot complementarity: $\Phi(k)=-\gen^{\,k}$ bijects the nontrivial spectral slots onto the nonterminal additive slots $\Fx{\Omega}\setminus\{-1\}$, the two removed points being $\mu_2$, the intertwiner the half-cycle element. | T | Thm. 3.2 |
| B6p20013 | Hermitian phase calculus on $K=\F_{\p^{2}}$: norm and trace $\Fp$-valued, the phase circle $U_{\p+1}$ of order $\p+1$ with Frobenius as inversion, the quarter-turn $\im$ Frobenius-fixed and off the circle ($\Nm(\im)=-1$), the trace-zero $\eta$ with $\eta^{2}=\nu$ a nonsquare, $\Tr(a+b\eta)=2a$, $\Nm=a^{2}-\nu b^{2}$. | T | Lem. 4.1 |
| B7p20014 | Flat ground state: the full-modulus Ramanujan sum $c_\p(n)\equiv-1$ for every $n\not\equiv0$; the mode at the spectral origin carries no prime information. | T | Prop. 4.2 |
| B8p20015 | The finite critical line: the half-turn $2^{-1}=2\kp+1=-\pi$; $\Tr(z)=1$ exactly on the $\p$ points $z=2^{-1}+\eta\theta$, with energy $\Nm(z)=\tfrac14-\nu\theta^{2}$; de-framed, $2^{-1}/\p=(2\kp+1)/\p\to\half$ from above [chart]. | T | Prop. 4.4 |
| B9p20016 | The two agreement loci: the Klein four-group $\langle\phi,\rho\rangle$ of Frobenius and the functional-equation half-turn fixes exactly $\Fp$ (the prime meridian), $L_{1/2}$ (the critical line) and their meeting $\{2^{-1}\}$; no other line is fixed. | T | Thm. 4.5 |
| B10p20017 | The Subject constants on the shell: $\pi=2\kp$, $2\pi\equiv-1$, $\im=\gen^{-\kp}$, $\im^{2}\equiv-1$, $\E=\gen^{\,\im}$ on the odd lift, $\gen^{\,\pi}\equiv-1$, $\E^{\,\im\pi}\equiv-1$; on $\F_{13}$: $\gen=2$, $\im=5$, $\E=6$, $\pi=6$. | T | § 1.3, Rem. 1.2 |
| D. The reading of $\zeta$ on the line: the dictionary, the cells, the strip | |||
| D1p20025 | The dictionary [chart]: horizon $\sqrt \p\leftrightarrow$ Riemann–Siegel length $\sqrt{T/2\pi}$, half-turn $\leftrightarrow n^{-1/2}$, scale $\leftrightarrow\log n$; a shell of cardinality $\p$ reads $\zeta$ on the line to $T=2\pi \p$, one cycle of the shell, and a height is the scale coordinate of the shell that reads it, its count using residues below $\sqrt{T/2\pi}$ only. | D | Def. 5.1 |
| D5p20029 | The cells: the heights of a Carrier’s cycle are its residues, residue $y$ the cell from $2\pi y$ to $2\pi(y+1)$; a cell is clean when its zeros lie on the line, which Turing’s count decides from the labels below $\sqrt{y+1}$, and passes when the frame’s reading certifies it. The hypothesis of the Carrier: every residue has a clean cell. | D | Def. 5.4, Prop. 5.5, Lem. 5.2 master: 00:Z11 |
| D8p20080 | The strip: the Euler product excludes zeros with real part at least one, and the functional equation confines the nontrivial zeros to the open strip in Klein-four orbits of size two on the line and four off it; the Davenport–Heilbronn vector, without the product, is not multiplicative and has an off-line zero. No core witness: the statement is analytic. | T | Thm. 5.6 |
| D9p20083 | The finite negative control: on $\F_{13}(\sqrt2)$ the polynomial $((X-2)^{2}-2)((X+1)^{2}-2)$ has exactly the roots $2\pm\eta$, $-1\pm\eta$, of traces $4$, $4$, $11$, $11$ against the line’s $1$, the root set closed under conjugation and under the half-turn; finitude, conjugation and the reflection force no root onto the line. | T | Prop. 5.7 |
| E. The scale-shift and the shell theorem | |||
| E1p20032 | The scale-evolution generator: on the shell the scale-shift $x\mapsto\gen^{\,r}x$ is a unitary permutation of $\Fx{\p}$ with the complex characters as eigenvectors; in the analytic chart [chart] the dilation group $U_r=e^{ir\Hh}$ has the self-adjoint generator $\Hh=-i(x\partial_x+\half)$ with generalised eigenfunctions $x^{-\bar\rho}$, $\rho=\half+i\gamma$, the symmetrizing $\half$ the half-turn of B8; the chart assignment is used nowhere as a shell identity. | T | Prop. 4.6 |
| E12p20043 | The shell theorem. On every shell, with no hypothesis: (i) $v$ expands in the constant mode and the nonterminal modes of the quarter-turn meridian; (ii) every readout lies on $\Tr=1$, real part $2^{-1}=2\kp+1=-\pi$; (iii) the scale-shift has the modes as eigenvectors, eigenphases $2\pi j/(\p-1)$ independent of $v$. No off-line mode; true of every vector, the Davenport–Heilbronn vector included. | T | Thm. 4.7 master: 00:Z10 |
| E13p20044 | Shell-basis completeness is not a clause of E12: the $\p-1$ complex characters are an orthogonal basis of $\mathbb C^{\Fx{\p}}$ ($\lVert\chi_j\rVert^{2}=\p-1$; finite Parseval), true of every vector, the trivial character carrying the mean $\psi(\p-1)/(\p-1)$; the $\Fp$-valued power characters are never orthonormal and do not expand $v$; completeness for the zero set of $\zeta$ is D5, a different clause. | D | Rem. 4.8 |
| F. The closure, the hosted theorem and the controls | |||
| F1p20047 | Turing’s count on the shell. On every cell $C_y\le N^{\mathrm{crit}}_y\le\mathcal N_y$ (A7); the cell is clean when $\mathcal N_y=N^{\mathrm{crit}}_y$, and $C_y=\mathcal N_y$ certifies it, every zero simple. The shell estimates $\mathcal N$ by the comb count (Appendix B; uncertified) and reads $C$ from the main sum’s sign changes (A10), zeros on the line. An off-line zero is a phantom, $\mathcal N_y-N^{\mathrm{crit}}_y>0$. | T | Prop. 5.3, Prop. 5.5 master: 00:Z11 |
| F2p20081 | The hypothesis on a hosted Carrier. A cell is decided by the certificate of a shell reading it, an embedded Subject below the largest one, the host above; on the laboratory Carriers $233$, $30\,089$ and $2\,408\,561$ every cell of the cycle is clean, $1\,038$, $280\,186$ and $32\,984\,135$ zeros, all simple; the classical verification cleans every cell below $4.8\times10^{11}$ (A9). | T | Thm. 6.2 (the certificate analytic, with the package; the core decides the laboratory instances) master: 00:Z11 |
| F7p20079 | The closure of the heights. A height is a residue on the cycle of the shell that reads it, the largest shell is the Carrier’s and there is no height beyond its cycle (A2); no embedded Subject reads the cycle whole (A4). The hypothesis of the Carrier is a statement about the residues of its cycle, one clause per residue. | T | Thm. 6.1 |
| Z. Horizon: the physical Carrier | |||
| Z1p20059 | The physical Carrier: the cells from the largest embedded Subject up lie in no embedded cycle, the whole-state certificate of the hypothesis is a record no embedded reader holds, and its evaluation costs more than the totality counts; the predicate’s value there is $\Omega$-hard as a tally. Short derivations are neither claimed nor excluded; the laboratory cycles are its instances. | Ω | Rem. 6.3, § 8, § 6 |
| Z2p20060 | The heights as Carrier residues: under the frame-covariance of the height chart (A1) each height is a residue on the Carrier’s frequency latitude, its exact index below the resolution of every embedded Subject; every Subject reads to finite precision the heights its scale reaches, its own cells (D5). | Ω | § 8 |
Nothing matches that filter.
Status
- I
- Import. A standard result, a corpus result, or a measured datum 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 from the rows above it, or an exact instance check in integer arithmetic; a predicate whose content is a numerical observation carries its figures as declared [approx]/[chart] and is a theorem in the weaker sense that the linked witness reproduces them to the stated tolerance on the tested instances — the closing paragraph lists the two grades separately.
- Ω
- $\Omega$-hard. A value decided by the totality, in no embedded reader’s window; a demarcation of where the value is read, not an open item and not a claim that no proof exists.
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 (
p00004) — 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).
, ; B1 in both); the pillars A2–A4 are the master’s core theorems, the closure F7 is proved in the core on them with its laboratory instances decided by the kernel, the laboratory instances of the hosted theorem (F2) are those kernel decisions, the certificate itself analytic and with the package, the two finite lemmas of the cells (D5), the finite count of F1 (the chain, the certificate at equality, the phantom) and the finite control (D9) are core theorems, and the strip (D8) is proved on Mathlib. The analytic rows, the [chart] clauses and every [approx] figure remain with the package. $\Omega$-hard is the paper’s residue, two predicates, each a value read by the totality and by no embedded reader, named and classified: the physical Carrier’s cells beyond the largest embedded Subject with their whole-state certificate (Z1), and the heights as Carrier residues (Z2). Open predicates: none; whether the universal has a derivation of finite description is a question no predicate poses, and the $\Omega$ tag records where the value is read, not that no proof exists. The paper’s title names the finite holographic substrate (A5, Remark 1.1) whose cells the host decides (D5, F2); the hypothesis of the physical Carrier is the value of Z1, and no predicate asserts it.