| # | Description | Status | Sources |
|---|---|---|---|
| A. Inputs | |||
| A1p04001 | Finite sets and maps: a map between finite sets of equal cardinality is injective exactly when it is bijective; a set of cardinality at most $|U|$ injects into $U$; unique factorisation in $\Z$ (the Gödel code). | I | standard; [G"odel 1931; Smullyan 1991] |
| A2p04002 | Sufficiency: minimal sufficient statistics are unique up to bijection; invoked as motivation only — no probability enters, the operative notion is set-theoretic (B3). | I | [Lehmann & Scheff'e 1950; Keener 2010] |
| A3p04003 | The corpus: the shell $\Fp$, $\p=4\kap+1$, with its frame and quarter-turn (1:B2, B3); its frames $x\mapsto a+bx$ (1:C2; 00:C1); the Carrier and its readings as incomplete projections (00:A6, A6); finiteness and counting by return (00:A2, A7); $4\mid\p-1$ from the two involutions (00:B3); consolidation as frame maps, innovation as the extension $\Fpq$ where $\sqrt\nu$ is written (3:B5). | I | |
| A4p04004 | The empirical record: cross-modal alignment and unsupervised translation between independently trained embeddings; grokking; emergence, transfer under shared structure, latent knowledge, interpolation of arbitrary labels; hyperspherical embeddings; floating point as a finite subset of $\R$; sphere packing. | I | [Radford et al. 2021; Jha et al. 2025; Power et al. 2022; Wei et al. 2022; Hernandez et al. 2022; Burns et al. 2022; Zhang et al. 2017; Chen et al. 2020; Gao et al. 2021; Ethayarajh 2019; Wang & Isola 2020; Goldberg 1991; Conway & Sloane 1999] |
| B. The latent domain and adequacy | |||
| B1p04005 | The latent domain: a finite set $\mathcal Z\subset\mathcal U_t=\Fp$, the complete relational domain a model reconstructs from its data; the shell is the ambient set and a reading of it is a projection (00:A4). | D | Def. 1; Section 3 master: 00:A4 |
| B2p04006 | Observation maps: $g_m:\mathcal Z\to\mathcal X_m$ deterministic, one per modality, carrying its resolution; no stochastic model and no conditional independence is assumed; every cross-modal relation factors through $\mathcal Z$. | D | Eq. (2); Eq. (1) |
| B3p04007 | Adequacy: $E_m:\mathcal X_m\to W_m$ is adequate when $E_m\circ g_m=\varphi_m$ is a bijection $\mathcal Z\to W_m$; minimality, $W_m=\varphi_m(\mathcal Z)$, is part of the bijection, so the minimal adequate representation of Section 2 and Definition 2 are one notion. | D | Def. 2 |
| B4p04008 | Adequacy makes the observation map injective on the latent domain: $g_m(z)=g_m(z')$ forces $z=z'$; $\mathcal Z$ is the domain modality $m$ resolves completely. | T |    Section 3 |
| B5p04009 | Uniqueness up to bijection: for adequate $E_1$, $E_2$ of one $g$, $\psi=\varphi_2\circ\varphi_1^{-1}:W_1\to W_2$ is a bijection with $E_2\circ g=\psi\circ E_1\circ g$ — $E_2=\psi\circ E_1$ on $g(\mathcal Z)$, on all of $\mathcal X$ when $\mathcal X=g(\mathcal Z)$; $\psi$ is the unique map with this property. | T | Lemma 2; Lemma 1 |
| B6p04010 | The embedding into the shell: $|W_m|=|\mathcal Z|\le\p$, so an injection $\iota_m:W_m\hookrightarrow\mathcal U_t$ exists — the one place finiteness enters; canonically $\iota_m=\varphi_m^{-1}$ followed by the inclusion; $\psi_m:=\iota_m\circ\varphi_m:\mathcal Z\hookrightarrow\mathcal U_t$ is modality $m$'s chart of $\mathcal Z$. | T | Section 3 |
| C. The Universal Subspace Theorem | |||
| C1p04011 | Theorem 1 (i), (ii): every chart $\psi_m$ is injective, and $\Psi_{m\to n}:=\psi_n\circ\psi_m^{-1}:\psi_m(\mathcal Z)\to\psi_n(\mathcal Z)$ is a well-defined bijection, with $\Psi_{n\to k}\circ\Psi_{m\to n}=\Psi_{m\to k}$ and $\Psi_{m\to m}$ the identity. | T | Thm. 1 |
| C2p04012 | Theorem 1 (iii): with $\iota_m=\varphi_m^{-1}$ every chart is the inclusion $\mathcal Z\hookrightarrow\mathcal U_t$ and $\psi(\mathcal Z)=\mathcal Z$; canonical structurally (unique once $\mathcal Z$ is fixed), not algorithmically; “subspace” means subset. | T | Thm. 1 |
| C3p04013 | The canonical lift $L_m:=\varphi_m^{-1}\circ E_m:\mathcal X_m\to\mathcal Z$ satisfies $L_m\circ g_m=\mathrm{id}_{\mathcal Z}$, and $L_m(x)$ is the unique $z$ with $E_m(x)=\varphi_m(z)$. | T | Cor. 1 |
| C4p04014 | Cross-modal consistency: $\psi\circ L_m\circ g_m=\psi\circ L_n\circ g_n=\psi$ — observations of one latent state lift to one point — and $\iota_m(W_m)=\iota_n(W_n)=\psi(\mathcal Z)=\mathcal Z$. | T | Cor. 2 |
| C5p04015 | Charts of the shell itself: for $\mathcal Z=\Fp$ the charts respecting the arithmetic are the frames $x\mapsto a+bx$ (1:C2), $\p(\p-1)$ of them, and $\Psi_{m\to n}$ between two frames is the one affine map carrying the first to the second (simply transitive) — the corpus’s coordinate systems are the paper’s charts. | T | Section 3 |
| D. The reading | |||
| D1p04016 | Foundational embeddings are adequate representations of one finite latent domain: cross-modal alignment, transferability and semantic coherence are the bijections $\Psi_{m\to n}$ (C1), consequences of the shared domain, not of architecture; the empirical record (A4) is their registered consequence. Falsifier: two adequate embeddings of one domain with no bijective translation on the resolved states. | R | |
| D2p04017 | Scope and limits: the theorem uses the finiteness of $\mathcal Z$ alone, no algebraic or geometric property of $\mathcal U_t$; the shell as host is the ontology’s claim (A3); optimisation decides when a representation is recovered, not which; non-stationary or weakly factorisable data may admit none; coordinate alignment may be intractable; nonlinearity as expansion and depth as shell complexity are analogies (Y1). | D | Section 1; Section 5; Interp. 2, 3 |
| E. Finite ring geometry of embeddings | |||
| E1p04018 | The hypersphere [chart]: a Euclidean chart $\mathrm{Emb}:\mathcal Z\to\R^{d}$ equivariant for a symmetry acting transitively on $\mathcal Z$ and orthogonally on $\R^{d}$ has constant norm — $\mathrm{Emb}(\mathcal Z)\subset S^{d-1}$. The shell’s character chart $z\mapsto(\cos2\pi kz/\p,\sin2\pi kz/\p)_{k}$ is such a chart under translation, $\|\mathrm{Emb}(z)\|^{2}=\p-1$; in the shell’s arithmetic $\sum_{k}\g^{kz}\g^{k(n-z)}=n$ for every $z$. | T | Section 6 |
| E2p04019 | Quantisation [chart]: a digital embedding has coordinates in a finite $\mathcal Q\subset\R$; at step $\Delta$ the distinguishable points on a sphere of radius $R$ number $N(R)\sim C_d(R/\Delta)^{d-1}$ (grid counts fit exponent $d-1$ at $d=2,3$); at fixed $d$, $\Delta$ the capacity grows with $R$. | I | |
| E3p04020 | Gödel collapse: for distinct primes $p_1,\dots,p_d$ the code $G(x)=\prod p_i^{x_i}$ is injective on $\N^{d}$ (unique factorisation), and $G\bmod q$ stays injective on a finite set once $q$ exceeds its maximum; instance $d=3$, $x_i\le4$, primes $2,3,5$: $125$ codes, maximum $810\,000$, $q=810\,013$; signed coordinates are shifted first. | T | Section 6.3 |
| E4p04021 | The reading of Section 6: the sphere is the continuous shadow of the shell — uniform radius the absence of intrinsic attributes, direction the relational content; the coordinate count is a representational artefact, every quantised vector one element of one field (E3); the radius reads the resolved domain’s size; Gödel codes establish representability only, not geometry or training. | D | Section 6; 00:A8 |
| Y. Hypotheses | |||
| Y1p04024 | Depth and the shell hierarchy: whether nonlinear layers correspond to innovation steps $\mathcal U_t\hookrightarrow\mathcal U_{t+1}$ and depth to arithmetic complexity (Interpretations 2, 3) as a theorem; named as future work (iii), not claimed. | O | Section 7 |
| T. Tasks | |||
| T1p04025 | Learning objectives as approximations of adequacy (contrastive, masked prediction), algorithms for the projection maps $g_m$, and a general algebraic account of multimodal learning; named as future work (i), (ii), (iv), not claimed. | O | Section 7 |
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 (
p04008) — 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).