validation/ scripts reproduce the counts and draw the figures from the rows. The Lean core proves the identities for every shell $\p=4\kap+1$ of the totality with no axioms, and decides the counts of C4 and C9 and the drift certificates of F4 and A17 by the kernel on the three pairs; D5 is proved on Mathlib for every shell (Chevalley–Warning).
The carried rows of block A name their origin row in the source column and keep its accession key; the master ledger carries them under those rows. The marks are [chart] for a continuum reading of a finite object and [data] for a measured bound.70
| # | Description | Status | Sources |
|---|---|---|---|
| A. Inputs: imported and carried, not derived here | |||
| A1p03002 | Quadratic forms over $\Fp$: classified by dimension and discriminant; isotropic from dimension three; in dimension four the hyperbolic class (discriminant a square, Witt index two) and the elliptic class (discriminant a nonsquare, Witt index one), with $|\mathrm{O}^{\pm}_{4}|$. | I | |
| A2p07001 | $\mathrm{PSL}_2(\p^{2})\cong\mathrm{P}\Omega^{-}_{4}(\p)$; the spinor map on $2\times2$ Hermitian matrices, the continuum counterpart. | I | Prop. 2.5(vii); [Taylor 1992]; [Penrose & Rindler 1984] |
| A3p07002 | The inverse-square law of gravitation holds to separations of $52\,\mu$m [data]. | I | Rem. A3 (rem:data), p. 6">2.8; [Lee et al. 2020] |
| A4p00021 | The frame, Subject-only: $(\chron;0,1,\gen)$, origin, unit and the drive $x\mapsto\gen x$; $\gen$ the one nonsquare frame datum; the shell $\p=4\kap+1$, $\im=-\gen^{\kap}$, $\pi=2\kap$. | T |   |
| A5p00025 | An oriented frame is a unimodular basis. | D | |
| A6p00150 | The signature is the square class of the temporal coefficient $\nu=\gen$; the split and the non-split torus are the two signatures. | T | |
| A7p03005 | The forms $Q_{\nu}=-\nu t^{2}+x^{2}+y^{2}+z^{2}$, $\nu\in\Fpx$, hyperbolic for $\nu$ a square and elliptic for $\nu$ a nonsquare; $Q_{\nu}$ depends on the class of $\nu$ only. | D | |
| A8p03008 | The counts of the two four-dimensional classes: $\p^{3}+\p^{2}-\p$ null vectors for the hyperbolic class, $\p^{3}-\p^{2}+\p$ for the elliptic. | T | |
| A9p03011 | For $\nu$ a nonsquare the two classes of non-null vectors of $Q_{\nu}$ are equal in size, $(\p-1)(\p^{3}+\p)/2$ each, and invariant under the orthogonal group and under rescaling. | T | |
| A10p03013 | The norm-one group of the plane form $-\nu t^{2}+x^{2}$ is the cycle $C_{\p+1}$, the non-split torus, for $\nu$ a nonsquare, and the split torus $C_{\p-1}$ for $\nu$ a square. | T | |
| A11p00190 | The Hopf section: the frame moves factor as the affine group times the non-split torus, $G=B\cdot T$, on the frames by elements. | T | |
| A12p38050 | The frame triple: one projective direction, one shell cell, one drive phase; the $\p+1$ directions of $\mathbb{P}^{1}(\Fp)$. | T | |
| A13p00152 | $\mathrm{PGL}_2(\Fp)\cong\mathrm{SO}_3(\Fp)$; the census of its elements by type. | T | |
| A14p00183 | The frame group has one form: $\mathrm{SU}_2(\F_{\p^{2}}/\Fp)=\mathrm{SL}_2(\Fp)$ for the Hermitian form $wJ$, $w^{\p}=-w$; the sphere $ad-bc=1$. | T | |
| A15p00139 | Origin and antipode: the origin $[0:1]$ and the antipode $[1:0]$ of the frame’s line; the antipode is no residue, the antipodal point $\p/2$ of the additive cycle between $2\kap$ and $2\kap+1$. | T | |
| A16p00028 | The squares are the even drive steps: a residue’s quadratic class is its drive-step parity; registered transport is even, the one-way multiplier $\gen$ odd. | T | |
| A17p00042 | Time is the drive: each Subject’s clock is its own drive $x\mapsto\gen x$. A chronon is one drive step; a registered duration is the count of chronons, the Subject’s chart count, injective on every registrable depth; the Carrier has no clock. | T | |
| A18p00044 | Distance is decoherence: separation is the count of decoherence steps along a direction of the sky. Falsifier: a registered separation that is not such a count. | R | |
| A19p00182 | $S^{3}$, declared: the continuum chart of the spin cover $\mathrm{SL}_2(\Fp)$ [chart]. | D | |
| A20p00198 | The metric $3$-chart, declared: the continuum chart through which the inverse-square law is read [chart]. | D | |
| A21p38053 | The nesting condition $\p^{2}<\Om$: the Subject’s pair space fits the Carrier; equivalent to $\kap/\dS<1/(\sqrt{\Om}+1)$ [chart]. | T | |
| A22p07041 | The finite upper half-plane $H_{\p}=\mathbb{P}^{1}(\F_{\p^{2}})\setminus\mathbb{P}^{1}(\Fp)$, $\p(\p-1)$ points, with $\mathrm{GL}_2(\Fp)$ transitive and the non-split torus as stabiliser. | I | Prop. 2.5(viii); [Terras 1999] |
| A23p00162 | Completeness is primality: the Carrier’s chart $\F_{\Om}$ is a field and has no proper nonzero ideal. | T | |
| A24p38044 | The per-chronon drift rate: an embedded shell’s chart count, its position in its own chart of the Carrier’s cycle, advances by $1/(\Om-1)$ of the cycle per chronon; on a hosted Carrier the host’s clock drives every shell at that rate. | T | |
| A25p38054 | The joint cycle of a hosted pair: the advance per shell revolution is $\kap/\dS=(\p-1)/(\Om-1)$ of the Carrier’s chart cycle, and on a hosted Carrier run through its cycle the joint state returns after $\mathrm{lcm}(\p-1,\Om-1)$ chronons. | T | |
| A26p38016 | One retarded flow law: registration is retarded along the drift, the same across the three representations. | T | |
| A27p00140 | Observation is the Hopf section: the Subject registers its past cone through the cone chart, one chronon of lookback per station. Falsifier: a registration off the past cone. | R | |
| A28p21018 | The drive has a single arrow; its reversal would need the Frobenius-branch clock. | T | |
| A29p00008 | The Carrier: a timeless torsor of $\Om$ attribute-free manifestations, its cardinality its one absolute characteristic; a Subject’s frame charts it as the prime field $\FOm$, the frame’s chart and never the Carrier. | D | |
| A30p00153 | Thermodynamic entropy is the registration count: the entropy of the first law is the record $\kap(\p+1)=(\p^{2}-1)/4$, one $k_B$ per channel, $S_{\mathrm{th}}=k_B\,\kap(\p+1)$ [chart], the count itself and not its logarithm. Falsifier: a horizon whose Clausius entropy at the thermometer temperature is not $k_B$ times its channel count. | R | |
| A31p21052 | The weak-acceleration floor of registration against the drift is $a_{0}=c/T_H=cH_{0}/2\pi$, with $T_H=2\pi/H_{0}$ the drive period by the angle–count dictionary: $1.04\times10^{-10}$ m s$^{-2}$ at $H_{0}=67.4$ km s$^{-1}$ Mpc$^{-1}$, against the fitted $1.20\pm0.24\times10^{-10}$ [chart]. | T |  |
| A32p00032 | Temperature carries the acceleration domain: $[\Theta]=[E][k_B]^{-1}=[L][T]^{-2}$, flag-free, with $\Theta_P=E_P/|k_B|$, and the Unruh combination $\hbar a/2\pi c\,k_B$ closes as a domain identity; neither mass nor temperature is primitive. | T | |
| A33p00165 | On a Carrier of even capacity $\dS$ ($\Om\equiv1\pmod 8$) the register $\{\dS,\Om,c,\hbar,G,k_B\}$ is generator-free in the capacity: $G=2\dS=-c^{2}$, $2c^{2}\equiv1$, $\hbar^{2}\equiv-1$ and $k_B^{2}\equiv-2\pmod\Om$, with $|k_B|=\hbar/c$; $G$ is exact and the rest hold up to sign. | T | |
| A34p07053 | The de Sitter temperature of a horizon with Hubble rate $H$ is $T_{\mathrm{dS}}=\hbar H/2\pi k_B$ [chart]. | I | Prop. 6.3(ii); [Gibbons & Hawking 1977] |
| B. The register and the shell: the construction’s hypotheses and its necessity chain | |||
| B1p07003 | Every frame move of $G=\mathrm{PGL}_2(\Fp)$ factors uniquely as scale, translation and rotation, on $C_{4\kap}$, $C_{4\kap+1}$ and $C_{4\kap+2}$, of consecutive orders; on the spin cover the section obstructs at $-I$. | T | Prop. 3.3(i); rests on A11 |
| B2p07004 | Space has the three degrees of freedom of phase decoherence of the Subject’s frame, the cycles $\p-1$, $\p$, $\p+1$. Falsifier: P1’s. | R | |
| B3p07038 | Registration: the Subject registers the orbits of an action, of size moves over stabiliser, named at each use (the drive on the register, the trivial action on the register pair, the quarter-turn group on the nonzero pairs); a move, a label or a coordinate is not registered, and a count of registrations is a count of orbits. | D | Def. 2.4(i) |
| B4p07042 | The necessity chain: time’s coefficient is the drive’s generator $\gen$, a nonsquare; the temporal plane $-\gen t^{2}+x^{2}$ is anisotropic with norm-one group $C_{\p+1}$, the third cycle, and the register square is elliptic; a square coefficient gives the split plane, the cycle $C_{\p-1}$ again, and no time. | T | |
| B5p07049 | The registrable depth: the Subject’s register pair takes $\p^{2}$ values, the pair space of the nesting condition, and the states of a registrable duration are pairwise distinct, so a registrable duration has at most $\p^{2}$ chronons. | T | |
| B6p07050 | The register: the capacity register is the ring $\Z_{\p}$, the additive cycle $C_{\p}$ of the $4\kap+1$ cells; its translations $z\mapsto z+b$ are the unipotent moves of the frame, and each nontrivial translation fixes exactly one direction of the frame’s line, the antipode $[1:0]$. | T | Lem. B6 (lem:register), p. 7">3.1 |
| B7p07055 | The registrable duration and the record: a registrable duration is a sequence of chronons whose register-pair states are pairwise distinct, since registration distinguishes states only; its record is the sequence of chart counts registered along it, one per chronon, and contains the record of each initial segment. | D | Def. 2.4(ii) |
| C. The forms, the cone and the Hopf fibration | |||
| C1p07005 | The register square $\mathrm{Herm}_2(K)=\mathrm{Sym}^{2}(V)\oplus\Fp\,\eta J$ with $\det X=x_{0}^{2}-x_{1}^{2}-x_{3}^{2}+\gen x_{2}^{2}$; the map $\varphi$ is an isometry onto $Q_{\gen}$. | T | |
| C2p07006 | The congruence $X\mapsto AXA^{\dagger}$ of $\mathrm{SL}_2(K)$ preserves the register square and its determinant, has kernel $\pm I$ and image of order $\p^{2}(\p^{4}-1)/2$, the finite Lorentz group. | T | Thm. 4.1(iii); rests on A13 |
| C3p07007 | The cone is $\mathbb{P}^{1}(K)$: $[v]\mapsto[vv^{\dagger}]$ is a bijection onto the null lines of the register square, $\p^{2}+1$ directions. | T | Thm. 4.1(ii) |
| C4p07008 | Space and the causal rays: the $\p+1$ points of $\mathbb{P}^{1}(\Fp)$ are the null directions inside space; the $\p(\p-1)$ others, the finite upper half-plane, carry a time component and are the cone chart. | T | Thm. 4.1(ii) |
| C5p07009 | Exactly two four-dimensional classes: the frame quadric $(M_{2}(\Fp),\det)$ hyperbolic, the register square elliptic; Lorentzian exactly when $K$ is a field; $(3,1)$ names the elliptic class by the index chart [chart], in signs $(-+++)$ or equally $(+---)$, one class without inertia. | T | |
| C6p07010 | No inertia: $\langle1,1,1,\gen\rangle\cong\langle1,\gen,\gen,\gen\rangle$; a similitude of multiplier $\gen$ exchanges the two non-null classes; the null cone is the invariant of a change of unit. | T | |
| C7p07031 | The frame’s orbits: on the cone, the $\p+1$ null directions of space (Borel stabilisers) and the $\p(\p-1)$ causal rays (torus stabilisers); $\mathrm{SL}_2(\Fp)$ transitive on the rays with stabiliser $C_{\p+1}$, the exact fibration; the Borel a section in $G$, none on the spin cover. | T | Thm. 4.1(iv); rests on C9 |
| C8p07032 | The Hopf base is the set of oriented nonsquare axes of space: a causal ray’s stabiliser fixes one nonsquare axis, whose roots are the ray and its conjugate; every direction of space is a root pair on $\mathbb{P}^{1}(K)$; the fibration covers the causal rays only. | T | Thm. 4.1(iv); rests on C9 |
| C9p07040 | The class equation: every element of $G$ has order dividing $\p-1$, $\p$ or $\p+1$; the maximal cyclic subgroups are the split tori, the unipotent groups and the non-split tori, $\p(\p+1)/2$, $\p+1$ and $\p(\p-1)/2$ of them, partitioning $G\setminus\{1\}$. | T | Prop. 3.3(ii) |
| C10p07051 | The fixed points: a split torus fixes exactly two points of $\mathbb{P}^{1}(\Fp)$, a unipotent group one and a non-split torus none, by the square class of the discriminant; the three kinds of cycle are the three kinds of direction of space, a square-norm axis, a null direction and a nonsquare axis. | T | Prop. 3.3(iii) |
| D. Time and the horizon | |||
| D1p07011 | The stabiliser of the time vector $\eta J$ in $\mathrm{SL}_2(K)$ is exactly the spin cover $\mathrm{SL}_2(\Fp)$, which acts on $\mathrm{Sym}^{2}(V)$ through $\mathrm{PSL}_2(\Fp)$, of index two in $G$; the moves of odd drive parity lie outside it. | T | Thm. 4.1(iii); rests on A13 |
| D3p07013 | The drive on the square: $\mathrm{diag}(\gen,1)$ carries $[z]$ to $[\gen z]$ and $\eta J$ to $\gen\,\eta J$; its unimodular lift $\mathrm{diag}(\eta,\eta^{-1})$ carries $\eta J$ to $-\eta J$; the even transport $\mathrm{diag}(\gen,\gen^{-1})$ fixes $\eta J$ and dilates the origin and the antipode by $\gen^{-2}$ and $\gen^{2}$. | T | Thm. 4.1(v); rests on A10 |
| D4p07014 | $N^{1}$ and the non-split torus are conjugate in $\mathrm{SL}_2(K)$; the spinor closes in two circuits, of order $\p+1$ in $\mathrm{SL}_2(K)$ and $(\p+1)/2$ on the square. | T | Thm. 4.1(v); rests on A10 |
| D5p07015 | No definite space: every three-dimensional subspace of the register square contains a null vector. | T | Thm. 4.1(vi); rests on A1 |
| D6p07033 | $K^{\times}/\Fpx$ is regular on $\mathbb{P}^{1}(\Fp)$; the antipode $[1:0]$ is its element of order two, reached from the origin at the half step $2\kap+1$ by every generator; the unimodular torus reaches only the even steps. | T | Thm. 4.1(vi); rests on A1 |
| E. The figures | |||
| E1p07043 | The drawing conventions of the figures: finite sets placed on a circle, on the orbital sphere of [Akhtman & Voether 2026], in the laboratory’s sky chart of the fibration [chart] and its host view of the cone [chart]; no row rests on a figure. | D | Def. E1 (def:charts), p. 6">2.9 |
| F. The arrow: causality is the drift | |||
| F1p07044 | Every embedded shell drifts against its own chart of the Carrier by $1/(\Om-1)$ of the cycle per chronon and $\kap/\dS$ per revolution, below $1/(\sqrt{\Om}+1)$ exactly when $\p^{2}<\Om$ [chart]; the cycle’s order $\Om-1$ is the same for every Subject, and no rate between two Subjects is defined. | T | |
| F2p07045 | Causal order between stations is the drift read through the cone chart: the cone gives the null directions and the drift the order along them, one chronon of depth per rung. Falsifier: a registered order of events on the cone that differs from the order of the chart count, or a registration that precedes the drift. | R | |
| F3p07046 | The time reversal is not a Lorentz move: the congruence image is $\Omega^{-}_{4}(\p)$, of index four in $\mathrm{O}^{-}_{4}(\p)$; the time reversal is the Frobenius of $K$, and it, a spatial reflection and the total inversion lie outside the image. | T | |
| F4p07047 | The drift is one-directional: one chronon is one step of the Carrier’s chart cycle, a registered duration has at most $\p^{2}<\Om-1$ chronons, so the chart count is injective on every registrable depth and no recurrence is registrable; on a hosted Carrier the pair returns after $\mathrm{lcm}(4\kap,4\dS)$ chronons, the laboratory’s period. | T | |
| F5p07052 | The second law of the record: along a registrable duration the record gains one chart count per chronon, its entries pairwise distinct, and no count recurs below $\Om-1$; its entropy $S_{\mathrm{th}}(n)=k_B\,n$ [chart] never decreases on a registrable duration; the record holds at most $\p^{2}=4\kap(\p+1)+1$ entries, the $\kap(\p+1)$ orbits of the quarter-turn group on the nonzero pair states plus the origin. | T | |
| F6p07056 | One drift rate for every observer: every Subject’s chronon is one step of the Carrier’s chart cycle, so the drift has one rate for every observer, read as the Hubble rate [chart]; the arithmetic defines no rate between two Subjects. Falsifier: a drift rate that differs between observers at one epoch, at fixed $\Om$. | R | Real. F6 (real:rate), p. 15">5.4; rests on F1 |
| X. What the construction explains | |||
| X1p07020 | Why Lorentzian: a finite four-geometry is hyperbolic or elliptic, and the register square is elliptic because time’s coefficient is the drive’s generator, a nonsquare. | T | |
| X2p07021 | Why three spatial dimensions: space is $\mathrm{Sym}^{2}(V)$, of dimension three, and the frame moves have exactly three cyclic symmetries, the three kinds of direction of that space. | T | |
| X4p07023 | Why spin one half: the kernel of the congruence is $\pm I$ and the spinor closes in two circuits. | T | |
| X5p07024 | Why time is relational: there is no inertia, and a change of unit exchanges the label. | T | |
| X6p07048 | Why causality has an arrow: every embedded shell’s chart count is a one-directional count on a cycle of one order for every observer, it orders the shell’s revolutions, and the time reversal is not a Lorentz move. | T | |
| P. Falsifiable predictions | |||
| P1p07026 | Exactly three spatial dimensions at every scale the Subject registers, read through the declared metric chart. Falsifier: a short-range departure from the inverse-square law of the extra-dimension form; holds to $52\,\mu$m [data]. | T | |
| P2p07054 | The floor is the Carrier’s temperature: the de Sitter temperature of the Carrier’s horizon, $T_{\mathrm{dS}}=\hbar H_{0}/2\pi k_B$, and the floor $a_{0}=cH_{0}/2\pi$ are one number in the acceleration domain, $k_BT_{\mathrm{dS}}=(\hbar/c)\,a_{0}$ with $|k_B|=\hbar/c$ the chart’s unit [chart]: $2.66\times10^{-30}$ K and $1.04\times10^{-10}$ m s$^{-2}$ at $H_{0}=67.4$. Falsifier: a measured floor that departs from $cH_{0}/2\pi$. | T | |
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. Proved at the statement the source column names, in this paper or in the origin paper of a carried row; machine-verified in exact arithmetic by the named witness where a witness is named.
- R
- Realisation. States what a physical term denotes on the substrate: constitutive, not interpretive, and carrying its falsifier.
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 (
p03013) — 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/FrcMathlib) — 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).